Theorem: IMOSL.IMO2012A5.Case2.RGoodSubcase22.Eq1 (IMOSLLean4/IMO2012/A5/A5Cases/Case2.lean)

State before:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
x : R
⊢ f (x + 1) + f (x - 1) + f x = -1
Tactic:
rw [hf.toGoodCase2.Eq6, h, zero_sub, mul_neg_one, neg_add_rev, neg_add_cancel_right]
State after:
no goals