internlm/Lean-Github huggingface dataset:
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.R_elts_claim2
Proof state before:
case inr.inr.inr
R : Type u_1
S : Type ?u.172967
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
r s : R
hr : r * r = 0
h : s * r + r * (s + 1) = 0
h0✝ : r * s * (r * s) = 0
h0 : r = r * s
hs : r * (s * (s + 1) + 1) = r * 0
⊢ r = 0
Tactic:
rwa [mul_zero, mul_add_one r, ← mul_assoc, ← h0,
  mul_add_one r, ← h0, add_add_cancel_right] at hs
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.𝔽₂_solution
Proof 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
hR : ∀ (r : R), r = 0 ∨ r = 1
h : 1 = 0
⊢ 2 = 0
Tactic:
apply congrArg f at h
Proof 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
hR : ∀ (r : R), r = 0 ∨ r = 1
h : f 1 = f 0
⊢ 2 = 0
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.𝔽₂_solution
Proof 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
hR : ∀ (r : R), r = 0 ∨ r = 1
h : f 1 = f 0
⊢ 2 = 0
Tactic:
rw [hf.map_one, hf.map_zero, zero_eq_neg] at h
Proof 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
hR : ∀ (r : R), r = 0 ∨ r = 1
h : 1 = 0
⊢ 2 = 0
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.𝔽₂_solution
Proof 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
hR : ∀ (r : R), r = 0 ∨ r = 1
h : 1 = 0
⊢ 2 = 0
Tactic:
rw [← mul_one 2, h, mul_zero]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.𝔽₂_solution
Proof 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
hR : ∀ (r : R), r = 0 ∨ r = 1
h : Function.Bijective 𝔽₂.cast
⊢ f 𝔽₂.O.cast = ↑(𝔽₂Map 𝔽₂.O)
Tactic:
change f 0 = ((-1 : ℤ) : S)
Proof 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
hR : ∀ (r : R), r = 0 ∨ r = 1
h : Function.Bijective 𝔽₂.cast
⊢ f 0 = ↑(-1)
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.𝔽₂_solution
Proof 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
hR : ∀ (r : R), r = 0 ∨ r = 1
h : Function.Bijective 𝔽₂.cast
⊢ f 0 = ↑(-1)
Tactic:
rw [hf.map_zero, Int.cast_neg, Int.cast_one]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.𝔽₂ε_solution
Proof 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 ↦ ?_⟩
Proof 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
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.𝔽₂ε_solution
Proof 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
Proof 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
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.𝔽₂ε_solution
Proof 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⟩)
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.𝔽₂ε_solution
Proof 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⟩)
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.𝔽₂ε_solution
Proof 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
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.𝔽₂ε_solution
Proof 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)
Proof 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)
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.𝔽₂ε_solution
Proof 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]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.𝔽₂ε_solution
Proof 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)
Proof 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
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.𝔽₂ε_solution
Proof 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
Proof 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
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.𝔽₂ε_solution
Proof 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
Proof 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
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.𝔽₂ε_solution
Proof 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
Proof 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
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.𝔽₂ε_solution
Proof 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
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.𝔽₄_solution
Proof 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 * (r + 1) + 1 = 0
⊢ ∃ φ ι, ∀ (x : R), f x = ι (𝔽₄Map (φ x))
Tactic:
have X : (1 : R) ≠ 0 := λ X ↦ hS <| by
  apply congrArg f at X; rw [hf.map_one, hf.map_zero, zero_eq_neg] at X
  rw [← mul_one 2, X, mul_zero]
Proof 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 * (r + 1) + 1 = 0
X : 1 ≠ 0
⊢ ∃ φ ι, ∀ (x : R), f x = ι (𝔽₄Map (φ x))
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.𝔽₄_solution
Proof 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 * (r + 1) + 1 = 0
X : 1 ≠ 0
⊢ ∃ φ ι, ∀ (x : R), f x = ι (𝔽₄Map (φ x))
Tactic:
obtain ⟨hr0, hr1⟩ := (reduced_𝔽₄_iff hS hf).mp hr
Proof state after:
case intro
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 * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f r + f (r + 1) = 1
hr1 : f r * f (r + 1) = -1
⊢ ∃ φ ι, ∀ (x : R), f x = ι (𝔽₄Map (φ x))
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.𝔽₄_solution
Proof state before:
case intro
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 * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f r + f (r + 1) = 1
hr1 : f r * f (r + 1) = -1
⊢ ∃ φ ι, ∀ (x : R), f x = ι (𝔽₄Map (φ x))
Tactic:
have hr' : r * r + r = 1 := by rwa [← mul_add_one r, ← add_eq_zero_iff_eq]
Proof state after:
case intro
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 * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f r + f (r + 1) = 1
hr1 : f r * f (r + 1) = -1
hr' : r * r + r = 1
⊢ ∃ φ ι, ∀ (x : R), f x = ι (𝔽₄Map (φ x))
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.𝔽₄_solution
Proof state before:
case intro
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 * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f r + f (r + 1) = 1
hr1 : f r * f (r + 1) = -1
hr' : r * r + r = 1
h : Function.Bijective (𝔽₄.cast r)
⊢ ∃ φ ι, ∀ (x : R), f x = ι (𝔽₄Map (φ x))
Tactic:
rw [← eq_sub_iff_add_eq'] at hr0
Proof state after:
case intro
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 * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f (r + 1) = 1 - f r
hr1 : f r * f (r + 1) = -1
hr' : r * r + r = 1
h : Function.Bijective (𝔽₄.cast r)
⊢ ∃ φ ι, ∀ (x : R), f x = ι (𝔽₄Map (φ x))
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.𝔽₄_solution
Proof state before:
case intro
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 * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f (r + 1) = 1 - f r
hr1 : f r * f (r + 1) = -1
hr' : r * r + r = 1
h : Function.Bijective (𝔽₄.cast r)
⊢ ∃ φ ι, ∀ (x : R), f x = ι (𝔽₄Map (φ x))
Tactic:
rw [hr0, ← neg_sub, mul_neg, neg_inj, mul_sub_one, sub_eq_iff_eq_add'] at hr1
Proof state after:
case intro
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 * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f (r + 1) = 1 - f r
hr1 : f r * f r = f r + 1
hr' : r * r + r = 1
h : Function.Bijective (𝔽₄.cast r)
⊢ ∃ φ ι, ∀ (x : R), f x = ι (𝔽₄Map (φ x))
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.𝔽₄_solution
Proof state before:
case intro
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 * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f (r + 1) = 1 - f r
hr1 : f r * f r = f r + 1
hr' : r * r + r = 1
h : Function.Bijective (𝔽₄.cast r)
⊢ ∃ φ ι, ∀ (x : R), f x = ι (𝔽₄Map (φ x))
Tactic:
let ι := ℤφ.castRingHom hr1
Proof state after:
case intro
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 * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f (r + 1) = 1 - f r
hr1 : f r * f r = f r + 1
hr' : r * r + r = 1
h : Function.Bijective (𝔽₄.cast r)
ι : ℤφ →+* S := ℤφ.castRingHom hr1
⊢ ∃ φ ι, ∀ (x : R), f x = ι (𝔽₄Map (φ x))
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.𝔽₄_solution
Proof state before:
case intro
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 * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f (r + 1) = 1 - f r
hr1 : f r * f r = f r + 1
hr' : r * r + r = 1
h : Function.Bijective (𝔽₄.cast r)
ι : ℤφ →+* S := ℤφ.castRingHom hr1
⊢ ∃ φ ι, ∀ (x : R), f x = ι (𝔽₄Map (φ x))
Tactic:
have h0 : ∀ x, f (𝔽₄.cast r x) = ι (𝔽₄Map x)
  | 𝔽₄.O => by change f 0 = ι (-1)
               rw [hf.map_zero, ι.map_neg, ι.map_one]
  | 𝔽₄.I => (hf.map_one).trans ι.map_zero.symm
  | 𝔽₄.X => (ℤφ.cast_φ _).symm
  | 𝔽₄.Y => by change f (r + 1) = ((1 : ℤ) : S) + (-1 : ℤ) • f r
               rw [Int.cast_one, neg_one_zsmul, hr0, sub_eq_add_neg]
Proof state after:
case intro
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 * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f (r + 1) = 1 - f r
hr1 : f r * f r = f r + 1
hr' : r * r + r = 1
h : Function.Bijective (𝔽₄.cast r)
ι : ℤφ →+* S := ℤφ.castRingHom hr1
h0 : ∀ (x : 𝔽₄), f (𝔽₄.cast r x) = ι (𝔽₄Map x)
⊢ ∃ φ ι, ∀ (x : R), f x = ι (𝔽₄Map (φ x))
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.𝔽₄_solution
Proof state before:
case intro
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 * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f (r + 1) = 1 - f r
hr1 : f r * f r = f r + 1
hr' : r * r + r = 1
h : Function.Bijective (𝔽₄.cast r)
ι : ℤφ →+* S := ℤφ.castRingHom hr1
h0 : ∀ (x : 𝔽₄), f (𝔽₄.cast r x) = ι (𝔽₄Map x)
⊢ ∃ φ ι, ∀ (x : R), f x = ι (𝔽₄Map (φ x))
Tactic:
let ρ := RingEquiv.ofBijective (𝔽₄.castRingHom hr') h
Proof state after:
case intro
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 * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f (r + 1) = 1 - f r
hr1 : f r * f r = f r + 1
hr' : r * r + r = 1
h : Function.Bijective (𝔽₄.cast r)
ι : ℤφ →+* S := ℤφ.castRingHom hr1
h0 : ∀ (x : 𝔽₄), f (𝔽₄.cast r x) = ι (𝔽₄Map x)
ρ : 𝔽₄ ≃+* R := RingEquiv.ofBijective (𝔽₄.castRingHom hr') h
⊢ ∃ φ ι, ∀ (x : R), f x = ι (𝔽₄Map (φ x))
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.𝔽₄_solution
Proof state before:
case intro
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 * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f (r + 1) = 1 - f r
hr1 : f r * f r = f r + 1
hr' : r * r + r = 1
h : Function.Bijective (𝔽₄.cast r)
ι : ℤφ →+* S := ℤφ.castRingHom hr1
h0 : ∀ (x : 𝔽₄), f (𝔽₄.cast r x) = ι (𝔽₄Map x)
ρ : 𝔽₄ ≃+* R := RingEquiv.ofBijective (𝔽₄.castRingHom hr') h
⊢ ∃ φ ι, ∀ (x : R), f x = ι (𝔽₄Map (φ x))
Tactic:
exact ⟨ρ.symm, ι, λ x ↦ h0 _ ▸ congrArg f (Equiv.apply_symm_apply ρ.toEquiv _).symm⟩
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.𝔽₄_solution
Proof 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 * (r + 1) + 1 = 0
X : 1 = 0
⊢ 2 = 0
Tactic:
apply congrArg f at X
Proof 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 * (r + 1) + 1 = 0
X : f 1 = f 0
⊢ 2 = 0
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.𝔽₄_solution
Proof 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 * (r + 1) + 1 = 0
X : f 1 = f 0
⊢ 2 = 0
Tactic:
rw [hf.map_one, hf.map_zero, zero_eq_neg] at X
Proof 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 * (r + 1) + 1 = 0
X : 1 = 0
⊢ 2 = 0
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.𝔽₄_solution
Proof 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 * (r + 1) + 1 = 0
X : 1 = 0
⊢ 2 = 0
Tactic:
rw [← mul_one 2, X, mul_zero]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.𝔽₄_solution
Proof 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 * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f r + f (r + 1) = 1
hr1 : f r * f (r + 1) = -1
⊢ r * r + r = 1
Tactic:
rwa [← mul_add_one r, ← add_eq_zero_iff_eq]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.𝔽₄_solution
Proof 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 * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f r + f (r + 1) = 1
hr1 : f r * f (r + 1) = -1
hr' : r * r + r = 1
⊢ Function.Bijective (𝔽₄.cast r)
Tactic:
refine ⟨𝔽₄.castRingHom_injective hr' X, λ x ↦ ?_⟩
Proof 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 * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f r + f (r + 1) = 1
hr1 : f r * f (r + 1) = -1
hr' : r * r + r = 1
x : R
⊢ ∃ a, 𝔽₄.cast r a = x
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.𝔽₄_solution
Proof 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 * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f r + f (r + 1) = 1
hr1 : f r * f (r + 1) = -1
hr' : r * r + r = 1
x : R
⊢ ∃ a, 𝔽₄.cast r a = x
Tactic:
have h0 {x} (h0 : x * x = 0) : x = 0 := R_elts_claim2 hS hf h0 hr
Proof 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 * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f r + f (r + 1) = 1
hr1 : f r * f (r + 1) = -1
hr' : r * r + r = 1
x : R
h0 : ∀ {x : R}, x * x = 0 → x = 0
⊢ ∃ a, 𝔽₄.cast r a = x
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.𝔽₄_solution
Proof 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 * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f r + f (r + 1) = 1
hr1 : f r * f (r + 1) = -1
hr' : r * r + r = 1
x : R
h0 : ∀ {x : R}, x * x = 0 → x = 0
⊢ ∃ a, 𝔽₄.cast r a = x
Tactic:
rcases R_elts_cases hS hf x with (h1 | h1) | h1
Proof 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 * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f r + f (r + 1) = 1
hr1 : f r * f (r + 1) = -1
hr' : r * r + r = 1
x : R
h0 : ∀ {x : R}, x * x = 0 → x = 0
h1 : (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 * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f r + f (r + 1) = 1
hr1 : f r * f (r + 1) = -1
hr' : r * r + r = 1
x : R
h0 : ∀ {x : R}, x * x = 0 → x = 0
h1 : 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 * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f r + f (r + 1) = 1
hr1 : f r * f (r + 1) = -1
hr' : r * r + r = 1
x : R
h0 : ∀ {x : R}, x * x = 0 → x = 0
h1 : x * (x + 1) + 1 = 0
⊢ ∃ a, 𝔽₄.cast r a = x
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.𝔽₄_solution
Proof 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 * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f r + f (r + 1) = 1
hr1 : f r * f (r + 1) = -1
hr' : r * r + r = 1
x : R
h0 : ∀ {x : R}, x * x = 0 → x = 0
h1 : x * (x + 1) + 1 = 0
⊢ ∃ a, 𝔽₄.cast r a = x
Tactic:
rcases R_elts_cases hS hf (x + r) with (h2 | h2) | h2
Proof state after:
case inr.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 * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f r + f (r + 1) = 1
hr1 : f r * f (r + 1) = -1
hr' : r * r + r = 1
x : R
h0 : ∀ {x : R}, x * x = 0 → x = 0
h1 : x * (x + 1) + 1 = 0
h2 : (x + r + 1) * (x + r + 1) = 0
⊢ ∃ a, 𝔽₄.cast r a = x

case inr.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 * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f r + f (r + 1) = 1
hr1 : f r * f (r + 1) = -1
hr' : r * r + r = 1
x : R
h0 : ∀ {x : R}, x * x = 0 → x = 0
h1 : x * (x + 1) + 1 = 0
h2 : (x + r) * (x + r) = 0
⊢ ∃ a, 𝔽₄.cast r a = x

case inr.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 * (r + 1) + 1 = 0
X : 1 ≠ 0
hr0 : f r + f (r + 1) = 1
hr1 : f r * f (r + 1) = -1
hr' : r * r + r = 1
x : R
h0 : ∀ {x : R}, x * x = 0 → x = 0
h1 : x * (x + 1) + 1 = 0
h2 : (x + r) * (x + r + 1) + 1 = 0
⊢ ∃ a, 𝔽₄.cast r a = x