Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.𝔽₂ε_solution (IMOSLLean4/IMO2012/A5/A5Cases/Case3.lean)

State before:
R : Type u_1
S : Type u_2
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r : R
hr : r ≠ 0
hr0 : r * r = 0
⊢ Function.Bijective (𝔽₂ε.cast r)
Tactic:
refine ⟨𝔽₂ε.castRingHom_injective hr0 hr, λ x ↦ ?_⟩
State after:
R : Type u_1
S : Type u_2
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r : R
hr : r ≠ 0
hr0 : r * r = 0
x : R
⊢ ∃ a, 𝔽₂ε.cast r a = x

State before:
R : Type u_1
S : Type u_2
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r : R
hr : r ≠ 0
hr0 : r * r = 0
x : R
⊢ ∃ a, 𝔽₂ε.cast r a = x
Tactic:
rcases R_elts_cases hS hf x with (h0 | h0) | h0
State after:
case inl.inl
R : Type u_1
S : Type u_2
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r : R
hr : r ≠ 0
hr0 : r * r = 0
x : R
h0 : (x + 1) * (x + 1) = 0
⊢ ∃ a, 𝔽₂ε.cast r a = x

case inl.inr
R : Type u_1
S : Type u_2
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r : R
hr : r ≠ 0
hr0 : r * r = 0
x : R
h0 : x * x = 0
⊢ ∃ a, 𝔽₂ε.cast r a = x

case inr
R : Type u_1
S : Type u_2
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r : R
hr : r ≠ 0
hr0 : r * r = 0
x : R
h0 : x * (x + 1) + 1 = 0
⊢ ∃ a, 𝔽₂ε.cast r a = x

State before:
case inl.inl
R : Type u_1
S : Type u_2
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r : R
hr : r ≠ 0
hr0 : r * r = 0
x : R
h0 : (x + 1) * (x + 1) = 0
⊢ ∃ a, 𝔽₂ε.cast r a = x
Tactic:
exact ((R_elts_claim1 hS hf hr0 h0).resolve_left hr).elim
  (λ h1 ↦ ⟨1, (add_eq_zero_iff_eq.mp h1).symm⟩)
  (λ h1 ↦ ⟨𝔽₂ε.Y, add_eq_iff_eq_add.mpr h1⟩)
State after:
no goals

State before:
case inl.inr
R : Type u_1
S : Type u_2
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r : R
hr : r ≠ 0
hr0 : r * r = 0
x : R
h0 : x * x = 0
⊢ ∃ a, 𝔽₂ε.cast r a = x
Tactic:
exact ((R_elts_claim1 hS hf hr0 h0).resolve_left hr).elim
  (λ h1 ↦ ⟨0, h1.symm⟩) (λ h1 ↦ ⟨𝔽₂ε.X, h1⟩)
State after:
no goals

State before:
case inr
R : Type u_1
S : Type u_2
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r : R
hr : r ≠ 0
hr0 : r * r = 0
x : R
h0 : x * (x + 1) + 1 = 0
⊢ ∃ a, 𝔽₂ε.cast r a = x
Tactic:
exact absurd (R_elts_claim2 hS hf hr0 h0) hr
State after:
no goals

State before:
R : Type u_1
S : Type u_2
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r : R
hr : r ≠ 0
hr0 : r * r = 0
h : Function.Bijective (𝔽₂ε.cast r)
⊢ f (𝔽₂ε.cast r 𝔽₂ε.O) = ↑(𝔽₂εMap 𝔽₂ε.O)
Tactic:
change f 0 = ((-1 : ℤ) : S)
State after:
R : Type u_1
S : Type u_2
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r : R
hr : r ≠ 0
hr0 : r * r = 0
h : Function.Bijective (𝔽₂ε.cast r)
⊢ f 0 = ↑(-1)

State before:
R : Type u_1
S : Type u_2
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r : R
hr : r ≠ 0
hr0 : r * r = 0
h : Function.Bijective (𝔽₂ε.cast r)
⊢ f 0 = ↑(-1)
Tactic:
rw [hf.map_zero, Int.cast_neg, Int.cast_one]
State after:
no goals

State before:
R : Type u_1
S : Type u_2
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r : R
hr : r ≠ 0
hr0 : r * r = 0
h : Function.Bijective (𝔽₂ε.cast r)
⊢ f (𝔽₂ε.cast r 𝔽₂ε.X) = ↑(𝔽₂εMap 𝔽₂ε.X)
Tactic:
change f r = ((1 : ℤ) : S)
State after:
R : Type u_1
S : Type u_2
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r : R
hr : r ≠ 0
hr0 : r * r = 0
h : Function.Bijective (𝔽₂ε.cast r)
⊢ f r = ↑1

State before:
R : Type u_1
S : Type u_2
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r : R
hr : r ≠ 0
hr0 : r * r = 0
h : Function.Bijective (𝔽₂ε.cast r)
⊢ f r = ↑1
Tactic:
have h0 := Eq2 hf.toNontrivialGood r
State after:
R : Type u_1
S : Type u_2
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r : R
hr : r ≠ 0
hr0 : r * r = 0
h : Function.Bijective (𝔽₂ε.cast r)
h0 : f (r * r + 1) = f r ^ 2 - 1
⊢ f r = ↑1

State before:
R : Type u_1
S : Type u_2
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r : R
hr : r ≠ 0
hr0 : r * r = 0
h : Function.Bijective (𝔽₂ε.cast r)
h0 : f (r * r + 1) = f r ^ 2 - 1
⊢ f r = ↑1
Tactic:
rw [hr0, zero_add, hf.map_one, eq_comm, sub_eq_zero, _root_.sq_eq_one_iff] at h0
State after:
R : Type u_1
S : Type u_2
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r : R
hr : r ≠ 0
hr0 : r * r = 0
h : Function.Bijective (𝔽₂ε.cast r)
h0 : f r = 1 ∨ f r = -1
⊢ f r = ↑1

State before:
R : Type u_1
S : Type u_2
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r : R
hr : r ≠ 0
hr0 : r * r = 0
h : Function.Bijective (𝔽₂ε.cast r)
h0 : f r = 1 ∨ f r = -1
⊢ f r = ↑1
Tactic:
refine (h0.resolve_right λ h1 ↦ hr ?_).trans Int.cast_one.symm
State after:
R : Type u_1
S : Type u_2
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r : R
hr : r ≠ 0
hr0 : r * r = 0
h : Function.Bijective (𝔽₂ε.cast r)
h0 : f r = 1 ∨ f r = -1
h1 : f r = -1
⊢ r = 0

State before:
R : Type u_1
S : Type u_2
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r : R
hr : r ≠ 0
hr0 : r * r = 0
h : Function.Bijective (𝔽₂ε.cast r)
h0 : f r = 1 ∨ f r = -1
h1 : f r = -1
⊢ r = 0
Tactic:
exact map_eq_neg_one_reduced_imp hS hf h1
State after:
no goals