Theorem: IMOSL.IMO2012A5.Case3.Eq3_v2 (IMOSLLean4/IMO2012/A5/A5Cases/Case3.lean)

State before:
R : Type u_2
S : Type u_1
inst✝³ : Semiring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
x : R
⊢ f (x + 1) * f (x * x + x) = (f x ^ 2 - 1) * (f x - 1) + f (x + 1) * f x
Tactic:
have h := Eq3 hf (x + 1)
State after:
R : Type u_2
S : Type u_1
inst✝³ : Semiring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
x : R
h :
  f (x + 1) * f ((x + 1) * (x + 1) + (x + 1)) =
    (f (x + 1 + 1) ^ 2 - 1) * (f (x + 1 + 1) - 1) + f (x + 1) * f (x + 1 + 1)
⊢ f (x + 1) * f (x * x + x) = (f x ^ 2 - 1) * (f x - 1) + f (x + 1) * f x

State before:
R : Type u_2
S : Type u_1
inst✝³ : Semiring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
x : R
h :
  f (x + 1) * f ((x + 1) * (x + 1) + (x + 1)) =
    (f (x + 1 + 1) ^ 2 - 1) * (f (x + 1 + 1) - 1) + f (x + 1) * f (x + 1 + 1)
⊢ f (x + 1) * f (x * x + x) = (f x ^ 2 - 1) * (f x - 1) + f (x + 1) * f x
Tactic:
rwa [add_add_cancel_right, add_one_mul_self, add_add_add_cancel_right] at h
State after:
no goals