internlm/Lean-Github huggingface dataset:
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:
assume ih : ∀ (l : List Nat), List.length l = n → a ∈ l → a ∣ prod l
Proof state after:
case Induction_Step
a n : ℕ
ih : ∀ (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 Induction_Step
a n : ℕ
ih : ∀ (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 l : List Nat
Proof state after:
case Induction_Step
a n : ℕ
ih : ∀ (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 Induction_Step
a n : ℕ
ih : ∀ (l : List ℕ), List.length l = n → a ∈ l → a ∣ prod l
l : List ℕ
⊢ List.length l = n + 1 → a ∈ l → a ∣ prod l
Tactic:
assume h1 : l.length = n + 1
Proof state after:
case Induction_Step
a n : ℕ
ih : ∀ (l : List ℕ), List.length l = n → a ∈ l → a ∣ prod l
l : List ℕ
h1 : List.length l = n + 1
⊢ a ∈ l → a ∣ prod l
Theorem: HTPI.list_elt_dvd_prod_by_length
Proof state before:
case Induction_Step
a n : ℕ
ih : ∀ (l : List ℕ), List.length l = n → a ∈ l → a ∣ prod l
l : List ℕ
h1 : List.length l = n + 1
⊢ a ∈ l → a ∣ prod l
Tactic:
obtain (b : Nat) (h2 : ∃ (L : List Nat),
  l = b :: L ∧ L.length = n) from exists_cons_of_length_eq_succ h1
Proof state after:
case Induction_Step
a n : ℕ
ih : ∀ (l : List ℕ), List.length l = n → a ∈ l → a ∣ prod l
l : List ℕ
h1 : List.length l = n + 1
b : ℕ
h2 : ∃ L, l = b :: L ∧ List.length L = n
⊢ a ∈ l → a ∣ prod l
Theorem: HTPI.list_elt_dvd_prod_by_length
Proof state before:
case Induction_Step
a n : ℕ
ih : ∀ (l : List ℕ), List.length l = n → a ∈ l → a ∣ prod l
l : List ℕ
h1 : List.length l = n + 1
b : ℕ
h2 : ∃ L, l = b :: L ∧ List.length L = n
⊢ a ∈ l → a ∣ prod l
Tactic:
obtain (L : List Nat) (h3 : l = b :: L ∧ L.length = n) from h2
Proof state after:
case Induction_Step
a n : ℕ
ih : ∀ (l : List ℕ), List.length l = n → a ∈ l → a ∣ prod l
l : List ℕ
h1 : List.length l = n + 1
b : ℕ
h2 : ∃ L, l = b :: L ∧ List.length L = n
L : List ℕ
h3 : l = b :: L ∧ List.length L = n
⊢ a ∈ l → a ∣ prod l
Theorem: HTPI.list_elt_dvd_prod_by_length
Proof state before:
case Induction_Step
a n : ℕ
ih : ∀ (l : List ℕ), List.length l = n → a ∈ l → a ∣ prod l
l : List ℕ
h1 : List.length l = n + 1
b : ℕ
h2 : ∃ L, l = b :: L ∧ List.length L = n
L : List ℕ
h3 : l = b :: L ∧ List.length L = n
⊢ a ∈ l → a ∣ prod l
Tactic:
have h4 : a ∈ L → a ∣ prod L := ih L h3.right
Proof state after:
case Induction_Step
a n : ℕ
ih : ∀ (l : List ℕ), List.length l = n → a ∈ l → a ∣ prod l
l : List ℕ
h1 : List.length l = n + 1
b : ℕ
h2 : ∃ L, l = b :: L ∧ List.length L = n
L : List ℕ
h3 : l = b :: L ∧ List.length L = n
h4 : a ∈ L → a ∣ prod L
⊢ a ∈ l → a ∣ prod l
Theorem: HTPI.list_elt_dvd_prod_by_length
Proof state before:
case Induction_Step
a n : ℕ
ih : ∀ (l : List ℕ), List.length l = n → a ∈ l → a ∣ prod l
l : List ℕ
h1 : List.length l = n + 1
b : ℕ
h2 : ∃ L, l = b :: L ∧ List.length L = n
L : List ℕ
h3 : l = b :: L ∧ List.length L = n
h4 : a ∈ L → a ∣ prod L
⊢ a ∈ l → a ∣ prod l
Tactic:
assume h5 : a ∈ l
Proof state after:
case Induction_Step
a n : ℕ
ih : ∀ (l : List ℕ), List.length l = n → a ∈ l → a ∣ prod l
l : List ℕ
h1 : List.length l = n + 1
b : ℕ
h2 : ∃ L, l = b :: L ∧ List.length L = n
L : List ℕ
h3 : l = b :: L ∧ List.length L = n
h4 : a ∈ L → a ∣ prod L
h5 : a ∈ l
⊢ a ∣ prod l
Theorem: HTPI.list_elt_dvd_prod_by_length
Proof state before:
case Induction_Step
a n : ℕ
ih : ∀ (l : List ℕ), List.length l = n → a ∈ l → a ∣ prod l
l : List ℕ
h1 : List.length l = n + 1
b : ℕ
h2 : ∃ L, l = b :: L ∧ List.length L = n
L : List ℕ
h3 : l = b :: L ∧ List.length L = n
h4 : a ∈ L → a ∣ prod L
h5 : a ∈ l
⊢ a ∣ prod l
Tactic:
rewrite [h3.left, prod_cons]
Proof state after:
case Induction_Step
a n : ℕ
ih : ∀ (l : List ℕ), List.length l = n → a ∈ l → a ∣ prod l
l : List ℕ
h1 : List.length l = n + 1
b : ℕ
h2 : ∃ L, l = b :: L ∧ List.length L = n
L : List ℕ
h3 : l = b :: L ∧ List.length L = n
h4 : a ∈ L → a ∣ prod L
h5 : a ∈ l
⊢ a ∣ b * prod L
Theorem: HTPI.list_elt_dvd_prod_by_length
Proof state before:
case Induction_Step
a n : ℕ
ih : ∀ (l : List ℕ), List.length l = n → a ∈ l → a ∣ prod l
l : List ℕ
h1 : List.length l = n + 1
b : ℕ
h2 : ∃ L, l = b :: L ∧ List.length L = n
L : List ℕ
h3 : l = b :: L ∧ List.length L = n
h4 : a ∈ L → a ∣ prod L
h5 : a ∈ l
⊢ a ∣ b * prod L
Tactic:
rewrite [h3.left, List.mem_cons] at h5
Proof state after:
case Induction_Step
a n : ℕ
ih : ∀ (l : List ℕ), List.length l = n → a ∈ l → a ∣ prod l
l : List ℕ
h1 : List.length l = n + 1
b : ℕ
h2 : ∃ L, l = b :: L ∧ List.length L = n
L : List ℕ
h3 : l = b :: L ∧ List.length L = n
h4 : a ∈ L → a ∣ prod L
h5 : a = b ∨ a ∈ L
⊢ a ∣ b * prod L
Theorem: HTPI.list_elt_dvd_prod_by_length
Proof state before:
case Induction_Step
a n : ℕ
ih : ∀ (l : List ℕ), List.length l = n → a ∈ l → a ∣ prod l
l : List ℕ
h1 : List.length l = n + 1
b : ℕ
h2 : ∃ L, l = b :: L ∧ List.length L = n
L : List ℕ
h3 : l = b :: L ∧ List.length L = n
h4 : a ∈ L → a ∣ prod L
h5 : a = b ∨ a ∈ L
⊢ a ∣ b * prod L
Tactic:
by_cases on h5
Proof state after:
case Induction_Step.Case_1
a n : ℕ
ih : ∀ (l : List ℕ), List.length l = n → a ∈ l → a ∣ prod l
l : List ℕ
h1 : List.length l = n + 1
b : ℕ
h2 : ∃ L, l = b :: L ∧ List.length L = n
L : List ℕ
h3 : l = b :: L ∧ List.length L = n
h4 : a ∈ L → a ∣ prod L
h5 : a = b
⊢ a ∣ b * prod L

case Induction_Step.Case_2
a n : ℕ
ih : ∀ (l : List ℕ), List.length l = n → a ∈ l → a ∣ prod l
l : List ℕ
h1 : List.length l = n + 1
b : ℕ
h2 : ∃ L, l = b :: L ∧ List.length L = n
L : List ℕ
h3 : l = b :: L ∧ List.length L = n
h4 : a ∈ L → a ∣ prod L
h5 : a ∈ L
⊢ a ∣ b * prod L
Theorem: HTPI.list_elt_dvd_prod_by_length
Proof state before:
case Induction_Step.Case_1
a n : ℕ
ih : ∀ (l : List ℕ), List.length l = n → a ∈ l → a ∣ prod l
l : List ℕ
h1 : List.length l = n + 1
b : ℕ
h2 : ∃ L, l = b :: L ∧ List.length L = n
L : List ℕ
h3 : l = b :: L ∧ List.length L = n
h4 : a ∈ L → a ∣ prod L
h5 : a = b
⊢ a ∣ b * prod L
Tactic:
apply Exists.intro (prod L)
Proof state after:
case Induction_Step.Case_1
a n : ℕ
ih : ∀ (l : List ℕ), List.length l = n → a ∈ l → a ∣ prod l
l : List ℕ
h1 : List.length l = n + 1
b : ℕ
h2 : ∃ L, l = b :: L ∧ List.length L = n
L : List ℕ
h3 : l = b :: L ∧ List.length L = n
h4 : a ∈ L → a ∣ prod L
h5 : a = b
⊢ b * prod L = a * prod L
Theorem: HTPI.list_elt_dvd_prod_by_length
Proof state before:
case Induction_Step.Case_1
a n : ℕ
ih : ∀ (l : List ℕ), List.length l = n → a ∈ l → a ∣ prod l
l : List ℕ
h1 : List.length l = n + 1
b : ℕ
h2 : ∃ L, l = b :: L ∧ List.length L = n
L : List ℕ
h3 : l = b :: L ∧ List.length L = n
h4 : a ∈ L → a ∣ prod L
h5 : a = b
⊢ b * prod L = a * prod L
Tactic:
rewrite [h5]
Proof state after:
case Induction_Step.Case_1
a n : ℕ
ih : ∀ (l : List ℕ), List.length l = n → a ∈ l → a ∣ prod l
l : List ℕ
h1 : List.length l = n + 1
b : ℕ
h2 : ∃ L, l = b :: L ∧ List.length L = n
L : List ℕ
h3 : l = b :: L ∧ List.length L = n
h4 : a ∈ L → a ∣ prod L
h5 : a = b
⊢ b * prod L = b * prod L
Theorem: HTPI.list_elt_dvd_prod_by_length
Proof state before:
case Induction_Step.Case_1
a n : ℕ
ih : ∀ (l : List ℕ), List.length l = n → a ∈ l → a ∣ prod l
l : List ℕ
h1 : List.length l = n + 1
b : ℕ
h2 : ∃ L, l = b :: L ∧ List.length L = n
L : List ℕ
h3 : l = b :: L ∧ List.length L = n
h4 : a ∈ L → a ∣ prod L
h5 : a = b
⊢ b * prod L = b * prod L
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.list_elt_dvd_prod_by_length
Proof state before:
case Induction_Step.Case_2
a n : ℕ
ih : ∀ (l : List ℕ), List.length l = n → a ∈ l → a ∣ prod l
l : List ℕ
h1 : List.length l = n + 1
b : ℕ
h2 : ∃ L, l = b :: L ∧ List.length L = n
L : List ℕ
h3 : l = b :: L ∧ List.length L = n
h4 : a ∈ L → a ∣ prod L
h5 : a ∈ L
⊢ a ∣ b * prod L
Tactic:
have h6 : a ∣ prod L := h4 h5
Proof state after:
case Induction_Step.Case_2
a n : ℕ
ih : ∀ (l : List ℕ), List.length l = n → a ∈ l → a ∣ prod l
l : List ℕ
h1 : List.length l = n + 1
b : ℕ
h2 : ∃ L, l = b :: L ∧ List.length L = n
L : List ℕ
h3 : l = b :: L ∧ List.length L = n
h4 : a ∈ L → a ∣ prod L
h5 : a ∈ L
h6 : a ∣ prod L
⊢ a ∣ b * prod L
Theorem: HTPI.list_elt_dvd_prod_by_length
Proof state before:
case Induction_Step.Case_2
a n : ℕ
ih : ∀ (l : List ℕ), List.length l = n → a ∈ l → a ∣ prod l
l : List ℕ
h1 : List.length l = n + 1
b : ℕ
h2 : ∃ L, l = b :: L ∧ List.length L = n
L : List ℕ
h3 : l = b :: L ∧ List.length L = n
h4 : a ∈ L → a ∣ prod L
h5 : a ∈ L
h6 : a ∣ prod L
⊢ a ∣ b * prod L
Tactic:
have h7 : prod L ∣ b * prod L := by
  apply Exists.intro b
  ring
  done
Proof state after:
case Induction_Step.Case_2
a n : ℕ
ih : ∀ (l : List ℕ), List.length l = n → a ∈ l → a ∣ prod l
l : List ℕ
h1 : List.length l = n + 1
b : ℕ
h2 : ∃ L, l = b :: L ∧ List.length L = n
L : List ℕ
h3 : l = b :: L ∧ List.length L = n
h4 : a ∈ L → a ∣ prod L
h5 : a ∈ L
h6 : a ∣ prod L
h7 : prod L ∣ b * prod L
⊢ a ∣ b * prod L
Theorem: HTPI.list_elt_dvd_prod_by_length
Proof state before:
case Induction_Step.Case_2
a n : ℕ
ih : ∀ (l : List ℕ), List.length l = n → a ∈ l → a ∣ prod l
l : List ℕ
h1 : List.length l = n + 1
b : ℕ
h2 : ∃ L, l = b :: L ∧ List.length L = n
L : List ℕ
h3 : l = b :: L ∧ List.length L = n
h4 : a ∈ L → a ∣ prod L
h5 : a ∈ L
h6 : a ∣ prod L
h7 : prod L ∣ b * prod L
⊢ a ∣ b * prod L
Tactic:
show a ∣ b * prod L from dvd_trans h6 h7
Proof state after:
no goals
Theorem: HTPI.list_elt_dvd_prod_by_length
Proof state before:
a n : ℕ
ih : ∀ (l : List ℕ), List.length l = n → a ∈ l → a ∣ prod l
l : List ℕ
h1 : List.length l = n + 1
b : ℕ
h2 : ∃ L, l = b :: L ∧ List.length L = n
L : List ℕ
h3 : l = b :: L ∧ List.length L = n
h4 : a ∈ L → a ∣ prod L
h5 : a ∈ L
h6 : a ∣ prod L
⊢ prod L ∣ b * prod L
Tactic:
apply Exists.intro b
Proof state after:
a n : ℕ
ih : ∀ (l : List ℕ), List.length l = n → a ∈ l → a ∣ prod l
l : List ℕ
h1 : List.length l = n + 1
b : ℕ
h2 : ∃ L, l = b :: L ∧ List.length L = n
L : List ℕ
h3 : l = b :: L ∧ List.length L = n
h4 : a ∈ L → a ∣ prod L
h5 : a ∈ L
h6 : a ∣ prod L
⊢ b * prod L = prod L * b
Theorem: HTPI.list_elt_dvd_prod_by_length
Proof state before:
a n : ℕ
ih : ∀ (l : List ℕ), List.length l = n → a ∈ l → a ∣ prod l
l : List ℕ
h1 : List.length l = n + 1
b : ℕ
h2 : ∃ L, l = b :: L ∧ List.length L = n
L : List ℕ
h3 : l = b :: L ∧ List.length L = n
h4 : a ∈ L → a ∣ prod L
h5 : a ∈ L
h6 : a ∣ prod L
⊢ b * prod L = prod L * b
Tactic:
ring
Proof state after:
no goals
Theorem: HTPI.list_elt_dvd_prod
Proof state before:
a : ℕ
l : List ℕ
h : a ∈ l
⊢ a ∣ prod l
Tactic:
set n : Nat := l.length
Proof state after:
a : ℕ
l : List ℕ
h : a ∈ l
n : ℕ := List.length l
⊢ a ∣ prod l
Theorem: HTPI.list_elt_dvd_prod
Proof state before:
a : ℕ
l : List ℕ
h : a ∈ l
n : ℕ := List.length l
⊢ a ∣ prod l
Tactic:
have h1 : l.length = n := by rfl
Proof state after:
a : ℕ
l : List ℕ
h : a ∈ l
n : ℕ := List.length l
h1 : List.length l = n
⊢ a ∣ prod l
Theorem: HTPI.list_elt_dvd_prod
Proof state before:
a : ℕ
l : List ℕ
h : a ∈ l
n : ℕ := List.length l
h1 : List.length l = n
⊢ a ∣ prod l
Tactic:
show a ∣ prod l from list_elt_dvd_prod_by_length a n l h1 h
Proof state after:
no goals
Theorem: HTPI.list_elt_dvd_prod
Proof state before:
a : ℕ
l : List ℕ
h : a ∈ l
n : ℕ := List.length l
⊢ List.length l = n
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.exists_prime_factorization
Proof state before:
⊢ ∀ n ≥ 1, ∃ l, prime_factorization n l
Tactic:
by_strong_induc
Proof state after:
⊢ ∀ (n : ℕ), (∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l) → n ≥ 1 → ∃ l, prime_factorization n l
Theorem: HTPI.exists_prime_factorization
Proof state before:
⊢ ∀ (n : ℕ), (∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l) → n ≥ 1 → ∃ l, prime_factorization n l
Tactic:
fix n : Nat
Proof state after:
n : ℕ
⊢ (∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l) → n ≥ 1 → ∃ l, prime_factorization n l
Theorem: HTPI.exists_prime_factorization
Proof state before:
n : ℕ
⊢ (∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l) → n ≥ 1 → ∃ l, prime_factorization n l
Tactic:
assume ih : ∀ n_1 < n, n_1 ≥ 1 →
  ∃ (l : List Nat), prime_factorization n_1 l
Proof state after:
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
⊢ n ≥ 1 → ∃ l, prime_factorization n l
Theorem: HTPI.exists_prime_factorization
Proof state before:
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
⊢ n ≥ 1 → ∃ l, prime_factorization n l
Tactic:
assume h1 : n ≥ 1
Proof state after:
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
⊢ ∃ l, prime_factorization n l
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
⊢ ∃ l, prime_factorization n l
Tactic:
by_cases h2 : n = 1
Proof state after:
case pos
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : n = 1
⊢ ∃ l, prime_factorization n l

case neg
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : ¬n = 1
⊢ ∃ l, prime_factorization n l
Theorem: HTPI.exists_prime_factorization
Proof state before:
case pos
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : n = 1
⊢ ∃ l, prime_factorization n l
Tactic:
apply Exists.intro []
Proof state after:
case pos
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : n = 1
⊢ prime_factorization n []
Theorem: HTPI.exists_prime_factorization
Proof state before:
case pos
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : n = 1
⊢ prime_factorization n []
Tactic:
define
Proof state after:
case pos
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : n = 1
⊢ nondec_prime_list [] ∧ prod [] = n
Theorem: HTPI.exists_prime_factorization
Proof state before:
case pos
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : n = 1
⊢ nondec_prime_list [] ∧ prod [] = n
Tactic:
apply And.intro
Proof state after:
case pos.left
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : n = 1
⊢ nondec_prime_list []

case pos.right
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : n = 1
⊢ prod [] = n
Theorem: HTPI.exists_prime_factorization
Proof state before:
case pos.left
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : n = 1
⊢ nondec_prime_list []
Tactic:
define
Proof state after:
case pos.left
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : n = 1
⊢ all_prime [] ∧ nondec []
Theorem: HTPI.exists_prime_factorization
Proof state before:
case pos.left
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : n = 1
⊢ all_prime [] ∧ nondec []
Tactic:
show all_prime [] ∧ nondec [] from
  And.intro all_prime_nil nondec_nil
Proof state after:
no goals
Theorem: HTPI.exists_prime_factorization
Proof state before:
case pos.right
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : n = 1
⊢ prod [] = n
Tactic:
rewrite [prod_nil, h2]
Proof state after:
case pos.right
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : n = 1
⊢ 1 = 1
Theorem: HTPI.exists_prime_factorization
Proof state before:
case pos.right
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : n = 1
⊢ 1 = 1
Tactic:
rfl
Proof state after:
no goals
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
⊢ ∃ l, prime_factorization n l
Tactic:
have h3 : n ≥ 2 := lt_of_le_of_ne' h1 h2
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
⊢ ∃ 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
⊢ ∃ l, prime_factorization n l
Tactic:
obtain (p : Nat) (h4 : prime_factor p n ∧ ∀ (q : Nat),
  prime_factor q n → p ≤ q) from exists_least_prime_factor h3
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
⊢ ∃ 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
⊢ ∃ l, prime_factorization n l
Tactic:
have p_prime_factor : prime_factor p n := h4.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_factor p n
⊢ ∃ 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_factor p n
⊢ ∃ l, prime_factorization n l
Tactic:
define at p_prime_factor
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
⊢ ∃ 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
⊢ ∃ l, prime_factorization n l
Tactic:
have p_prime : prime p := p_prime_factor.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
⊢ ∃ 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
⊢ ∃ l, prime_factorization n l
Tactic:
have p_dvd_n : p ∣ n := p_prime_factor.right
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
⊢ ∃ 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
⊢ ∃ l, prime_factorization n l
Tactic:
have p_least : ∀ (q : Nat), prime_factor q n → p ≤ q := h4.right
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
⊢ ∃ 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
⊢ ∃ l, prime_factorization n l
Tactic:
obtain (m : Nat) (n_eq_pm : n = p * m) from p_dvd_n
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
⊢ ∃ 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
⊢ ∃ l, prime_factorization n l
Tactic:
have h5 : m ≠ 0 := by
  contradict h1 with h6
  have h7 : n = 0 :=
    calc n
      _ = p * m := n_eq_pm
      _ = p * 0 := by rw [h6]
      _ = 0 := by ring
  rewrite [h7]
  decide
  done
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
⊢ ∃ 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
⊢ ∃ l, prime_factorization n l
Tactic:
have m_pos : 0 < m := Nat.pos_of_ne_zero h5
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
⊢ ∃ 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
⊢ ∃ l, prime_factorization n l
Tactic:
have m_lt_n : m < n := by
  define at p_prime
  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
  done
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, 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, prime_factorization n l
Tactic:
obtain (L : List Nat) (h6 : prime_factorization m L)
  from ih m m_lt_n m_pos
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 : prime_factorization m L
⊢ ∃ l, prime_factorization n l