Theorem: Imo2017P2.good_neg (Compfiles/Imo2017P2.lean)

State before:
R : Type u_1
inst✝ : Ring R
f : R → R
h : good f
x y : R
⊢ (-f) ((-f) x * (-f) y) + (-f) (x + y) = (-f) (x * y)
Tactic:
repeat rw [Pi.neg_apply]
State after:
R : Type u_1
inst✝ : Ring 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✝ : Ring 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

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