Theorem: HTPI.Theorem_7_2_5 (HTPILib/Chap7.lean)

State before:
⊢ ∀ (l1 l2 : List ℕ), nondec_prime_list l1 → nondec_prime_list l2 → prod l1 = prod l2 → l1 = l2
Tactic:
apply List.rec
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

State before:
case nil

⊢ ∀ (l2 : List ℕ), nondec_prime_list [] → nondec_prime_list l2 → prod [] = prod l2 → [] = l2
Tactic:
fix l2 : List Nat
State after:
case nil
l2 : List ℕ
⊢ nondec_prime_list [] → nondec_prime_list l2 → prod [] = prod l2 → [] = l2

State before:
case nil
l2 : List ℕ
⊢ nondec_prime_list [] → nondec_prime_list l2 → prod [] = prod l2 → [] = l2
Tactic:
assume h1 : nondec_prime_list []
State after:
case nil
l2 : List ℕ
h1 : nondec_prime_list []
⊢ nondec_prime_list l2 → prod [] = prod l2 → [] = l2

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
State after:
case nil
l2 : List ℕ
h1 : nondec_prime_list []
h2 : nondec_prime_list l2
⊢ prod [] = prod l2 → [] = l2

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
State after:
case nil
l2 : List ℕ
h1 : nondec_prime_list []
h2 : nondec_prime_list l2
h3 : prod [] = prod l2
⊢ [] = l2

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
State after:
case nil
l2 : List ℕ
h1 : nondec_prime_list []
h2 : nondec_prime_list l2
h3 : l2 = []
⊢ [] = l2

State before:
case nil
l2 : List ℕ
h1 : nondec_prime_list []
h2 : nondec_prime_list l2
h3 : l2 = []
⊢ [] = l2
Tactic:
show [] = l2 from h3.symm
State after:
no goals

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
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

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
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

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
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

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
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

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)
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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]
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

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
State after:
no goals

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
State after:
no goals