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

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

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