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

State before:
R : Type ?u.124008
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
⊢ f x = -1 ∨ f x = 0
Tactic:
have Rchar' := Rchar' hf h
State after:
R : Type ?u.124008
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
Rchar' : 2 = -1
⊢ f x = -1 ∨ f x = 0

State before:
R : Type ?u.124008
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
Rchar' : 2 = -1
⊢ f x = -1 ∨ f x = 0
Tactic:
have h1 : f (x * x + 1) = (f x + 1) * f x := by
  rw [hf.is_good, ← two_mul, Rchar', neg_one_mul, hf.map_even, add_one_mul (f x)]
State after:
R : Type ?u.124008
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
Rchar' : 2 = -1
h1 : f (x * x + 1) = (f x + 1) * f x
⊢ f x = -1 ∨ f x = 0

State before:
R : Type ?u.124008
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
Rchar' : 2 = -1
h1 : f (x * x + 1) = (f x + 1) * f x
⊢ f x = -1 ∨ f x = 0
Tactic:
have h2 : f (x * x - 1) = f x * f x - 1 := by
  rw [Case2.Eq1 hf.toNontrivialGood hf.map_even, sub_self, hf.map_zero, sub_eq_add_neg]
State after:
R : Type ?u.124008
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
Rchar' : 2 = -1
h1 : f (x * x + 1) = (f x + 1) * f x
h2 : f (x * x - 1) = f x * f x - 1
⊢ f x = -1 ∨ f x = 0

State before:
R : Type ?u.124008
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
Rchar' : 2 = -1
h1 : f (x * x + 1) = (f x + 1) * f x
h2 : f (x * x - 1) = f x * f x - 1
⊢ f x = -1 ∨ f x = 0
Tactic:
have h3 : f (x * x) = (f x + 1 + 1) * f x := by
  have h2 := hf.is_good (x + 1) (x - 1)
  rw [Eq2 hf h, add_one_mul x, mul_sub_one, sub_add_sub_cancel, sub_add_cancel,
    add_add_sub_cancel, ← two_mul, Rchar', neg_one_mul, hf.map_even] at h2
  exact h2.trans (add_one_mul _ (f x)).symm
State after:
R : Type ?u.124008
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
Rchar' : 2 = -1
h1 : f (x * x + 1) = (f x + 1) * f x
h2 : f (x * x - 1) = f x * f x - 1
h3 : f (x * x) = (f x + 1 + 1) * f x
⊢ f x = -1 ∨ f x = 0

State before:
R : Type ?u.124008
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
Rchar' : 2 = -1
h1 : f (x * x + 1) = (f x + 1) * f x
h2 : f (x * x - 1) = f x * f x - 1
h3 : f (x * x) = (f x + 1 + 1) * f x
⊢ f x = -1 ∨ f x = 0
Tactic:
have h4 := Eq1 hf h (x * x)
State after:
R : Type ?u.124008
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
Rchar' : 2 = -1
h1 : f (x * x + 1) = (f x + 1) * f x
h2 : f (x * x - 1) = f x * f x - 1
h3 : f (x * x) = (f x + 1 + 1) * f x
h4 : f (x * x + 1) + f (x * x - 1) + f (x * x) = -1
⊢ f x = -1 ∨ f x = 0

State before:
R : Type ?u.124008
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
Rchar' : 2 = -1
h1 : f (x * x + 1) = (f x + 1) * f x
h2 : f (x * x - 1) = f x * f x - 1
h3 : f (x * x) = (f x + 1 + 1) * f x
h4 : f (x * x + 1) + f (x * x - 1) + f (x * x) = -1
⊢ f x = -1 ∨ f x = 0
Tactic:
rw [h1, h2, h3, ← add_sub_assoc, ← add_mul, ← add_sub_right_comm,
  sub_eq_neg_self, ← add_mul, mul_eq_zero, add_add_add_comm] at h4
State after:
R : Type ?u.124008
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
Rchar' : 2 = -1
h1 : f (x * x + 1) = (f x + 1) * f x
h2 : f (x * x - 1) = f x * f x - 1
h3 : f (x * x) = (f x + 1 + 1) * f x
h4 : f x + 1 + (f x + 1) + (f x + 1) = 0 ∨ f x = 0
⊢ f x = -1 ∨ f x = 0

State before:
R : Type ?u.124008
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
Rchar' : 2 = -1
h1 : f (x * x + 1) = (f x + 1) * f x
h2 : f (x * x - 1) = f x * f x - 1
h3 : f (x * x) = (f x + 1 + 1) * f x
h4 : f x + 1 + (f x + 1) + (f x + 1) = 0 ∨ f x = 0
⊢ f x = -1 ∨ f x = 0
Tactic:
clear h1 h2 h3
State after:
R : Type ?u.124008
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
Rchar' : 2 = -1
h4 : f x + 1 + (f x + 1) + (f x + 1) = 0 ∨ f x = 0
⊢ f x = -1 ∨ f x = 0

State before:
R : Type ?u.124008
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
Rchar' : 2 = -1
h4 : f x + 1 + (f x + 1) + (f x + 1) = 0 ∨ f x = 0
⊢ f x = -1 ∨ f x = 0
Tactic:
revert h4
State after:
R : Type ?u.124008
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
Rchar' : 2 = -1
⊢ f x + 1 + (f x + 1) + (f x + 1) = 0 ∨ f x = 0 → f x = -1 ∨ f x = 0

State before:
R : Type ?u.124008
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
Rchar' : 2 = -1
⊢ f x + 1 + (f x + 1) + (f x + 1) = 0 ∨ f x = 0 → f x = -1 ∨ f x = 0
Tactic:
refine Or.imp_left λ h1 ↦ ?_
State after:
R : Type ?u.124008
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
Rchar' : 2 = -1
h1 : f x + 1 + (f x + 1) + (f x + 1) = 0
⊢ f x = -1

State before:
R : Type ?u.124008
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
Rchar' : 2 = -1
h1 : f x + 1 + (f x + 1) + (f x + 1) = 0
⊢ f x = -1
Tactic:
rw [← two_mul, ← add_one_mul 2 (f x + 1), mul_eq_zero, two_add_one_eq_three] at h1
State after:
R : Type ?u.124008
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
Rchar' : 2 = -1
h1 : 3 = 0 ∨ f x + 1 = 0
⊢ f x = -1

State before:
R : Type ?u.124008
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
Rchar' : 2 = -1
h1 : 3 = 0 ∨ f x + 1 = 0
⊢ f x = -1
Tactic:
exact eq_neg_of_add_eq_zero_left (h1.resolve_left h0)
State after:
no goals

State before:
R : Type ?u.124008
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
Rchar' : 2 = -1
⊢ f (x * x + 1) = (f x + 1) * f x
Tactic:
rw [hf.is_good, ← two_mul, Rchar', neg_one_mul, hf.map_even, add_one_mul (f x)]
State after:
no goals

State before:
R : Type ?u.124008
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
Rchar' : 2 = -1
h1 : f (x * x + 1) = (f x + 1) * f x
⊢ f (x * x - 1) = f x * f x - 1
Tactic:
rw [Case2.Eq1 hf.toNontrivialGood hf.map_even, sub_self, hf.map_zero, sub_eq_add_neg]
State after:
no goals

State before:
R : Type ?u.124008
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
Rchar' : 2 = -1
h1 : f (x * x + 1) = (f x + 1) * f x
h2 : f (x * x - 1) = f x * f x - 1
⊢ f (x * x) = (f x + 1 + 1) * f x
Tactic:
have h2 := hf.is_good (x + 1) (x - 1)
State after:
R : Type ?u.124008
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
Rchar' : 2 = -1
h1 : f (x * x + 1) = (f x + 1) * f x
h2✝ : f (x * x - 1) = f x * f x - 1
h2 : f ((x + 1) * (x - 1) + 1) = f (x + 1) * f (x - 1) + f (x + 1 + (x - 1))
⊢ f (x * x) = (f x + 1 + 1) * f x

State before:
R : Type ?u.124008
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
Rchar' : 2 = -1
h1 : f (x * x + 1) = (f x + 1) * f x
h2✝ : f (x * x - 1) = f x * f x - 1
h2 : f ((x + 1) * (x - 1) + 1) = f (x + 1) * f (x - 1) + f (x + 1 + (x - 1))
⊢ f (x * x) = (f x + 1 + 1) * f x
Tactic:
rw [Eq2 hf h, add_one_mul x, mul_sub_one, sub_add_sub_cancel, sub_add_cancel,
  add_add_sub_cancel, ← two_mul, Rchar', neg_one_mul, hf.map_even] at h2
State after:
R : Type ?u.124008
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
Rchar' : 2 = -1
h1 : f (x * x + 1) = (f x + 1) * f x
h2✝ : f (x * x - 1) = f x * f x - 1
h2 : f (x * x) = (f x + 1) * f x + f x
⊢ f (x * x) = (f x + 1 + 1) * f x

State before:
R : Type ?u.124008
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
Rchar' : 2 = -1
h1 : f (x * x + 1) = (f x + 1) * f x
h2✝ : f (x * x - 1) = f x * f x - 1
h2 : f (x * x) = (f x + 1) * f x + f x
⊢ f (x * x) = (f x + 1 + 1) * f x
Tactic:
exact h2.trans (add_one_mul _ (f x)).symm
State after:
no goals