Theorem: IMOSL.IMO2012A5.Case3.Eq3 (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 * f (x * x + x) = (f (x + 1) ^ 2 - 1) * (f (x + 1) - 1) + f x * f (x + 1)
Tactic:
have h : x * (x + 1) = x * x + x := mul_add_one x x
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 : x * (x + 1) = x * x + x
⊢ f x * f (x * x + x) = (f (x + 1) ^ 2 - 1) * (f (x + 1) - 1) + f x * f (x + 1)

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 : x * (x + 1) = x * x + x
⊢ f x * f (x * x + x) = (f (x + 1) ^ 2 - 1) * (f (x + 1) - 1) + f x * f (x + 1)
Tactic:
rw [← Eq2_v2 hf, ← Eq1 hf, mul_sub_one, ← add_sub_right_comm, h, add_assoc,
  ← hf.is_good, mul_assoc, hf.is_good, h, add_add_cancel_middle₁, add_sub_cancel_right]
State after:
no goals