[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Add α
inst✝¹ : Semigroup α
inst✝ : LeftDistribClass α
a b c : α
h₁ : a ∣ b
h₂ : a ∣ c
d : α
hd : b = a * d
e : α
he : c = a * e
⊢ a * (d + e) = b + c
[PROOFSTEP]
simp [left_distrib, hd, he]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Semigroup α
inst✝ : HasDistribNeg α
a b c : α
⊢ (∃ b_1, -b = a * ↑(Equiv.neg α).symm b_1) ↔ a ∣ b
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Semigroup α
inst✝ : HasDistribNeg α
a b c : α
⊢ (∃ b_1, b = a * b_1) ↔ a ∣ b
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Semigroup α
inst✝ : HasDistribNeg α
a b c : α
⊢ (∃ b_1, b = -a * ↑(Equiv.neg α).symm b_1) ↔ a ∣ b
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Semigroup α
inst✝ : HasDistribNeg α
a b c : α
⊢ (∃ b_1, b = a * b_1) ↔ a ∣ b
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : NonUnitalRing α
a b c : α
h₁ : a ∣ b
h₂ : a ∣ c
⊢ a ∣ b - c
[PROOFSTEP]
simpa only [← sub_eq_add_neg] using h₁.add h₂.neg_right
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : NonUnitalRing α
a b c : α
h : a ∣ c
H : a ∣ b + c
⊢ a ∣ b
[PROOFSTEP]
simpa only [add_sub_cancel] using dvd_sub H h
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : NonUnitalRing α
a b c : α
h : a ∣ b
⊢ a ∣ b + c ↔ a ∣ c
[PROOFSTEP]
rw [add_comm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : NonUnitalRing α
a b c : α
h : a ∣ b
⊢ a ∣ c + b ↔ a ∣ c
[PROOFSTEP]
exact dvd_add_left h
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : NonUnitalRing α
a b c : α
h : a ∣ c
⊢ a ∣ b - c ↔ a ∣ b
[PROOFSTEP]
simpa only [← sub_eq_add_neg] using dvd_add_left ((dvd_neg (α := α)).2 h)
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : NonUnitalRing α
a b c : α
h : a ∣ b
⊢ a ∣ b - c ↔ a ∣ c
[PROOFSTEP]
rw [sub_eq_add_neg, dvd_add_right h, dvd_neg (α := α)]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : NonUnitalRing α
a b c : α
h : a ∣ b - c
⊢ a ∣ b ↔ a ∣ c
[PROOFSTEP]
rw [← sub_add_cancel b c, dvd_add_right h]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : NonUnitalRing α
a b c : α
⊢ a ∣ b - c ↔ a ∣ c - b
[PROOFSTEP]
rw [← dvd_neg (α := α), neg_sub]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : NonUnitalCommRing α
a✝ b✝ c k a b x y : α
hab : k ∣ a - b
hxy : k ∣ x - y
⊢ k ∣ a * x - b * y
[PROOFSTEP]
convert dvd_add (hxy.mul_left a) (hab.mul_right y) using 1
[GOAL]
case h.e'_4
α : Type u_1
β : Type u_2
inst✝ : NonUnitalCommRing α
a✝ b✝ c k a b x y : α
hab : k ∣ a - b
hxy : k ∣ x - y
⊢ a * x - b * y = a * (x - y) + (a - b) * y
[PROOFSTEP]
rw [mul_sub_left_distrib, mul_sub_right_distrib]
[GOAL]
case h.e'_4
α : Type u_1
β : Type u_2
inst✝ : NonUnitalCommRing α
a✝ b✝ c k a b x y : α
hab : k ∣ a - b
hxy : k ∣ x - y
⊢ a * x - b * y = a * x - a * y + (a * y - b * y)
[PROOFSTEP]
simp only [sub_eq_add_neg, add_assoc, neg_add_cancel_left]
