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

State before:
R : Type ?u.29081
S : Type u_1
inst✝³ : CommSemiring R
inst✝² : CharTwo R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
a : S
⊢ a ^ 2 * ((a ^ 2 - 1) ^ 2 + 1) - ((a ^ 2 - 1) * (a - 1) + a * a) ^ 2 = (1 - 2 * a) * (a ^ 2 - 1)
Tactic:
ring
State after:
no goals