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

State before:
n : ℕ
h : n ≥ 1
⊢ ∃! l, prime_factorization n l
Tactic:
exists_unique
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

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

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

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
State after:
case Uniqueness
n : ℕ
h : n ≥ 1
l1 l2 : List ℕ
⊢ prime_factorization n l1 → prime_factorization n l2 → l1 = l2

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
State after:
case Uniqueness
n : ℕ
h : n ≥ 1
l1 l2 : List ℕ
h1 : prime_factorization n l1
⊢ prime_factorization n l2 → l1 = l2

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
State after:
case Uniqueness
n : ℕ
h : n ≥ 1
l1 l2 : List ℕ
h1 : prime_factorization n l1
h2 : prime_factorization n l2
⊢ l1 = l2

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

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

State before:
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
Tactic:
have h3 : prod l1 = n := h1.right
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
h3 : prod l1 = n
⊢ l1 = l2

State before:
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
h3 : prod l1 = n
⊢ l1 = l2
Tactic:
rewrite [←h2.right] at h3
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
h3 : prod l1 = prod l2
⊢ l1 = l2

State before:
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
h3 : prod l1 = prod l2
⊢ l1 = l2
Tactic:
show l1 = l2 from Theorem_7_2_5 l1 l2 h1.left h2.left h3
State after:
no goals