Theorem: IMOSL.IMO2012A5.Case2.RGoodSubcase22.Rchar (IMOSLLean4/IMO2012/A5/A5Cases/Case2.lean)

State before:
R : Type u_1
S : Type ?u.109330
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
⊢ 3 = 0
Tactic:
rw [← two_add_one_eq_three, ← eq_neg_iff_add_eq_zero]
State after:
R : Type u_1
S : Type ?u.109330
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
⊢ 2 = -1

State before:
R : Type u_1
S : Type ?u.109330
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
⊢ 2 = -1
Tactic:
refine hf.period_imp_eq _ _ λ x ↦ ?_
State after:
R : Type u_1
S : Type ?u.109330
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
x : R
⊢ f (x + 2) = f (x + -1)

State before:
R : Type u_1
S : Type ?u.109330
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
x : R
⊢ f (x + 2) = f (x + -1)
Tactic:
have h0 := Eq1 hf h (x + 1)
State after:
R : Type u_1
S : Type ?u.109330
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
x : R
h0 : f (x + 1 + 1) + f (x + 1 - 1) + f (x + 1) = -1
⊢ f (x + 2) = f (x + -1)

State before:
R : Type u_1
S : Type ?u.109330
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 0
x : R
h0 : f (x + 1 + 1) + f (x + 1 - 1) + f (x + 1) = -1
⊢ f (x + 2) = f (x + -1)
Tactic:
rwa [add_sub_cancel_right, add_assoc x, one_add_one_eq_two, ← Eq1 hf h x,
  ← add_rotate, add_left_inj, add_right_inj, sub_eq_add_neg] at h0
State after:
no goals