internlm/Lean-Github huggingface dataset:
Theorem: HTPI.Theorem_7_2_5
Proof state before:
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
Tactic:
fix p : Nat
Proof state after:
case cons
p : ℕ
⊢ ∀ (tail : List ℕ),
    (∀ (l2 : List ℕ), nondec_prime_list tail → nondec_prime_list l2 → prod tail = prod l2 → tail = l2) →
      ∀ (l2 : List ℕ),
        nondec_prime_list (p :: tail) → nondec_prime_list l2 → prod (p :: tail) = prod l2 → p :: tail = l2
Theorem: HTPI.Theorem_7_2_5
Proof state before:
case cons
p : ℕ
⊢ ∀ (tail : List ℕ),
    (∀ (l2 : List ℕ), nondec_prime_list tail → nondec_prime_list l2 → prod tail = prod l2 → tail = l2) →
      ∀ (l2 : List ℕ),
        nondec_prime_list (p :: tail) → nondec_prime_list l2 → prod (p :: tail) = prod l2 → p :: tail = l2
Tactic:
fix L1 : List Nat
Proof state after:
case cons
p : ℕ
L1 : List ℕ
⊢ (∀ (l2 : List ℕ), nondec_prime_list L1 → nondec_prime_list l2 → prod L1 = prod l2 → L1 = l2) →
    ∀ (l2 : List ℕ), nondec_prime_list (p :: L1) → nondec_prime_list l2 → prod (p :: L1) = prod l2 → p :: L1 = l2
Theorem: HTPI.Theorem_7_2_5
Proof state before:
case cons
p : ℕ
L1 : List ℕ
⊢ (∀ (l2 : List ℕ), nondec_prime_list L1 → nondec_prime_list l2 → prod L1 = prod l2 → L1 = l2) →
    ∀ (l2 : List ℕ), nondec_prime_list (p :: L1) → nondec_prime_list l2 → prod (p :: L1) = prod l2 → p :: L1 = l2
Tactic:
assume ih : ∀ (L2 : List Nat), nondec_prime_list L1 →
  nondec_prime_list L2 → prod L1 = prod L2 → L1 = L2
Proof state after:
case cons
p : ℕ
L1 : List ℕ
ih : ∀ (l2 : List ℕ), nondec_prime_list L1 → nondec_prime_list l2 → prod L1 = prod l2 → L1 = l2
⊢ ∀ (l2 : List ℕ), nondec_prime_list (p :: L1) → nondec_prime_list l2 → prod (p :: L1) = prod l2 → p :: L1 = l2
Theorem: HTPI.Theorem_7_2_5
Proof state before:
case cons
p : ℕ
L1 : List ℕ
ih : ∀ (l2 : List ℕ), nondec_prime_list L1 → nondec_prime_list l2 → prod L1 = prod l2 → L1 = l2
⊢ ∀ (l2 : List ℕ), nondec_prime_list (p :: L1) → nondec_prime_list l2 → prod (p :: L1) = prod l2 → p :: L1 = l2
Tactic:
fix l2 : List Nat
Proof state after:
case cons
p : ℕ
L1 : List ℕ
ih : ∀ (l2 : List ℕ), nondec_prime_list L1 → nondec_prime_list l2 → prod L1 = prod l2 → L1 = l2
l2 : List ℕ
⊢ nondec_prime_list (p :: L1) → nondec_prime_list l2 → prod (p :: L1) = prod l2 → p :: L1 = l2
Theorem: HTPI.Theorem_7_2_5
Proof state before:
case cons
p : ℕ
L1 : List ℕ
ih : ∀ (l2 : List ℕ), nondec_prime_list L1 → nondec_prime_list l2 → prod L1 = prod l2 → L1 = l2
l2 : List ℕ
⊢ nondec_prime_list (p :: L1) → nondec_prime_list l2 → prod (p :: L1) = prod l2 → p :: L1 = l2
Tactic:
assume h1 : nondec_prime_list (p :: L1)
Proof state after:
case cons
p : ℕ
L1 : List ℕ
ih : ∀ (l2 : List ℕ), nondec_prime_list L1 → nondec_prime_list l2 → prod L1 = prod l2 → L1 = l2
l2 : List ℕ
h1 : nondec_prime_list (p :: L1)
⊢ nondec_prime_list l2 → prod (p :: L1) = prod l2 → p :: L1 = l2
Theorem: HTPI.Theorem_7_2_5
Proof state before:
case cons
p : ℕ
L1 : List ℕ
ih : ∀ (l2 : List ℕ), nondec_prime_list L1 → nondec_prime_list l2 → prod L1 = prod l2 → L1 = l2
l2 : List ℕ
h1 : nondec_prime_list (p :: L1)
⊢ nondec_prime_list l2 → prod (p :: L1) = prod l2 → p :: L1 = l2
Tactic:
assume h2 : nondec_prime_list l2
Proof state after:
case cons
p : ℕ
L1 : List ℕ
ih : ∀ (l2 : List ℕ), nondec_prime_list L1 → nondec_prime_list l2 → prod L1 = prod l2 → L1 = l2
l2 : List ℕ
h1 : nondec_prime_list (p :: L1)
h2 : nondec_prime_list l2
⊢ prod (p :: L1) = prod l2 → p :: L1 = l2
Theorem: HTPI.Theorem_7_2_5
Proof state before:
case cons
p : ℕ
L1 : List ℕ
ih : ∀ (l2 : List ℕ), nondec_prime_list L1 → nondec_prime_list l2 → prod L1 = prod l2 → L1 = l2
l2 : List ℕ
h1 : nondec_prime_list (p :: L1)
h2 : nondec_prime_list l2
⊢ prod (p :: L1) = prod l2 → p :: L1 = l2
Tactic:
assume h3 : prod (p :: L1) = prod l2
Proof state after:
case cons
p : ℕ
L1 : List ℕ
ih : ∀ (l2 : List ℕ), nondec_prime_list L1 → nondec_prime_list l2 → prod L1 = prod l2 → L1 = l2
l2 : List ℕ
h1 : nondec_prime_list (p :: L1)
h2 : nondec_prime_list l2
h3 : prod (p :: L1) = prod l2
⊢ p :: L1 = l2
Theorem: HTPI.Theorem_7_2_5
Proof state before:
case cons
p : ℕ
L1 : List ℕ
ih : ∀ (l2 : List ℕ), nondec_prime_list L1 → nondec_prime_list l2 → prod L1 = prod l2 → L1 = l2
l2 : List ℕ
h1 : nondec_prime_list (p :: L1)
h2 : nondec_prime_list l2
h3 : prod (p :: L1) = prod l2
⊢ p :: L1 = l2
Tactic:
have h4 : ¬prod (p :: L1) = 1 := cons_prod_not_one h1
Proof state after:
case cons
p : ℕ
L1 : List ℕ
ih : ∀ (l2 : List ℕ), nondec_prime_list L1 → nondec_prime_list l2 → prod L1 = prod l2 → L1 = l2
l2 : List ℕ
h1 : nondec_prime_list (p :: L1)
h2 : nondec_prime_list l2
h3 : prod (p :: L1) = prod l2
h4 : ¬prod (p :: L1) = 1
⊢ p :: L1 = l2
Theorem: HTPI.Theorem_7_2_5
Proof state before:
case cons
p : ℕ
L1 : List ℕ
ih : ∀ (l2 : List ℕ), nondec_prime_list L1 → nondec_prime_list l2 → prod L1 = prod l2 → L1 = l2
l2 : List ℕ
h1 : nondec_prime_list (p :: L1)
h2 : nondec_prime_list l2
h3 : prod (p :: L1) = prod l2
h4 : ¬prod (p :: L1) = 1
⊢ p :: L1 = l2
Tactic:
rewrite [h3, ←list_nil_iff_prod_one h2] at h4
Proof state after:
case cons
p : ℕ
L1 : List ℕ
ih : ∀ (l2 : List ℕ), nondec_prime_list L1 → nondec_prime_list l2 → prod L1 = prod l2 → L1 = l2
l2 : List ℕ
h1 : nondec_prime_list (p :: L1)
h2 : nondec_prime_list l2
h3 : prod (p :: L1) = prod l2
h4 : ¬l2 = []
⊢ p :: L1 = l2
Theorem: HTPI.Theorem_7_2_5
Proof state before:
case cons
p : ℕ
L1 : List ℕ
ih : ∀ (l2 : List ℕ), nondec_prime_list L1 → nondec_prime_list l2 → prod L1 = prod l2 → L1 = l2
l2 : List ℕ
h1 : nondec_prime_list (p :: L1)
h2 : nondec_prime_list l2
h3 : prod (p :: L1) = prod l2
h4 : ¬l2 = []
⊢ p :: L1 = l2
Tactic:
obtain (q : Nat) (h5 : ∃ (L : List Nat), l2 = q :: L) from
  List.exists_cons_of_ne_nil h4
Proof state after:
case cons
p : ℕ
L1 : List ℕ
ih : ∀ (l2 : List ℕ), nondec_prime_list L1 → nondec_prime_list l2 → prod L1 = prod l2 → L1 = l2
l2 : List ℕ
h1 : nondec_prime_list (p :: L1)
h2 : nondec_prime_list l2
h3 : prod (p :: L1) = prod l2
h4 : ¬l2 = []
q : ℕ
h5 : ∃ L, l2 = q :: L
⊢ p :: L1 = l2
Theorem: HTPI.Theorem_7_2_5
Proof state before:
case cons
p : ℕ
L1 : List ℕ
ih : ∀ (l2 : List ℕ), nondec_prime_list L1 → nondec_prime_list l2 → prod L1 = prod l2 → L1 = l2
l2 : List ℕ
h1 : nondec_prime_list (p :: L1)
h2 : nondec_prime_list l2
h3 : prod (p :: L1) = prod l2
h4 : ¬l2 = []
q : ℕ
h5 : ∃ L, l2 = q :: L
⊢ p :: L1 = l2
Tactic:
obtain (L2 : List Nat) (h6 : l2 = q :: L2) from h5
Proof state after:
case cons
p : ℕ
L1 : List ℕ
ih : ∀ (l2 : List ℕ), nondec_prime_list L1 → nondec_prime_list l2 → prod L1 = prod l2 → L1 = l2
l2 : List ℕ
h1 : nondec_prime_list (p :: L1)
h2 : nondec_prime_list l2
h3 : prod (p :: L1) = prod l2
h4 : ¬l2 = []
q : ℕ
h5 : ∃ L, l2 = q :: L
L2 : List ℕ
h6 : l2 = q :: L2
⊢ p :: L1 = l2
Theorem: HTPI.Theorem_7_2_5
Proof state before:
case cons
p : ℕ
L1 : List ℕ
ih : ∀ (l2 : List ℕ), nondec_prime_list L1 → nondec_prime_list l2 → prod L1 = prod l2 → L1 = l2
l2 : List ℕ
h1 : nondec_prime_list (p :: L1)
h2 : nondec_prime_list l2
h3 : prod (p :: L1) = prod l2
h4 : ¬l2 = []
q : ℕ
h5 : ∃ L, l2 = q :: L
L2 : List ℕ
h6 : l2 = q :: L2
⊢ p :: L1 = l2
Tactic:
rewrite [h6] at h2
Proof state after:
case cons
p : ℕ
L1 : List ℕ
ih : ∀ (l2 : List ℕ), nondec_prime_list L1 → nondec_prime_list l2 → prod L1 = prod l2 → L1 = l2
l2 : List ℕ
h1 : nondec_prime_list (p :: L1)
h3 : prod (p :: L1) = prod l2
h4 : ¬l2 = []
q : ℕ
h5 : ∃ L, l2 = q :: L
L2 : List ℕ
h2 : nondec_prime_list (q :: L2)
h6 : l2 = q :: L2
⊢ p :: L1 = l2
Theorem: HTPI.Theorem_7_2_5
Proof state before:
case cons
p : ℕ
L1 : List ℕ
ih : ∀ (l2 : List ℕ), nondec_prime_list L1 → nondec_prime_list l2 → prod L1 = prod l2 → L1 = l2
l2 : List ℕ
h1 : nondec_prime_list (p :: L1)
h3 : prod (p :: L1) = prod l2
h4 : ¬l2 = []
q : ℕ
h5 : ∃ L, l2 = q :: L
L2 : List ℕ
h2 : nondec_prime_list (q :: L2)
h6 : l2 = q :: L2
⊢ p :: L1 = l2
Tactic:
rewrite [h6] at h3
Proof state after:
case cons
p : ℕ
L1 : List ℕ
ih : ∀ (l2 : List ℕ), nondec_prime_list L1 → nondec_prime_list l2 → prod L1 = prod l2 → L1 = l2
l2 : List ℕ
h1 : nondec_prime_list (p :: L1)
h4 : ¬l2 = []
q : ℕ
h5 : ∃ L, l2 = q :: L
L2 : List ℕ
h3 : prod (p :: L1) = prod (q :: L2)
h2 : nondec_prime_list (q :: L2)
h6 : l2 = q :: L2
⊢ p :: L1 = l2
Theorem: HTPI.Theorem_7_2_5
Proof state before:
case cons
p : ℕ
L1 : List ℕ
ih : ∀ (l2 : List ℕ), nondec_prime_list L1 → nondec_prime_list l2 → prod L1 = prod l2 → L1 = l2
l2 : List ℕ
h1 : nondec_prime_list (p :: L1)
h4 : ¬l2 = []
q : ℕ
h5 : ∃ L, l2 = q :: L
L2 : List ℕ
h3 : prod (p :: L1) = prod (q :: L2)
h2 : nondec_prime_list (q :: L2)
h6 : l2 = q :: L2
⊢ p :: L1 = l2
Tactic:
have h7 : p ≤ q := first_le_first h1 h2 h3
Proof state after:
case cons
p : ℕ
L1 : List ℕ
ih : ∀ (l2 : List ℕ), nondec_prime_list L1 → nondec_prime_list l2 → prod L1 = prod l2 → L1 = l2
l2 : List ℕ
h1 : nondec_prime_list (p :: L1)
h4 : ¬l2 = []
q : ℕ
h5 : ∃ L, l2 = q :: L
L2 : List ℕ
h3 : prod (p :: L1) = prod (q :: L2)
h2 : nondec_prime_list (q :: L2)
h6 : l2 = q :: L2
h7 : p ≤ q
⊢ p :: L1 = l2
Theorem: HTPI.Theorem_7_2_5
Proof state before:
case cons
p : ℕ
L1 : List ℕ
ih : ∀ (l2 : List ℕ), nondec_prime_list L1 → nondec_prime_list l2 → prod L1 = prod l2 → L1 = l2
l2 : List ℕ
h1 : nondec_prime_list (p :: L1)
h4 : ¬l2 = []
q : ℕ
h5 : ∃ L, l2 = q :: L
L2 : List ℕ
h3 : prod (p :: L1) = prod (q :: L2)
h2 : nondec_prime_list (q :: L2)
h6 : l2 = q :: L2
h7 : p ≤ q
⊢ p :: L1 = l2
Tactic:
have h8 : q ≤ p := first_le_first h2 h1 h3.symm
Proof state after:
case cons
p : ℕ
L1 : List ℕ
ih : ∀ (l2 : List ℕ), nondec_prime_list L1 → nondec_prime_list l2 → prod L1 = prod l2 → L1 = l2
l2 : List ℕ
h1 : nondec_prime_list (p :: L1)
h4 : ¬l2 = []
q : ℕ
h5 : ∃ L, l2 = q :: L
L2 : List ℕ
h3 : prod (p :: L1) = prod (q :: L2)
h2 : nondec_prime_list (q :: L2)
h6 : l2 = q :: L2
h7 : p ≤ q
h8 : q ≤ p
⊢ p :: L1 = l2
Theorem: HTPI.Theorem_7_2_5
Proof state before:
case cons
p : ℕ
L1 : List ℕ
ih : ∀ (l2 : List ℕ), nondec_prime_list L1 → nondec_prime_list l2 → prod L1 = prod l2 → L1 = l2
l2 : List ℕ
h1 : nondec_prime_list (p :: L1)
h4 : ¬l2 = []
q : ℕ
h5 : ∃ L, l2 = q :: L
L2 : List ℕ
h3 : prod (p :: L1) = prod (q :: L2)
h2 : nondec_prime_list (q :: L2)
h6 : l2 = q :: L2
h7 : p ≤ q
h8 : q ≤ p
⊢ p :: L1 = l2
Tactic:
have h9 : p = q := by linarith
Proof state after:
case cons
p : ℕ
L1 : List ℕ
ih : ∀ (l2 : List ℕ), nondec_prime_list L1 → nondec_prime_list l2 → prod L1 = prod l2 → L1 = l2
l2 : List ℕ
h1 : nondec_prime_list (p :: L1)
h4 : ¬l2 = []
q : ℕ
h5 : ∃ L, l2 = q :: L
L2 : List ℕ
h3 : prod (p :: L1) = prod (q :: L2)
h2 : nondec_prime_list (q :: L2)
h6 : l2 = q :: L2
h7 : p ≤ q
h8 : q ≤ p
h9 : p = q
⊢ p :: L1 = l2
Theorem: HTPI.Theorem_7_2_5
Proof state before:
case cons
p : ℕ
L1 : List ℕ
ih : ∀ (l2 : List ℕ), nondec_prime_list L1 → nondec_prime_list l2 → prod L1 = prod l2 → L1 = l2
l2 : List ℕ
h1 : nondec_prime_list (p :: L1)
h4 : ¬l2 = []
q : ℕ
h5 : ∃ L, l2 = q :: L
L2 : List ℕ
h3 : prod (p :: L1) = prod (q :: L2)
h2 : nondec_prime_list (q :: L2)
h6 : l2 = q :: L2
h7 : p ≤ q
h8 : q ≤ p
h9 : p = q
⊢ p :: L1 = l2
Tactic:
rewrite [h9, prod_cons, prod_cons] at h3
Proof state after:
case cons
p : ℕ
L1 : List ℕ
ih : ∀ (l2 : List ℕ), nondec_prime_list L1 → nondec_prime_list l2 → prod L1 = prod l2 → L1 = l2
l2 : List ℕ
h1 : nondec_prime_list (p :: L1)
h4 : ¬l2 = []
q : ℕ
h5 : ∃ L, l2 = q :: L
L2 : List ℕ
h3 : q * prod L1 = q * prod L2
h2 : nondec_prime_list (q :: L2)
h6 : l2 = q :: L2
h7 : p ≤ q
h8 : q ≤ p
h9 : p = q
⊢ p :: L1 = l2
Theorem: HTPI.Theorem_7_2_5
Proof state before:
case cons
p : ℕ
L1 : List ℕ
ih : ∀ (l2 : List ℕ), nondec_prime_list L1 → nondec_prime_list l2 → prod L1 = prod l2 → L1 = l2
l2 : List ℕ
h1 : nondec_prime_list (p :: L1)
h4 : ¬l2 = []
q : ℕ
h5 : ∃ L, l2 = q :: L
L2 : List ℕ
h3 : q * prod L1 = q * prod L2
h2 : nondec_prime_list (q :: L2)
h6 : l2 = q :: L2
h7 : p ≤ q
h8 : q ≤ p
h9 : p = q
⊢ p :: L1 = l2
Tactic:
have h10 : nondec_prime_list L1 := nondec_prime_list_tail h1
Proof state after:
case cons
p : ℕ
L1 : List ℕ
ih : ∀ (l2 : List ℕ), nondec_prime_list L1 → nondec_prime_list l2 → prod L1 = prod l2 → L1 = l2
l2 : List ℕ
h1 : nondec_prime_list (p :: L1)
h4 : ¬l2 = []
q : ℕ
h5 : ∃ L, l2 = q :: L
L2 : List ℕ
h3 : q * prod L1 = q * prod L2
h2 : nondec_prime_list (q :: L2)
h6 : l2 = q :: L2
h7 : p ≤ q
h8 : q ≤ p
h9 : p = q
h10 : nondec_prime_list L1
⊢ p :: L1 = l2
Theorem: HTPI.Theorem_7_2_5
Proof state before:
case cons
p : ℕ
L1 : List ℕ
ih : ∀ (l2 : List ℕ), nondec_prime_list L1 → nondec_prime_list l2 → prod L1 = prod l2 → L1 = l2
l2 : List ℕ
h1 : nondec_prime_list (p :: L1)
h4 : ¬l2 = []
q : ℕ
h5 : ∃ L, l2 = q :: L
L2 : List ℕ
h3 : q * prod L1 = q * prod L2
h2 : nondec_prime_list (q :: L2)
h6 : l2 = q :: L2
h7 : p ≤ q
h8 : q ≤ p
h9 : p = q
h10 : nondec_prime_list L1
⊢ p :: L1 = l2
Tactic:
have h11 : nondec_prime_list L2 := nondec_prime_list_tail h2
Proof state after:
case cons
p : ℕ
L1 : List ℕ
ih : ∀ (l2 : List ℕ), nondec_prime_list L1 → nondec_prime_list l2 → prod L1 = prod l2 → L1 = l2
l2 : List ℕ
h1 : nondec_prime_list (p :: L1)
h4 : ¬l2 = []
q : ℕ
h5 : ∃ L, l2 = q :: L
L2 : List ℕ
h3 : q * prod L1 = q * prod L2
h2 : nondec_prime_list (q :: L2)
h6 : l2 = q :: L2
h7 : p ≤ q
h8 : q ≤ p
h9 : p = q
h10 : nondec_prime_list L1
h11 : nondec_prime_list L2
⊢ p :: L1 = l2
Theorem: HTPI.Theorem_7_2_5
Proof state before:
case cons
p : ℕ
L1 : List ℕ
ih : ∀ (l2 : List ℕ), nondec_prime_list L1 → nondec_prime_list l2 → prod L1 = prod l2 → L1 = l2
l2 : List ℕ
h1 : nondec_prime_list (p :: L1)
h4 : ¬l2 = []
q : ℕ
h5 : ∃ L, l2 = q :: L
L2 : List ℕ
h3 : q * prod L1 = q * prod L2
h2 : nondec_prime_list (q :: L2)
h6 : l2 = q :: L2
h7 : p ≤ q
h8 : q ≤ p
h9 : p = q
h10 : nondec_prime_list L1
h11 : nondec_prime_list L2
⊢ p :: L1 = l2
Tactic:
define at h2
Proof state after:
case cons
p : ℕ
L1 : List ℕ
ih : ∀ (l2 : List ℕ), nondec_prime_list L1 → nondec_prime_list l2 → prod L1 = prod l2 → L1 = l2
l2 : List ℕ
h1 : nondec_prime_list (p :: L1)
h4 : ¬l2 = []
q : ℕ
h5 : ∃ L, l2 = q :: L
L2 : List ℕ
h3 : q * prod L1 = q * prod L2
h2 : all_prime (q :: L2) ∧ nondec (q :: L2)
h6 : l2 = q :: L2
h7 : p ≤ q
h8 : q ≤ p
h9 : p = q
h10 : nondec_prime_list L1
h11 : nondec_prime_list L2
⊢ p :: L1 = l2
Theorem: HTPI.Theorem_7_2_5
Proof state before:
case cons
p : ℕ
L1 : List ℕ
ih : ∀ (l2 : List ℕ), nondec_prime_list L1 → nondec_prime_list l2 → prod L1 = prod l2 → L1 = l2
l2 : List ℕ
h1 : nondec_prime_list (p :: L1)
h4 : ¬l2 = []
q : ℕ
h5 : ∃ L, l2 = q :: L
L2 : List ℕ
h3 : q * prod L1 = q * prod L2
h2 : all_prime (q :: L2) ∧ nondec (q :: L2)
h6 : l2 = q :: L2
h7 : p ≤ q
h8 : q ≤ p
h9 : p = q
h10 : nondec_prime_list L1
h11 : nondec_prime_list L2
⊢ p :: L1 = l2
Tactic:
have h12 : all_prime (q :: L2) := h2.left
Proof state after:
case cons
p : ℕ
L1 : List ℕ
ih : ∀ (l2 : List ℕ), nondec_prime_list L1 → nondec_prime_list l2 → prod L1 = prod l2 → L1 = l2
l2 : List ℕ
h1 : nondec_prime_list (p :: L1)
h4 : ¬l2 = []
q : ℕ
h5 : ∃ L, l2 = q :: L
L2 : List ℕ
h3 : q * prod L1 = q * prod L2
h2 : all_prime (q :: L2) ∧ nondec (q :: L2)
h6 : l2 = q :: L2
h7 : p ≤ q
h8 : q ≤ p
h9 : p = q
h10 : nondec_prime_list L1
h11 : nondec_prime_list L2
h12 : all_prime (q :: L2)
⊢ p :: L1 = l2
Theorem: HTPI.Theorem_7_2_5
Proof state before:
case cons
p : ℕ
L1 : List ℕ
ih : ∀ (l2 : List ℕ), nondec_prime_list L1 → nondec_prime_list l2 → prod L1 = prod l2 → L1 = l2
l2 : List ℕ
h1 : nondec_prime_list (p :: L1)
h4 : ¬l2 = []
q : ℕ
h5 : ∃ L, l2 = q :: L
L2 : List ℕ
h3 : q * prod L1 = q * prod L2
h2 : all_prime (q :: L2) ∧ nondec (q :: L2)
h6 : l2 = q :: L2
h7 : p ≤ q
h8 : q ≤ p
h9 : p = q
h10 : nondec_prime_list L1
h11 : nondec_prime_list L2
h12 : all_prime (q :: L2)
⊢ p :: L1 = l2
Tactic:
rewrite [all_prime_cons] at h12
Proof state after:
case cons
p : ℕ
L1 : List ℕ
ih : ∀ (l2 : List ℕ), nondec_prime_list L1 → nondec_prime_list l2 → prod L1 = prod l2 → L1 = l2
l2 : List ℕ
h1 : nondec_prime_list (p :: L1)
h4 : ¬l2 = []
q : ℕ
h5 : ∃ L, l2 = q :: L
L2 : List ℕ
h3 : q * prod L1 = q * prod L2
h2 : all_prime (q :: L2) ∧ nondec (q :: L2)
h6 : l2 = q :: L2
h7 : p ≤ q
h8 : q ≤ p
h9 : p = q
h10 : nondec_prime_list L1
h11 : nondec_prime_list L2
h12 : prime q ∧ all_prime L2
⊢ p :: L1 = l2
Theorem: HTPI.Theorem_7_2_5
Proof state before:
case cons
p : ℕ
L1 : List ℕ
ih : ∀ (l2 : List ℕ), nondec_prime_list L1 → nondec_prime_list l2 → prod L1 = prod l2 → L1 = l2
l2 : List ℕ
h1 : nondec_prime_list (p :: L1)
h4 : ¬l2 = []
q : ℕ
h5 : ∃ L, l2 = q :: L
L2 : List ℕ
h3 : q * prod L1 = q * prod L2
h2 : all_prime (q :: L2) ∧ nondec (q :: L2)
h6 : l2 = q :: L2
h7 : p ≤ q
h8 : q ≤ p
h9 : p = q
h10 : nondec_prime_list L1
h11 : nondec_prime_list L2
h12 : prime q ∧ all_prime L2
⊢ p :: L1 = l2
Tactic:
have h13 : q > 0 := prime_pos h12.left
Proof state after:
case cons
p : ℕ
L1 : List ℕ
ih : ∀ (l2 : List ℕ), nondec_prime_list L1 → nondec_prime_list l2 → prod L1 = prod l2 → L1 = l2
l2 : List ℕ
h1 : nondec_prime_list (p :: L1)
h4 : ¬l2 = []
q : ℕ
h5 : ∃ L, l2 = q :: L
L2 : List ℕ
h3 : q * prod L1 = q * prod L2
h2 : all_prime (q :: L2) ∧ nondec (q :: L2)
h6 : l2 = q :: L2
h7 : p ≤ q
h8 : q ≤ p
h9 : p = q
h10 : nondec_prime_list L1
h11 : nondec_prime_list L2
h12 : prime q ∧ all_prime L2
h13 : q > 0
⊢ p :: L1 = l2
Theorem: HTPI.Theorem_7_2_5
Proof state before:
case cons
p : ℕ
L1 : List ℕ
ih : ∀ (l2 : List ℕ), nondec_prime_list L1 → nondec_prime_list l2 → prod L1 = prod l2 → L1 = l2
l2 : List ℕ
h1 : nondec_prime_list (p :: L1)
h4 : ¬l2 = []
q : ℕ
h5 : ∃ L, l2 = q :: L
L2 : List ℕ
h3 : q * prod L1 = q * prod L2
h2 : all_prime (q :: L2) ∧ nondec (q :: L2)
h6 : l2 = q :: L2
h7 : p ≤ q
h8 : q ≤ p
h9 : p = q
h10 : nondec_prime_list L1
h11 : nondec_prime_list L2
h12 : prime q ∧ all_prime L2
h13 : q > 0
⊢ p :: L1 = l2
Tactic:
have h14 : prod L1 = prod L2 := Nat.eq_of_mul_eq_mul_left h13 h3
Proof state after:
case cons
p : ℕ
L1 : List ℕ
ih : ∀ (l2 : List ℕ), nondec_prime_list L1 → nondec_prime_list l2 → prod L1 = prod l2 → L1 = l2
l2 : List ℕ
h1 : nondec_prime_list (p :: L1)
h4 : ¬l2 = []
q : ℕ
h5 : ∃ L, l2 = q :: L
L2 : List ℕ
h3 : q * prod L1 = q * prod L2
h2 : all_prime (q :: L2) ∧ nondec (q :: L2)
h6 : l2 = q :: L2
h7 : p ≤ q
h8 : q ≤ p
h9 : p = q
h10 : nondec_prime_list L1
h11 : nondec_prime_list L2
h12 : prime q ∧ all_prime L2
h13 : q > 0
h14 : prod L1 = prod L2
⊢ p :: L1 = l2
Theorem: HTPI.Theorem_7_2_5
Proof state before:
case cons
p : ℕ
L1 : List ℕ
ih : ∀ (l2 : List ℕ), nondec_prime_list L1 → nondec_prime_list l2 → prod L1 = prod l2 → L1 = l2
l2 : List ℕ
h1 : nondec_prime_list (p :: L1)
h4 : ¬l2 = []
q : ℕ
h5 : ∃ L, l2 = q :: L
L2 : List ℕ
h3 : q * prod L1 = q * prod L2
h2 : all_prime (q :: L2) ∧ nondec (q :: L2)
h6 : l2 = q :: L2
h7 : p ≤ q
h8 : q ≤ p
h9 : p = q
h10 : nondec_prime_list L1
h11 : nondec_prime_list L2
h12 : prime q ∧ all_prime L2
h13 : q > 0
h14 : prod L1 = prod L2
⊢ p :: L1 = l2
Tactic:
have h15 : L1 = L2 := ih L2 h10 h11 h14
Proof state after:
case cons
p : ℕ
L1 : List ℕ
ih : ∀ (l2 : List ℕ), nondec_prime_list L1 → nondec_prime_list l2 → prod L1 = prod l2 → L1 = l2
l2 : List ℕ
h1 : nondec_prime_list (p :: L1)
h4 : ¬l2 = []
q : ℕ
h5 : ∃ L, l2 = q :: L
L2 : List ℕ
h3 : q * prod L1 = q * prod L2
h2 : all_prime (q :: L2) ∧ nondec (q :: L2)
h6 : l2 = q :: L2
h7 : p ≤ q
h8 : q ≤ p
h9 : p = q
h10 : nondec_prime_list L1
h11 : nondec_prime_list L2
h12 : prime q ∧ all_prime L2
h13 : q > 0
h14 : prod L1 = prod L2
h15 : L1 = L2
⊢ p :: L1 = l2
Theorem: HTPI.Theorem_7_2_5
Proof state before:
case cons
p : ℕ
L1 : List ℕ
ih : ∀ (l2 : List ℕ), nondec_prime_list L1 → nondec_prime_list l2 → prod L1 = prod l2 → L1 = l2
l2 : List ℕ
h1 : nondec_prime_list (p :: L1)
h4 : ¬l2 = []
q : ℕ
h5 : ∃ L, l2 = q :: L
L2 : List ℕ
h3 : q * prod L1 = q * prod L2
h2 : all_prime (q :: L2) ∧ nondec (q :: L2)
h6 : l2 = q :: L2
h7 : p ≤ q
h8 : q ≤ p
h9 : p = q
h10 : nondec_prime_list L1
h11 : nondec_prime_list L2
h12 : prime q ∧ all_prime L2
h13 : q > 0
h14 : prod L1 = prod L2
h15 : L1 = L2
⊢ p :: L1 = l2
Tactic:
rewrite [h6, h9, h15]
Proof state after:
case cons
p : ℕ
L1 : List ℕ
ih : ∀ (l2 : List ℕ), nondec_prime_list L1 → nondec_prime_list l2 → prod L1 = prod l2 → L1 = l2
l2 : List ℕ
h1 : nondec_prime_list (p :: L1)
h4 : ¬l2 = []
q : ℕ
h5 : ∃ L, l2 = q :: L
L2 : List ℕ
h3 : q * prod L1 = q * prod L2
h2 : all_prime (q :: L2) ∧ nondec (q :: L2)
h6 : l2 = q :: L2
h7 : p ≤ q
h8 : q ≤ p
h9 : p = q
h10 : nondec_prime_list L1
h11 : nondec_prime_list L2
h12 : prime q ∧ all_prime L2
h13 : q > 0
h14 : prod L1 = prod L2
h15 : L1 = L2
⊢ q :: L2 = q :: L2
Theorem: HTPI.Theorem_7_2_5
Proof state before:
case cons
p : ℕ
L1 : List ℕ
ih : ∀ (l2 : List ℕ), nondec_prime_list L1 → nondec_prime_list l2 → prod L1 = prod l2 → L1 = l2
l2 : List ℕ
h1 : nondec_prime_list (p :: L1)
h4 : ¬l2 = []
q : ℕ
h5 : ∃ L, l2 = q :: L
L2 : List ℕ
h3 : q * prod L1 = q * prod L2
h2 : all_prime (q :: L2) ∧ nondec (q :: L2)
h6 : l2 = q :: L2
h7 : p ≤ q
h8 : q ≤ p
h9 : p = q
h10 : nondec_prime_list L1
h11 : nondec_prime_list L2
h12 : prime q ∧ all_prime L2
h13 : q > 0
h14 : prod L1 = prod L2
h15 : L1 = L2
⊢ q :: L2 = q :: L2
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.Theorem_7_2_5
Proof state before:
p : ℕ
L1 : List ℕ
ih : ∀ (l2 : List ℕ), nondec_prime_list L1 → nondec_prime_list l2 → prod L1 = prod l2 → L1 = l2
l2 : List ℕ
h1 : nondec_prime_list (p :: L1)
h4 : ¬l2 = []
q : ℕ
h5 : ∃ L, l2 = q :: L
L2 : List ℕ
h3 : prod (p :: L1) = prod (q :: L2)
h2 : nondec_prime_list (q :: L2)
h6 : l2 = q :: L2
h7 : p ≤ q
h8 : q ≤ p
⊢ p = q
Tactic:
linarith
Proof state after:
no goals
Theorem: HTPI.fund_thm_arith
Proof state before:
n : ℕ
h : n ≥ 1
⊢ ∃! l, prime_factorization n l
Tactic:
exists_unique
Proof state after:
case Existence
n : ℕ
h : n ≥ 1
⊢ ∃ l, prime_factorization n l

case Uniqueness
n : ℕ
h : n ≥ 1
⊢ ∀ (l_1 l_2 : List ℕ), prime_factorization n l_1 → prime_factorization n l_2 → l_1 = l_2
Theorem: HTPI.fund_thm_arith
Proof state before:
case Existence
n : ℕ
h : n ≥ 1
⊢ ∃ l, prime_factorization n l
Tactic:
show ∃ (l : List Nat), prime_factorization n l from
  exists_prime_factorization n h
Proof state after:
no goals
Theorem: HTPI.fund_thm_arith
Proof state before:
case Uniqueness
n : ℕ
h : n ≥ 1
⊢ ∀ (l_1 l_2 : List ℕ), prime_factorization n l_1 → prime_factorization n l_2 → l_1 = l_2
Tactic:
fix l1 : List Nat
Proof state after:
case Uniqueness
n : ℕ
h : n ≥ 1
l1 : List ℕ
⊢ ∀ (l_2 : List ℕ), prime_factorization n l1 → prime_factorization n l_2 → l1 = l_2
Theorem: HTPI.fund_thm_arith
Proof state before:
case Uniqueness
n : ℕ
h : n ≥ 1
l1 : List ℕ
⊢ ∀ (l_2 : List ℕ), prime_factorization n l1 → prime_factorization n l_2 → l1 = l_2
Tactic:
fix l2 : List Nat
Proof state after:
case Uniqueness
n : ℕ
h : n ≥ 1
l1 l2 : List ℕ
⊢ prime_factorization n l1 → prime_factorization n l2 → l1 = l2
Theorem: HTPI.fund_thm_arith
Proof state before:
case Uniqueness
n : ℕ
h : n ≥ 1
l1 l2 : List ℕ
⊢ prime_factorization n l1 → prime_factorization n l2 → l1 = l2
Tactic:
assume h1 : prime_factorization n l1
Proof state after:
case Uniqueness
n : ℕ
h : n ≥ 1
l1 l2 : List ℕ
h1 : prime_factorization n l1
⊢ prime_factorization n l2 → l1 = l2
Theorem: HTPI.fund_thm_arith
Proof state before:
case Uniqueness
n : ℕ
h : n ≥ 1
l1 l2 : List ℕ
h1 : prime_factorization n l1
⊢ prime_factorization n l2 → l1 = l2
Tactic:
assume h2 : prime_factorization n l2
Proof state after:
case Uniqueness
n : ℕ
h : n ≥ 1
l1 l2 : List ℕ
h1 : prime_factorization n l1
h2 : prime_factorization n l2
⊢ l1 = l2
Theorem: HTPI.fund_thm_arith
Proof state before:
case Uniqueness
n : ℕ
h : n ≥ 1
l1 l2 : List ℕ
h1 : prime_factorization n l1
h2 : prime_factorization n l2
⊢ l1 = l2
Tactic:
define at h1
Proof state after:
case Uniqueness
n : ℕ
h : n ≥ 1
l1 l2 : List ℕ
h1 : nondec_prime_list l1 ∧ prod l1 = n
h2 : prime_factorization n l2
⊢ l1 = l2
Theorem: HTPI.fund_thm_arith
Proof state before:
case Uniqueness
n : ℕ
h : n ≥ 1
l1 l2 : List ℕ
h1 : nondec_prime_list l1 ∧ prod l1 = n
h2 : prime_factorization n l2
⊢ l1 = l2
Tactic:
define at h2
Proof state after:
case Uniqueness
n : ℕ
h : n ≥ 1
l1 l2 : List ℕ
h1 : nondec_prime_list l1 ∧ prod l1 = n
h2 : nondec_prime_list l2 ∧ prod l2 = n
⊢ l1 = l2