Theorem: nzero_mul_left_cancel (ECTate/Algebra/Ring/Basic.lean)

State before:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b c : R
⊢ a ≠ 0 → a * b = a * c → b = c
Tactic:
intro a_ne_z ab_eq_ac
State after:
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

State before:
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
Tactic:
rw [←add_left_inj (-(a * c)), add_neg_self (a * c), neg_mul_eq_mul_neg, ←mul_add] at ab_eq_ac
State after:
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

State before:
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
Tactic:
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
State after:
no goals

State before:
case inl
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
h : a = 0
⊢ b = c
Tactic:
exact False.elim (a_ne_z h)
State after:
no goals

State before:
case inr
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
h : b + -c = 0
⊢ b = c
Tactic:
rw [←add_left_inj (-c), add_neg_self c]
State after:
case inr
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
h : b + -c = 0
⊢ b + -c = 0

State before:
case inr
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
h : b + -c = 0
⊢ b + -c = 0
Tactic:
exact h
State after:
no goals