Theorem: IMOSL.IMO2017A6.good_map_map_zero_sq (IMOSLLean4/IMO2017/A6/A6.lean)

State before:
R : Type u_1
inst✝ : Ring R
f : R → R
h : good f
⊢ f (f 0 ^ 2) = 0
Tactic:
specialize h 0 0
State after:
R : Type u_1
inst✝ : Ring R
f : R → R
h : f (f 0 * f 0) + f (0 + 0) = f (0 * 0)
⊢ f (f 0 ^ 2) = 0

State before:
R : Type u_1
inst✝ : Ring R
f : R → R
h : f (f 0 * f 0) + f (0 + 0) = f (0 * 0)
⊢ f (f 0 ^ 2) = 0
Tactic:
rwa [add_zero, mul_zero, add_left_eq_self, ← sq] at h
State after:
no goals