Theorem: IMOSL.IMO2012A5.Case1.Eq4 (IMOSLLean4/IMO2012/A5/A5Cases/Case1.lean)

State before:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : f (-1) ≠ 0
x : R
⊢ f (2 * x + 1) = f x - f (-x)
Tactic:
rw [hf.is_good, map_two hf h, one_mul, add_comm 2, Eq2 hf h, sub_neg_eq_add]
State after:
no goals