Theorem: IMOSL.IMO2012A5.Case2.Eq2 (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 := hf.is_good (x - 1) (1 + 1)
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 - 1) * (1 + 1) + 1) = f (x - 1) * f (1 + 1) + f (x - 1 + (1 + 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 - 1) * (1 + 1) + 1) = f (x - 1) * f (1 + 1) + f (x - 1 + (1 + 1))
⊢ f (x * 2 - 1) = f (x - 1) * f 2 + f (x + 1)
Tactic:
rwa [sub_add_add_cancel, one_add_one_eq_two, mul_two, add_assoc,
  sub_add_cancel, ← add_sub_right_comm, ← mul_two] at h0
State after:
no goals