Theorem: IMOSL.IMO2017A6.good_neg (IMOSLLean4/IMO2017/A6/A6.lean)

State before:
R : Type u_1
inst✝ : NonAssocRing R
f : R → R
h : good f
x y : R
⊢ (-f) ((-f) x * (-f) y) + (-f) (x + y) = (-f) (x * y)
Tactic:
simp only [Pi.neg_apply]
State after:
R : Type u_1
inst✝ : NonAssocRing R
f : R → R
h : good f
x y : R
⊢ -f (-f x * -f y) + -f (x + y) = -f (x * y)

State before:
R : Type u_1
inst✝ : NonAssocRing R
f : R → R
h : good f
x y : R
⊢ -f (-f x * -f y) + -f (x + y) = -f (x * y)
Tactic:
rw [neg_mul_neg, ← neg_add, h]
State after:
no goals