Theorem: IMOSL.IMO2012A5.Case2.RGoodSubcase22.value_bash (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
h0 : 3 ≠ 0
x : R
⊢ x = 0 ∨ x = 1 ∨ x = -1
Tactic:
have h1 (x) : x = 0 ∨ f x = 0 :=
  (map_eq_neg_one_or_zero hf h h0 x).imp_left (map_eq_neg_one_imp hf h)
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
h0 : 3 ≠ 0
x : R
h1 : ∀ (x : R), x = 0 ∨ f x = 0
⊢ x = 0 ∨ x = 1 ∨ x = -1

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
h0 : 3 ≠ 0
x : R
h1 : ∀ (x : R), x = 0 ∨ f x = 0
⊢ x = 0 ∨ x = 1 ∨ x = -1
Tactic:
refine (h1 x).imp_right λ h2 ↦ (h1 (x - 1)).imp eq_of_sub_eq_zero λ h3 ↦
  (h1 (x + 1)).elim eq_neg_of_add_eq_zero_left λ h4 ↦ ?_
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
h0 : 3 ≠ 0
x : R
h1 : ∀ (x : R), x = 0 ∨ f x = 0
h2 : f x = 0
h3 : f (x - 1) = 0
h4 : f (x + 1) = 0
⊢ x = -1

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
h0 : 3 ≠ 0
x : R
h1 : ∀ (x : R), x = 0 ∨ f x = 0
h2 : f x = 0
h3 : f (x - 1) = 0
h4 : f (x + 1) = 0
⊢ x = -1
Tactic:
have h5 := Eq1 hf h x
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
h0 : 3 ≠ 0
x : R
h1 : ∀ (x : R), x = 0 ∨ f x = 0
h2 : f x = 0
h3 : f (x - 1) = 0
h4 : f (x + 1) = 0
h5 : f (x + 1) + f (x - 1) + f x = -1
⊢ x = -1

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
h0 : 3 ≠ 0
x : R
h1 : ∀ (x : R), x = 0 ∨ f x = 0
h2 : f x = 0
h3 : f (x - 1) = 0
h4 : f (x + 1) = 0
h5 : f (x + 1) + f (x - 1) + f x = -1
⊢ x = -1
Tactic:
rw [h2, h3, h4, add_zero, add_zero, eq_comm, neg_eq_zero] at h5
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
h0 : 3 ≠ 0
x : R
h1 : ∀ (x : R), x = 0 ∨ f x = 0
h2 : f x = 0
h3 : f (x - 1) = 0
h4 : f (x + 1) = 0
h5 : 1 = 0
⊢ x = -1

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
h0 : 3 ≠ 0
x : R
h1 : ∀ (x : R), x = 0 ∨ f x = 0
h2 : f x = 0
h3 : f (x - 1) = 0
h4 : f (x + 1) = 0
h5 : 1 = 0
⊢ x = -1
Tactic:
rw [← mul_one 3, h5, mul_zero] at h0
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
h0 : 0 ≠ 0
x : R
h1 : ∀ (x : R), x = 0 ∨ f x = 0
h2 : f x = 0
h3 : f (x - 1) = 0
h4 : f (x + 1) = 0
h5 : 1 = 0
⊢ x = -1

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
h0 : 0 ≠ 0
x : R
h1 : ∀ (x : R), x = 0 ∨ f x = 0
h2 : f x = 0
h3 : f (x - 1) = 0
h4 : f (x + 1) = 0
h5 : 1 = 0
⊢ x = -1
Tactic:
exact absurd rfl h0
State after:
no goals