Theorem: IMOSL.IMO2012A5.Case1.GoodSubcase12.Rchar (IMOSLLean4/IMO2012/A5/A5Cases/Case1.lean)

State before:
R : Type u_1
S : Type ?u.32555
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodSubcase12 f
⊢ 3 = 0
Tactic:
refine hf.period_imp_zero λ x ↦ ?_
State after:
R : Type u_1
S : Type ?u.32555
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodSubcase12 f
x : R
⊢ f (x + 3) = f x

State before:
R : Type u_1
S : Type ?u.32555
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodSubcase12 f
x : R
⊢ f (x + 3) = f x
Tactic:
have h := triple_sum_eq_zero hf
State after:
R : Type u_1
S : Type ?u.32555
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodSubcase12 f
x : R
h : ∀ (x : R), f x + f (x + 1) + f (x + 2) = 0
⊢ f (x + 3) = f x

State before:
R : Type u_1
S : Type ?u.32555
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodSubcase12 f
x : R
h : ∀ (x : R), f x + f (x + 1) + f (x + 2) = 0
⊢ f (x + 3) = f x
Tactic:
have h0 := h (x + 1)
State after:
R : Type u_1
S : Type ?u.32555
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodSubcase12 f
x : R
h : ∀ (x : R), f x + f (x + 1) + f (x + 2) = 0
h0 : f (x + 1) + f (x + 1 + 1) + f (x + 1 + 2) = 0
⊢ f (x + 3) = f x

State before:
R : Type u_1
S : Type ?u.32555
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodSubcase12 f
x : R
h : ∀ (x : R), f x + f (x + 1) + f (x + 2) = 0
h0 : f (x + 1) + f (x + 1 + 1) + f (x + 1 + 2) = 0
⊢ f (x + 3) = f x
Tactic:
rwa [add_assoc x, one_add_one_eq_two, ← add_rotate, ← h x, add_left_inj,
  add_left_inj, add_assoc, add_comm 1, two_add_one_eq_three] at h0
State after:
no goals