internlm/Lean-Github huggingface dataset:
Theorem: Imo1965P2.lemma1
Proof state before:
case pos
a : Fin 3 → Fin 3 → ℝ
p : Fin 3 → Fin 3
hp : Function.Bijective p
hab : propsAB a
i j : Fin 3
h0 : if p i = p j then 0 < a (p i) (p j) else a (p i) (p j) < 0
h1 : i = j
⊢ 0 < (fun i j => a (p i) (p j)) i j
Tactic:
subst h1
Proof state after:
case pos
a : Fin 3 → Fin 3 → ℝ
p : Fin 3 → Fin 3
hp : Function.Bijective p
hab : propsAB a
i : Fin 3
h0 : if p i = p i then 0 < a (p i) (p i) else a (p i) (p i) < 0
⊢ 0 < (fun i j => a (p i) (p j)) i i
Theorem: Imo1965P2.lemma1
Proof state before:
case pos
a : Fin 3 → Fin 3 → ℝ
p : Fin 3 → Fin 3
hp : Function.Bijective p
hab : propsAB a
i : Fin 3
h0 : if p i = p i then 0 < a (p i) (p i) else a (p i) (p i) < 0
⊢ 0 < (fun i j => a (p i) (p j)) i i
Tactic:
simp only [reduceIte] at h0
Proof state after:
case pos
a : Fin 3 → Fin 3 → ℝ
p : Fin 3 → Fin 3
hp : Function.Bijective p
hab : propsAB a
i : Fin 3
h0 : 0 < a (p i) (p i)
⊢ 0 < (fun i j => a (p i) (p j)) i i
Theorem: Imo1965P2.lemma1
Proof state before:
case pos
a : Fin 3 → Fin 3 → ℝ
p : Fin 3 → Fin 3
hp : Function.Bijective p
hab : propsAB a
i : Fin 3
h0 : 0 < a (p i) (p i)
⊢ 0 < (fun i j => a (p i) (p j)) i i
Tactic:
exact h0
Proof state after:
no goals
Theorem: Imo1965P2.lemma1
Proof state before:
case neg
a : Fin 3 → Fin 3 → ℝ
p : Fin 3 → Fin 3
hp : Function.Bijective p
hab : propsAB a
i j : Fin 3
h0 : if p i = p j then 0 < a (p i) (p j) else a (p i) (p j) < 0
h1 : ¬i = j
⊢ (fun i j => a (p i) (p j)) i j < 0
Tactic:
have h2 : p i ≠ p j := fun a ↦ h1 (hp.1 a)
Proof state after:
case neg
a : Fin 3 → Fin 3 → ℝ
p : Fin 3 → Fin 3
hp : Function.Bijective p
hab : propsAB a
i j : Fin 3
h0 : if p i = p j then 0 < a (p i) (p j) else a (p i) (p j) < 0
h1 : ¬i = j
h2 : p i ≠ p j
⊢ (fun i j => a (p i) (p j)) i j < 0
Theorem: Imo1965P2.lemma1
Proof state before:
case neg
a : Fin 3 → Fin 3 → ℝ
p : Fin 3 → Fin 3
hp : Function.Bijective p
hab : propsAB a
i j : Fin 3
h0 : if p i = p j then 0 < a (p i) (p j) else a (p i) (p j) < 0
h1 : ¬i = j
h2 : p i ≠ p j
⊢ (fun i j => a (p i) (p j)) i j < 0
Tactic:
simp only [h2] at h0
Proof state after:
case neg
a : Fin 3 → Fin 3 → ℝ
p : Fin 3 → Fin 3
hp : Function.Bijective p
hab : propsAB a
i j : Fin 3
h1 : ¬i = j
h2 : p i ≠ p j
h0 : if False then 0 < a (p i) (p j) else a (p i) (p j) < 0
⊢ (fun i j => a (p i) (p j)) i j < 0
Theorem: Imo1965P2.lemma1
Proof state before:
case neg
a : Fin 3 → Fin 3 → ℝ
p : Fin 3 → Fin 3
hp : Function.Bijective p
hab : propsAB a
i j : Fin 3
h1 : ¬i = j
h2 : p i ≠ p j
h0 : if False then 0 < a (p i) (p j) else a (p i) (p j) < 0
⊢ (fun i j => a (p i) (p j)) i j < 0
Tactic:
exact h0
Proof state after:
no goals
Theorem: Imo1965P2.lemma2
Proof state before:
a : Fin 3 → Fin 3 → ℝ
p : Fin 3 → Fin 3
hp : Function.Bijective p
hc : ∀ (i : Fin 3), 0 < ∑ j : Fin 3, a i j
⊢ ∀ (i : Fin 3), 0 < ∑ j : Fin 3, a (p i) (p j)
Tactic:
intro i
Proof state after:
a : Fin 3 → Fin 3 → ℝ
p : Fin 3 → Fin 3
hp : Function.Bijective p
hc : ∀ (i : Fin 3), 0 < ∑ j : Fin 3, a i j
i : Fin 3
⊢ 0 < ∑ j : Fin 3, a (p i) (p j)
Theorem: Imo1965P2.lemma2
Proof state before:
a : Fin 3 → Fin 3 → ℝ
p : Fin 3 → Fin 3
hp : Function.Bijective p
hc : ∀ (i : Fin 3), 0 < ∑ j : Fin 3, a i j
i : Fin 3
⊢ 0 < ∑ j : Fin 3, a (p i) (p j)
Tactic:
rw [Function.Bijective.sum_comp hp]
Proof state after:
a : Fin 3 → Fin 3 → ℝ
p : Fin 3 → Fin 3
hp : Function.Bijective p
hc : ∀ (i : Fin 3), 0 < ∑ j : Fin 3, a i j
i : Fin 3
⊢ 0 < ∑ i_1 : Fin 3, a (p i) i_1
Theorem: Imo1965P2.lemma2
Proof state before:
a : Fin 3 → Fin 3 → ℝ
p : Fin 3 → Fin 3
hp : Function.Bijective p
hc : ∀ (i : Fin 3), 0 < ∑ j : Fin 3, a i j
i : Fin 3
⊢ 0 < ∑ i_1 : Fin 3, a (p i) i_1
Tactic:
exact hc (p i)
Proof state after:
no goals
Theorem: Imo2008P3.p_lemma
Proof state before:
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
⊢ ∃ n, p ∣ n ^ 2 + 1 ∧ ↑p > 2 * ↑n + √(2 * ↑n)
Tactic:
haveI := Fact.mk hpp
Proof state after:
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
⊢ ∃ n, p ∣ n ^ 2 + 1 ∧ ↑p > 2 * ↑n + √(2 * ↑n)
Theorem: Imo2008P3.p_lemma
Proof state before:
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
⊢ ∃ n, p ∣ n ^ 2 + 1 ∧ ↑p > 2 * ↑n + √(2 * ↑n)
Tactic:
have hp_mod_4_ne_3 : p % 4 ≠ 3 := by linarith [show p % 4 = 1 from hp_mod_4_eq_1]
Proof state after:
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
⊢ ∃ n, p ∣ n ^ 2 + 1 ∧ ↑p > 2 * ↑n + √(2 * ↑n)
Theorem: Imo2008P3.p_lemma
Proof state before:
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
⊢ ∃ n, p ∣ n ^ 2 + 1 ∧ ↑p > 2 * ↑n + √(2 * ↑n)
Tactic:
obtain ⟨y, hy⟩ := ZMod.exists_sq_eq_neg_one_iff.mpr hp_mod_4_ne_3
Proof state after:
case intro
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
⊢ ∃ n, p ∣ n ^ 2 + 1 ∧ ↑p > 2 * ↑n + √(2 * ↑n)
Theorem: Imo2008P3.p_lemma
Proof state before:
case intro
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
⊢ ∃ n, p ∣ n ^ 2 + 1 ∧ ↑p > 2 * ↑n + √(2 * ↑n)
Tactic:
let m := ZMod.valMinAbs y
Proof state after:
case intro
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
⊢ ∃ n, p ∣ n ^ 2 + 1 ∧ ↑p > 2 * ↑n + √(2 * ↑n)
Theorem: Imo2008P3.p_lemma
Proof state before:
case intro
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
⊢ ∃ n, p ∣ n ^ 2 + 1 ∧ ↑p > 2 * ↑n + √(2 * ↑n)
Tactic:
let n := Int.natAbs m
Proof state after:
case intro
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
⊢ ∃ n, p ∣ n ^ 2 + 1 ∧ ↑p > 2 * ↑n + √(2 * ↑n)
Theorem: Imo2008P3.p_lemma
Proof state before:
case intro
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
⊢ ∃ n, p ∣ n ^ 2 + 1 ∧ ↑p > 2 * ↑n + √(2 * ↑n)
Tactic:
have hnat₁ : p ∣ n ^ 2 + 1 := by
  refine Int.natCast_dvd_natCast.mp ?_
  simp only [n, Int.natAbs_sq, Int.natCast_pow, Int.ofNat_succ, Int.natCast_dvd_natCast.mp]
  refine (ZMod.intCast_zmod_eq_zero_iff_dvd (m ^ 2 + 1) p).mp ?_
  simp only [m, Int.cast_pow, Int.cast_add, Int.cast_one, ZMod.coe_valMinAbs]
  rw [pow_two, ← hy]; exact add_left_neg 1
Proof state after:
case intro
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₁ : p ∣ n ^ 2 + 1
⊢ ∃ n, p ∣ n ^ 2 + 1 ∧ ↑p > 2 * ↑n + √(2 * ↑n)
Theorem: Imo2008P3.p_lemma
Proof state before:
case intro
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₁ : p ∣ n ^ 2 + 1
⊢ ∃ n, p ∣ n ^ 2 + 1 ∧ ↑p > 2 * ↑n + √(2 * ↑n)
Tactic:
have hnat₂ : n ≤ p / 2 := ZMod.natAbs_valMinAbs_le y
Proof state after:
case intro
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₁ : p ∣ n ^ 2 + 1
hnat₂ : n ≤ p / 2
⊢ ∃ n, p ∣ n ^ 2 + 1 ∧ ↑p > 2 * ↑n + √(2 * ↑n)
Theorem: Imo2008P3.p_lemma
Proof state before:
case intro
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₁ : p ∣ n ^ 2 + 1
hnat₂ : n ≤ p / 2
⊢ ∃ n, p ∣ n ^ 2 + 1 ∧ ↑p > 2 * ↑n + √(2 * ↑n)
Tactic:
have hnat₃ : p ≥ 2 * n := by omega
Proof state after:
case intro
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₁ : p ∣ n ^ 2 + 1
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
⊢ ∃ n, p ∣ n ^ 2 + 1 ∧ ↑p > 2 * ↑n + √(2 * ↑n)
Theorem: Imo2008P3.p_lemma
Proof state before:
case intro
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₁ : p ∣ n ^ 2 + 1
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
⊢ ∃ n, p ∣ n ^ 2 + 1 ∧ ↑p > 2 * ↑n + √(2 * ↑n)
Tactic:
set k : ℕ := p - 2 * n with hnat₄
Proof state after:
case intro
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₁ : p ∣ n ^ 2 + 1
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
⊢ ∃ n, p ∣ n ^ 2 + 1 ∧ ↑p > 2 * ↑n + √(2 * ↑n)
Theorem: Imo2008P3.p_lemma
Proof state before:
case intro
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₁ : p ∣ n ^ 2 + 1
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
⊢ ∃ n, p ∣ n ^ 2 + 1 ∧ ↑p > 2 * ↑n + √(2 * ↑n)
Tactic:
have hnat₅ : p ∣ k ^ 2 + 4 := by
  cases' hnat₁ with x hx
  have : (p : ℤ) ∣ (k : ℤ) ^ 2 + 4 := by
    use (p : ℤ) - 4 * n + 4 * x
    have hcast₁ : (k : ℤ) = p - 2 * n := by assumption_mod_cast
    have hcast₂ : (n : ℤ) ^ 2 + 1 = p * x := by assumption_mod_cast
    linear_combination ((k : ℤ) + p - 2 * n) * hcast₁ + 4 * hcast₂
  assumption_mod_cast
Proof state after:
case intro
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₁ : p ∣ n ^ 2 + 1
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
hnat₅ : p ∣ k ^ 2 + 4
⊢ ∃ n, p ∣ n ^ 2 + 1 ∧ ↑p > 2 * ↑n + √(2 * ↑n)
Theorem: Imo2008P3.p_lemma
Proof state before:
case intro
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₁ : p ∣ n ^ 2 + 1
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
hnat₅ : p ∣ k ^ 2 + 4
⊢ ∃ n, p ∣ n ^ 2 + 1 ∧ ↑p > 2 * ↑n + √(2 * ↑n)
Tactic:
have hnat₆ : k ^ 2 + 4 ≥ p := Nat.le_of_dvd (k ^ 2 + 3).succ_pos hnat₅
Proof state after:
case intro
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₁ : p ∣ n ^ 2 + 1
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
hnat₅ : p ∣ k ^ 2 + 4
hnat₆ : k ^ 2 + 4 ≥ p
⊢ ∃ n, p ∣ n ^ 2 + 1 ∧ ↑p > 2 * ↑n + √(2 * ↑n)
Theorem: Imo2008P3.p_lemma
Proof state before:
case intro
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₁ : p ∣ n ^ 2 + 1
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
hnat₅ : p ∣ k ^ 2 + 4
hnat₆ : k ^ 2 + 4 ≥ p
⊢ ∃ n, p ∣ n ^ 2 + 1 ∧ ↑p > 2 * ↑n + √(2 * ↑n)
Tactic:
have hreal₁ : (k : ℝ) = p - 2 * n := by assumption_mod_cast
Proof state after:
case intro
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₁ : p ∣ n ^ 2 + 1
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
hnat₅ : p ∣ k ^ 2 + 4
hnat₆ : k ^ 2 + 4 ≥ p
hreal₁ : ↑k = ↑p - 2 * ↑n
⊢ ∃ n, p ∣ n ^ 2 + 1 ∧ ↑p > 2 * ↑n + √(2 * ↑n)
Theorem: Imo2008P3.p_lemma
Proof state before:
case intro
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₁ : p ∣ n ^ 2 + 1
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
hnat₅ : p ∣ k ^ 2 + 4
hnat₆ : k ^ 2 + 4 ≥ p
hreal₁ : ↑k = ↑p - 2 * ↑n
⊢ ∃ n, p ∣ n ^ 2 + 1 ∧ ↑p > 2 * ↑n + √(2 * ↑n)
Tactic:
have hreal₂ : (p : ℝ) > 20 := by assumption_mod_cast
Proof state after:
case intro
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₁ : p ∣ n ^ 2 + 1
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
hnat₅ : p ∣ k ^ 2 + 4
hnat₆ : k ^ 2 + 4 ≥ p
hreal₁ : ↑k = ↑p - 2 * ↑n
hreal₂ : ↑p > 20
⊢ ∃ n, p ∣ n ^ 2 + 1 ∧ ↑p > 2 * ↑n + √(2 * ↑n)
Theorem: Imo2008P3.p_lemma
Proof state before:
case intro
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₁ : p ∣ n ^ 2 + 1
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
hnat₅ : p ∣ k ^ 2 + 4
hnat₆ : k ^ 2 + 4 ≥ p
hreal₁ : ↑k = ↑p - 2 * ↑n
hreal₂ : ↑p > 20
⊢ ∃ n, p ∣ n ^ 2 + 1 ∧ ↑p > 2 * ↑n + √(2 * ↑n)
Tactic:
have hreal₃ : (k : ℝ) ^ 2 + 4 ≥ p := by assumption_mod_cast
Proof state after:
case intro
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₁ : p ∣ n ^ 2 + 1
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
hnat₅ : p ∣ k ^ 2 + 4
hnat₆ : k ^ 2 + 4 ≥ p
hreal₁ : ↑k = ↑p - 2 * ↑n
hreal₂ : ↑p > 20
hreal₃ : ↑k ^ 2 + 4 ≥ ↑p
⊢ ∃ n, p ∣ n ^ 2 + 1 ∧ ↑p > 2 * ↑n + √(2 * ↑n)
Theorem: Imo2008P3.p_lemma
Proof state before:
case intro
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₁ : p ∣ n ^ 2 + 1
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
hnat₅ : p ∣ k ^ 2 + 4
hnat₆ : k ^ 2 + 4 ≥ p
hreal₁ : ↑k = ↑p - 2 * ↑n
hreal₂ : ↑p > 20
hreal₃ : ↑k ^ 2 + 4 ≥ ↑p
⊢ ∃ n, p ∣ n ^ 2 + 1 ∧ ↑p > 2 * ↑n + √(2 * ↑n)
Tactic:
have hreal₅ : (k : ℝ) > 4 := by
  refine lt_of_pow_lt_pow_left 2 k.cast_nonneg ?_
  linarith only [hreal₂, hreal₃]
Proof state after:
case intro
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₁ : p ∣ n ^ 2 + 1
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
hnat₅ : p ∣ k ^ 2 + 4
hnat₆ : k ^ 2 + 4 ≥ p
hreal₁ : ↑k = ↑p - 2 * ↑n
hreal₂ : ↑p > 20
hreal₃ : ↑k ^ 2 + 4 ≥ ↑p
hreal₅ : ↑k > 4
⊢ ∃ n, p ∣ n ^ 2 + 1 ∧ ↑p > 2 * ↑n + √(2 * ↑n)
Theorem: Imo2008P3.p_lemma
Proof state before:
case intro
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₁ : p ∣ n ^ 2 + 1
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
hnat₅ : p ∣ k ^ 2 + 4
hnat₆ : k ^ 2 + 4 ≥ p
hreal₁ : ↑k = ↑p - 2 * ↑n
hreal₂ : ↑p > 20
hreal₃ : ↑k ^ 2 + 4 ≥ ↑p
hreal₅ : ↑k > 4
⊢ ∃ n, p ∣ n ^ 2 + 1 ∧ ↑p > 2 * ↑n + √(2 * ↑n)
Tactic:
have hreal₆ : (k : ℝ) > sqrt (2 * n) := by
  refine lt_of_pow_lt_pow_left 2 k.cast_nonneg ?_
  rw [sq_sqrt (mul_nonneg zero_le_two n.cast_nonneg)]
  linarith only [hreal₁, hreal₃, hreal₅]
Proof state after:
case intro
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₁ : p ∣ n ^ 2 + 1
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
hnat₅ : p ∣ k ^ 2 + 4
hnat₆ : k ^ 2 + 4 ≥ p
hreal₁ : ↑k = ↑p - 2 * ↑n
hreal₂ : ↑p > 20
hreal₃ : ↑k ^ 2 + 4 ≥ ↑p
hreal₅ : ↑k > 4
hreal₆ : ↑k > √(2 * ↑n)
⊢ ∃ n, p ∣ n ^ 2 + 1 ∧ ↑p > 2 * ↑n + √(2 * ↑n)
Theorem: Imo2008P3.p_lemma
Proof state before:
case intro
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₁ : p ∣ n ^ 2 + 1
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
hnat₅ : p ∣ k ^ 2 + 4
hnat₆ : k ^ 2 + 4 ≥ p
hreal₁ : ↑k = ↑p - 2 * ↑n
hreal₂ : ↑p > 20
hreal₃ : ↑k ^ 2 + 4 ≥ ↑p
hreal₅ : ↑k > 4
hreal₆ : ↑k > √(2 * ↑n)
⊢ ∃ n, p ∣ n ^ 2 + 1 ∧ ↑p > 2 * ↑n + √(2 * ↑n)
Tactic:
exact ⟨n, hnat₁, by linarith only [hreal₆, hreal₁]⟩
Proof state after:
no goals
Theorem: Imo2008P3.p_lemma
Proof state before:
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
⊢ p % 4 ≠ 3
Tactic:
linarith [show p % 4 = 1 from hp_mod_4_eq_1]
Proof state after:
no goals
Theorem: Imo2008P3.p_lemma
Proof state before:
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
⊢ p ∣ n ^ 2 + 1
Tactic:
refine Int.natCast_dvd_natCast.mp ?_
Proof state after:
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
⊢ ↑p ∣ ↑(n ^ 2 + 1)
Theorem: Imo2008P3.p_lemma
Proof state before:
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
⊢ ↑p ∣ ↑(n ^ 2 + 1)
Tactic:
simp only [n, Int.natAbs_sq, Int.natCast_pow, Int.ofNat_succ, Int.natCast_dvd_natCast.mp]
Proof state after:
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
⊢ ↑p ∣ m ^ 2 + 1
Theorem: Imo2008P3.p_lemma
Proof state before:
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
⊢ ↑p ∣ m ^ 2 + 1
Tactic:
refine (ZMod.intCast_zmod_eq_zero_iff_dvd (m ^ 2 + 1) p).mp ?_
Proof state after:
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
⊢ ↑(m ^ 2 + 1) = 0
Theorem: Imo2008P3.p_lemma
Proof state before:
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
⊢ ↑(m ^ 2 + 1) = 0
Tactic:
simp only [m, Int.cast_pow, Int.cast_add, Int.cast_one, ZMod.coe_valMinAbs]
Proof state after:
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
⊢ y ^ 2 + 1 = 0
Theorem: Imo2008P3.p_lemma
Proof state before:
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
⊢ y ^ 2 + 1 = 0
Tactic:
rw [pow_two, ← hy]
Proof state after:
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
⊢ -1 + 1 = 0
Theorem: Imo2008P3.p_lemma
Proof state before:
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
⊢ -1 + 1 = 0
Tactic:
exact add_left_neg 1
Proof state after:
no goals
Theorem: Imo2008P3.p_lemma
Proof state before:
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₁ : p ∣ n ^ 2 + 1
hnat₂ : n ≤ p / 2
⊢ p ≥ 2 * n
Tactic:
omega
Proof state after:
no goals
Theorem: Imo2008P3.p_lemma
Proof state before:
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₁ : p ∣ n ^ 2 + 1
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
⊢ p ∣ k ^ 2 + 4
Tactic:
cases' hnat₁ with x hx
Proof state after:
case intro
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
x : ℕ
hx : n ^ 2 + 1 = p * x
⊢ p ∣ k ^ 2 + 4
Theorem: Imo2008P3.p_lemma
Proof state before:
case intro
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
x : ℕ
hx : n ^ 2 + 1 = p * x
⊢ p ∣ k ^ 2 + 4
Tactic:
have : (p : ℤ) ∣ (k : ℤ) ^ 2 + 4 := by
  use (p : ℤ) - 4 * n + 4 * x
  have hcast₁ : (k : ℤ) = p - 2 * n := by assumption_mod_cast
  have hcast₂ : (n : ℤ) ^ 2 + 1 = p * x := by assumption_mod_cast
  linear_combination ((k : ℤ) + p - 2 * n) * hcast₁ + 4 * hcast₂
Proof state after:
case intro
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this✝ : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
x : ℕ
hx : n ^ 2 + 1 = p * x
this : ↑p ∣ ↑k ^ 2 + 4
⊢ p ∣ k ^ 2 + 4
Theorem: Imo2008P3.p_lemma
Proof state before:
case intro
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this✝ : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
x : ℕ
hx : n ^ 2 + 1 = p * x
this : ↑p ∣ ↑k ^ 2 + 4
⊢ p ∣ k ^ 2 + 4
Tactic:
assumption_mod_cast
Proof state after:
no goals
Theorem: Imo2008P3.p_lemma
Proof state before:
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
x : ℕ
hx : n ^ 2 + 1 = p * x
⊢ ↑p ∣ ↑k ^ 2 + 4
Tactic:
use (p : ℤ) - 4 * n + 4 * x
Proof state after:
case h
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
x : ℕ
hx : n ^ 2 + 1 = p * x
⊢ ↑k ^ 2 + 4 = ↑p * (↑p - 4 * ↑n + 4 * ↑x)
Theorem: Imo2008P3.p_lemma
Proof state before:
case h
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
x : ℕ
hx : n ^ 2 + 1 = p * x
⊢ ↑k ^ 2 + 4 = ↑p * (↑p - 4 * ↑n + 4 * ↑x)
Tactic:
have hcast₁ : (k : ℤ) = p - 2 * n := by assumption_mod_cast
Proof state after:
case h
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
x : ℕ
hx : n ^ 2 + 1 = p * x
hcast₁ : ↑k = ↑p - 2 * ↑n
⊢ ↑k ^ 2 + 4 = ↑p * (↑p - 4 * ↑n + 4 * ↑x)