Theorem: Imo2017P2.good_map_eq_zero (Compfiles/Imo2017P2.lean)

State before:
R : Type u_1
D : Type u_2
inst✝ : DivisionRing D
f : D → D
h : good f
h0 : f ≠ 0
c : D
h1 : f c = 0
h2 : ¬c = 1
⊢ f = 0
Tactic:
have h3 := good_special_equality h (mul_inv_cancel <| sub_ne_zero_of_ne h2)
State after:
R : Type u_1
D : Type u_2
inst✝ : DivisionRing D
f : D → D
h : good f
h0 : f ≠ 0
c : D
h1 : f c = 0
h2 : ¬c = 1
h3 : f (f (c - 1 + 1) * f ((c - 1)⁻¹ + 1)) = 0
⊢ f = 0

State before:
R : Type u_1
D : Type u_2
inst✝ : DivisionRing D
f : D → D
h : good f
h0 : f ≠ 0
c : D
h1 : f c = 0
h2 : ¬c = 1
h3 : f (f (c - 1 + 1) * f ((c - 1)⁻¹ + 1)) = 0
⊢ f = 0
Tactic:
rw [sub_add_cancel, h1, zero_mul] at h3
State after:
R : Type u_1
D : Type u_2
inst✝ : DivisionRing D
f : D → D
h : good f
h0 : f ≠ 0
c : D
h1 : f c = 0
h2 : ¬c = 1
h3 : f 0 = 0
⊢ f = 0

State before:
R : Type u_1
D : Type u_2
inst✝ : DivisionRing D
f : D → D
h : good f
h0 : f ≠ 0
c : D
h1 : f c = 0
h2 : ¬c = 1
h3 : f 0 = 0
⊢ f = 0
Tactic:
ext x
State after:
case h
R : Type u_1
D : Type u_2
inst✝ : DivisionRing D
f : D → D
h : good f
h0 : f ≠ 0
c : D
h1 : f c = 0
h2 : ¬c = 1
h3 : f 0 = 0
x : D
⊢ f x = 0 x

State before:
case h
R : Type u_1
D : Type u_2
inst✝ : DivisionRing D
f : D → D
h : good f
h0 : f ≠ 0
c : D
h1 : f c = 0
h2 : ¬c = 1
h3 : f 0 = 0
x : D
⊢ f x = 0 x
Tactic:
rw [Pi.zero_apply, ← h3, ← mul_zero x, ← h,
  h3, mul_zero, h3, zero_add, add_zero]
State after:
no goals