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

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