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

State before:
R : Type u_2
S : Type u_1
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
h1 : f (x + 1) = 0 ∧ f (x - 1) = 0
⊢ x = 0
Tactic:
rw [sub_eq_add_neg, ← Rchar' hf h, ← one_add_one_eq_two, ← add_assoc] at h1
State after:
R : Type u_2
S : Type u_1
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
h1 : f (x + 1) = 0 ∧ f (x + 1 + 1) = 0
⊢ x = 0

State before:
R : Type u_2
S : Type u_1
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
h1 : f (x + 1) = 0 ∧ f (x + 1 + 1) = 0
⊢ x = 0
Tactic:
replace h1 := hf.toReducedGood.period_imp_zero
  (Eq5 hf.toNontrivialGood hf.map_even h1.1 h1.2)
State after:
R : Type u_2
S : Type u_1
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
h1 : 2 * (x + 1) + 1 = 0
⊢ x = 0

State before:
R : Type u_2
S : Type u_1
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
h1 : 2 * (x + 1) + 1 = 0
⊢ x = 0
Tactic:
rwa [Rchar' hf h, neg_one_mul, neg_add_rev, neg_add_cancel_comm, neg_eq_zero] at h1
State after:
no goals

State before:
R : Type u_2
S : Type u_1
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
⊢ f (x + 1) = 0 ∧ f (x - 1) = 0
Tactic:
have h1 : f (x + 1) + f (x - 1) = 0 := by
  rw [eq_sub_of_add_eq (Eq1 hf h x), h0, sub_self]
State after:
R : Type u_2
S : Type u_1
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
h1 : f (x + 1) + f (x - 1) = 0
⊢ f (x + 1) = 0 ∧ f (x - 1) = 0

State before:
R : Type u_2
S : Type u_1
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
h1 : f (x + 1) + f (x - 1) = 0
⊢ f (x + 1) = 0 ∧ f (x - 1) = 0
Tactic:
obtain h2 | h2 : f (x + 1) = 0 ∨ f (x - 1) = 0 := by
  rw [← mul_eq_zero, Eq2 hf h, h0, neg_add_self, zero_mul]
State after:
case inl
R : Type u_2
S : Type u_1
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
h1 : f (x + 1) + f (x - 1) = 0
h2 : f (x + 1) = 0
⊢ f (x + 1) = 0 ∧ f (x - 1) = 0

case inr
R : Type u_2
S : Type u_1
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
h1 : f (x + 1) + f (x - 1) = 0
h2 : f (x - 1) = 0
⊢ f (x + 1) = 0 ∧ f (x - 1) = 0

State before:
R : Type u_2
S : Type u_1
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
⊢ f (x + 1) + f (x - 1) = 0
Tactic:
rw [eq_sub_of_add_eq (Eq1 hf h x), h0, sub_self]
State after:
no goals

State before:
R : Type u_2
S : Type u_1
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
h1 : f (x + 1) + f (x - 1) = 0
⊢ f (x + 1) = 0 ∨ f (x - 1) = 0
Tactic:
rw [← mul_eq_zero, Eq2 hf h, h0, neg_add_self, zero_mul]
State after:
no goals

State before:
case inl
R : Type u_2
S : Type u_1
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
h1 : f (x + 1) + f (x - 1) = 0
h2 : f (x + 1) = 0
⊢ f (x + 1) = 0 ∧ f (x - 1) = 0
Tactic:
rw [h2, zero_add] at h1
State after:
case inl
R : Type u_2
S : Type u_1
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
h1 : f (x - 1) = 0
h2 : f (x + 1) = 0
⊢ f (x + 1) = 0 ∧ f (x - 1) = 0

State before:
case inl
R : Type u_2
S : Type u_1
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
h1 : f (x - 1) = 0
h2 : f (x + 1) = 0
⊢ f (x + 1) = 0 ∧ f (x - 1) = 0
Tactic:
exact ⟨h2, h1⟩
State after:
no goals

State before:
case inr
R : Type u_2
S : Type u_1
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
h1 : f (x + 1) + f (x - 1) = 0
h2 : f (x - 1) = 0
⊢ f (x + 1) = 0 ∧ f (x - 1) = 0
Tactic:
rw [h2, add_zero] at h1
State after:
case inr
R : Type u_2
S : Type u_1
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
h1 : f (x + 1) = 0
h2 : f (x - 1) = 0
⊢ f (x + 1) = 0 ∧ f (x - 1) = 0

State before:
case inr
R : Type u_2
S : Type u_1
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
h1 : f (x + 1) = 0
h2 : f (x - 1) = 0
⊢ f (x + 1) = 0 ∧ f (x - 1) = 0
Tactic:
exact ⟨h1, h2⟩
State after:
no goals