case h.e'_4
α : Type u_1
β : Type ?u.14179
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
α : Type u_1
β : Type ?u.14179
inst✝ : NonUnitalCommRing α
a✝ b✝ c k a b x y : α
hab : k ∣ a - b
hxy : k ∣ x - y
⊢ k ∣ a * x - b * y
convert dvd_add (hxy.mul_left a) (hab.mul_right y) using 1
case h.e'_4
α : Type u_1
β : Type ?u.14179
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)
case h.e'_4
α : Type u_1
β : Type ?u.14179
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
rw [mul_sub_left_distrib, mul_sub_right_distrib]
no goals
case h.e'_4
α : Type u_1
β : Type ?u.14179
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)
simp only [sub_eq_add_neg, add_assoc, neg_add_cancel_left]