internlm/Lean-Github huggingface dataset:
Theorem: HTPI.Theorem_7_2_4
Proof state before:
case nil
p : ℕ
h1 : prime p
⊢ p ∣ prod [] → ∃ a ∈ [], p ∣ a
Tactic:
rewrite [prod_nil]
Proof state after:
case nil
p : ℕ
h1 : prime p
⊢ p ∣ 1 → ∃ a ∈ [], p ∣ a
Theorem: HTPI.Theorem_7_2_4
Proof state before:
case nil
p : ℕ
h1 : prime p
⊢ p ∣ 1 → ∃ a ∈ [], p ∣ a
Tactic:
assume h2 : p ∣ 1
Proof state after:
case nil
p : ℕ
h1 : prime p
h2 : p ∣ 1
⊢ ∃ a ∈ [], p ∣ a
Theorem: HTPI.Theorem_7_2_4
Proof state before:
case nil
p : ℕ
h1 : prime p
h2 : p ∣ 1
⊢ ∃ a ∈ [], p ∣ a
Tactic:
show ∃ a ∈ [], p ∣ a from
  absurd (eq_one_of_dvd_one h2) (prime_not_one h1)
Proof state after:
no goals
Theorem: HTPI.Theorem_7_2_4
Proof state before:
case cons
p : ℕ
h1 : prime p
⊢ ∀ (head : ℕ) (tail : List ℕ),
    (p ∣ prod tail → ∃ a ∈ tail, p ∣ a) → p ∣ prod (head :: tail) → ∃ a ∈ head :: tail, p ∣ a
Tactic:
fix b : Nat
Proof state after:
case cons
p : ℕ
h1 : prime p
b : ℕ
⊢ ∀ (tail : List ℕ), (p ∣ prod tail → ∃ a ∈ tail, p ∣ a) → p ∣ prod (b :: tail) → ∃ a ∈ b :: tail, p ∣ a
Theorem: HTPI.Theorem_7_2_4
Proof state before:
case cons
p : ℕ
h1 : prime p
b : ℕ
⊢ ∀ (tail : List ℕ), (p ∣ prod tail → ∃ a ∈ tail, p ∣ a) → p ∣ prod (b :: tail) → ∃ a ∈ b :: tail, p ∣ a
Tactic:
fix L : List Nat
Proof state after:
case cons
p : ℕ
h1 : prime p
b : ℕ
L : List ℕ
⊢ (p ∣ prod L → ∃ a ∈ L, p ∣ a) → p ∣ prod (b :: L) → ∃ a ∈ b :: L, p ∣ a
Theorem: HTPI.Theorem_7_2_4
Proof state before:
case cons
p : ℕ
h1 : prime p
b : ℕ
L : List ℕ
⊢ (p ∣ prod L → ∃ a ∈ L, p ∣ a) → p ∣ prod (b :: L) → ∃ a ∈ b :: L, p ∣ a
Tactic:
assume ih : p ∣ prod L → ∃ a ∈ L, p ∣ a
Proof state after:
case cons
p : ℕ
h1 : prime p
b : ℕ
L : List ℕ
ih : p ∣ prod L → ∃ a ∈ L, p ∣ a
⊢ p ∣ prod (b :: L) → ∃ a ∈ b :: L, p ∣ a
Theorem: HTPI.Theorem_7_2_4
Proof state before:
case cons
p : ℕ
h1 : prime p
b : ℕ
L : List ℕ
ih : p ∣ prod L → ∃ a ∈ L, p ∣ a
⊢ p ∣ prod (b :: L) → ∃ a ∈ b :: L, p ∣ a
Tactic:
assume h2 : p ∣ prod (b :: L)
Proof state after:
case cons
p : ℕ
h1 : prime p
b : ℕ
L : List ℕ
ih : p ∣ prod L → ∃ a ∈ L, p ∣ a
h2 : p ∣ prod (b :: L)
⊢ ∃ a ∈ b :: L, p ∣ a
Theorem: HTPI.Theorem_7_2_4
Proof state before:
case cons
p : ℕ
h1 : prime p
b : ℕ
L : List ℕ
ih : p ∣ prod L → ∃ a ∈ L, p ∣ a
h2 : p ∣ prod (b :: L)
⊢ ∃ a ∈ b :: L, p ∣ a
Tactic:
rewrite [prod_cons] at h2
Proof state after:
case cons
p : ℕ
h1 : prime p
b : ℕ
L : List ℕ
ih : p ∣ prod L → ∃ a ∈ L, p ∣ a
h2 : p ∣ b * prod L
⊢ ∃ a ∈ b :: L, p ∣ a
Theorem: HTPI.Theorem_7_2_4
Proof state before:
case cons
p : ℕ
h1 : prime p
b : ℕ
L : List ℕ
ih : p ∣ prod L → ∃ a ∈ L, p ∣ a
h2 : p ∣ b * prod L
⊢ ∃ a ∈ b :: L, p ∣ a
Tactic:
have h3 : p ∣ b ∨ p ∣ prod L := Theorem_7_2_3 h1 h2
Proof state after:
case cons
p : ℕ
h1 : prime p
b : ℕ
L : List ℕ
ih : p ∣ prod L → ∃ a ∈ L, p ∣ a
h2 : p ∣ b * prod L
h3 : p ∣ b ∨ p ∣ prod L
⊢ ∃ a ∈ b :: L, p ∣ a
Theorem: HTPI.Theorem_7_2_4
Proof state before:
case cons
p : ℕ
h1 : prime p
b : ℕ
L : List ℕ
ih : p ∣ prod L → ∃ a ∈ L, p ∣ a
h2 : p ∣ b * prod L
h3 : p ∣ b ∨ p ∣ prod L
⊢ ∃ a ∈ b :: L, p ∣ a
Tactic:
by_cases on h3
Proof state after:
case cons.Case_1
p : ℕ
h1 : prime p
b : ℕ
L : List ℕ
ih : p ∣ prod L → ∃ a ∈ L, p ∣ a
h2 : p ∣ b * prod L
h3 : p ∣ b
⊢ ∃ a ∈ b :: L, p ∣ a

case cons.Case_2
p : ℕ
h1 : prime p
b : ℕ
L : List ℕ
ih : p ∣ prod L → ∃ a ∈ L, p ∣ a
h2 : p ∣ b * prod L
h3 : p ∣ prod L
⊢ ∃ a ∈ b :: L, p ∣ a
Theorem: HTPI.Theorem_7_2_4
Proof state before:
case cons.Case_1
p : ℕ
h1 : prime p
b : ℕ
L : List ℕ
ih : p ∣ prod L → ∃ a ∈ L, p ∣ a
h2 : p ∣ b * prod L
h3 : p ∣ b
⊢ ∃ a ∈ b :: L, p ∣ a
Tactic:
apply Exists.intro b
Proof state after:
case cons.Case_1
p : ℕ
h1 : prime p
b : ℕ
L : List ℕ
ih : p ∣ prod L → ∃ a ∈ L, p ∣ a
h2 : p ∣ b * prod L
h3 : p ∣ b
⊢ b ∈ b :: L ∧ p ∣ b
Theorem: HTPI.Theorem_7_2_4
Proof state before:
case cons.Case_1
p : ℕ
h1 : prime p
b : ℕ
L : List ℕ
ih : p ∣ prod L → ∃ a ∈ L, p ∣ a
h2 : p ∣ b * prod L
h3 : p ∣ b
⊢ b ∈ b :: L ∧ p ∣ b
Tactic:
show b ∈ b :: L ∧ p ∣ b from
  And.intro (List.mem_cons_self b L) h3
Proof state after:
no goals
Theorem: HTPI.Theorem_7_2_4
Proof state before:
case cons.Case_2
p : ℕ
h1 : prime p
b : ℕ
L : List ℕ
ih : p ∣ prod L → ∃ a ∈ L, p ∣ a
h2 : p ∣ b * prod L
h3 : p ∣ prod L
⊢ ∃ a ∈ b :: L, p ∣ a
Tactic:
obtain (a : Nat) (h4 : a ∈ L ∧ p ∣ a) from ih h3
Proof state after:
case cons.Case_2
p : ℕ
h1 : prime p
b : ℕ
L : List ℕ
ih : p ∣ prod L → ∃ a ∈ L, p ∣ a
h2 : p ∣ b * prod L
h3 : p ∣ prod L
a : ℕ
h4 : a ∈ L ∧ p ∣ a
⊢ ∃ a ∈ b :: L, p ∣ a
Theorem: HTPI.Theorem_7_2_4
Proof state before:
case cons.Case_2
p : ℕ
h1 : prime p
b : ℕ
L : List ℕ
ih : p ∣ prod L → ∃ a ∈ L, p ∣ a
h2 : p ∣ b * prod L
h3 : p ∣ prod L
a : ℕ
h4 : a ∈ L ∧ p ∣ a
⊢ ∃ a ∈ b :: L, p ∣ a
Tactic:
apply Exists.intro a
Proof state after:
case cons.Case_2
p : ℕ
h1 : prime p
b : ℕ
L : List ℕ
ih : p ∣ prod L → ∃ a ∈ L, p ∣ a
h2 : p ∣ b * prod L
h3 : p ∣ prod L
a : ℕ
h4 : a ∈ L ∧ p ∣ a
⊢ a ∈ b :: L ∧ p ∣ a
Theorem: HTPI.Theorem_7_2_4
Proof state before:
case cons.Case_2
p : ℕ
h1 : prime p
b : ℕ
L : List ℕ
ih : p ∣ prod L → ∃ a ∈ L, p ∣ a
h2 : p ∣ b * prod L
h3 : p ∣ prod L
a : ℕ
h4 : a ∈ L ∧ p ∣ a
⊢ a ∈ b :: L ∧ p ∣ a
Tactic:
show a ∈ b :: L ∧ p ∣ a from
  And.intro (List.mem_cons_of_mem b h4.left) h4.right
Proof state after:
no goals
Theorem: HTPI.prime_in_list
Proof state before:
p : ℕ
l : List ℕ
h1 : prime p
h2 : all_prime l
h3 : p ∣ prod l
⊢ p ∈ l
Tactic:
obtain (a : Nat) (h4 : a ∈ l ∧ p ∣ a) from Theorem_7_2_4 h1 l h3
Proof state after:
p : ℕ
l : List ℕ
h1 : prime p
h2 : all_prime l
h3 : p ∣ prod l
a : ℕ
h4 : a ∈ l ∧ p ∣ a
⊢ p ∈ l
Theorem: HTPI.prime_in_list
Proof state before:
p : ℕ
l : List ℕ
h1 : prime p
h2 : all_prime l
h3 : p ∣ prod l
a : ℕ
h4 : a ∈ l ∧ p ∣ a
⊢ p ∈ l
Tactic:
define at h2
Proof state after:
p : ℕ
l : List ℕ
h1 : prime p
h2 : ∀ p ∈ l, prime p
h3 : p ∣ prod l
a : ℕ
h4 : a ∈ l ∧ p ∣ a
⊢ p ∈ l
Theorem: HTPI.prime_in_list
Proof state before:
p : ℕ
l : List ℕ
h1 : prime p
h2 : ∀ p ∈ l, prime p
h3 : p ∣ prod l
a : ℕ
h4 : a ∈ l ∧ p ∣ a
⊢ p ∈ l
Tactic:
have h5 : prime a := h2 a h4.left
Proof state after:
p : ℕ
l : List ℕ
h1 : prime p
h2 : ∀ p ∈ l, prime p
h3 : p ∣ prod l
a : ℕ
h4 : a ∈ l ∧ p ∣ a
h5 : prime a
⊢ p ∈ l
Theorem: HTPI.prime_in_list
Proof state before:
p : ℕ
l : List ℕ
h1 : prime p
h2 : ∀ p ∈ l, prime p
h3 : p ∣ prod l
a : ℕ
h4 : a ∈ l ∧ p ∣ a
h5 : prime a
⊢ p ∈ l
Tactic:
have h6 : p = 1 ∨ p = a := dvd_prime h5 h4.right
Proof state after:
p : ℕ
l : List ℕ
h1 : prime p
h2 : ∀ p ∈ l, prime p
h3 : p ∣ prod l
a : ℕ
h4 : a ∈ l ∧ p ∣ a
h5 : prime a
h6 : p = 1 ∨ p = a
⊢ p ∈ l
Theorem: HTPI.prime_in_list
Proof state before:
p : ℕ
l : List ℕ
h1 : prime p
h2 : ∀ p ∈ l, prime p
h3 : p ∣ prod l
a : ℕ
h4 : a ∈ l ∧ p ∣ a
h5 : prime a
h6 : p = 1 ∨ p = a
⊢ p ∈ l
Tactic:
disj_syll h6 (prime_not_one h1)
Proof state after:
p : ℕ
l : List ℕ
h1 : prime p
h2 : ∀ p ∈ l, prime p
h3 : p ∣ prod l
a : ℕ
h4 : a ∈ l ∧ p ∣ a
h5 : prime a
h6 : p = a
⊢ p ∈ l
Theorem: HTPI.prime_in_list
Proof state before:
p : ℕ
l : List ℕ
h1 : prime p
h2 : ∀ p ∈ l, prime p
h3 : p ∣ prod l
a : ℕ
h4 : a ∈ l ∧ p ∣ a
h5 : prime a
h6 : p = a
⊢ p ∈ l
Tactic:
rewrite [h6]
Proof state after:
p : ℕ
l : List ℕ
h1 : prime p
h2 : ∀ p ∈ l, prime p
h3 : p ∣ prod l
a : ℕ
h4 : a ∈ l ∧ p ∣ a
h5 : prime a
h6 : p = a
⊢ a ∈ l
Theorem: HTPI.prime_in_list
Proof state before:
p : ℕ
l : List ℕ
h1 : prime p
h2 : ∀ p ∈ l, prime p
h3 : p ∣ prod l
a : ℕ
h4 : a ∈ l ∧ p ∣ a
h5 : prime a
h6 : p = a
⊢ a ∈ l
Tactic:
show a ∈ l from h4.left
Proof state after:
no goals
Theorem: HTPI.first_le_first
Proof state before:
p q : ℕ
l m : List ℕ
h1 : nondec_prime_list (p :: l)
h2 : nondec_prime_list (q :: m)
h3 : prod (p :: l) = prod (q :: m)
⊢ p ≤ q
Tactic:
define at h1
Proof state after:
p q : ℕ
l m : List ℕ
h1 : all_prime (p :: l) ∧ nondec (p :: l)
h2 : nondec_prime_list (q :: m)
h3 : prod (p :: l) = prod (q :: m)
⊢ p ≤ q
Theorem: HTPI.first_le_first
Proof state before:
p q : ℕ
l m : List ℕ
h1 : all_prime (p :: l) ∧ nondec (p :: l)
h2 : nondec_prime_list (q :: m)
h3 : prod (p :: l) = prod (q :: m)
⊢ p ≤ q
Tactic:
define at h2
Proof state after:
p q : ℕ
l m : List ℕ
h1 : all_prime (p :: l) ∧ nondec (p :: l)
h2 : all_prime (q :: m) ∧ nondec (q :: m)
h3 : prod (p :: l) = prod (q :: m)
⊢ p ≤ q
Theorem: HTPI.first_le_first
Proof state before:
p q : ℕ
l m : List ℕ
h1 : all_prime (p :: l) ∧ nondec (p :: l)
h2 : all_prime (q :: m) ∧ nondec (q :: m)
h3 : prod (p :: l) = prod (q :: m)
⊢ p ≤ q
Tactic:
have h4 : q ∣ prod (p :: l) := by
  define
  apply Exists.intro (prod m)
  rewrite [←prod_cons]
  show prod (p :: l) = prod (q :: m) from h3
  done
Proof state after:
p q : ℕ
l m : List ℕ
h1 : all_prime (p :: l) ∧ nondec (p :: l)
h2 : all_prime (q :: m) ∧ nondec (q :: m)
h3 : prod (p :: l) = prod (q :: m)
h4 : q ∣ prod (p :: l)
⊢ p ≤ q
Theorem: HTPI.first_le_first
Proof state before:
p q : ℕ
l m : List ℕ
h1 : all_prime (p :: l) ∧ nondec (p :: l)
h2 : all_prime (q :: m) ∧ nondec (q :: m)
h3 : prod (p :: l) = prod (q :: m)
h4 : q ∣ prod (p :: l)
⊢ p ≤ q
Tactic:
have h5 : all_prime (q :: m) := h2.left
Proof state after:
p q : ℕ
l m : List ℕ
h1 : all_prime (p :: l) ∧ nondec (p :: l)
h2 : all_prime (q :: m) ∧ nondec (q :: m)
h3 : prod (p :: l) = prod (q :: m)
h4 : q ∣ prod (p :: l)
h5 : all_prime (q :: m)
⊢ p ≤ q
Theorem: HTPI.first_le_first
Proof state before:
p q : ℕ
l m : List ℕ
h1 : all_prime (p :: l) ∧ nondec (p :: l)
h2 : all_prime (q :: m) ∧ nondec (q :: m)
h3 : prod (p :: l) = prod (q :: m)
h4 : q ∣ prod (p :: l)
h5 : all_prime (q :: m)
⊢ p ≤ q
Tactic:
rewrite [all_prime_cons] at h5
Proof state after:
p q : ℕ
l m : List ℕ
h1 : all_prime (p :: l) ∧ nondec (p :: l)
h2 : all_prime (q :: m) ∧ nondec (q :: m)
h3 : prod (p :: l) = prod (q :: m)
h4 : q ∣ prod (p :: l)
h5 : prime q ∧ all_prime m
⊢ p ≤ q
Theorem: HTPI.first_le_first
Proof state before:
p q : ℕ
l m : List ℕ
h1 : all_prime (p :: l) ∧ nondec (p :: l)
h2 : all_prime (q :: m) ∧ nondec (q :: m)
h3 : prod (p :: l) = prod (q :: m)
h4 : q ∣ prod (p :: l)
h5 : prime q ∧ all_prime m
⊢ p ≤ q
Tactic:
have h6 : q ∈ p :: l := prime_in_list h5.left h1.left h4
Proof state after:
p q : ℕ
l m : List ℕ
h1 : all_prime (p :: l) ∧ nondec (p :: l)
h2 : all_prime (q :: m) ∧ nondec (q :: m)
h3 : prod (p :: l) = prod (q :: m)
h4 : q ∣ prod (p :: l)
h5 : prime q ∧ all_prime m
h6 : q ∈ p :: l
⊢ p ≤ q
Theorem: HTPI.first_le_first
Proof state before:
p q : ℕ
l m : List ℕ
h1 : all_prime (p :: l) ∧ nondec (p :: l)
h2 : all_prime (q :: m) ∧ nondec (q :: m)
h3 : prod (p :: l) = prod (q :: m)
h4 : q ∣ prod (p :: l)
h5 : prime q ∧ all_prime m
h6 : q ∈ p :: l
⊢ p ≤ q
Tactic:
have h7 : nondec (p :: l) := h1.right
Proof state after:
p q : ℕ
l m : List ℕ
h1 : all_prime (p :: l) ∧ nondec (p :: l)
h2 : all_prime (q :: m) ∧ nondec (q :: m)
h3 : prod (p :: l) = prod (q :: m)
h4 : q ∣ prod (p :: l)
h5 : prime q ∧ all_prime m
h6 : q ∈ p :: l
h7 : nondec (p :: l)
⊢ p ≤ q
Theorem: HTPI.first_le_first
Proof state before:
p q : ℕ
l m : List ℕ
h1 : all_prime (p :: l) ∧ nondec (p :: l)
h2 : all_prime (q :: m) ∧ nondec (q :: m)
h3 : prod (p :: l) = prod (q :: m)
h4 : q ∣ prod (p :: l)
h5 : prime q ∧ all_prime m
h6 : q ∈ p :: l
h7 : nondec (p :: l)
⊢ p ≤ q
Tactic:
rewrite [nondec_cons] at h7
Proof state after:
p q : ℕ
l m : List ℕ
h1 : all_prime (p :: l) ∧ nondec (p :: l)
h2 : all_prime (q :: m) ∧ nondec (q :: m)
h3 : prod (p :: l) = prod (q :: m)
h4 : q ∣ prod (p :: l)
h5 : prime q ∧ all_prime m
h6 : q ∈ p :: l
h7 : (∀ m ∈ l, p ≤ m) ∧ nondec l
⊢ p ≤ q
Theorem: HTPI.first_le_first
Proof state before:
p q : ℕ
l m : List ℕ
h1 : all_prime (p :: l) ∧ nondec (p :: l)
h2 : all_prime (q :: m) ∧ nondec (q :: m)
h3 : prod (p :: l) = prod (q :: m)
h4 : q ∣ prod (p :: l)
h5 : prime q ∧ all_prime m
h6 : q ∈ p :: l
h7 : (∀ m ∈ l, p ≤ m) ∧ nondec l
⊢ p ≤ q
Tactic:
rewrite [List.mem_cons] at h6
Proof state after:
p q : ℕ
l m : List ℕ
h1 : all_prime (p :: l) ∧ nondec (p :: l)
h2 : all_prime (q :: m) ∧ nondec (q :: m)
h3 : prod (p :: l) = prod (q :: m)
h4 : q ∣ prod (p :: l)
h5 : prime q ∧ all_prime m
h6 : q = p ∨ q ∈ l
h7 : (∀ m ∈ l, p ≤ m) ∧ nondec l
⊢ p ≤ q
Theorem: HTPI.first_le_first
Proof state before:
p q : ℕ
l m : List ℕ
h1 : all_prime (p :: l) ∧ nondec (p :: l)
h2 : all_prime (q :: m) ∧ nondec (q :: m)
h3 : prod (p :: l) = prod (q :: m)
h4 : q ∣ prod (p :: l)
h5 : prime q ∧ all_prime m
h6 : q = p ∨ q ∈ l
h7 : (∀ m ∈ l, p ≤ m) ∧ nondec l
⊢ p ≤ q
Tactic:
by_cases on h6
Proof state after:
case Case_1
p q : ℕ
l m : List ℕ
h1 : all_prime (p :: l) ∧ nondec (p :: l)
h2 : all_prime (q :: m) ∧ nondec (q :: m)
h3 : prod (p :: l) = prod (q :: m)
h4 : q ∣ prod (p :: l)
h5 : prime q ∧ all_prime m
h7 : (∀ m ∈ l, p ≤ m) ∧ nondec l
h6 : q = p
⊢ p ≤ q

case Case_2
p q : ℕ
l m : List ℕ
h1 : all_prime (p :: l) ∧ nondec (p :: l)
h2 : all_prime (q :: m) ∧ nondec (q :: m)
h3 : prod (p :: l) = prod (q :: m)
h4 : q ∣ prod (p :: l)
h5 : prime q ∧ all_prime m
h7 : (∀ m ∈ l, p ≤ m) ∧ nondec l
h6 : q ∈ l
⊢ p ≤ q
Theorem: HTPI.first_le_first
Proof state before:
p q : ℕ
l m : List ℕ
h1 : all_prime (p :: l) ∧ nondec (p :: l)
h2 : all_prime (q :: m) ∧ nondec (q :: m)
h3 : prod (p :: l) = prod (q :: m)
⊢ q ∣ prod (p :: l)
Tactic:
define
Proof state after:
p q : ℕ
l m : List ℕ
h1 : all_prime (p :: l) ∧ nondec (p :: l)
h2 : all_prime (q :: m) ∧ nondec (q :: m)
h3 : prod (p :: l) = prod (q :: m)
⊢ ∃ c, prod (p :: l) = q * c
Theorem: HTPI.first_le_first
Proof state before:
p q : ℕ
l m : List ℕ
h1 : all_prime (p :: l) ∧ nondec (p :: l)
h2 : all_prime (q :: m) ∧ nondec (q :: m)
h3 : prod (p :: l) = prod (q :: m)
⊢ ∃ c, prod (p :: l) = q * c
Tactic:
apply Exists.intro (prod m)
Proof state after:
p q : ℕ
l m : List ℕ
h1 : all_prime (p :: l) ∧ nondec (p :: l)
h2 : all_prime (q :: m) ∧ nondec (q :: m)
h3 : prod (p :: l) = prod (q :: m)
⊢ prod (p :: l) = q * prod m
Theorem: HTPI.first_le_first
Proof state before:
p q : ℕ
l m : List ℕ
h1 : all_prime (p :: l) ∧ nondec (p :: l)
h2 : all_prime (q :: m) ∧ nondec (q :: m)
h3 : prod (p :: l) = prod (q :: m)
⊢ prod (p :: l) = q * prod m
Tactic:
rewrite [←prod_cons]
Proof state after:
p q : ℕ
l m : List ℕ
h1 : all_prime (p :: l) ∧ nondec (p :: l)
h2 : all_prime (q :: m) ∧ nondec (q :: m)
h3 : prod (p :: l) = prod (q :: m)
⊢ prod (p :: l) = prod (q :: m)
Theorem: HTPI.first_le_first
Proof state before:
p q : ℕ
l m : List ℕ
h1 : all_prime (p :: l) ∧ nondec (p :: l)
h2 : all_prime (q :: m) ∧ nondec (q :: m)
h3 : prod (p :: l) = prod (q :: m)
⊢ prod (p :: l) = prod (q :: m)
Tactic:
show prod (p :: l) = prod (q :: m) from h3
Proof state after:
no goals
Theorem: HTPI.first_le_first
Proof state before:
case Case_1
p q : ℕ
l m : List ℕ
h1 : all_prime (p :: l) ∧ nondec (p :: l)
h2 : all_prime (q :: m) ∧ nondec (q :: m)
h3 : prod (p :: l) = prod (q :: m)
h4 : q ∣ prod (p :: l)
h5 : prime q ∧ all_prime m
h7 : (∀ m ∈ l, p ≤ m) ∧ nondec l
h6 : q = p
⊢ p ≤ q
Tactic:
linarith
Proof state after:
no goals
Theorem: HTPI.first_le_first
Proof state before:
case Case_2
p q : ℕ
l m : List ℕ
h1 : all_prime (p :: l) ∧ nondec (p :: l)
h2 : all_prime (q :: m) ∧ nondec (q :: m)
h3 : prod (p :: l) = prod (q :: m)
h4 : q ∣ prod (p :: l)
h5 : prime q ∧ all_prime m
h7 : (∀ m ∈ l, p ≤ m) ∧ nondec l
h6 : q ∈ l
⊢ p ≤ q
Tactic:
have h8 : ∀ m ∈ l, p ≤ m := h7.left
Proof state after:
case Case_2
p q : ℕ
l m : List ℕ
h1 : all_prime (p :: l) ∧ nondec (p :: l)
h2 : all_prime (q :: m) ∧ nondec (q :: m)
h3 : prod (p :: l) = prod (q :: m)
h4 : q ∣ prod (p :: l)
h5 : prime q ∧ all_prime m
h7 : (∀ m ∈ l, p ≤ m) ∧ nondec l
h6 : q ∈ l
h8 : ∀ m ∈ l, p ≤ m
⊢ p ≤ q
Theorem: HTPI.first_le_first
Proof state before:
case Case_2
p q : ℕ
l m : List ℕ
h1 : all_prime (p :: l) ∧ nondec (p :: l)
h2 : all_prime (q :: m) ∧ nondec (q :: m)
h3 : prod (p :: l) = prod (q :: m)
h4 : q ∣ prod (p :: l)
h5 : prime q ∧ all_prime m
h7 : (∀ m ∈ l, p ≤ m) ∧ nondec l
h6 : q ∈ l
h8 : ∀ m ∈ l, p ≤ m
⊢ p ≤ q
Tactic:
show p ≤ q from h8 q h6
Proof state after:
no goals
Theorem: HTPI.nondec_prime_list_tail
Proof state before:
p : ℕ
l : List ℕ
h : nondec_prime_list (p :: l)
⊢ nondec_prime_list l
Tactic:
define at h
Proof state after:
p : ℕ
l : List ℕ
h : all_prime (p :: l) ∧ nondec (p :: l)
⊢ nondec_prime_list l
Theorem: HTPI.nondec_prime_list_tail
Proof state before:
p : ℕ
l : List ℕ
h : all_prime (p :: l) ∧ nondec (p :: l)
⊢ nondec_prime_list l
Tactic:
define
Proof state after:
p : ℕ
l : List ℕ
h : all_prime (p :: l) ∧ nondec (p :: l)
⊢ all_prime l ∧ nondec l
Theorem: HTPI.nondec_prime_list_tail
Proof state before:
p : ℕ
l : List ℕ
h : all_prime (p :: l) ∧ nondec (p :: l)
⊢ all_prime l ∧ nondec l
Tactic:
rewrite [all_prime_cons, nondec_cons] at h
Proof state after:
p : ℕ
l : List ℕ
h : (prime p ∧ all_prime l) ∧ (∀ m ∈ l, p ≤ m) ∧ nondec l
⊢ all_prime l ∧ nondec l
Theorem: HTPI.nondec_prime_list_tail
Proof state before:
p : ℕ
l : List ℕ
h : (prime p ∧ all_prime l) ∧ (∀ m ∈ l, p ≤ m) ∧ nondec l
⊢ all_prime l ∧ nondec l
Tactic:
show all_prime l ∧ nondec l from And.intro h.left.right h.right.right
Proof state after:
no goals
Theorem: HTPI.cons_prod_not_one
Proof state before:
p : ℕ
l : List ℕ
h : nondec_prime_list (p :: l)
⊢ prod (p :: l) ≠ 1
Tactic:
define at h
Proof state after:
p : ℕ
l : List ℕ
h : all_prime (p :: l) ∧ nondec (p :: l)
⊢ prod (p :: l) ≠ 1
Theorem: HTPI.cons_prod_not_one
Proof state before:
p : ℕ
l : List ℕ
h : all_prime (p :: l) ∧ nondec (p :: l)
⊢ prod (p :: l) ≠ 1
Tactic:
have h1 : all_prime (p :: l) := h.left
Proof state after:
p : ℕ
l : List ℕ
h : all_prime (p :: l) ∧ nondec (p :: l)
h1 : all_prime (p :: l)
⊢ prod (p :: l) ≠ 1
Theorem: HTPI.cons_prod_not_one
Proof state before:
p : ℕ
l : List ℕ
h : all_prime (p :: l) ∧ nondec (p :: l)
h1 : all_prime (p :: l)
⊢ prod (p :: l) ≠ 1
Tactic:
rewrite [all_prime_cons] at h1
Proof state after:
p : ℕ
l : List ℕ
h : all_prime (p :: l) ∧ nondec (p :: l)
h1 : prime p ∧ all_prime l
⊢ prod (p :: l) ≠ 1
Theorem: HTPI.cons_prod_not_one
Proof state before:
p : ℕ
l : List ℕ
h : all_prime (p :: l) ∧ nondec (p :: l)
h1 : prime p ∧ all_prime l
⊢ prod (p :: l) ≠ 1
Tactic:
rewrite [prod_cons]
Proof state after:
p : ℕ
l : List ℕ
h : all_prime (p :: l) ∧ nondec (p :: l)
h1 : prime p ∧ all_prime l
⊢ p * prod l ≠ 1
Theorem: HTPI.cons_prod_not_one
Proof state before:
p : ℕ
l : List ℕ
h : all_prime (p :: l) ∧ nondec (p :: l)
h1 : prime p ∧ all_prime l
⊢ p * prod l ≠ 1
Tactic:
by_contra h2
Proof state after:
p : ℕ
l : List ℕ
h : all_prime (p :: l) ∧ nondec (p :: l)
h1 : prime p ∧ all_prime l
h2 : p * prod l = 1
⊢ False
Theorem: HTPI.cons_prod_not_one
Proof state before:
p : ℕ
l : List ℕ
h : all_prime (p :: l) ∧ nondec (p :: l)
h1 : prime p ∧ all_prime l
h2 : p * prod l = 1
⊢ False
Tactic:
show False from (prime_not_one h1.left) (eq_one_of_prod_one h2)
Proof state after:
no goals
Theorem: HTPI.list_nil_iff_prod_one
Proof state before:
l : List ℕ
h : nondec_prime_list l
⊢ l = [] ↔ prod l = 1
Tactic:
apply Iff.intro
Proof state after:
case mp
l : List ℕ
h : nondec_prime_list l
⊢ l = [] → prod l = 1

case mpr
l : List ℕ
h : nondec_prime_list l
⊢ prod l = 1 → l = []
Theorem: HTPI.list_nil_iff_prod_one
Proof state before:
case mp
l : List ℕ
h : nondec_prime_list l
⊢ l = [] → prod l = 1
Tactic:
assume h1 : l = []
Proof state after:
case mp
l : List ℕ
h : nondec_prime_list l
h1 : l = []
⊢ prod l = 1
Theorem: HTPI.list_nil_iff_prod_one
Proof state before:
case mp
l : List ℕ
h : nondec_prime_list l
h1 : l = []
⊢ prod l = 1
Tactic:
rewrite [h1]
Proof state after:
case mp
l : List ℕ
h : nondec_prime_list l
h1 : l = []
⊢ prod [] = 1
Theorem: HTPI.list_nil_iff_prod_one
Proof state before:
case mp
l : List ℕ
h : nondec_prime_list l
h1 : l = []
⊢ prod [] = 1
Tactic:
show prod [] = 1 from prod_nil
Proof state after:
no goals
Theorem: HTPI.list_nil_iff_prod_one
Proof state before:
case mpr
l : List ℕ
h : nondec_prime_list l
⊢ prod l = 1 → l = []
Tactic:
contrapos
Proof state after:
case mpr
l : List ℕ
h : nondec_prime_list l
⊢ ¬l = [] → ¬prod l = 1
Theorem: HTPI.list_nil_iff_prod_one
Proof state before:
case mpr
l : List ℕ
h : nondec_prime_list l
⊢ ¬l = [] → ¬prod l = 1
Tactic:
assume h1 : ¬l = []
Proof state after:
case mpr
l : List ℕ
h : nondec_prime_list l
h1 : ¬l = []
⊢ ¬prod l = 1
Theorem: HTPI.list_nil_iff_prod_one
Proof state before:
case mpr
l : List ℕ
h : nondec_prime_list l
h1 : ¬l = []
⊢ ¬prod l = 1
Tactic:
obtain (p : Nat) (h2 : ∃ (L : List Nat), l = p :: L) from
  List.exists_cons_of_ne_nil h1
Proof state after:
case mpr
l : List ℕ
h : nondec_prime_list l
h1 : ¬l = []
p : ℕ
h2 : ∃ L, l = p :: L
⊢ ¬prod l = 1
Theorem: HTPI.list_nil_iff_prod_one
Proof state before:
case mpr
l : List ℕ
h : nondec_prime_list l
h1 : ¬l = []
p : ℕ
h2 : ∃ L, l = p :: L
⊢ ¬prod l = 1
Tactic:
obtain (L : List Nat) (h3 : l = p :: L) from h2
Proof state after:
case mpr
l : List ℕ
h : nondec_prime_list l
h1 : ¬l = []
p : ℕ
h2 : ∃ L, l = p :: L
L : List ℕ
h3 : l = p :: L
⊢ ¬prod l = 1
Theorem: HTPI.list_nil_iff_prod_one
Proof state before:
case mpr
l : List ℕ
h : nondec_prime_list l
h1 : ¬l = []
p : ℕ
h2 : ∃ L, l = p :: L
L : List ℕ
h3 : l = p :: L
⊢ ¬prod l = 1
Tactic:
rewrite [h3] at h
Proof state after:
case mpr
l : List ℕ
h1 : ¬l = []
p : ℕ
h2 : ∃ L, l = p :: L
L : List ℕ
h : nondec_prime_list (p :: L)
h3 : l = p :: L
⊢ ¬prod l = 1
Theorem: HTPI.list_nil_iff_prod_one
Proof state before:
case mpr
l : List ℕ
h1 : ¬l = []
p : ℕ
h2 : ∃ L, l = p :: L
L : List ℕ
h : nondec_prime_list (p :: L)
h3 : l = p :: L
⊢ ¬prod l = 1
Tactic:
rewrite [h3]
Proof state after:
case mpr
l : List ℕ
h1 : ¬l = []
p : ℕ
h2 : ∃ L, l = p :: L
L : List ℕ
h : nondec_prime_list (p :: L)
h3 : l = p :: L
⊢ ¬prod (p :: L) = 1
Theorem: HTPI.list_nil_iff_prod_one
Proof state before:
case mpr
l : List ℕ
h1 : ¬l = []
p : ℕ
h2 : ∃ L, l = p :: L
L : List ℕ
h : nondec_prime_list (p :: L)
h3 : l = p :: L
⊢ ¬prod (p :: L) = 1
Tactic:
show ¬prod (p :: L) = 1 from cons_prod_not_one h
Proof state after:
no goals
Theorem: HTPI.prime_pos
Proof state before:
p : ℕ
h : prime p
⊢ p > 0
Tactic:
define at h
Proof state after:
p : ℕ
h : 2 ≤ p ∧ ¬∃ a b, a * b = p ∧ a < p ∧ b < p
⊢ p > 0
Theorem: HTPI.prime_pos
Proof state before:
p : ℕ
h : 2 ≤ p ∧ ¬∃ a b, a * b = p ∧ a < p ∧ b < p
⊢ p > 0
Tactic:
linarith
Proof state after:
no goals
Theorem: HTPI.Theorem_7_2_5
Proof state before:
⊢ ∀ (l1 l2 : List ℕ), nondec_prime_list l1 → nondec_prime_list l2 → prod l1 = prod l2 → l1 = l2
Tactic:
apply List.rec
Proof state after:
case nil

⊢ ∀ (l2 : List ℕ), nondec_prime_list [] → nondec_prime_list l2 → prod [] = prod l2 → [] = l2

case cons

⊢ ∀ (head : ℕ) (tail : List ℕ),
    (∀ (l2 : List ℕ), nondec_prime_list tail → nondec_prime_list l2 → prod tail = prod l2 → tail = l2) →
      ∀ (l2 : List ℕ),
        nondec_prime_list (head :: tail) → nondec_prime_list l2 → prod (head :: tail) = prod l2 → head :: tail = l2
Theorem: HTPI.Theorem_7_2_5
Proof state before:
case nil

⊢ ∀ (l2 : List ℕ), nondec_prime_list [] → nondec_prime_list l2 → prod [] = prod l2 → [] = l2
Tactic:
fix l2 : List Nat
Proof state after:
case nil
l2 : List ℕ
⊢ nondec_prime_list [] → nondec_prime_list l2 → prod [] = prod l2 → [] = l2
Theorem: HTPI.Theorem_7_2_5
Proof state before:
case nil
l2 : List ℕ
⊢ nondec_prime_list [] → nondec_prime_list l2 → prod [] = prod l2 → [] = l2
Tactic:
assume h1 : nondec_prime_list []
Proof state after:
case nil
l2 : List ℕ
h1 : nondec_prime_list []
⊢ nondec_prime_list l2 → prod [] = prod l2 → [] = l2
Theorem: HTPI.Theorem_7_2_5
Proof state before:
case nil
l2 : List ℕ
h1 : nondec_prime_list []
⊢ nondec_prime_list l2 → prod [] = prod l2 → [] = l2
Tactic:
assume h2 : nondec_prime_list l2
Proof state after:
case nil
l2 : List ℕ
h1 : nondec_prime_list []
h2 : nondec_prime_list l2
⊢ prod [] = prod l2 → [] = l2
Theorem: HTPI.Theorem_7_2_5
Proof state before:
case nil
l2 : List ℕ
h1 : nondec_prime_list []
h2 : nondec_prime_list l2
⊢ prod [] = prod l2 → [] = l2
Tactic:
assume h3 : prod [] = prod l2
Proof state after:
case nil
l2 : List ℕ
h1 : nondec_prime_list []
h2 : nondec_prime_list l2
h3 : prod [] = prod l2
⊢ [] = l2
Theorem: HTPI.Theorem_7_2_5
Proof state before:
case nil
l2 : List ℕ
h1 : nondec_prime_list []
h2 : nondec_prime_list l2
h3 : prod [] = prod l2
⊢ [] = l2
Tactic:
rewrite [prod_nil, eq_comm, ←list_nil_iff_prod_one h2] at h3
Proof state after:
case nil
l2 : List ℕ
h1 : nondec_prime_list []
h2 : nondec_prime_list l2
h3 : l2 = []
⊢ [] = l2
Theorem: HTPI.Theorem_7_2_5
Proof state before:
case nil
l2 : List ℕ
h1 : nondec_prime_list []
h2 : nondec_prime_list l2
h3 : l2 = []
⊢ [] = l2
Tactic:
show [] = l2 from h3.symm
Proof state after:
no goals