internlm/Lean-Github huggingface dataset:
Theorem: HTPI.exists_prime_factor
Proof state before:
case neg
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ∃ a b, a * b = n ∧ a < n ∧ b < n
⊢ ∃ p, prime_factor p n
Tactic:
obtain (a : Nat) (h3 : ∃ (b : Nat), a * b = n ∧ a < n ∧ b < n) from h2
Proof state after:
case neg
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ∃ a b, a * b = n ∧ a < n ∧ b < n
a : ℕ
h3 : ∃ b, a * b = n ∧ a < n ∧ b < n
⊢ ∃ p, prime_factor p n
Theorem: HTPI.exists_prime_factor
Proof state before:
case neg
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ∃ a b, a * b = n ∧ a < n ∧ b < n
a : ℕ
h3 : ∃ b, a * b = n ∧ a < n ∧ b < n
⊢ ∃ p, prime_factor p n
Tactic:
obtain (b : Nat) (h4 : a * b = n ∧ a < n ∧ b < n) from h3
Proof state after:
case neg
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ∃ a b, a * b = n ∧ a < n ∧ b < n
a : ℕ
h3 : ∃ b, a * b = n ∧ a < n ∧ b < n
b : ℕ
h4 : a * b = n ∧ a < n ∧ b < n
⊢ ∃ p, prime_factor p n
Theorem: HTPI.exists_prime_factor
Proof state before:
case neg
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ∃ a b, a * b = n ∧ a < n ∧ b < n
a : ℕ
h3 : ∃ b, a * b = n ∧ a < n ∧ b < n
b : ℕ
h4 : a * b = n ∧ a < n ∧ b < n
⊢ ∃ p, prime_factor p n
Tactic:
have h5 : 2 ≤ a := by
  by_contra h6
  have h7 : a ≤ 1 := by linarith
  have h8 : n ≤ b :=
    calc n
      _ = a * b := h4.left.symm
      _ ≤ 1 * b := by rel [h7]
      _ = b := by ring
  linarith        done
Proof state after:
case neg
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ∃ a b, a * b = n ∧ a < n ∧ b < n
a : ℕ
h3 : ∃ b, a * b = n ∧ a < n ∧ b < n
b : ℕ
h4 : a * b = n ∧ a < n ∧ b < n
h5 : 2 ≤ a
⊢ ∃ p, prime_factor p n
Theorem: HTPI.exists_prime_factor
Proof state before:
case neg
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ∃ a b, a * b = n ∧ a < n ∧ b < n
a : ℕ
h3 : ∃ b, a * b = n ∧ a < n ∧ b < n
b : ℕ
h4 : a * b = n ∧ a < n ∧ b < n
h5 : 2 ≤ a
⊢ ∃ p, prime_factor p n
Tactic:
have h6 : ∃ (p : Nat), prime_factor p a := ih a h4.right.left h5
Proof state after:
case neg
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ∃ a b, a * b = n ∧ a < n ∧ b < n
a : ℕ
h3 : ∃ b, a * b = n ∧ a < n ∧ b < n
b : ℕ
h4 : a * b = n ∧ a < n ∧ b < n
h5 : 2 ≤ a
h6 : ∃ p, prime_factor p a
⊢ ∃ p, prime_factor p n
Theorem: HTPI.exists_prime_factor
Proof state before:
case neg
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ∃ a b, a * b = n ∧ a < n ∧ b < n
a : ℕ
h3 : ∃ b, a * b = n ∧ a < n ∧ b < n
b : ℕ
h4 : a * b = n ∧ a < n ∧ b < n
h5 : 2 ≤ a
h6 : ∃ p, prime_factor p a
⊢ ∃ p, prime_factor p n
Tactic:
obtain (p : Nat) (h7 : prime_factor p a) from h6
Proof state after:
case neg
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ∃ a b, a * b = n ∧ a < n ∧ b < n
a : ℕ
h3 : ∃ b, a * b = n ∧ a < n ∧ b < n
b : ℕ
h4 : a * b = n ∧ a < n ∧ b < n
h5 : 2 ≤ a
h6 : ∃ p, prime_factor p a
p : ℕ
h7 : prime_factor p a
⊢ ∃ p, prime_factor p n
Theorem: HTPI.exists_prime_factor
Proof state before:
case neg
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ∃ a b, a * b = n ∧ a < n ∧ b < n
a : ℕ
h3 : ∃ b, a * b = n ∧ a < n ∧ b < n
b : ℕ
h4 : a * b = n ∧ a < n ∧ b < n
h5 : 2 ≤ a
h6 : ∃ p, prime_factor p a
p : ℕ
h7 : prime_factor p a
⊢ ∃ p, prime_factor p n
Tactic:
apply Exists.intro p
Proof state after:
case neg
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ∃ a b, a * b = n ∧ a < n ∧ b < n
a : ℕ
h3 : ∃ b, a * b = n ∧ a < n ∧ b < n
b : ℕ
h4 : a * b = n ∧ a < n ∧ b < n
h5 : 2 ≤ a
h6 : ∃ p, prime_factor p a
p : ℕ
h7 : prime_factor p a
⊢ prime_factor p n
Theorem: HTPI.exists_prime_factor
Proof state before:
case neg
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ∃ a b, a * b = n ∧ a < n ∧ b < n
a : ℕ
h3 : ∃ b, a * b = n ∧ a < n ∧ b < n
b : ℕ
h4 : a * b = n ∧ a < n ∧ b < n
h5 : 2 ≤ a
h6 : ∃ p, prime_factor p a
p : ℕ
h7 : prime_factor p a
⊢ prime_factor p n
Tactic:
define
Proof state after:
case neg
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ∃ a b, a * b = n ∧ a < n ∧ b < n
a : ℕ
h3 : ∃ b, a * b = n ∧ a < n ∧ b < n
b : ℕ
h4 : a * b = n ∧ a < n ∧ b < n
h5 : 2 ≤ a
h6 : ∃ p, prime_factor p a
p : ℕ
h7 : prime_factor p a
⊢ prime p ∧ p ∣ n
Theorem: HTPI.exists_prime_factor
Proof state before:
case neg
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ∃ a b, a * b = n ∧ a < n ∧ b < n
a : ℕ
h3 : ∃ b, a * b = n ∧ a < n ∧ b < n
b : ℕ
h4 : a * b = n ∧ a < n ∧ b < n
h5 : 2 ≤ a
h6 : ∃ p, prime_factor p a
p : ℕ
h7 : prime_factor p a
⊢ prime p ∧ p ∣ n
Tactic:
define at h7
Proof state after:
case neg
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ∃ a b, a * b = n ∧ a < n ∧ b < n
a : ℕ
h3 : ∃ b, a * b = n ∧ a < n ∧ b < n
b : ℕ
h4 : a * b = n ∧ a < n ∧ b < n
h5 : 2 ≤ a
h6 : ∃ p, prime_factor p a
p : ℕ
h7 : prime p ∧ p ∣ a
⊢ prime p ∧ p ∣ n
Theorem: HTPI.exists_prime_factor
Proof state before:
case neg
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ∃ a b, a * b = n ∧ a < n ∧ b < n
a : ℕ
h3 : ∃ b, a * b = n ∧ a < n ∧ b < n
b : ℕ
h4 : a * b = n ∧ a < n ∧ b < n
h5 : 2 ≤ a
h6 : ∃ p, prime_factor p a
p : ℕ
h7 : prime p ∧ p ∣ a
⊢ prime p ∧ p ∣ n
Tactic:
apply And.intro h7.left
Proof state after:
case neg
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ∃ a b, a * b = n ∧ a < n ∧ b < n
a : ℕ
h3 : ∃ b, a * b = n ∧ a < n ∧ b < n
b : ℕ
h4 : a * b = n ∧ a < n ∧ b < n
h5 : 2 ≤ a
h6 : ∃ p, prime_factor p a
p : ℕ
h7 : prime p ∧ p ∣ a
⊢ p ∣ n
Theorem: HTPI.exists_prime_factor
Proof state before:
case neg
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ∃ a b, a * b = n ∧ a < n ∧ b < n
a : ℕ
h3 : ∃ b, a * b = n ∧ a < n ∧ b < n
b : ℕ
h4 : a * b = n ∧ a < n ∧ b < n
h5 : 2 ≤ a
h6 : ∃ p, prime_factor p a
p : ℕ
h7 : prime p ∧ p ∣ a
⊢ p ∣ n
Tactic:
have h8 : a ∣ n := by
  apply Exists.intro b
  show n = a * b from (h4.left).symm
  done
Proof state after:
case neg
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ∃ a b, a * b = n ∧ a < n ∧ b < n
a : ℕ
h3 : ∃ b, a * b = n ∧ a < n ∧ b < n
b : ℕ
h4 : a * b = n ∧ a < n ∧ b < n
h5 : 2 ≤ a
h6 : ∃ p, prime_factor p a
p : ℕ
h7 : prime p ∧ p ∣ a
h8 : a ∣ n
⊢ p ∣ n
Theorem: HTPI.exists_prime_factor
Proof state before:
case neg
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ∃ a b, a * b = n ∧ a < n ∧ b < n
a : ℕ
h3 : ∃ b, a * b = n ∧ a < n ∧ b < n
b : ℕ
h4 : a * b = n ∧ a < n ∧ b < n
h5 : 2 ≤ a
h6 : ∃ p, prime_factor p a
p : ℕ
h7 : prime p ∧ p ∣ a
h8 : a ∣ n
⊢ p ∣ n
Tactic:
show p ∣ n from dvd_trans h7.right h8
Proof state after:
no goals
Theorem: HTPI.exists_prime_factor
Proof state before:
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ∃ a b, a * b = n ∧ a < n ∧ b < n
a : ℕ
h3 : ∃ b, a * b = n ∧ a < n ∧ b < n
b : ℕ
h4 : a * b = n ∧ a < n ∧ b < n
⊢ 2 ≤ a
Tactic:
by_contra h6
Proof state after:
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ∃ a b, a * b = n ∧ a < n ∧ b < n
a : ℕ
h3 : ∃ b, a * b = n ∧ a < n ∧ b < n
b : ℕ
h4 : a * b = n ∧ a < n ∧ b < n
h6 : ¬2 ≤ a
⊢ False
Theorem: HTPI.exists_prime_factor
Proof state before:
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ∃ a b, a * b = n ∧ a < n ∧ b < n
a : ℕ
h3 : ∃ b, a * b = n ∧ a < n ∧ b < n
b : ℕ
h4 : a * b = n ∧ a < n ∧ b < n
h6 : ¬2 ≤ a
⊢ False
Tactic:
have h7 : a ≤ 1 := by linarith
Proof state after:
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ∃ a b, a * b = n ∧ a < n ∧ b < n
a : ℕ
h3 : ∃ b, a * b = n ∧ a < n ∧ b < n
b : ℕ
h4 : a * b = n ∧ a < n ∧ b < n
h6 : ¬2 ≤ a
h7 : a ≤ 1
⊢ False
Theorem: HTPI.exists_prime_factor
Proof state before:
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ∃ a b, a * b = n ∧ a < n ∧ b < n
a : ℕ
h3 : ∃ b, a * b = n ∧ a < n ∧ b < n
b : ℕ
h4 : a * b = n ∧ a < n ∧ b < n
h6 : ¬2 ≤ a
h7 : a ≤ 1
⊢ False
Tactic:
have h8 : n ≤ b :=
  calc n
    _ = a * b := h4.left.symm
    _ ≤ 1 * b := by rel [h7]
    _ = b := by ring
Proof state after:
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ∃ a b, a * b = n ∧ a < n ∧ b < n
a : ℕ
h3 : ∃ b, a * b = n ∧ a < n ∧ b < n
b : ℕ
h4 : a * b = n ∧ a < n ∧ b < n
h6 : ¬2 ≤ a
h7 : a ≤ 1
h8 : n ≤ b
⊢ False
Theorem: HTPI.exists_prime_factor
Proof state before:
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ∃ a b, a * b = n ∧ a < n ∧ b < n
a : ℕ
h3 : ∃ b, a * b = n ∧ a < n ∧ b < n
b : ℕ
h4 : a * b = n ∧ a < n ∧ b < n
h6 : ¬2 ≤ a
h7 : a ≤ 1
h8 : n ≤ b
⊢ False
Tactic:
linarith
Proof state after:
no goals
Theorem: HTPI.exists_prime_factor
Proof state before:
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ∃ a b, a * b = n ∧ a < n ∧ b < n
a : ℕ
h3 : ∃ b, a * b = n ∧ a < n ∧ b < n
b : ℕ
h4 : a * b = n ∧ a < n ∧ b < n
h6 : ¬2 ≤ a
⊢ a ≤ 1
Tactic:
linarith
Proof state after:
no goals
Theorem: HTPI.exists_prime_factor
Proof state before:
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ∃ a b, a * b = n ∧ a < n ∧ b < n
a : ℕ
h3 : ∃ b, a * b = n ∧ a < n ∧ b < n
b : ℕ
h4 : a * b = n ∧ a < n ∧ b < n
h6 : ¬2 ≤ a
h7 : a ≤ 1
⊢ a * b ≤ 1 * b
Tactic:
rel [h7]
Proof state after:
no goals
Theorem: HTPI.exists_prime_factor
Proof state before:
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ∃ a b, a * b = n ∧ a < n ∧ b < n
a : ℕ
h3 : ∃ b, a * b = n ∧ a < n ∧ b < n
b : ℕ
h4 : a * b = n ∧ a < n ∧ b < n
h6 : ¬2 ≤ a
h7 : a ≤ 1
⊢ 1 * b = b
Tactic:
ring
Proof state after:
no goals
Theorem: HTPI.exists_prime_factor
Proof state before:
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ∃ a b, a * b = n ∧ a < n ∧ b < n
a : ℕ
h3 : ∃ b, a * b = n ∧ a < n ∧ b < n
b : ℕ
h4 : a * b = n ∧ a < n ∧ b < n
h5 : 2 ≤ a
h6 : ∃ p, prime_factor p a
p : ℕ
h7 : prime p ∧ p ∣ a
⊢ a ∣ n
Tactic:
apply Exists.intro b
Proof state after:
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ∃ a b, a * b = n ∧ a < n ∧ b < n
a : ℕ
h3 : ∃ b, a * b = n ∧ a < n ∧ b < n
b : ℕ
h4 : a * b = n ∧ a < n ∧ b < n
h5 : 2 ≤ a
h6 : ∃ p, prime_factor p a
p : ℕ
h7 : prime p ∧ p ∣ a
⊢ n = a * b
Theorem: HTPI.exists_prime_factor
Proof state before:
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ∃ a b, a * b = n ∧ a < n ∧ b < n
a : ℕ
h3 : ∃ b, a * b = n ∧ a < n ∧ b < n
b : ℕ
h4 : a * b = n ∧ a < n ∧ b < n
h5 : 2 ≤ a
h6 : ∃ p, prime_factor p a
p : ℕ
h7 : prime p ∧ p ∣ a
⊢ n = a * b
Tactic:
show n = a * b from (h4.left).symm
Proof state after:
no goals
Theorem: HTPI.exists_least_prime_factor
Proof state before:
n : ℕ
h : 2 ≤ n
⊢ ∃ p, prime_factor p n ∧ ∀ (q : ℕ), prime_factor q n → p ≤ q
Tactic:
set S : Set Nat := {p : Nat | prime_factor p n}
Proof state after:
n : ℕ
h : 2 ≤ n
S : Set ℕ := {p | prime_factor p n}
⊢ ∃ p, prime_factor p n ∧ ∀ (q : ℕ), prime_factor q n → p ≤ q
Theorem: HTPI.exists_least_prime_factor
Proof state before:
n : ℕ
h : 2 ≤ n
S : Set ℕ := {p | prime_factor p n}
⊢ ∃ p, prime_factor p n ∧ ∀ (q : ℕ), prime_factor q n → p ≤ q
Tactic:
have h2 : ∃ (p : Nat), p ∈ S := exists_prime_factor n h
Proof state after:
n : ℕ
h : 2 ≤ n
S : Set ℕ := {p | prime_factor p n}
h2 : ∃ p, p ∈ S
⊢ ∃ p, prime_factor p n ∧ ∀ (q : ℕ), prime_factor q n → p ≤ q
Theorem: HTPI.exists_least_prime_factor
Proof state before:
n : ℕ
h : 2 ≤ n
S : Set ℕ := {p | prime_factor p n}
h2 : ∃ p, p ∈ S
⊢ ∃ p, prime_factor p n ∧ ∀ (q : ℕ), prime_factor q n → p ≤ q
Tactic:
show ∃ (p : Nat), prime_factor p n ∧
  ∀ (q : Nat), prime_factor q n → p ≤ q from well_ord_princ S h2
Proof state after:
no goals
Theorem: HTPI.all_prime_nil
Proof state before:
⊢ all_prime []
Tactic:
define
Proof state after:
⊢ ∀ p ∈ [], prime p
Theorem: HTPI.all_prime_nil
Proof state before:
⊢ ∀ p ∈ [], prime p
Tactic:
fix p : Nat
Proof state after:
p : ℕ
⊢ p ∈ [] → prime p
Theorem: HTPI.all_prime_nil
Proof state before:
p : ℕ
⊢ p ∈ [] → prime p
Tactic:
contrapos
Proof state after:
p : ℕ
⊢ ¬prime p → p ∉ []
Theorem: HTPI.all_prime_nil
Proof state before:
p : ℕ
⊢ ¬prime p → p ∉ []
Tactic:
assume h1 : ¬prime p
Proof state after:
p : ℕ
h1 : ¬prime p
⊢ p ∉ []
Theorem: HTPI.all_prime_nil
Proof state before:
p : ℕ
h1 : ¬prime p
⊢ p ∉ []
Tactic:
show p ∉ [] from List.not_mem_nil p
Proof state after:
no goals
Theorem: HTPI.all_prime_cons
Proof state before:
n : ℕ
L : List ℕ
⊢ all_prime (n :: L) ↔ prime n ∧ all_prime L
Tactic:
apply Iff.intro
Proof state after:
case mp
n : ℕ
L : List ℕ
⊢ all_prime (n :: L) → prime n ∧ all_prime L

case mpr
n : ℕ
L : List ℕ
⊢ prime n ∧ all_prime L → all_prime (n :: L)
Theorem: HTPI.all_prime_cons
Proof state before:
case mp
n : ℕ
L : List ℕ
⊢ all_prime (n :: L) → prime n ∧ all_prime L
Tactic:
assume h1 : all_prime (n :: L)
Proof state after:
case mp
n : ℕ
L : List ℕ
h1 : all_prime (n :: L)
⊢ prime n ∧ all_prime L
Theorem: HTPI.all_prime_cons
Proof state before:
case mp
n : ℕ
L : List ℕ
h1 : all_prime (n :: L)
⊢ prime n ∧ all_prime L
Tactic:
define at h1
Proof state after:
case mp
n : ℕ
L : List ℕ
h1 : ∀ p ∈ n :: L, prime p
⊢ prime n ∧ all_prime L
Theorem: HTPI.all_prime_cons
Proof state before:
case mp
n : ℕ
L : List ℕ
h1 : ∀ p ∈ n :: L, prime p
⊢ prime n ∧ all_prime L
Tactic:
apply And.intro (h1 n (List.mem_cons_self n L))
Proof state after:
case mp
n : ℕ
L : List ℕ
h1 : ∀ p ∈ n :: L, prime p
⊢ all_prime L
Theorem: HTPI.all_prime_cons
Proof state before:
case mp
n : ℕ
L : List ℕ
h1 : ∀ p ∈ n :: L, prime p
⊢ all_prime L
Tactic:
define
Proof state after:
case mp
n : ℕ
L : List ℕ
h1 : ∀ p ∈ n :: L, prime p
⊢ ∀ p ∈ L, prime p
Theorem: HTPI.all_prime_cons
Proof state before:
case mp
n : ℕ
L : List ℕ
h1 : ∀ p ∈ n :: L, prime p
⊢ ∀ p ∈ L, prime p
Tactic:
fix p : Nat
Proof state after:
case mp
n : ℕ
L : List ℕ
h1 : ∀ p ∈ n :: L, prime p
p : ℕ
⊢ p ∈ L → prime p
Theorem: HTPI.all_prime_cons
Proof state before:
case mp
n : ℕ
L : List ℕ
h1 : ∀ p ∈ n :: L, prime p
p : ℕ
⊢ p ∈ L → prime p
Tactic:
assume h2 : p ∈ L
Proof state after:
case mp
n : ℕ
L : List ℕ
h1 : ∀ p ∈ n :: L, prime p
p : ℕ
h2 : p ∈ L
⊢ prime p
Theorem: HTPI.all_prime_cons
Proof state before:
case mp
n : ℕ
L : List ℕ
h1 : ∀ p ∈ n :: L, prime p
p : ℕ
h2 : p ∈ L
⊢ prime p
Tactic:
show prime p from h1 p (List.mem_cons_of_mem n h2)
Proof state after:
no goals
Theorem: HTPI.all_prime_cons
Proof state before:
case mpr
n : ℕ
L : List ℕ
⊢ prime n ∧ all_prime L → all_prime (n :: L)
Tactic:
assume h1 : prime n ∧ all_prime L
Proof state after:
case mpr
n : ℕ
L : List ℕ
h1 : prime n ∧ all_prime L
⊢ all_prime (n :: L)
Theorem: HTPI.all_prime_cons
Proof state before:
case mpr
n : ℕ
L : List ℕ
h1 : prime n ∧ all_prime L
⊢ all_prime (n :: L)
Tactic:
define : all_prime L at h1
Proof state after:
case mpr
n : ℕ
L : List ℕ
h1 : prime n ∧ ∀ p ∈ L, prime p
⊢ all_prime (n :: L)
Theorem: HTPI.all_prime_cons
Proof state before:
case mpr
n : ℕ
L : List ℕ
h1 : prime n ∧ ∀ p ∈ L, prime p
⊢ all_prime (n :: L)
Tactic:
define
Proof state after:
case mpr
n : ℕ
L : List ℕ
h1 : prime n ∧ ∀ p ∈ L, prime p
⊢ ∀ p ∈ n :: L, prime p
Theorem: HTPI.all_prime_cons
Proof state before:
case mpr
n : ℕ
L : List ℕ
h1 : prime n ∧ ∀ p ∈ L, prime p
⊢ ∀ p ∈ n :: L, prime p
Tactic:
fix p : Nat
Proof state after:
case mpr
n : ℕ
L : List ℕ
h1 : prime n ∧ ∀ p ∈ L, prime p
p : ℕ
⊢ p ∈ n :: L → prime p
Theorem: HTPI.all_prime_cons
Proof state before:
case mpr
n : ℕ
L : List ℕ
h1 : prime n ∧ ∀ p ∈ L, prime p
p : ℕ
⊢ p ∈ n :: L → prime p
Tactic:
assume h2 : p ∈ n :: L
Proof state after:
case mpr
n : ℕ
L : List ℕ
h1 : prime n ∧ ∀ p ∈ L, prime p
p : ℕ
h2 : p ∈ n :: L
⊢ prime p
Theorem: HTPI.all_prime_cons
Proof state before:
case mpr
n : ℕ
L : List ℕ
h1 : prime n ∧ ∀ p ∈ L, prime p
p : ℕ
h2 : p ∈ n :: L
⊢ prime p
Tactic:
rewrite [List.mem_cons] at h2
Proof state after:
case mpr
n : ℕ
L : List ℕ
h1 : prime n ∧ ∀ p ∈ L, prime p
p : ℕ
h2 : p = n ∨ p ∈ L
⊢ prime p
Theorem: HTPI.all_prime_cons
Proof state before:
case mpr
n : ℕ
L : List ℕ
h1 : prime n ∧ ∀ p ∈ L, prime p
p : ℕ
h2 : p = n ∨ p ∈ L
⊢ prime p
Tactic:
by_cases on h2
Proof state after:
case mpr.Case_1
n : ℕ
L : List ℕ
h1 : prime n ∧ ∀ p ∈ L, prime p
p : ℕ
h2 : p = n
⊢ prime p

case mpr.Case_2
n : ℕ
L : List ℕ
h1 : prime n ∧ ∀ p ∈ L, prime p
p : ℕ
h2 : p ∈ L
⊢ prime p
Theorem: HTPI.all_prime_cons
Proof state before:
case mpr.Case_1
n : ℕ
L : List ℕ
h1 : prime n ∧ ∀ p ∈ L, prime p
p : ℕ
h2 : p = n
⊢ prime p
Tactic:
rewrite [h2]
Proof state after:
case mpr.Case_1
n : ℕ
L : List ℕ
h1 : prime n ∧ ∀ p ∈ L, prime p
p : ℕ
h2 : p = n
⊢ prime n
Theorem: HTPI.all_prime_cons
Proof state before:
case mpr.Case_1
n : ℕ
L : List ℕ
h1 : prime n ∧ ∀ p ∈ L, prime p
p : ℕ
h2 : p = n
⊢ prime n
Tactic:
show prime n from h1.left
Proof state after:
no goals
Theorem: HTPI.all_prime_cons
Proof state before:
case mpr.Case_2
n : ℕ
L : List ℕ
h1 : prime n ∧ ∀ p ∈ L, prime p
p : ℕ
h2 : p ∈ L
⊢ prime p
Tactic:
show prime p from h1.right p h2
Proof state after:
no goals
Theorem: HTPI.nondec_nil
Proof state before:
⊢ nondec []
Tactic:
define
Proof state after:
⊢ True
Theorem: HTPI.nondec_nil
Proof state before:
⊢ True
Tactic:
trivial
Proof state after:
no goals
Theorem: HTPI.nondec_cons
Proof state before:
n : ℕ
L : List ℕ
⊢ nondec (n :: L) ↔ (∀ m ∈ L, n ≤ m) ∧ nondec L
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.prod_nil
Proof state before:
⊢ prod [] = 1
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.prod_cons
Proof state before:
n : ℕ
L : List ℕ
⊢ prod (n :: L) = n * prod L
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.exists_cons_of_length_eq_succ
Proof state before:
A : Type
l : List A
n : ℕ
h : List.length l = n + 1
⊢ ∃ a L, l = a :: L ∧ List.length L = n
Tactic:
have h1 : ¬l.length = 0 := by linarith
Proof state after:
A : Type
l : List A
n : ℕ
h : List.length l = n + 1
h1 : ¬List.length l = 0
⊢ ∃ a L, l = a :: L ∧ List.length L = n
Theorem: HTPI.exists_cons_of_length_eq_succ
Proof state before:
A : Type
l : List A
n : ℕ
h : List.length l = n + 1
h1 : ¬List.length l = 0
⊢ ∃ a L, l = a :: L ∧ List.length L = n
Tactic:
rewrite [List.length_eq_zero] at h1
Proof state after:
A : Type
l : List A
n : ℕ
h : List.length l = n + 1
h1 : ¬l = []
⊢ ∃ a L, l = a :: L ∧ List.length L = n
Theorem: HTPI.exists_cons_of_length_eq_succ
Proof state before:
A : Type
l : List A
n : ℕ
h : List.length l = n + 1
h1 : ¬l = []
⊢ ∃ a L, l = a :: L ∧ List.length L = n
Tactic:
obtain (a : A) (h2 : ∃ (L : List A), l = a :: L) from
  List.exists_cons_of_ne_nil h1
Proof state after:
A : Type
l : List A
n : ℕ
h : List.length l = n + 1
h1 : ¬l = []
a : A
h2 : ∃ L, l = a :: L
⊢ ∃ a L, l = a :: L ∧ List.length L = n
Theorem: HTPI.exists_cons_of_length_eq_succ
Proof state before:
A : Type
l : List A
n : ℕ
h : List.length l = n + 1
h1 : ¬l = []
a : A
h2 : ∃ L, l = a :: L
⊢ ∃ a L, l = a :: L ∧ List.length L = n
Tactic:
obtain (L : List A) (h3 : l = a :: L) from h2
Proof state after:
A : Type
l : List A
n : ℕ
h : List.length l = n + 1
h1 : ¬l = []
a : A
h2 : ∃ L, l = a :: L
L : List A
h3 : l = a :: L
⊢ ∃ a L, l = a :: L ∧ List.length L = n
Theorem: HTPI.exists_cons_of_length_eq_succ
Proof state before:
A : Type
l : List A
n : ℕ
h : List.length l = n + 1
h1 : ¬l = []
a : A
h2 : ∃ L, l = a :: L
L : List A
h3 : l = a :: L
⊢ ∃ a L, l = a :: L ∧ List.length L = n
Tactic:
apply Exists.intro a
Proof state after:
A : Type
l : List A
n : ℕ
h : List.length l = n + 1
h1 : ¬l = []
a : A
h2 : ∃ L, l = a :: L
L : List A
h3 : l = a :: L
⊢ ∃ L, l = a :: L ∧ List.length L = n
Theorem: HTPI.exists_cons_of_length_eq_succ
Proof state before:
A : Type
l : List A
n : ℕ
h : List.length l = n + 1
h1 : ¬l = []
a : A
h2 : ∃ L, l = a :: L
L : List A
h3 : l = a :: L
⊢ ∃ L, l = a :: L ∧ List.length L = n
Tactic:
apply Exists.intro L
Proof state after:
A : Type
l : List A
n : ℕ
h : List.length l = n + 1
h1 : ¬l = []
a : A
h2 : ∃ L, l = a :: L
L : List A
h3 : l = a :: L
⊢ l = a :: L ∧ List.length L = n
Theorem: HTPI.exists_cons_of_length_eq_succ
Proof state before:
A : Type
l : List A
n : ℕ
h : List.length l = n + 1
h1 : ¬l = []
a : A
h2 : ∃ L, l = a :: L
L : List A
h3 : l = a :: L
⊢ l = a :: L ∧ List.length L = n
Tactic:
apply And.intro h3
Proof state after:
A : Type
l : List A
n : ℕ
h : List.length l = n + 1
h1 : ¬l = []
a : A
h2 : ∃ L, l = a :: L
L : List A
h3 : l = a :: L
⊢ List.length L = n
Theorem: HTPI.exists_cons_of_length_eq_succ
Proof state before:
A : Type
l : List A
n : ℕ
h : List.length l = n + 1
h1 : ¬l = []
a : A
h2 : ∃ L, l = a :: L
L : List A
h3 : l = a :: L
⊢ List.length L = n
Tactic:
have h4 : (a :: L).length = L.length + 1 := List.length_cons a L
Proof state after:
A : Type
l : List A
n : ℕ
h : List.length l = n + 1
h1 : ¬l = []
a : A
h2 : ∃ L, l = a :: L
L : List A
h3 : l = a :: L
h4 : List.length (a :: L) = List.length L + 1
⊢ List.length L = n
Theorem: HTPI.exists_cons_of_length_eq_succ
Proof state before:
A : Type
l : List A
n : ℕ
h : List.length l = n + 1
h1 : ¬l = []
a : A
h2 : ∃ L, l = a :: L
L : List A
h3 : l = a :: L
h4 : List.length (a :: L) = List.length L + 1
⊢ List.length L = n
Tactic:
rewrite [←h3, h] at h4
Proof state after:
A : Type
l : List A
n : ℕ
h : List.length l = n + 1
h1 : ¬l = []
a : A
h2 : ∃ L, l = a :: L
L : List A
h3 : l = a :: L
h4 : n + 1 = List.length L + 1
⊢ List.length L = n
Theorem: HTPI.exists_cons_of_length_eq_succ
Proof state before:
A : Type
l : List A
n : ℕ
h : List.length l = n + 1
h1 : ¬l = []
a : A
h2 : ∃ L, l = a :: L
L : List A
h3 : l = a :: L
h4 : n + 1 = List.length L + 1
⊢ List.length L = n
Tactic:
show L.length = n from (Nat.add_right_cancel h4).symm
Proof state after:
no goals
Theorem: HTPI.exists_cons_of_length_eq_succ
Proof state before:
A : Type
l : List A
n : ℕ
h : List.length l = n + 1
⊢ ¬List.length l = 0
Tactic:
linarith
Proof state after:
no goals
Theorem: HTPI.list_elt_dvd_prod_by_length
Proof state before:
a : ℕ
⊢ ∀ (n : ℕ) (l : List ℕ), List.length l = n → a ∈ l → a ∣ prod l
Tactic:
by_induc
Proof state after:
case Base_Case
a : ℕ
⊢ ∀ (l : List ℕ), List.length l = 0 → a ∈ l → a ∣ prod l

case Induction_Step
a : ℕ
⊢ ∀ (n : ℕ),
    (∀ (l : List ℕ), List.length l = n → a ∈ l → a ∣ prod l) →
      ∀ (l : List ℕ), List.length l = n + 1 → a ∈ l → a ∣ prod l
Theorem: HTPI.list_elt_dvd_prod_by_length
Proof state before:
case Base_Case
a : ℕ
⊢ ∀ (l : List ℕ), List.length l = 0 → a ∈ l → a ∣ prod l
Tactic:
fix l : List Nat
Proof state after:
case Base_Case
a : ℕ
l : List ℕ
⊢ List.length l = 0 → a ∈ l → a ∣ prod l
Theorem: HTPI.list_elt_dvd_prod_by_length
Proof state before:
case Base_Case
a : ℕ
l : List ℕ
⊢ List.length l = 0 → a ∈ l → a ∣ prod l
Tactic:
assume h1 : l.length = 0
Proof state after:
case Base_Case
a : ℕ
l : List ℕ
h1 : List.length l = 0
⊢ a ∈ l → a ∣ prod l
Theorem: HTPI.list_elt_dvd_prod_by_length
Proof state before:
case Base_Case
a : ℕ
l : List ℕ
h1 : List.length l = 0
⊢ a ∈ l → a ∣ prod l
Tactic:
rewrite [List.length_eq_zero] at h1
Proof state after:
case Base_Case
a : ℕ
l : List ℕ
h1 : l = []
⊢ a ∈ l → a ∣ prod l
Theorem: HTPI.list_elt_dvd_prod_by_length
Proof state before:
case Base_Case
a : ℕ
l : List ℕ
h1 : l = []
⊢ a ∈ l → a ∣ prod l
Tactic:
rewrite [h1]
Proof state after:
case Base_Case
a : ℕ
l : List ℕ
h1 : l = []
⊢ a ∈ [] → a ∣ prod []
Theorem: HTPI.list_elt_dvd_prod_by_length
Proof state before:
case Base_Case
a : ℕ
l : List ℕ
h1 : l = []
⊢ a ∈ [] → a ∣ prod []
Tactic:
contrapos
Proof state after:
case Base_Case
a : ℕ
l : List ℕ
h1 : l = []
⊢ ¬a ∣ prod [] → a ∉ []
Theorem: HTPI.list_elt_dvd_prod_by_length
Proof state before:
case Base_Case
a : ℕ
l : List ℕ
h1 : l = []
⊢ ¬a ∣ prod [] → a ∉ []
Tactic:
assume h2 : ¬a ∣ prod []
Proof state after:
case Base_Case
a : ℕ
l : List ℕ
h1 : l = []
h2 : ¬a ∣ prod []
⊢ a ∉ []
Theorem: HTPI.list_elt_dvd_prod_by_length
Proof state before:
case Base_Case
a : ℕ
l : List ℕ
h1 : l = []
h2 : ¬a ∣ prod []
⊢ a ∉ []
Tactic:
show a ∉ [] from List.not_mem_nil a
Proof state after:
no goals
Theorem: HTPI.list_elt_dvd_prod_by_length
Proof state before:
case Induction_Step
a : ℕ
⊢ ∀ (n : ℕ),
    (∀ (l : List ℕ), List.length l = n → a ∈ l → a ∣ prod l) →
      ∀ (l : List ℕ), List.length l = n + 1 → a ∈ l → a ∣ prod l
Tactic:
fix n : Nat
Proof state after:
case Induction_Step
a n : ℕ
⊢ (∀ (l : List ℕ), List.length l = n → a ∈ l → a ∣ prod l) → ∀ (l : List ℕ), List.length l = n + 1 → a ∈ l → a ∣ prod l