Theorem: IMOSL.IMO2012A5.Case2.CommCase.Eq6_ring_id (IMOSLLean4/IMO2012/A5/A5Cases/Case2.lean)

State before:
R : Type ?u.45782
S✝ : Type ?u.45785
inst✝³ : Ring R
inst✝² : CommRing S✝
inst✝¹ : NoZeroDivisors S✝
f : R → S✝
hf : NontrivialGood f
h : ∀ (x : R), f (-x) = f x
S : Type u_1
inst✝ : CommRing S
a b c d : S
⊢ a * (c * d + b) - a * (b * d + c) - ((c + 1) * (b * d + c) - (b + 1) * (c * d + b)) =
    (b + c - (a + 1) * (d - 1)) * (b - c)
Tactic:
ring
State after:
no goals