Theorem: IMOSL.IMO2012A5.Case1.GoodSubcase12.triple_sum_eq_zero (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 : GoodSubcase12 f
x : R
⊢ f x + f (x + 1) + f (x + 2) = 0
Tactic:
have h := Eq1 hf.toNontrivialGood x
State after:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodSubcase12 f
x : R
h : f (-x) = f (x + 1) * f (-1) + f x
⊢ f x + f (x + 1) + f (x + 2) = 0

State before:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodSubcase12 f
x : R
h : f (-x) = f (x + 1) * f (-1) + f x
⊢ f x + f (x + 1) + f (x + 2) = 0
Tactic:
rwa [Case1.Eq2 hf.toNontrivialGood (map_neg_one_ne_zero hf), hf.map_neg_one,
  mul_one, neg_eq_iff_add_eq_zero, add_comm, add_comm (f _)] at h
State after:
no goals