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

State before:
R : Type ?u.57818
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 - 1) ^ 2 - 1) * ((b - 1) ^ 2 - 1) - ((a * b - 1) ^ 2 - 1) = 2 * (a * b * (2 + 1 - (a + b)))
Tactic:
ring
State after:
no goals