cases (@mul_eq_zero _ _ _ a (b + -c)).1 ab_eq_ac with
| inl h => exact False.elim (a_ne_z h)
| inr h =>
  rw [←add_left_inj (-c), add_neg_self c]
  exact h
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
no goals