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

State before:
R : Type u_2
S : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : NonAssocSemiring S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (-x) = f x
x : R
⊢ f (x * 2 + 1) = f (x + 1) * f 2 + f (x - 1)
Tactic:
have h0 := Eq2 hf (-x)
State after:
R : Type u_2
S : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : NonAssocSemiring S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (-x) = f x
x : R
h0 : f (-x * 2 - 1) = f (-x - 1) * f 2 + f (-x + 1)
⊢ f (x * 2 + 1) = f (x + 1) * f 2 + f (x - 1)

State before:
R : Type u_2
S : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : NonAssocSemiring S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (-x) = f x
x : R
h0 : f (-x * 2 - 1) = f (-x - 1) * f 2 + f (-x + 1)
⊢ f (x * 2 + 1) = f (x + 1) * f 2 + f (x - 1)
Tactic:
rwa [neg_mul, ← neg_add', h, ← neg_add', h, neg_add_eq_sub, ← neg_sub, h] at h0
State after:
no goals