Theorem: IMOSL.IMO2012A5.Case1.Eq1 (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 (-x) = f (x + 1) * f (-1) + f x
Tactic:
have h0 := hf.is_good (x + 1) (-1)
State after:
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
h0 : f ((x + 1) * -1 + 1) = f (x + 1) * f (-1) + f (x + 1 + -1)
⊢ f (-x) = f (x + 1) * f (-1) + f x

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
h0 : f ((x + 1) * -1 + 1) = f (x + 1) * f (-1) + f (x + 1 + -1)
⊢ f (-x) = f (x + 1) * f (-1) + f x
Tactic:
rwa [add_neg_cancel_right, mul_neg_one (x + 1), neg_add, neg_add_cancel_right] at h0
State after:
no goals