internlm/Lean-Github huggingface dataset:
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.𝔽₄_solution
Proof state before:
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
Tactic:
rw [_root_.add_comm x r, add_assoc, mul_add, add_mul, add_mul, add_assoc, add_assoc,
  add_assoc, h1, add_zero, mul_add_one r, ← add_assoc (x * r), add_left_comm, hr'] at h2
Proof state after:
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 + r * x + 1 = 0
⊢ ∃ a, 𝔽₄.cast r a = x
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.𝔽₄_solution
Proof state before:
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 + r * x + 1 = 0
⊢ ∃ a, 𝔽₄.cast r a = x
Tactic:
rcases R_elts_cases hS hf (x * r) with (h3 | h3) | h3
Proof state after:
case inr.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 + r * x + 1 = 0
h3 : (x * r + 1) * (x * r + 1) = 0
⊢ ∃ a, 𝔽₄.cast r a = x

case inr.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 + r * x + 1 = 0
h3 : x * r * (x * r) = 0
⊢ ∃ a, 𝔽₄.cast r a = x

case inr.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 + r * x + 1 = 0
h3 : x * r * (x * r + 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 * (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
Tactic:
exact ⟨1, (add_eq_zero_iff_eq.mp (h0 h1)).symm⟩
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 * (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
Tactic:
exact ⟨0, (h0 h1).symm⟩
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.𝔽₄_solution
Proof state before:
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
Tactic:
exact ⟨𝔽₄.Y, (add_eq_zero_iff_eq.mp <| (add_assoc x r 1).symm.trans (h0 h2)).symm⟩
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.𝔽₄_solution
Proof state before:
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
Tactic:
exact ⟨𝔽₄.X, (add_eq_zero_iff_eq.mp (h0 h2)).symm⟩
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.𝔽₄_solution
Proof state before:
case inr.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 + r * x + 1 = 0
h3 : (x * r + 1) * (x * r + 1) = 0
⊢ ∃ a, 𝔽₄.cast r a = x
Tactic:
apply h0 at h3
Proof state after:
case inr.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 + r * x + 1 = 0
h3 : x * r + 1 = 0
⊢ ∃ a, 𝔽₄.cast r a = x
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.𝔽₄_solution
Proof state before:
case inr.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 + r * x + 1 = 0
h3 : x * r + 1 = 0
⊢ ∃ a, 𝔽₄.cast r a = x
Tactic:
rw [add_right_comm, h3, zero_add] at h2
Proof state after:
case inr.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 : r * x = 0
h3 : x * r + 1 = 0
⊢ ∃ a, 𝔽₄.cast r a = x
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.𝔽₄_solution
Proof state before:
case inr.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 : r * x = 0
h3 : r * (x * r + 1) = r * 0
⊢ ∃ a, 𝔽₄.cast r a = x
Tactic:
rw [mul_zero, mul_add_one r, ← mul_assoc, h2, zero_mul, zero_add] at h3
Proof state after:
case inr.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 : r * x = 0
h3 : r = 0
⊢ ∃ a, 𝔽₄.cast r a = x
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.𝔽₄_solution
Proof state before:
case inr.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 : r * x = 0
h3 : r = 0
⊢ ∃ a, 𝔽₄.cast r a = x
Tactic:
rw [h3, zero_mul, zero_add] at hr
Proof state after:
case inr.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 : 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 : r * x = 0
h3 : r = 0
⊢ ∃ a, 𝔽₄.cast r a = x
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.𝔽₄_solution
Proof state before:
case inr.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 : 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 : r * x = 0
h3 : r = 0
⊢ ∃ a, 𝔽₄.cast r a = x
Tactic:
exact absurd hr X
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.𝔽₄_solution
Proof state before:
case inr.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 + r * x + 1 = 0
h3 : x * r * (x * r) = 0
⊢ ∃ a, 𝔽₄.cast r a = x
Tactic:
apply h0 at h3
Proof state after:
case inr.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 + r * x + 1 = 0
h3 : x * r = 0
⊢ ∃ a, 𝔽₄.cast r a = x
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.𝔽₄_solution
Proof state before:
case inr.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 + r * x + 1 = 0
h3 : x * r = 0
⊢ ∃ a, 𝔽₄.cast r a = x
Tactic:
rw [h3, zero_add, add_eq_zero_iff_eq] at h2
Proof state after:
case inr.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 : r * x = 1
h3 : x * r = 0
⊢ ∃ a, 𝔽₄.cast r a = x
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.𝔽₄_solution
Proof state before:
case inr.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 : r * x = 1
h3 : x * r = 0
⊢ ∃ a, 𝔽₄.cast r a = x
Tactic:
have h4 : r = 0 := by rw [← one_mul r, ← h2, mul_assoc, h3, mul_zero]
Proof state after:
case inr.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 : r * x = 1
h3 : x * r = 0
h4 : r = 0
⊢ ∃ a, 𝔽₄.cast r a = x
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.𝔽₄_solution
Proof state before:
case inr.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 : r * x = 1
h3 : x * r = 0
h4 : r = 0
⊢ ∃ a, 𝔽₄.cast r a = x
Tactic:
rw [h4, zero_mul, zero_add] at hr
Proof state after:
case inr.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 : 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 : r * x = 1
h3 : x * r = 0
h4 : r = 0
⊢ ∃ a, 𝔽₄.cast r a = x
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.𝔽₄_solution
Proof state before:
case inr.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 : 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 : r * x = 1
h3 : x * r = 0
h4 : r = 0
⊢ ∃ a, 𝔽₄.cast r a = x
Tactic:
exact absurd hr X
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
x : R
h0 : ∀ {x : R}, x * x = 0 → x = 0
h1 : x * (x + 1) + 1 = 0
h2 : r * x = 1
h3 : x * r = 0
⊢ r = 0
Tactic:
rw [← one_mul r, ← h2, mul_assoc, h3, mul_zero]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.𝔽₄_solution
Proof state before:
case inr.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 + r * x + 1 = 0
h3 : x * r * (x * r + 1) + 1 = 0
⊢ ∃ a, 𝔽₄.cast r a = x
Tactic:
rw [add_right_comm, add_eq_zero_iff_eq] at h2
Proof state after:
case inr.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 + 1 = r * x
h3 : x * r * (x * r + 1) + 1 = 0
⊢ ∃ a, 𝔽₄.cast r a = x
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.𝔽₄_solution
Proof state before:
case inr.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 + 1 = r * x
h3 : x * r * (x * r + 1) + 1 = 0
⊢ ∃ a, 𝔽₄.cast r a = x
Tactic:
rw [mul_add_one x, add_assoc, add_eq_zero_iff_eq] at h1
Proof state after:
case inr.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 = x + 1
h2 : x * r + 1 = r * x
h3 : x * r * (x * r + 1) + 1 = 0
⊢ ∃ a, 𝔽₄.cast r a = x
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.𝔽₄_solution
Proof state before:
case inr.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 = x + 1
h2 : x * r + 1 = r * x
h3 : x * r * (x * r + 1) + 1 = 0
⊢ ∃ a, 𝔽₄.cast r a = x
Tactic:
rw [h2, ← mul_assoc, mul_assoc x, add_eq_iff_eq_add'.mp hr', mul_add_one x, add_mul,
  h1, add_assoc, add_add_cancel_right, ← add_one_mul _ x, h2, mul_assoc, h1] at h3
Proof state after:
case inr.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 = x + 1
h2 : x * r + 1 = r * x
h3 : r * (x + 1) = 0
⊢ ∃ a, 𝔽₄.cast r a = x
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.𝔽₄_solution
Proof state before:
case inr.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 = x + 1
h2 : x * r + 1 = r * x
h3 : r * (x + 1) * x = 0 * x
⊢ ∃ a, 𝔽₄.cast r a = x
Tactic:
rw [zero_mul, mul_assoc, add_one_mul x, h1, add_add_cancel_middle₂, mul_one] at h3
Proof state after:
case inr.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 = x + 1
h2 : x * r + 1 = r * x
h3 : r = 0
⊢ ∃ a, 𝔽₄.cast r a = x
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.𝔽₄_solution
Proof state before:
case inr.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 = x + 1
h2 : x * r + 1 = r * x
h3 : r = 0
⊢ ∃ a, 𝔽₄.cast r a = x
Tactic:
rw [h3, zero_mul, zero_add] at hr
Proof state after:
case inr.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 : 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 = x + 1
h2 : x * r + 1 = r * x
h3 : r = 0
⊢ ∃ a, 𝔽₄.cast r a = x
Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.𝔽₄_solution
Proof state before:
case inr.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 : 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 = x + 1
h2 : x * r + 1 = r * x
h3 : r = 0
⊢ ∃ a, 𝔽₄.cast r a = x
Tactic:
exact absurd hr X
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 + 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
⊢ f (𝔽₄.cast r 𝔽₄.O) = ι (𝔽₄Map 𝔽₄.O)
Tactic:
change f 0 = ι (-1)
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 + 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
⊢ 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 * (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
⊢ f 0 = ι (-1)
Tactic:
rw [hf.map_zero, ι.map_neg, ι.map_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 * (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
⊢ f (𝔽₄.cast r 𝔽₄.Y) = ι (𝔽₄Map 𝔽₄.Y)
Tactic:
change f (r + 1) = ((1 : ℤ) : S) + (-1 : ℤ) • f 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 * (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
⊢ f (r + 1) = ↑1 + -1 • f r
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 + 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
⊢ f (r + 1) = ↑1 + -1 • f r
Tactic:
rw [Int.cast_one, neg_one_zsmul, hr0, sub_eq_add_neg]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A7.le_max_one_sq
Proof state before:
R : Type u_1
inst✝ : LinearOrderedRing R
a : R
⊢ a ≤ max 1 (a ^ 2)
Tactic:
apply (le_abs_self a).trans
Proof state after:
R : Type u_1
inst✝ : LinearOrderedRing R
a : R
⊢ |a| ≤ max 1 (a ^ 2)
Theorem: IMOSL.IMO2012A7.le_max_one_sq
Proof state before:
R : Type u_1
inst✝ : LinearOrderedRing R
a : R
⊢ |a| ≤ max 1 (a ^ 2)
Tactic:
rw [← sq_abs, le_max_iff]
Proof state after:
R : Type u_1
inst✝ : LinearOrderedRing R
a : R
⊢ |a| ≤ 1 ∨ |a| ≤ |a| ^ 2
Theorem: IMOSL.IMO2012A7.le_max_one_sq
Proof state before:
R : Type u_1
inst✝ : LinearOrderedRing R
a : R
⊢ |a| ≤ 1 ∨ |a| ≤ |a| ^ 2
Tactic:
exact (le_total |a| 1).imp_right λ h ↦ le_self_pow h (Nat.succ_ne_zero 1)
Proof state after:
no goals
Theorem: IMOSL.IMO2012A7.pos_part_mul_pos_part_main_formula
Proof state before:
R : Type u_1
inst✝ : LinearOrderedRing R
a b : R
⊢ a⁺ * b⁺ = (min (a * b) (min (max a (a * b ^ 2)) (max b (a ^ 2 * b))))⁺
Tactic:
rcases le_total a 0 with h | h
Proof state after:
case inl
R : Type u_1
inst✝ : LinearOrderedRing R
a b : R
h : a ≤ 0
⊢ a⁺ * b⁺ = (min (a * b) (min (max a (a * b ^ 2)) (max b (a ^ 2 * b))))⁺

case inr
R : Type u_1
inst✝ : LinearOrderedRing R
a b : R
h : 0 ≤ a
⊢ a⁺ * b⁺ = (min (a * b) (min (max a (a * b ^ 2)) (max b (a ^ 2 * b))))⁺
Theorem: IMOSL.IMO2012A7.pos_part_mul_pos_part_main_formula
Proof state before:
case inr
R : Type u_1
inst✝ : LinearOrderedRing R
a b : R
h : 0 ≤ a
⊢ a⁺ * b⁺ = (min (a * b) (min (max a (a * b ^ 2)) (max b (a ^ 2 * b))))⁺
Tactic:
rcases le_total b 0 with h0 | h0
Proof state after:
case inr.inl
R : Type u_1
inst✝ : LinearOrderedRing R
a b : R
h : 0 ≤ a
h0 : b ≤ 0
⊢ a⁺ * b⁺ = (min (a * b) (min (max a (a * b ^ 2)) (max b (a ^ 2 * b))))⁺

case inr.inr
R : Type u_1
inst✝ : LinearOrderedRing R
a b : R
h : 0 ≤ a
h0 : 0 ≤ b
⊢ a⁺ * b⁺ = (min (a * b) (min (max a (a * b ^ 2)) (max b (a ^ 2 * b))))⁺