rw [←add_left_inj (-(a * c)), add_neg_self (a * c), neg_mul_eq_mul_neg, ←mul_add] at ab_eq_ac
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b c : R
a_ne_z : a ≠ 0
ab_eq_ac : a * b = a * c
⊢ b = c
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b c : R
a_ne_z : a ≠ 0
ab_eq_ac : a * (b + -c) = 0
⊢ b = c