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

State before:
R : Type u_1
inst✝ : Ring R
f : R → R
h : good f
⊢ f (f 0 ^ 2) = 0
Tactic:
have h1 : (-1 : R) * (-1) = 1 := by rw [neg_mul_neg, mul_one]
State after:
R : Type u_1
inst✝ : Ring R
f : R → R
h : good f
h1 : -1 * -1 = 1
⊢ f (f 0 ^ 2) = 0

State before:
R : Type u_1
inst✝ : Ring R
f : R → R
h : good f
h1 : -1 * -1 = 1
⊢ f (f 0 ^ 2) = 0
Tactic:
have h2 := good_special_equality h h1
State after:
R : Type u_1
inst✝ : Ring R
f : R → R
h : good f
h1 : -1 * -1 = 1
h2 : f (f (-1 + 1) * f (-1 + 1)) = 0
⊢ f (f 0 ^ 2) = 0

State before:
R : Type u_1
inst✝ : Ring R
f : R → R
h : good f
h1 : -1 * -1 = 1
h2 : f (f (-1 + 1) * f (-1 + 1)) = 0
⊢ f (f 0 ^ 2) = 0
Tactic:
rwa [neg_add_self, ← sq] at h2
State after:
no goals

State before:
R : Type u_1
inst✝ : Ring R
f : R → R
h : good f
⊢ -1 * -1 = 1
Tactic:
rw [neg_mul_neg, mul_one]
State after:
no goals