Theorem: IMOSL.IMO2012A5.Case2.map_even_of_map_one (IMOSLLean4/IMO2012/A5/A5Cases/Case2.lean)

State before:
R : Type u_1
S : Type u_2
inst✝¹ : NonAssocRing R
inst✝ : NonAssocSemiring S
f : R → S
hf : good f
h : f (-1) = 0
x : R
⊢ f (-x) = f x
Tactic:
specialize hf (x + 1) (-1)
State after:
R : Type u_1
S : Type u_2
inst✝¹ : NonAssocRing R
inst✝ : NonAssocSemiring S
f : R → S
h : f (-1) = 0
x : R
hf : f ((x + 1) * -1 + 1) = f (x + 1) * f (-1) + f (x + 1 + -1)
⊢ f (-x) = f x

State before:
R : Type u_1
S : Type u_2
inst✝¹ : NonAssocRing R
inst✝ : NonAssocSemiring S
f : R → S
h : f (-1) = 0
x : R
hf : f ((x + 1) * -1 + 1) = f (x + 1) * f (-1) + f (x + 1 + -1)
⊢ f (-x) = f x
Tactic:
rwa [h, mul_zero, zero_add, add_neg_cancel_right,
  mul_neg_one, neg_add, neg_add_cancel_right] at hf
State after:
no goals