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

State before:
R : Type u_2
S : Type u_1
inst✝³ : CommSemiring R
inst✝² : CharTwo R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
x : R
⊢ f ((x ^ 2) ^ 2) = (f x ^ 2 - 1) ^ 2 - 1
Tactic:
rw [← add_add_cancel_right (x ^ 2) 1, add_one_sq, sq, sq, Eq2 hf, Eq2 hf]
State after:
no goals