Theorem: IMOSL.IMO2012A5.Case1.Eq3 (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 y : R
⊢ f (-x) * f (-y) + f (-(x + y)) = f x * f y + f (x + y)
Tactic:
rw [neg_add, ← hf.is_good, neg_mul_neg, hf.is_good]
State after:
no goals