internlm/Lean-Github huggingface dataset:
Theorem: existsOfSlowMono
Proof state before:
case cons.cons
b y : ℕ
l : List ℕ
a x : ℕ
hl_mono : a < x ∧ List.Chain (fun u v => u < v) x (y :: l)
hl_slow : x ≤ 2 * a ∧ List.Chain (fun u v => v ≤ 2 * u) x (y :: l)
hl_cons : x :: y :: l ≠ []
hb : b < List.getLast (y :: l) (_ : ¬y :: l = [])
n : ℕ
hn : n ∈ Set.Icc a b
h : n ∈ Set.Icc x b → ∃ lᵢ, lᵢ ∈ y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
⊢ ∃ lᵢ, lᵢ ∈ x :: y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
Tactic:
have : ∀ lᵢ, lᵢ ∈ x :: y :: l ↔ lᵢ = x ∨ lᵢ ∈ y :: l := by simp
Proof state after:
case cons.cons
b y : ℕ
l : List ℕ
a x : ℕ
hl_mono : a < x ∧ List.Chain (fun u v => u < v) x (y :: l)
hl_slow : x ≤ 2 * a ∧ List.Chain (fun u v => v ≤ 2 * u) x (y :: l)
hl_cons : x :: y :: l ≠ []
hb : b < List.getLast (y :: l) (_ : ¬y :: l = [])
n : ℕ
hn : n ∈ Set.Icc a b
h : n ∈ Set.Icc x b → ∃ lᵢ, lᵢ ∈ y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
this : ∀ (lᵢ : ℕ), lᵢ ∈ x :: y :: l ↔ lᵢ = x ∨ lᵢ ∈ y :: l
⊢ ∃ lᵢ, lᵢ ∈ x :: y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
Theorem: existsOfSlowMono
Proof state before:
case cons.cons
b y : ℕ
l : List ℕ
a x : ℕ
hl_mono : a < x ∧ List.Chain (fun u v => u < v) x (y :: l)
hl_slow : x ≤ 2 * a ∧ List.Chain (fun u v => v ≤ 2 * u) x (y :: l)
hl_cons : x :: y :: l ≠ []
hb : b < List.getLast (y :: l) (_ : ¬y :: l = [])
n : ℕ
hn : n ∈ Set.Icc a b
h : n ∈ Set.Icc x b → ∃ lᵢ, lᵢ ∈ y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
this : ∀ (lᵢ : ℕ), lᵢ ∈ x :: y :: l ↔ lᵢ = x ∨ lᵢ ∈ y :: l
⊢ ∃ lᵢ, lᵢ ∈ x :: y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
Tactic:
simp_rw [this]
Proof state after:
case cons.cons
b y : ℕ
l : List ℕ
a x : ℕ
hl_mono : a < x ∧ List.Chain (fun u v => u < v) x (y :: l)
hl_slow : x ≤ 2 * a ∧ List.Chain (fun u v => v ≤ 2 * u) x (y :: l)
hl_cons : x :: y :: l ≠ []
hb : b < List.getLast (y :: l) (_ : ¬y :: l = [])
n : ℕ
hn : n ∈ Set.Icc a b
h : n ∈ Set.Icc x b → ∃ lᵢ, lᵢ ∈ y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
this : ∀ (lᵢ : ℕ), lᵢ ∈ x :: y :: l ↔ lᵢ = x ∨ lᵢ ∈ y :: l
⊢ ∃ lᵢ, (lᵢ = x ∨ lᵢ ∈ y :: l) ∧ lᵢ ∈ Set.Ioc n (2 * n)
Theorem: existsOfSlowMono
Proof state before:
case cons.cons
b y : ℕ
l : List ℕ
a x : ℕ
hl_mono : a < x ∧ List.Chain (fun u v => u < v) x (y :: l)
hl_slow : x ≤ 2 * a ∧ List.Chain (fun u v => v ≤ 2 * u) x (y :: l)
hl_cons : x :: y :: l ≠ []
hb : b < List.getLast (y :: l) (_ : ¬y :: l = [])
n : ℕ
hn : n ∈ Set.Icc a b
h : n ∈ Set.Icc x b → ∃ lᵢ, lᵢ ∈ y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
this : ∀ (lᵢ : ℕ), lᵢ ∈ x :: y :: l ↔ lᵢ = x ∨ lᵢ ∈ y :: l
⊢ ∃ lᵢ, (lᵢ = x ∨ lᵢ ∈ y :: l) ∧ lᵢ ∈ Set.Ioc n (2 * n)
Tactic:
simp only [or_and_right]
Proof state after:
case cons.cons
b y : ℕ
l : List ℕ
a x : ℕ
hl_mono : a < x ∧ List.Chain (fun u v => u < v) x (y :: l)
hl_slow : x ≤ 2 * a ∧ List.Chain (fun u v => v ≤ 2 * u) x (y :: l)
hl_cons : x :: y :: l ≠ []
hb : b < List.getLast (y :: l) (_ : ¬y :: l = [])
n : ℕ
hn : n ∈ Set.Icc a b
h : n ∈ Set.Icc x b → ∃ lᵢ, lᵢ ∈ y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
this : ∀ (lᵢ : ℕ), lᵢ ∈ x :: y :: l ↔ lᵢ = x ∨ lᵢ ∈ y :: l
⊢ ∃ lᵢ, lᵢ = x ∧ lᵢ ∈ Set.Ioc n (2 * n) ∨ lᵢ ∈ y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
Theorem: existsOfSlowMono
Proof state before:
case cons.cons
b y : ℕ
l : List ℕ
a x : ℕ
hl_mono : a < x ∧ List.Chain (fun u v => u < v) x (y :: l)
hl_slow : x ≤ 2 * a ∧ List.Chain (fun u v => v ≤ 2 * u) x (y :: l)
hl_cons : x :: y :: l ≠ []
hb : b < List.getLast (y :: l) (_ : ¬y :: l = [])
n : ℕ
hn : n ∈ Set.Icc a b
h : n ∈ Set.Icc x b → ∃ lᵢ, lᵢ ∈ y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
this : ∀ (lᵢ : ℕ), lᵢ ∈ x :: y :: l ↔ lᵢ = x ∨ lᵢ ∈ y :: l
⊢ ∃ lᵢ, lᵢ = x ∧ lᵢ ∈ Set.Ioc n (2 * n) ∨ lᵢ ∈ y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
Tactic:
rw [exists_or]
Proof state after:
case cons.cons
b y : ℕ
l : List ℕ
a x : ℕ
hl_mono : a < x ∧ List.Chain (fun u v => u < v) x (y :: l)
hl_slow : x ≤ 2 * a ∧ List.Chain (fun u v => v ≤ 2 * u) x (y :: l)
hl_cons : x :: y :: l ≠ []
hb : b < List.getLast (y :: l) (_ : ¬y :: l = [])
n : ℕ
hn : n ∈ Set.Icc a b
h : n ∈ Set.Icc x b → ∃ lᵢ, lᵢ ∈ y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
this : ∀ (lᵢ : ℕ), lᵢ ∈ x :: y :: l ↔ lᵢ = x ∨ lᵢ ∈ y :: l
⊢ (∃ x_1, x_1 = x ∧ x_1 ∈ Set.Ioc n (2 * n)) ∨ ∃ x, x ∈ y :: l ∧ x ∈ Set.Ioc n (2 * n)
Theorem: existsOfSlowMono
Proof state before:
case cons.cons
b y : ℕ
l : List ℕ
a x : ℕ
hl_mono : a < x ∧ List.Chain (fun u v => u < v) x (y :: l)
hl_slow : x ≤ 2 * a ∧ List.Chain (fun u v => v ≤ 2 * u) x (y :: l)
hl_cons : x :: y :: l ≠ []
hb : b < List.getLast (y :: l) (_ : ¬y :: l = [])
n : ℕ
hn : n ∈ Set.Icc a b
h : n ∈ Set.Icc x b → ∃ lᵢ, lᵢ ∈ y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
this : ∀ (lᵢ : ℕ), lᵢ ∈ x :: y :: l ↔ lᵢ = x ∨ lᵢ ∈ y :: l
⊢ (∃ x_1, x_1 = x ∧ x_1 ∈ Set.Ioc n (2 * n)) ∨ ∃ x, x ∈ y :: l ∧ x ∈ Set.Ioc n (2 * n)
Tactic:
cases le_or_lt x n with
| inl hx =>
  apply Or.inr
  simp only [Set.mem_Ico] at *
  specialize h (And.intro hx hn.right)
  exact h
| inr hx =>
  apply Or.inl
  simp at *
  apply And.intro <;> linarith
Proof state after:
no goals
Theorem: existsOfSlowMono
Proof state before:
b y : ℕ
l : List ℕ
a x : ℕ
hl_mono : a < x ∧ List.Chain (fun u v => u < v) x (y :: l)
hl_slow : x ≤ 2 * a ∧ List.Chain (fun u v => v ≤ 2 * u) x (y :: l)
hl_cons : x :: y :: l ≠ []
hb : b < List.getLast (y :: l) (_ : ¬y :: l = [])
n : ℕ
hn : n ∈ Set.Icc a b
h : n ∈ Set.Icc x b → ∃ lᵢ, lᵢ ∈ y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
⊢ ∀ (lᵢ : ℕ), lᵢ ∈ x :: y :: l ↔ lᵢ = x ∨ lᵢ ∈ y :: l
Tactic:
simp
Proof state after:
no goals
Theorem: existsOfSlowMono
Proof state before:
case cons.cons.inl
b y : ℕ
l : List ℕ
a x : ℕ
hl_mono : a < x ∧ List.Chain (fun u v => u < v) x (y :: l)
hl_slow : x ≤ 2 * a ∧ List.Chain (fun u v => v ≤ 2 * u) x (y :: l)
hl_cons : x :: y :: l ≠ []
hb : b < List.getLast (y :: l) (_ : ¬y :: l = [])
n : ℕ
hn : n ∈ Set.Icc a b
h : n ∈ Set.Icc x b → ∃ lᵢ, lᵢ ∈ y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
this : ∀ (lᵢ : ℕ), lᵢ ∈ x :: y :: l ↔ lᵢ = x ∨ lᵢ ∈ y :: l
hx : x ≤ n
⊢ (∃ x_1, x_1 = x ∧ x_1 ∈ Set.Ioc n (2 * n)) ∨ ∃ x, x ∈ y :: l ∧ x ∈ Set.Ioc n (2 * n)
Tactic:
apply Or.inr
Proof state after:
case cons.cons.inl.h
b y : ℕ
l : List ℕ
a x : ℕ
hl_mono : a < x ∧ List.Chain (fun u v => u < v) x (y :: l)
hl_slow : x ≤ 2 * a ∧ List.Chain (fun u v => v ≤ 2 * u) x (y :: l)
hl_cons : x :: y :: l ≠ []
hb : b < List.getLast (y :: l) (_ : ¬y :: l = [])
n : ℕ
hn : n ∈ Set.Icc a b
h : n ∈ Set.Icc x b → ∃ lᵢ, lᵢ ∈ y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
this : ∀ (lᵢ : ℕ), lᵢ ∈ x :: y :: l ↔ lᵢ = x ∨ lᵢ ∈ y :: l
hx : x ≤ n
⊢ ∃ x, x ∈ y :: l ∧ x ∈ Set.Ioc n (2 * n)
Theorem: existsOfSlowMono
Proof state before:
case cons.cons.inl.h
b y : ℕ
l : List ℕ
a x : ℕ
hl_mono : a < x ∧ List.Chain (fun u v => u < v) x (y :: l)
hl_slow : x ≤ 2 * a ∧ List.Chain (fun u v => v ≤ 2 * u) x (y :: l)
hl_cons : x :: y :: l ≠ []
hb : b < List.getLast (y :: l) (_ : ¬y :: l = [])
n : ℕ
hn : n ∈ Set.Icc a b
h : n ∈ Set.Icc x b → ∃ lᵢ, lᵢ ∈ y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
this : ∀ (lᵢ : ℕ), lᵢ ∈ x :: y :: l ↔ lᵢ = x ∨ lᵢ ∈ y :: l
hx : x ≤ n
⊢ ∃ x, x ∈ y :: l ∧ x ∈ Set.Ioc n (2 * n)
Tactic:
specialize h (And.intro hx hn.right)
Proof state after:
case cons.cons.inl.h
b y : ℕ
l : List ℕ
a x : ℕ
hl_mono : a < x ∧ List.Chain (fun u v => u < v) x (y :: l)
hl_slow : x ≤ 2 * a ∧ List.Chain (fun u v => v ≤ 2 * u) x (y :: l)
hl_cons : x :: y :: l ≠ []
hb : b < List.getLast (y :: l) (_ : ¬y :: l = [])
n : ℕ
hn : n ∈ Set.Icc a b
this : ∀ (lᵢ : ℕ), lᵢ ∈ x :: y :: l ↔ lᵢ = x ∨ lᵢ ∈ y :: l
hx : x ≤ n
h : ∃ lᵢ, lᵢ ∈ y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
⊢ ∃ x, x ∈ y :: l ∧ x ∈ Set.Ioc n (2 * n)
Theorem: existsOfSlowMono
Proof state before:
case cons.cons.inl.h
b y : ℕ
l : List ℕ
a x : ℕ
hl_mono : a < x ∧ List.Chain (fun u v => u < v) x (y :: l)
hl_slow : x ≤ 2 * a ∧ List.Chain (fun u v => v ≤ 2 * u) x (y :: l)
hl_cons : x :: y :: l ≠ []
hb : b < List.getLast (y :: l) (_ : ¬y :: l = [])
n : ℕ
hn : n ∈ Set.Icc a b
this : ∀ (lᵢ : ℕ), lᵢ ∈ x :: y :: l ↔ lᵢ = x ∨ lᵢ ∈ y :: l
hx : x ≤ n
h : ∃ lᵢ, lᵢ ∈ y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
⊢ ∃ x, x ∈ y :: l ∧ x ∈ Set.Ioc n (2 * n)
Tactic:
exact h
Proof state after:
no goals
Theorem: existsOfSlowMono
Proof state before:
case cons.cons.inr
b y : ℕ
l : List ℕ
a x : ℕ
hl_mono : a < x ∧ List.Chain (fun u v => u < v) x (y :: l)
hl_slow : x ≤ 2 * a ∧ List.Chain (fun u v => v ≤ 2 * u) x (y :: l)
hl_cons : x :: y :: l ≠ []
hb : b < List.getLast (y :: l) (_ : ¬y :: l = [])
n : ℕ
hn : n ∈ Set.Icc a b
h : n ∈ Set.Icc x b → ∃ lᵢ, lᵢ ∈ y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
this : ∀ (lᵢ : ℕ), lᵢ ∈ x :: y :: l ↔ lᵢ = x ∨ lᵢ ∈ y :: l
hx : n < x
⊢ (∃ x_1, x_1 = x ∧ x_1 ∈ Set.Ioc n (2 * n)) ∨ ∃ x, x ∈ y :: l ∧ x ∈ Set.Ioc n (2 * n)
Tactic:
apply Or.inl
Proof state after:
case cons.cons.inr.h
b y : ℕ
l : List ℕ
a x : ℕ
hl_mono : a < x ∧ List.Chain (fun u v => u < v) x (y :: l)
hl_slow : x ≤ 2 * a ∧ List.Chain (fun u v => v ≤ 2 * u) x (y :: l)
hl_cons : x :: y :: l ≠ []
hb : b < List.getLast (y :: l) (_ : ¬y :: l = [])
n : ℕ
hn : n ∈ Set.Icc a b
h : n ∈ Set.Icc x b → ∃ lᵢ, lᵢ ∈ y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
this : ∀ (lᵢ : ℕ), lᵢ ∈ x :: y :: l ↔ lᵢ = x ∨ lᵢ ∈ y :: l
hx : n < x
⊢ ∃ x_1, x_1 = x ∧ x_1 ∈ Set.Ioc n (2 * n)
Theorem: existsOfSlowMono
Proof state before:
case cons.cons.inr.h
b y : ℕ
l : List ℕ
a x : ℕ
hl_mono : a < x ∧ List.Chain (fun u v => u < v) x (y :: l)
hl_slow : x ≤ 2 * a ∧ List.Chain (fun u v => v ≤ 2 * u) x (y :: l)
hl_cons : x :: y :: l ≠ []
hb : b < List.getLast (y :: l) (_ : ¬y :: l = [])
n : ℕ
hn : n ∈ Set.Icc a b
h : n ∈ Set.Icc x b → ∃ lᵢ, lᵢ ∈ y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
this : ∀ (lᵢ : ℕ), lᵢ ∈ x :: y :: l ↔ lᵢ = x ∨ lᵢ ∈ y :: l
hx : n < x
⊢ ∃ x_1, x_1 = x ∧ x_1 ∈ Set.Ioc n (2 * n)
Tactic:
simp at *
Proof state after:
case cons.cons.inr.h
b y : ℕ
l : List ℕ
a x : ℕ
hb : b < List.getLast (y :: l) (_ : ¬y :: l = [])
n : ℕ
hx : n < x
hl_mono : a < x ∧ x < y ∧ List.Chain (fun u v => u < v) y l
hl_slow : x ≤ 2 * a ∧ y ≤ 2 * x ∧ List.Chain (fun u v => v ≤ 2 * u) y l
hl_cons : True
hn : a ≤ n ∧ n ≤ b
h : x ≤ n → n ≤ b → n < y ∧ y ≤ 2 * n ∨ ∃ a, a ∈ l ∧ n < a ∧ a ≤ 2 * n
this : True
⊢ n < x ∧ x ≤ 2 * n
Theorem: existsOfSlowMono
Proof state before:
case cons.cons.inr.h
b y : ℕ
l : List ℕ
a x : ℕ
hb : b < List.getLast (y :: l) (_ : ¬y :: l = [])
n : ℕ
hx : n < x
hl_mono : a < x ∧ x < y ∧ List.Chain (fun u v => u < v) y l
hl_slow : x ≤ 2 * a ∧ y ≤ 2 * x ∧ List.Chain (fun u v => v ≤ 2 * u) y l
hl_cons : True
hn : a ≤ n ∧ n ≤ b
h : x ≤ n → n ≤ b → n < y ∧ y ≤ 2 * n ∨ ∃ a, a ∈ l ∧ n < a ∧ a ≤ 2 * n
this : True
⊢ n < x ∧ x ≤ 2 * n
Tactic:
apply And.intro <;> linarith
Proof state after:
no goals
Theorem: landauTrick
Proof state before:
n : ℕ
hn_pos : 0 < n
hn_lt : n ≤ 4000
⊢ ∃ p, p ∈ Set.Ioc n (2 * n) ∧ Nat.Prime p
Tactic:
have hp : n ∈ Set.Icc 1 4000 → ∃ p, p ∈ nums ∧ p ∈ Set.Ioc n (2*n)
Proof state after:
case hp
n : ℕ
hn_pos : 0 < n
hn_lt : n ≤ 4000
⊢ n ∈ Set.Icc 1 4000 → ∃ p, p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)

n : ℕ
hn_pos : 0 < n
hn_lt : n ≤ 4000
hp : n ∈ Set.Icc 1 4000 → ∃ p, p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)
⊢ ∃ p, p ∈ Set.Ioc n (2 * n) ∧ Nat.Prime p
Theorem: landauTrick
Proof state before:
case hp
n : ℕ
hn_pos : 0 < n
hn_lt : n ≤ 4000
⊢ n ∈ Set.Icc 1 4000 → ∃ p, p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)

n : ℕ
hn_pos : 0 < n
hn_lt : n ≤ 4000
hp : n ∈ Set.Icc 1 4000 → ∃ p, p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)
⊢ ∃ p, p ∈ Set.Ioc n (2 * n) ∧ Nat.Prime p
Tactic:
. apply existsOfSlowMono <;> simp [nums]
Proof state after:
n : ℕ
hn_pos : 0 < n
hn_lt : n ≤ 4000
hp : n ∈ Set.Icc 1 4000 → ∃ p, p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)
⊢ ∃ p, p ∈ Set.Ioc n (2 * n) ∧ Nat.Prime p
Theorem: landauTrick
Proof state before:
n : ℕ
hn_pos : 0 < n
hn_lt : n ≤ 4000
hp : n ∈ Set.Icc 1 4000 → ∃ p, p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)
⊢ ∃ p, p ∈ Set.Ioc n (2 * n) ∧ Nat.Prime p
Tactic:
have hp : ∃ p, p ∈ nums ∧ p ∈ Set.Ioc n (2*n)
Proof state after:
case hp
n : ℕ
hn_pos : 0 < n
hn_lt : n ≤ 4000
hp : n ∈ Set.Icc 1 4000 → ∃ p, p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)
⊢ ∃ p, p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)

n : ℕ
hn_pos : 0 < n
hn_lt : n ≤ 4000
hp✝ : n ∈ Set.Icc 1 4000 → ∃ p, p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)
hp : ∃ p, p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)
⊢ ∃ p, p ∈ Set.Ioc n (2 * n) ∧ Nat.Prime p
Theorem: landauTrick
Proof state before:
case hp
n : ℕ
hn_pos : 0 < n
hn_lt : n ≤ 4000
hp : n ∈ Set.Icc 1 4000 → ∃ p, p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)
⊢ ∃ p, p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)

n : ℕ
hn_pos : 0 < n
hn_lt : n ≤ 4000
hp✝ : n ∈ Set.Icc 1 4000 → ∃ p, p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)
hp : ∃ p, p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)
⊢ ∃ p, p ∈ Set.Ioc n (2 * n) ∧ Nat.Prime p
Tactic:
. apply hp
  apply And.intro <;> linarith
Proof state after:
n : ℕ
hn_pos : 0 < n
hn_lt : n ≤ 4000
hp✝ : n ∈ Set.Icc 1 4000 → ∃ p, p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)
hp : ∃ p, p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)
⊢ ∃ p, p ∈ Set.Ioc n (2 * n) ∧ Nat.Prime p
Theorem: landauTrick
Proof state before:
n : ℕ
hn_pos : 0 < n
hn_lt : n ≤ 4000
hp✝ : n ∈ Set.Icc 1 4000 → ∃ p, p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)
hp : ∃ p, p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)
⊢ ∃ p, p ∈ Set.Ioc n (2 * n) ∧ Nat.Prime p
Tactic:
cases hp with
| intro p hp =>
  exists p
  apply And.intro hp.right
  refine List.all₂_iff_forall.mp ?_ p hp.left
  exact allPrimeNums
Proof state after:
no goals
Theorem: landauTrick
Proof state before:
case hp
n : ℕ
hn_pos : 0 < n
hn_lt : n ≤ 4000
⊢ n ∈ Set.Icc 1 4000 → ∃ p, p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)
Tactic:
apply existsOfSlowMono <;> simp [nums]
Proof state after:
no goals
Theorem: landauTrick
Proof state before:
case hp
n : ℕ
hn_pos : 0 < n
hn_lt : n ≤ 4000
hp : n ∈ Set.Icc 1 4000 → ∃ p, p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)
⊢ ∃ p, p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)
Tactic:
apply hp
Proof state after:
case hp
n : ℕ
hn_pos : 0 < n
hn_lt : n ≤ 4000
hp : n ∈ Set.Icc 1 4000 → ∃ p, p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)
⊢ n ∈ Set.Icc 1 4000
Theorem: landauTrick
Proof state before:
case hp
n : ℕ
hn_pos : 0 < n
hn_lt : n ≤ 4000
hp : n ∈ Set.Icc 1 4000 → ∃ p, p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)
⊢ n ∈ Set.Icc 1 4000
Tactic:
apply And.intro <;> linarith
Proof state after:
no goals
Theorem: landauTrick
Proof state before:
case intro
n : ℕ
hn_pos : 0 < n
hn_lt : n ≤ 4000
hp✝ : n ∈ Set.Icc 1 4000 → ∃ p, p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)
p : ℕ
hp : p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)
⊢ ∃ p, p ∈ Set.Ioc n (2 * n) ∧ Nat.Prime p
Tactic:
exists p
Proof state after:
case intro
n : ℕ
hn_pos : 0 < n
hn_lt : n ≤ 4000
hp✝ : n ∈ Set.Icc 1 4000 → ∃ p, p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)
p : ℕ
hp : p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)
⊢ p ∈ Set.Ioc n (2 * n) ∧ Nat.Prime p
Theorem: landauTrick
Proof state before:
case intro
n : ℕ
hn_pos : 0 < n
hn_lt : n ≤ 4000
hp✝ : n ∈ Set.Icc 1 4000 → ∃ p, p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)
p : ℕ
hp : p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)
⊢ p ∈ Set.Ioc n (2 * n) ∧ Nat.Prime p
Tactic:
apply And.intro hp.right
Proof state after:
case intro
n : ℕ
hn_pos : 0 < n
hn_lt : n ≤ 4000
hp✝ : n ∈ Set.Icc 1 4000 → ∃ p, p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)
p : ℕ
hp : p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)
⊢ Nat.Prime p
Theorem: landauTrick
Proof state before:
case intro
n : ℕ
hn_pos : 0 < n
hn_lt : n ≤ 4000
hp✝ : n ∈ Set.Icc 1 4000 → ∃ p, p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)
p : ℕ
hp : p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)
⊢ Nat.Prime p
Tactic:
refine List.all₂_iff_forall.mp ?_ p hp.left
Proof state after:
case intro
n : ℕ
hn_pos : 0 < n
hn_lt : n ≤ 4000
hp✝ : n ∈ Set.Icc 1 4000 → ∃ p, p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)
p : ℕ
hp : p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)
⊢ List.All₂ Nat.Prime nums
Theorem: landauTrick
Proof state before:
case intro
n : ℕ
hn_pos : 0 < n
hn_lt : n ≤ 4000
hp✝ : n ∈ Set.Icc 1 4000 → ∃ p, p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)
p : ℕ
hp : p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)
⊢ List.All₂ Nat.Prime nums
Tactic:
exact allPrimeNums
Proof state after:
no goals
Theorem: PrimeRange.prodNeZero
Proof state before:
k : ℕ
⊢ prod k ≠ 0
Tactic:
simp [prod, PrimeRange, List.mem_filter]
Proof state after:
no goals
Theorem: PrimeRange.prodDvdOfLt
Proof state before:
k p : ℕ
hp : Nat.Prime p
⊢ p < k → p ∣ prod k
Tactic:
intro hk
Proof state after:
k p : ℕ
hp : Nat.Prime p
hk : p < k
⊢ p ∣ prod k
Theorem: PrimeRange.prodDvdOfLt
Proof state before:
k p : ℕ
hp : Nat.Prime p
hk : p < k
⊢ p ∣ prod k
Tactic:
apply List.dvd_prod
Proof state after:
case ha
k p : ℕ
hp : Nat.Prime p
hk : p < k
⊢ p ∈ PrimeRange k
Theorem: PrimeRange.prodDvdOfLt
Proof state before:
case ha
k p : ℕ
hp : Nat.Prime p
hk : p < k
⊢ p ∈ PrimeRange k
Tactic:
simp [PrimeRange, List.mem_filter]
Proof state after:
case ha
k p : ℕ
hp : Nat.Prime p
hk : p < k
⊢ p < k ∧ Nat.Prime p
Theorem: PrimeRange.prodDvdOfLt
Proof state before:
case ha
k p : ℕ
hp : Nat.Prime p
hk : p < k
⊢ p < k ∧ Nat.Prime p
Tactic:
exact ⟨hk, hp⟩
Proof state after:
no goals
Theorem: gapAfterProdPrimeRange
Proof state before:
k u : ℕ
⊢ 2 ≤ u ∧ u ≤ Nat.succ k → ¬Nat.Prime (PrimeRange.prod (Nat.succ (Nat.succ k)) + u)
Tactic:
intros
Proof state after:
k u : ℕ
a✝ : 2 ≤ u ∧ u ≤ Nat.succ k
⊢ ¬Nat.Prime (PrimeRange.prod (Nat.succ (Nat.succ k)) + u)
Theorem: gapAfterProdPrimeRange
Proof state before:
k u : ℕ
a✝ : 2 ≤ u ∧ u ≤ Nat.succ k
⊢ ¬Nat.Prime (PrimeRange.prod (Nat.succ (Nat.succ k)) + u)
Tactic:
rw [Nat.prime_def_lt']
Proof state after:
k u : ℕ
a✝ : 2 ≤ u ∧ u ≤ Nat.succ k
⊢ ¬(2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u ∧
      ∀ (m : ℕ),
        2 ≤ m → m < PrimeRange.prod (Nat.succ (Nat.succ k)) + u → ¬m ∣ PrimeRange.prod (Nat.succ (Nat.succ k)) + u)
Theorem: gapAfterProdPrimeRange
Proof state before:
k u : ℕ
a✝ : 2 ≤ u ∧ u ≤ Nat.succ k
⊢ ¬(2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u ∧
      ∀ (m : ℕ),
        2 ≤ m → m < PrimeRange.prod (Nat.succ (Nat.succ k)) + u → ¬m ∣ PrimeRange.prod (Nat.succ (Nat.succ k)) + u)
Tactic:
simp
Proof state after:
k u : ℕ
a✝ : 2 ≤ u ∧ u ≤ Nat.succ k
⊢ 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u →
    ∃ x, x < PrimeRange.prod (Nat.succ (Nat.succ k)) + u ∧ 2 ≤ x ∧ x ∣ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
Theorem: gapAfterProdPrimeRange
Proof state before:
k u : ℕ
a✝ : 2 ≤ u ∧ u ≤ Nat.succ k
⊢ 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u →
    ∃ x, x < PrimeRange.prod (Nat.succ (Nat.succ k)) + u ∧ 2 ≤ x ∧ x ∣ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
Tactic:
intros
Proof state after:
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
⊢ ∃ x, x < PrimeRange.prod (Nat.succ (Nat.succ k)) + u ∧ 2 ≤ x ∧ x ∣ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
Theorem: gapAfterProdPrimeRange
Proof state before:
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
⊢ ∃ x, x < PrimeRange.prod (Nat.succ (Nat.succ k)) + u ∧ 2 ≤ x ∧ x ∣ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
Tactic:
have : u ≠ 1
Proof state after:
case this
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
⊢ u ≠ 1

k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
⊢ ∃ x, x < PrimeRange.prod (Nat.succ (Nat.succ k)) + u ∧ 2 ≤ x ∧ x ∣ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
Theorem: gapAfterProdPrimeRange
Proof state before:
case this
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
⊢ u ≠ 1

k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
⊢ ∃ x, x < PrimeRange.prod (Nat.succ (Nat.succ k)) + u ∧ 2 ≤ x ∧ x ∣ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
Tactic:
. linarith
Proof state after:
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
⊢ ∃ x, x < PrimeRange.prod (Nat.succ (Nat.succ k)) + u ∧ 2 ≤ x ∧ x ∣ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
Theorem: gapAfterProdPrimeRange
Proof state before:
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
⊢ ∃ x, x < PrimeRange.prod (Nat.succ (Nat.succ k)) + u ∧ 2 ≤ x ∧ x ∣ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
Tactic:
cases Nat.exists_prime_and_dvd this with
| intro p hp =>
  exists p
  have hu_pos : 0 < u
  . linarith
  have hpu : p ≤ u := Nat.le_of_dvd hu_pos hp.right
  apply And.intro
  . apply lt_of_le_of_lt hpu
    apply Nat.lt_add_of_pos_left
    apply PrimeRange.prodPos
  . apply And.intro
    . exact Nat.Prime.two_le hp.left
    . apply Nat.dvd_add _ hp.right
      apply PrimeRange.prodDvdOfLt hp.left
      linarith
Proof state after:
no goals
Theorem: gapAfterProdPrimeRange
Proof state before:
case this
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
⊢ u ≠ 1
Tactic:
linarith
Proof state after:
no goals
Theorem: gapAfterProdPrimeRange
Proof state before:
case intro
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ u
⊢ ∃ x, x < PrimeRange.prod (Nat.succ (Nat.succ k)) + u ∧ 2 ≤ x ∧ x ∣ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
Tactic:
exists p
Proof state after:
case intro
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ u
⊢ p < PrimeRange.prod (Nat.succ (Nat.succ k)) + u ∧ 2 ≤ p ∧ p ∣ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
Theorem: gapAfterProdPrimeRange
Proof state before:
case intro
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ u
⊢ p < PrimeRange.prod (Nat.succ (Nat.succ k)) + u ∧ 2 ≤ p ∧ p ∣ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
Tactic:
have hu_pos : 0 < u
Proof state after:
case hu_pos
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ u
⊢ 0 < u

case intro
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ u
hu_pos : 0 < u
⊢ p < PrimeRange.prod (Nat.succ (Nat.succ k)) + u ∧ 2 ≤ p ∧ p ∣ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
Theorem: gapAfterProdPrimeRange
Proof state before:
case hu_pos
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ u
⊢ 0 < u

case intro
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ u
hu_pos : 0 < u
⊢ p < PrimeRange.prod (Nat.succ (Nat.succ k)) + u ∧ 2 ≤ p ∧ p ∣ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
Tactic:
. linarith
Proof state after:
case intro
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ u
hu_pos : 0 < u
⊢ p < PrimeRange.prod (Nat.succ (Nat.succ k)) + u ∧ 2 ≤ p ∧ p ∣ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
Theorem: gapAfterProdPrimeRange
Proof state before:
case intro
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ u
hu_pos : 0 < u
⊢ p < PrimeRange.prod (Nat.succ (Nat.succ k)) + u ∧ 2 ≤ p ∧ p ∣ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
Tactic:
have hpu : p ≤ u := Nat.le_of_dvd hu_pos hp.right
Proof state after:
case intro
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ u
hu_pos : 0 < u
hpu : p ≤ u
⊢ p < PrimeRange.prod (Nat.succ (Nat.succ k)) + u ∧ 2 ≤ p ∧ p ∣ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
Theorem: gapAfterProdPrimeRange
Proof state before:
case intro
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ u
hu_pos : 0 < u
hpu : p ≤ u
⊢ p < PrimeRange.prod (Nat.succ (Nat.succ k)) + u ∧ 2 ≤ p ∧ p ∣ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
Tactic:
apply And.intro
Proof state after:
case intro.left
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ u
hu_pos : 0 < u
hpu : p ≤ u
⊢ p < PrimeRange.prod (Nat.succ (Nat.succ k)) + u

case intro.right
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ u
hu_pos : 0 < u
hpu : p ≤ u
⊢ 2 ≤ p ∧ p ∣ PrimeRange.prod (Nat.succ (Nat.succ k)) + u