internlm/Lean-Github huggingface dataset:
Theorem: HTPI.exists_prime_factorization
Proof state before:
case neg
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : ¬n = 1
h3 : n ≥ 2
p : ℕ
h4 : prime_factor p n ∧ ∀ (q : ℕ), prime_factor q n → p ≤ q
p_prime_factor : prime p ∧ p ∣ n
p_prime : prime p
p_dvd_n : p ∣ n
p_least : ∀ (q : ℕ), prime_factor q n → p ≤ q
m : ℕ
n_eq_pm : n = p * m
h5 : m ≠ 0
m_pos : 0 < m
m_lt_n : m < n
L : List ℕ
h6 : prime_factorization m L
⊢ ∃ l, prime_factorization n l
Tactic:
define at h6
Proof state after:
case neg
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : ¬n = 1
h3 : n ≥ 2
p : ℕ
h4 : prime_factor p n ∧ ∀ (q : ℕ), prime_factor q n → p ≤ q
p_prime_factor : prime p ∧ p ∣ n
p_prime : prime p
p_dvd_n : p ∣ n
p_least : ∀ (q : ℕ), prime_factor q n → p ≤ q
m : ℕ
n_eq_pm : n = p * m
h5 : m ≠ 0
m_pos : 0 < m
m_lt_n : m < n
L : List ℕ
h6 : nondec_prime_list L ∧ prod L = m
⊢ ∃ l, prime_factorization n l
Theorem: HTPI.exists_prime_factorization
Proof state before:
case neg
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : ¬n = 1
h3 : n ≥ 2
p : ℕ
h4 : prime_factor p n ∧ ∀ (q : ℕ), prime_factor q n → p ≤ q
p_prime_factor : prime p ∧ p ∣ n
p_prime : prime p
p_dvd_n : p ∣ n
p_least : ∀ (q : ℕ), prime_factor q n → p ≤ q
m : ℕ
n_eq_pm : n = p * m
h5 : m ≠ 0
m_pos : 0 < m
m_lt_n : m < n
L : List ℕ
h6 : nondec_prime_list L ∧ prod L = m
⊢ ∃ l, prime_factorization n l
Tactic:
have ndpl_L : nondec_prime_list L := h6.left
Proof state after:
case neg
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : ¬n = 1
h3 : n ≥ 2
p : ℕ
h4 : prime_factor p n ∧ ∀ (q : ℕ), prime_factor q n → p ≤ q
p_prime_factor : prime p ∧ p ∣ n
p_prime : prime p
p_dvd_n : p ∣ n
p_least : ∀ (q : ℕ), prime_factor q n → p ≤ q
m : ℕ
n_eq_pm : n = p * m
h5 : m ≠ 0
m_pos : 0 < m
m_lt_n : m < n
L : List ℕ
h6 : nondec_prime_list L ∧ prod L = m
ndpl_L : nondec_prime_list L
⊢ ∃ l, prime_factorization n l
Theorem: HTPI.exists_prime_factorization
Proof state before:
case neg
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : ¬n = 1
h3 : n ≥ 2
p : ℕ
h4 : prime_factor p n ∧ ∀ (q : ℕ), prime_factor q n → p ≤ q
p_prime_factor : prime p ∧ p ∣ n
p_prime : prime p
p_dvd_n : p ∣ n
p_least : ∀ (q : ℕ), prime_factor q n → p ≤ q
m : ℕ
n_eq_pm : n = p * m
h5 : m ≠ 0
m_pos : 0 < m
m_lt_n : m < n
L : List ℕ
h6 : nondec_prime_list L ∧ prod L = m
ndpl_L : nondec_prime_list L
⊢ ∃ l, prime_factorization n l
Tactic:
define at ndpl_L
Proof state after:
case neg
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : ¬n = 1
h3 : n ≥ 2
p : ℕ
h4 : prime_factor p n ∧ ∀ (q : ℕ), prime_factor q n → p ≤ q
p_prime_factor : prime p ∧ p ∣ n
p_prime : prime p
p_dvd_n : p ∣ n
p_least : ∀ (q : ℕ), prime_factor q n → p ≤ q
m : ℕ
n_eq_pm : n = p * m
h5 : m ≠ 0
m_pos : 0 < m
m_lt_n : m < n
L : List ℕ
h6 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
⊢ ∃ l, prime_factorization n l
Theorem: HTPI.exists_prime_factorization
Proof state before:
case neg
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : ¬n = 1
h3 : n ≥ 2
p : ℕ
h4 : prime_factor p n ∧ ∀ (q : ℕ), prime_factor q n → p ≤ q
p_prime_factor : prime p ∧ p ∣ n
p_prime : prime p
p_dvd_n : p ∣ n
p_least : ∀ (q : ℕ), prime_factor q n → p ≤ q
m : ℕ
n_eq_pm : n = p * m
h5 : m ≠ 0
m_pos : 0 < m
m_lt_n : m < n
L : List ℕ
h6 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
⊢ ∃ l, prime_factorization n l
Tactic:
apply Exists.intro (p :: L)
Proof state after:
case neg
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : ¬n = 1
h3 : n ≥ 2
p : ℕ
h4 : prime_factor p n ∧ ∀ (q : ℕ), prime_factor q n → p ≤ q
p_prime_factor : prime p ∧ p ∣ n
p_prime : prime p
p_dvd_n : p ∣ n
p_least : ∀ (q : ℕ), prime_factor q n → p ≤ q
m : ℕ
n_eq_pm : n = p * m
h5 : m ≠ 0
m_pos : 0 < m
m_lt_n : m < n
L : List ℕ
h6 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
⊢ prime_factorization n (p :: L)
Theorem: HTPI.exists_prime_factorization
Proof state before:
case neg
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : ¬n = 1
h3 : n ≥ 2
p : ℕ
h4 : prime_factor p n ∧ ∀ (q : ℕ), prime_factor q n → p ≤ q
p_prime_factor : prime p ∧ p ∣ n
p_prime : prime p
p_dvd_n : p ∣ n
p_least : ∀ (q : ℕ), prime_factor q n → p ≤ q
m : ℕ
n_eq_pm : n = p * m
h5 : m ≠ 0
m_pos : 0 < m
m_lt_n : m < n
L : List ℕ
h6 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
⊢ prime_factorization n (p :: L)
Tactic:
define
Proof state after:
case neg
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : ¬n = 1
h3 : n ≥ 2
p : ℕ
h4 : prime_factor p n ∧ ∀ (q : ℕ), prime_factor q n → p ≤ q
p_prime_factor : prime p ∧ p ∣ n
p_prime : prime p
p_dvd_n : p ∣ n
p_least : ∀ (q : ℕ), prime_factor q n → p ≤ q
m : ℕ
n_eq_pm : n = p * m
h5 : m ≠ 0
m_pos : 0 < m
m_lt_n : m < n
L : List ℕ
h6 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
⊢ nondec_prime_list (p :: L) ∧ prod (p :: L) = n
Theorem: HTPI.exists_prime_factorization
Proof state before:
case neg
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : ¬n = 1
h3 : n ≥ 2
p : ℕ
h4 : prime_factor p n ∧ ∀ (q : ℕ), prime_factor q n → p ≤ q
p_prime_factor : prime p ∧ p ∣ n
p_prime : prime p
p_dvd_n : p ∣ n
p_least : ∀ (q : ℕ), prime_factor q n → p ≤ q
m : ℕ
n_eq_pm : n = p * m
h5 : m ≠ 0
m_pos : 0 < m
m_lt_n : m < n
L : List ℕ
h6 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
⊢ nondec_prime_list (p :: L) ∧ prod (p :: L) = n
Tactic:
apply And.intro
Proof state after:
case neg.left
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : ¬n = 1
h3 : n ≥ 2
p : ℕ
h4 : prime_factor p n ∧ ∀ (q : ℕ), prime_factor q n → p ≤ q
p_prime_factor : prime p ∧ p ∣ n
p_prime : prime p
p_dvd_n : p ∣ n
p_least : ∀ (q : ℕ), prime_factor q n → p ≤ q
m : ℕ
n_eq_pm : n = p * m
h5 : m ≠ 0
m_pos : 0 < m
m_lt_n : m < n
L : List ℕ
h6 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
⊢ nondec_prime_list (p :: L)

case neg.right
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : ¬n = 1
h3 : n ≥ 2
p : ℕ
h4 : prime_factor p n ∧ ∀ (q : ℕ), prime_factor q n → p ≤ q
p_prime_factor : prime p ∧ p ∣ n
p_prime : prime p
p_dvd_n : p ∣ n
p_least : ∀ (q : ℕ), prime_factor q n → p ≤ q
m : ℕ
n_eq_pm : n = p * m
h5 : m ≠ 0
m_pos : 0 < m
m_lt_n : m < n
L : List ℕ
h6 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
⊢ prod (p :: L) = n
Theorem: HTPI.exists_prime_factorization
Proof state before:
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : ¬n = 1
h3 : n ≥ 2
p : ℕ
h4 : prime_factor p n ∧ ∀ (q : ℕ), prime_factor q n → p ≤ q
p_prime_factor : prime p ∧ p ∣ n
p_prime : prime p
p_dvd_n : p ∣ n
p_least : ∀ (q : ℕ), prime_factor q n → p ≤ q
m : ℕ
n_eq_pm : n = p * m
⊢ m ≠ 0
Tactic:
contradict h1 with h6
Proof state after:
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : ¬n = 1
h3 : n ≥ 2
p : ℕ
h4 : prime_factor p n ∧ ∀ (q : ℕ), prime_factor q n → p ≤ q
p_prime_factor : prime p ∧ p ∣ n
p_prime : prime p
p_dvd_n : p ∣ n
p_least : ∀ (q : ℕ), prime_factor q n → p ≤ q
m : ℕ
n_eq_pm : n = p * m
h6 : m = 0
⊢ ¬n ≥ 1
Theorem: HTPI.exists_prime_factorization
Proof state before:
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : ¬n = 1
h3 : n ≥ 2
p : ℕ
h4 : prime_factor p n ∧ ∀ (q : ℕ), prime_factor q n → p ≤ q
p_prime_factor : prime p ∧ p ∣ n
p_prime : prime p
p_dvd_n : p ∣ n
p_least : ∀ (q : ℕ), prime_factor q n → p ≤ q
m : ℕ
n_eq_pm : n = p * m
h6 : m = 0
⊢ ¬n ≥ 1
Tactic:
have h7 : n = 0 :=
  calc n
    _ = p * m := n_eq_pm
    _ = p * 0 := by rw [h6]
    _ = 0 := by ring
Proof state after:
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : ¬n = 1
h3 : n ≥ 2
p : ℕ
h4 : prime_factor p n ∧ ∀ (q : ℕ), prime_factor q n → p ≤ q
p_prime_factor : prime p ∧ p ∣ n
p_prime : prime p
p_dvd_n : p ∣ n
p_least : ∀ (q : ℕ), prime_factor q n → p ≤ q
m : ℕ
n_eq_pm : n = p * m
h6 : m = 0
h7 : n = 0
⊢ ¬n ≥ 1
Theorem: HTPI.exists_prime_factorization
Proof state before:
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : ¬n = 1
h3 : n ≥ 2
p : ℕ
h4 : prime_factor p n ∧ ∀ (q : ℕ), prime_factor q n → p ≤ q
p_prime_factor : prime p ∧ p ∣ n
p_prime : prime p
p_dvd_n : p ∣ n
p_least : ∀ (q : ℕ), prime_factor q n → p ≤ q
m : ℕ
n_eq_pm : n = p * m
h6 : m = 0
h7 : n = 0
⊢ ¬n ≥ 1
Tactic:
rewrite [h7]
Proof state after:
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : ¬n = 1
h3 : n ≥ 2
p : ℕ
h4 : prime_factor p n ∧ ∀ (q : ℕ), prime_factor q n → p ≤ q
p_prime_factor : prime p ∧ p ∣ n
p_prime : prime p
p_dvd_n : p ∣ n
p_least : ∀ (q : ℕ), prime_factor q n → p ≤ q
m : ℕ
n_eq_pm : n = p * m
h6 : m = 0
h7 : n = 0
⊢ ¬0 ≥ 1
Theorem: HTPI.exists_prime_factorization
Proof state before:
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : ¬n = 1
h3 : n ≥ 2
p : ℕ
h4 : prime_factor p n ∧ ∀ (q : ℕ), prime_factor q n → p ≤ q
p_prime_factor : prime p ∧ p ∣ n
p_prime : prime p
p_dvd_n : p ∣ n
p_least : ∀ (q : ℕ), prime_factor q n → p ≤ q
m : ℕ
n_eq_pm : n = p * m
h6 : m = 0
h7 : n = 0
⊢ ¬0 ≥ 1
Tactic:
decide
Proof state after:
no goals
Theorem: HTPI.exists_prime_factorization
Proof state before:
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : ¬n = 1
h3 : n ≥ 2
p : ℕ
h4 : prime_factor p n ∧ ∀ (q : ℕ), prime_factor q n → p ≤ q
p_prime_factor : prime p ∧ p ∣ n
p_prime : prime p
p_dvd_n : p ∣ n
p_least : ∀ (q : ℕ), prime_factor q n → p ≤ q
m : ℕ
n_eq_pm : n = p * m
h6 : m = 0
⊢ p * m = p * 0
Tactic:
rw [h6]
Proof state after:
no goals
Theorem: HTPI.exists_prime_factorization
Proof state before:
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : ¬n = 1
h3 : n ≥ 2
p : ℕ
h4 : prime_factor p n ∧ ∀ (q : ℕ), prime_factor q n → p ≤ q
p_prime_factor : prime p ∧ p ∣ n
p_prime : prime p
p_dvd_n : p ∣ n
p_least : ∀ (q : ℕ), prime_factor q n → p ≤ q
m : ℕ
n_eq_pm : n = p * m
h6 : m = 0
⊢ p * 0 = 0
Tactic:
ring
Proof state after:
no goals
Theorem: HTPI.exists_prime_factorization
Proof state before:
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : ¬n = 1
h3 : n ≥ 2
p : ℕ
h4 : prime_factor p n ∧ ∀ (q : ℕ), prime_factor q n → p ≤ q
p_prime_factor : prime p ∧ p ∣ n
p_prime : prime p
p_dvd_n : p ∣ n
p_least : ∀ (q : ℕ), prime_factor q n → p ≤ q
m : ℕ
n_eq_pm : n = p * m
h5 : m ≠ 0
m_pos : 0 < m
⊢ m < n
Tactic:
define at p_prime
Proof state after:
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : ¬n = 1
h3 : n ≥ 2
p : ℕ
h4 : prime_factor p n ∧ ∀ (q : ℕ), prime_factor q n → p ≤ q
p_prime_factor : prime p ∧ p ∣ n
p_prime : 2 ≤ p ∧ ¬∃ a b, a * b = p ∧ a < p ∧ b < p
p_dvd_n : p ∣ n
p_least : ∀ (q : ℕ), prime_factor q n → p ≤ q
m : ℕ
n_eq_pm : n = p * m
h5 : m ≠ 0
m_pos : 0 < m
⊢ m < n
Theorem: HTPI.exists_prime_factorization
Proof state before:
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : ¬n = 1
h3 : n ≥ 2
p : ℕ
h4 : prime_factor p n ∧ ∀ (q : ℕ), prime_factor q n → p ≤ q
p_prime_factor : prime p ∧ p ∣ n
p_prime : 2 ≤ p ∧ ¬∃ a b, a * b = p ∧ a < p ∧ b < p
p_dvd_n : p ∣ n
p_least : ∀ (q : ℕ), prime_factor q n → p ≤ q
m : ℕ
n_eq_pm : n = p * m
h5 : m ≠ 0
m_pos : 0 < m
⊢ m < n
Tactic:
show m < n from
  calc m
    _ < m + m := by linarith
    _ = 2 * m := by ring
    _ ≤ p * m := by rel [p_prime.left]
    _ = n := n_eq_pm.symm
Proof state after:
no goals
Theorem: HTPI.exists_prime_factorization
Proof state before:
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : ¬n = 1
h3 : n ≥ 2
p : ℕ
h4 : prime_factor p n ∧ ∀ (q : ℕ), prime_factor q n → p ≤ q
p_prime_factor : prime p ∧ p ∣ n
p_prime : 2 ≤ p ∧ ¬∃ a b, a * b = p ∧ a < p ∧ b < p
p_dvd_n : p ∣ n
p_least : ∀ (q : ℕ), prime_factor q n → p ≤ q
m : ℕ
n_eq_pm : n = p * m
h5 : m ≠ 0
m_pos : 0 < m
⊢ m < m + m
Tactic:
linarith
Proof state after:
no goals
Theorem: HTPI.exists_prime_factorization
Proof state before:
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : ¬n = 1
h3 : n ≥ 2
p : ℕ
h4 : prime_factor p n ∧ ∀ (q : ℕ), prime_factor q n → p ≤ q
p_prime_factor : prime p ∧ p ∣ n
p_prime : 2 ≤ p ∧ ¬∃ a b, a * b = p ∧ a < p ∧ b < p
p_dvd_n : p ∣ n
p_least : ∀ (q : ℕ), prime_factor q n → p ≤ q
m : ℕ
n_eq_pm : n = p * m
h5 : m ≠ 0
m_pos : 0 < m
⊢ m + m = 2 * m
Tactic:
ring
Proof state after:
no goals
Theorem: HTPI.exists_prime_factorization
Proof state before:
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : ¬n = 1
h3 : n ≥ 2
p : ℕ
h4 : prime_factor p n ∧ ∀ (q : ℕ), prime_factor q n → p ≤ q
p_prime_factor : prime p ∧ p ∣ n
p_prime : 2 ≤ p ∧ ¬∃ a b, a * b = p ∧ a < p ∧ b < p
p_dvd_n : p ∣ n
p_least : ∀ (q : ℕ), prime_factor q n → p ≤ q
m : ℕ
n_eq_pm : n = p * m
h5 : m ≠ 0
m_pos : 0 < m
⊢ 2 * m ≤ p * m
Tactic:
rel [p_prime.left]
Proof state after:
no goals
Theorem: HTPI.exists_prime_factorization
Proof state before:
case neg.left
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : ¬n = 1
h3 : n ≥ 2
p : ℕ
h4 : prime_factor p n ∧ ∀ (q : ℕ), prime_factor q n → p ≤ q
p_prime_factor : prime p ∧ p ∣ n
p_prime : prime p
p_dvd_n : p ∣ n
p_least : ∀ (q : ℕ), prime_factor q n → p ≤ q
m : ℕ
n_eq_pm : n = p * m
h5 : m ≠ 0
m_pos : 0 < m
m_lt_n : m < n
L : List ℕ
h6 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
⊢ nondec_prime_list (p :: L)
Tactic:
define
Proof state after:
case neg.left
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : ¬n = 1
h3 : n ≥ 2
p : ℕ
h4 : prime_factor p n ∧ ∀ (q : ℕ), prime_factor q n → p ≤ q
p_prime_factor : prime p ∧ p ∣ n
p_prime : prime p
p_dvd_n : p ∣ n
p_least : ∀ (q : ℕ), prime_factor q n → p ≤ q
m : ℕ
n_eq_pm : n = p * m
h5 : m ≠ 0
m_pos : 0 < m
m_lt_n : m < n
L : List ℕ
h6 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
⊢ all_prime (p :: L) ∧ nondec (p :: L)
Theorem: HTPI.exists_prime_factorization
Proof state before:
case neg.left
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : ¬n = 1
h3 : n ≥ 2
p : ℕ
h4 : prime_factor p n ∧ ∀ (q : ℕ), prime_factor q n → p ≤ q
p_prime_factor : prime p ∧ p ∣ n
p_prime : prime p
p_dvd_n : p ∣ n
p_least : ∀ (q : ℕ), prime_factor q n → p ≤ q
m : ℕ
n_eq_pm : n = p * m
h5 : m ≠ 0
m_pos : 0 < m
m_lt_n : m < n
L : List ℕ
h6 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
⊢ all_prime (p :: L) ∧ nondec (p :: L)
Tactic:
apply And.intro
Proof state after:
case neg.left.left
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : ¬n = 1
h3 : n ≥ 2
p : ℕ
h4 : prime_factor p n ∧ ∀ (q : ℕ), prime_factor q n → p ≤ q
p_prime_factor : prime p ∧ p ∣ n
p_prime : prime p
p_dvd_n : p ∣ n
p_least : ∀ (q : ℕ), prime_factor q n → p ≤ q
m : ℕ
n_eq_pm : n = p * m
h5 : m ≠ 0
m_pos : 0 < m
m_lt_n : m < n
L : List ℕ
h6 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
⊢ all_prime (p :: L)

case neg.left.right
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : ¬n = 1
h3 : n ≥ 2
p : ℕ
h4 : prime_factor p n ∧ ∀ (q : ℕ), prime_factor q n → p ≤ q
p_prime_factor : prime p ∧ p ∣ n
p_prime : prime p
p_dvd_n : p ∣ n
p_least : ∀ (q : ℕ), prime_factor q n → p ≤ q
m : ℕ
n_eq_pm : n = p * m
h5 : m ≠ 0
m_pos : 0 < m
m_lt_n : m < n
L : List ℕ
h6 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
⊢ nondec (p :: L)
Theorem: HTPI.exists_prime_factorization
Proof state before:
case neg.left.left
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : ¬n = 1
h3 : n ≥ 2
p : ℕ
h4 : prime_factor p n ∧ ∀ (q : ℕ), prime_factor q n → p ≤ q
p_prime_factor : prime p ∧ p ∣ n
p_prime : prime p
p_dvd_n : p ∣ n
p_least : ∀ (q : ℕ), prime_factor q n → p ≤ q
m : ℕ
n_eq_pm : n = p * m
h5 : m ≠ 0
m_pos : 0 < m
m_lt_n : m < n
L : List ℕ
h6 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
⊢ all_prime (p :: L)
Tactic:
rewrite [all_prime_cons]
Proof state after:
case neg.left.left
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : ¬n = 1
h3 : n ≥ 2
p : ℕ
h4 : prime_factor p n ∧ ∀ (q : ℕ), prime_factor q n → p ≤ q
p_prime_factor : prime p ∧ p ∣ n
p_prime : prime p
p_dvd_n : p ∣ n
p_least : ∀ (q : ℕ), prime_factor q n → p ≤ q
m : ℕ
n_eq_pm : n = p * m
h5 : m ≠ 0
m_pos : 0 < m
m_lt_n : m < n
L : List ℕ
h6 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
⊢ prime p ∧ all_prime L
Theorem: HTPI.exists_prime_factorization
Proof state before:
case neg.left.left
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : ¬n = 1
h3 : n ≥ 2
p : ℕ
h4 : prime_factor p n ∧ ∀ (q : ℕ), prime_factor q n → p ≤ q
p_prime_factor : prime p ∧ p ∣ n
p_prime : prime p
p_dvd_n : p ∣ n
p_least : ∀ (q : ℕ), prime_factor q n → p ≤ q
m : ℕ
n_eq_pm : n = p * m
h5 : m ≠ 0
m_pos : 0 < m
m_lt_n : m < n
L : List ℕ
h6 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
⊢ prime p ∧ all_prime L
Tactic:
show prime p ∧ all_prime L from And.intro p_prime ndpl_L.left
Proof state after:
no goals
Theorem: HTPI.exists_prime_factorization
Proof state before:
case neg.left.right
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : ¬n = 1
h3 : n ≥ 2
p : ℕ
h4 : prime_factor p n ∧ ∀ (q : ℕ), prime_factor q n → p ≤ q
p_prime_factor : prime p ∧ p ∣ n
p_prime : prime p
p_dvd_n : p ∣ n
p_least : ∀ (q : ℕ), prime_factor q n → p ≤ q
m : ℕ
n_eq_pm : n = p * m
h5 : m ≠ 0
m_pos : 0 < m
m_lt_n : m < n
L : List ℕ
h6 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
⊢ nondec (p :: L)
Tactic:
rewrite [nondec_cons]
Proof state after:
case neg.left.right
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : ¬n = 1
h3 : n ≥ 2
p : ℕ
h4 : prime_factor p n ∧ ∀ (q : ℕ), prime_factor q n → p ≤ q
p_prime_factor : prime p ∧ p ∣ n
p_prime : prime p
p_dvd_n : p ∣ n
p_least : ∀ (q : ℕ), prime_factor q n → p ≤ q
m : ℕ
n_eq_pm : n = p * m
h5 : m ≠ 0
m_pos : 0 < m
m_lt_n : m < n
L : List ℕ
h6 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
⊢ (∀ m ∈ L, p ≤ m) ∧ nondec L
Theorem: HTPI.exists_prime_factorization
Proof state before:
case neg.left.right
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : ¬n = 1
h3 : n ≥ 2
p : ℕ
h4 : prime_factor p n ∧ ∀ (q : ℕ), prime_factor q n → p ≤ q
p_prime_factor : prime p ∧ p ∣ n
p_prime : prime p
p_dvd_n : p ∣ n
p_least : ∀ (q : ℕ), prime_factor q n → p ≤ q
m : ℕ
n_eq_pm : n = p * m
h5 : m ≠ 0
m_pos : 0 < m
m_lt_n : m < n
L : List ℕ
h6 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
⊢ (∀ m ∈ L, p ≤ m) ∧ nondec L
Tactic:
apply And.intro _ ndpl_L.right
Proof state after:
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : ¬n = 1
h3 : n ≥ 2
p : ℕ
h4 : prime_factor p n ∧ ∀ (q : ℕ), prime_factor q n → p ≤ q
p_prime_factor : prime p ∧ p ∣ n
p_prime : prime p
p_dvd_n : p ∣ n
p_least : ∀ (q : ℕ), prime_factor q n → p ≤ q
m : ℕ
n_eq_pm : n = p * m
h5 : m ≠ 0
m_pos : 0 < m
m_lt_n : m < n
L : List ℕ
h6 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
⊢ ∀ m ∈ L, p ≤ m
Theorem: HTPI.exists_prime_factorization
Proof state before:
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : ¬n = 1
h3 : n ≥ 2
p : ℕ
h4 : prime_factor p n ∧ ∀ (q : ℕ), prime_factor q n → p ≤ q
p_prime_factor : prime p ∧ p ∣ n
p_prime : prime p
p_dvd_n : p ∣ n
p_least : ∀ (q : ℕ), prime_factor q n → p ≤ q
m : ℕ
n_eq_pm : n = p * m
h5 : m ≠ 0
m_pos : 0 < m
m_lt_n : m < n
L : List ℕ
h6 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
⊢ ∀ m ∈ L, p ≤ m
Tactic:
fix q : Nat
Proof state after:
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : ¬n = 1
h3 : n ≥ 2
p : ℕ
h4 : prime_factor p n ∧ ∀ (q : ℕ), prime_factor q n → p ≤ q
p_prime_factor : prime p ∧ p ∣ n
p_prime : prime p
p_dvd_n : p ∣ n
p_least : ∀ (q : ℕ), prime_factor q n → p ≤ q
m : ℕ
n_eq_pm : n = p * m
h5 : m ≠ 0
m_pos : 0 < m
m_lt_n : m < n
L : List ℕ
h6 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
q : ℕ
⊢ q ∈ L → p ≤ q
Theorem: HTPI.exists_prime_factorization
Proof state before:
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : ¬n = 1
h3 : n ≥ 2
p : ℕ
h4 : prime_factor p n ∧ ∀ (q : ℕ), prime_factor q n → p ≤ q
p_prime_factor : prime p ∧ p ∣ n
p_prime : prime p
p_dvd_n : p ∣ n
p_least : ∀ (q : ℕ), prime_factor q n → p ≤ q
m : ℕ
n_eq_pm : n = p * m
h5 : m ≠ 0
m_pos : 0 < m
m_lt_n : m < n
L : List ℕ
h6 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
q : ℕ
⊢ q ∈ L → p ≤ q
Tactic:
assume q_in_L : q ∈ L
Proof state after:
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : ¬n = 1
h3 : n ≥ 2
p : ℕ
h4 : prime_factor p n ∧ ∀ (q : ℕ), prime_factor q n → p ≤ q
p_prime_factor : prime p ∧ p ∣ n
p_prime : prime p
p_dvd_n : p ∣ n
p_least : ∀ (q : ℕ), prime_factor q n → p ≤ q
m : ℕ
n_eq_pm : n = p * m
h5 : m ≠ 0
m_pos : 0 < m
m_lt_n : m < n
L : List ℕ
h6 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
q : ℕ
q_in_L : q ∈ L
⊢ p ≤ q
Theorem: HTPI.exists_prime_factorization
Proof state before:
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : ¬n = 1
h3 : n ≥ 2
p : ℕ
h4 : prime_factor p n ∧ ∀ (q : ℕ), prime_factor q n → p ≤ q
p_prime_factor : prime p ∧ p ∣ n
p_prime : prime p
p_dvd_n : p ∣ n
p_least : ∀ (q : ℕ), prime_factor q n → p ≤ q
m : ℕ
n_eq_pm : n = p * m
h5 : m ≠ 0
m_pos : 0 < m
m_lt_n : m < n
L : List ℕ
h6 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
q : ℕ
q_in_L : q ∈ L
⊢ p ≤ q
Tactic:
have h7 : q ∣ prod L := list_elt_dvd_prod q_in_L
Proof state after:
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : ¬n = 1
h3 : n ≥ 2
p : ℕ
h4 : prime_factor p n ∧ ∀ (q : ℕ), prime_factor q n → p ≤ q
p_prime_factor : prime p ∧ p ∣ n
p_prime : prime p
p_dvd_n : p ∣ n
p_least : ∀ (q : ℕ), prime_factor q n → p ≤ q
m : ℕ
n_eq_pm : n = p * m
h5 : m ≠ 0
m_pos : 0 < m
m_lt_n : m < n
L : List ℕ
h6 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
q : ℕ
q_in_L : q ∈ L
h7 : q ∣ prod L
⊢ p ≤ q
Theorem: HTPI.exists_prime_factorization
Proof state before:
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : ¬n = 1
h3 : n ≥ 2
p : ℕ
h4 : prime_factor p n ∧ ∀ (q : ℕ), prime_factor q n → p ≤ q
p_prime_factor : prime p ∧ p ∣ n
p_prime : prime p
p_dvd_n : p ∣ n
p_least : ∀ (q : ℕ), prime_factor q n → p ≤ q
m : ℕ
n_eq_pm : n = p * m
h5 : m ≠ 0
m_pos : 0 < m
m_lt_n : m < n
L : List ℕ
h6 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
q : ℕ
q_in_L : q ∈ L
h7 : q ∣ prod L
⊢ p ≤ q
Tactic:
rewrite [h6.right] at h7
Proof state after:
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : ¬n = 1
h3 : n ≥ 2
p : ℕ
h4 : prime_factor p n ∧ ∀ (q : ℕ), prime_factor q n → p ≤ q
p_prime_factor : prime p ∧ p ∣ n
p_prime : prime p
p_dvd_n : p ∣ n
p_least : ∀ (q : ℕ), prime_factor q n → p ≤ q
m : ℕ
n_eq_pm : n = p * m
h5 : m ≠ 0
m_pos : 0 < m
m_lt_n : m < n
L : List ℕ
h6 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
q : ℕ
q_in_L : q ∈ L
h7 : q ∣ m
⊢ p ≤ q