Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.map_add_one_eq_zero_iff_map_eq (IMOSLLean4/IMO2012/A5/A5Cases/Case3.lean)

State before:
R : Type u_2
S : Type u_1
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : NontrivialGood f
x : R
⊢ f (x + 1) = 0 ↔ f x ^ 2 = 1
Tactic:
refine ⟨λ h0 ↦ ?_, λ h0 ↦ ?_⟩
State after:
case refine_1
R : Type u_2
S : Type u_1
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : NontrivialGood f
x : R
h0 : f (x + 1) = 0
⊢ f x ^ 2 = 1

case refine_2
R : Type u_2
S : Type u_1
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : NontrivialGood f
x : R
h0 : f x ^ 2 = 1
⊢ f (x + 1) = 0

State before:
case refine_1
R : Type u_2
S : Type u_1
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : NontrivialGood f
x : R
h0 : f (x + 1) = 0
⊢ f x ^ 2 = 1
Tactic:
have h1 := Eq3_v2 hf x
State after:
case refine_1
R : Type u_2
S : Type u_1
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : NontrivialGood f
x : R
h0 : f (x + 1) = 0
h1 : f (x + 1) * f (x * x + x) = (f x ^ 2 - 1) * (f x - 1) + f (x + 1) * f x
⊢ f x ^ 2 = 1

State before:
case refine_1
R : Type u_2
S : Type u_1
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : NontrivialGood f
x : R
h0 : f (x + 1) = 0
h1 : f (x + 1) * f (x * x + x) = (f x ^ 2 - 1) * (f x - 1) + f (x + 1) * f x
⊢ f x ^ 2 = 1
Tactic:
rw [h0, zero_mul, zero_mul, add_zero, zero_eq_mul] at h1
State after:
case refine_1
R : Type u_2
S : Type u_1
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : NontrivialGood f
x : R
h0 : f (x + 1) = 0
h1 : f x ^ 2 - 1 = 0 ∨ f x - 1 = 0
⊢ f x ^ 2 = 1

State before:
case refine_1
R : Type u_2
S : Type u_1
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : NontrivialGood f
x : R
h0 : f (x + 1) = 0
h1 : f x ^ 2 - 1 = 0 ∨ f x - 1 = 0
⊢ f x ^ 2 = 1
Tactic:
exact h1.elim eq_of_sub_eq_zero λ h1 ↦ eq_of_sub_eq_zero h1 ▸ one_pow 2
State after:
no goals

State before:
case refine_2
R : Type u_2
S : Type u_1
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : NontrivialGood f
x : R
h0 : f x ^ 2 = 1
⊢ f (x + 1) = 0
Tactic:
rcases main_cases hS hf x with (h1 | h1) | ⟨h1, h2⟩
State after:
case refine_2.inl.inl
R : Type u_2
S : Type u_1
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : NontrivialGood f
x : R
h0 : f x ^ 2 = 1
h1 : f x = 0
⊢ f (x + 1) = 0

case refine_2.inl.inr
R : Type u_2
S : Type u_1
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : NontrivialGood f
x : R
h0 : f x ^ 2 = 1
h1 : f (x + 1) = 0
⊢ f (x + 1) = 0

case refine_2.inr.intro
R : Type u_2
S : Type u_1
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : NontrivialGood f
x : R
h0 : f x ^ 2 = 1
h1 : f x + f (x + 1) = 1
h2 : f x * f (x + 1) = -1
⊢ f (x + 1) = 0

State before:
case refine_2.inl.inl
R : Type u_2
S : Type u_1
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : NontrivialGood f
x : R
h0 : f x ^ 2 = 1
h1 : f x = 0
⊢ f (x + 1) = 0
Tactic:
rw [h1, sq, zero_mul] at h0
State after:
case refine_2.inl.inl
R : Type u_2
S : Type u_1
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : NontrivialGood f
x : R
h0 : 0 = 1
h1 : f x = 0
⊢ f (x + 1) = 0

State before:
case refine_2.inl.inl
R : Type u_2
S : Type u_1
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : NontrivialGood f
x : R
h0 : 0 = 1
h1 : f x = 0
⊢ f (x + 1) = 0
Tactic:
rw [← mul_one (f _), ← h0, mul_zero]
State after:
no goals

State before:
case refine_2.inl.inr
R : Type u_2
S : Type u_1
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : NontrivialGood f
x : R
h0 : f x ^ 2 = 1
h1 : f (x + 1) = 0
⊢ f (x + 1) = 0
Tactic:
exact h1
State after:
no goals

State before:
case refine_2.inr.intro
R : Type u_2
S : Type u_1
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : NontrivialGood f
x : R
h0 : f x ^ 2 = 1
h1 : f x + f (x + 1) = 1
h2 : f x * (f x * f (x + 1)) = f x * -1
⊢ f (x + 1) = 0
Tactic:
rw [← mul_assoc, ← sq, h0, one_mul, mul_neg_one] at h2
State after:
case refine_2.inr.intro
R : Type u_2
S : Type u_1
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : NontrivialGood f
x : R
h0 : f x ^ 2 = 1
h1 : f x + f (x + 1) = 1
h2 : f (x + 1) = -f x
⊢ f (x + 1) = 0

State before:
case refine_2.inr.intro
R : Type u_2
S : Type u_1
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : NontrivialGood f
x : R
h0 : f x ^ 2 = 1
h1 : f x + f (x + 1) = 1
h2 : f (x + 1) = -f x
⊢ f (x + 1) = 0
Tactic:
rw [h2, add_neg_self] at h1
State after:
case refine_2.inr.intro
R : Type u_2
S : Type u_1
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : NontrivialGood f
x : R
h0 : f x ^ 2 = 1
h1 : 0 = 1
h2 : f (x + 1) = -f x
⊢ f (x + 1) = 0

State before:
case refine_2.inr.intro
R : Type u_2
S : Type u_1
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : NontrivialGood f
x : R
h0 : f x ^ 2 = 1
h1 : 0 = 1
h2 : f (x + 1) = -f x
⊢ f (x + 1) = 0
Tactic:
rw [← mul_one (f _), ← h1, mul_zero]
State after:
no goals