Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.Eq8 (IMOSLLean4/IMO2012/A5/A5Cases/Case2.lean)

State before:
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
x y : R
⊢ g (x + y) + g (x - y) = 2 • (g x + g y)
Tactic:
rw [two_nsmul, ← two_mul, ← sub_eq_zero, ← hg.Eq4, hg.Eq7, sub_self, mul_zero]
State after:
no goals