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

State before:
⊢ ∀ n ≥ 1, ∃ l, prime_factorization n l
Tactic:
by_strong_induc
State after:
⊢ ∀ (n : ℕ), (∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l) → n ≥ 1 → ∃ l, prime_factorization n l

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
State after:
n : ℕ
⊢ (∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l) → n ≥ 1 → ∃ l, prime_factorization n l

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
State after:
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
⊢ n ≥ 1 → ∃ l, prime_factorization n l

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
State after:
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
⊢ ∃ l, prime_factorization n l

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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 : List ℕ
h6 : prime_factorization m L
⊢ ∃ l, prime_factorization n l
Tactic:
define at h6
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 : nondec_prime_list L ∧ prod L = m
⊢ ∃ l, prime_factorization n l

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 : List ℕ
h6 : nondec_prime_list L ∧ prod L = m
⊢ ∃ l, prime_factorization n l
Tactic:
have ndpl_L : nondec_prime_list L := h6.left
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 : nondec_prime_list L ∧ prod L = m
ndpl_L : nondec_prime_list L
⊢ ∃ l, prime_factorization n l

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 : List ℕ
h6 : nondec_prime_list L ∧ prod L = m
ndpl_L : nondec_prime_list L
⊢ ∃ l, prime_factorization n l
Tactic:
define at ndpl_L
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 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
⊢ ∃ l, prime_factorization n l

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 : List ℕ
h6 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
⊢ ∃ l, prime_factorization n l
Tactic:
apply Exists.intro (p :: L)
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 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
⊢ prime_factorization n (p :: L)

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 : List ℕ
h6 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
⊢ prime_factorization n (p :: L)
Tactic:
define
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 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
⊢ nondec_prime_list (p :: L) ∧ prod (p :: L) = n

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 : List ℕ
h6 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
⊢ nondec_prime_list (p :: L) ∧ prod (p :: L) = n
Tactic:
apply And.intro
State after:
case neg.left
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 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
⊢ nondec_prime_list (p :: L)

case neg.right
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 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
⊢ prod (p :: L) = n

State before:
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
⊢ m ≠ 0
Tactic:
contradict h1 with h6
State after:
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
h6 : m = 0
⊢ ¬n ≥ 1

State before:
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
h6 : m = 0
⊢ ¬n ≥ 1
Tactic:
have h7 : n = 0 :=
  calc n
    _ = p * m := n_eq_pm
    _ = p * 0 := by rw [h6]
    _ = 0 := by ring
State after:
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
h6 : m = 0
h7 : n = 0
⊢ ¬n ≥ 1

State before:
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
h6 : m = 0
h7 : n = 0
⊢ ¬n ≥ 1
Tactic:
rewrite [h7]
State after:
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
h6 : m = 0
h7 : n = 0
⊢ ¬0 ≥ 1

State before:
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
h6 : m = 0
h7 : n = 0
⊢ ¬0 ≥ 1
Tactic:
decide
State after:
no goals

State before:
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
h6 : m = 0
⊢ p * m = p * 0
Tactic:
rw [h6]
State after:
no goals

State before:
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
h6 : m = 0
⊢ p * 0 = 0
Tactic:
ring
State after:
no goals

State before:
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 < n
Tactic:
define at p_prime
State after:
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 : 2 ≤ p ∧ ¬∃ a b, a * b = p ∧ a < p ∧ b < 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 < n

State before:
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 : 2 ≤ p ∧ ¬∃ a b, a * b = p ∧ a < p ∧ b < 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 < n
Tactic:
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
State after:
no goals

State before:
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 : 2 ≤ p ∧ ¬∃ a b, a * b = p ∧ a < p ∧ b < 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 < m + m
Tactic:
linarith
State after:
no goals

State before:
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 : 2 ≤ p ∧ ¬∃ a b, a * b = p ∧ a < p ∧ b < 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 + m = 2 * m
Tactic:
ring
State after:
no goals

State before:
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 : 2 ≤ p ∧ ¬∃ a b, a * b = p ∧ a < p ∧ b < 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
⊢ 2 * m ≤ p * m
Tactic:
rel [p_prime.left]
State after:
no goals

State before:
case neg.left
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 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
⊢ nondec_prime_list (p :: L)
Tactic:
define
State after:
case neg.left
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 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
⊢ all_prime (p :: L) ∧ nondec (p :: L)

State before:
case neg.left
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 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
⊢ all_prime (p :: L) ∧ nondec (p :: L)
Tactic:
apply And.intro
State after:
case neg.left.left
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 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
⊢ all_prime (p :: L)

case neg.left.right
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 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
⊢ nondec (p :: L)

State before:
case neg.left.left
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 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
⊢ all_prime (p :: L)
Tactic:
rewrite [all_prime_cons]
State after:
case neg.left.left
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 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
⊢ prime p ∧ all_prime L

State before:
case neg.left.left
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 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
⊢ prime p ∧ all_prime L
Tactic:
show prime p ∧ all_prime L from And.intro p_prime ndpl_L.left
State after:
no goals

State before:
case neg.left.right
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 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
⊢ nondec (p :: L)
Tactic:
rewrite [nondec_cons]
State after:
case neg.left.right
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 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
⊢ (∀ m ∈ L, p ≤ m) ∧ nondec L

State before:
case neg.left.right
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 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
⊢ (∀ m ∈ L, p ≤ m) ∧ nondec L
Tactic:
apply And.intro _ ndpl_L.right
State after:
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 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
⊢ ∀ m ∈ L, p ≤ m

State before:
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 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
⊢ ∀ m ∈ L, p ≤ m
Tactic:
fix q : Nat
State after:
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 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
q : ℕ
⊢ q ∈ L → p ≤ q

State before:
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 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
q : ℕ
⊢ q ∈ L → p ≤ q
Tactic:
assume q_in_L : q ∈ L
State after:
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 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
q : ℕ
q_in_L : q ∈ L
⊢ p ≤ q

State before:
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 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
q : ℕ
q_in_L : q ∈ L
⊢ p ≤ q
Tactic:
have h7 : q ∣ prod L := list_elt_dvd_prod q_in_L
State after:
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 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
q : ℕ
q_in_L : q ∈ L
h7 : q ∣ prod L
⊢ p ≤ q

State before:
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 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
q : ℕ
q_in_L : q ∈ L
h7 : q ∣ prod L
⊢ p ≤ q
Tactic:
rewrite [h6.right] at h7
State after:
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 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
q : ℕ
q_in_L : q ∈ L
h7 : q ∣ m
⊢ p ≤ q

State before:
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 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
q : ℕ
q_in_L : q ∈ L
h7 : q ∣ m
⊢ p ≤ q
Tactic:
have h8 : m ∣ n := by
  apply Exists.intro p
  rewrite [n_eq_pm]
  ring
  done
State after:
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 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
q : ℕ
q_in_L : q ∈ L
h7 : q ∣ m
h8 : m ∣ n
⊢ p ≤ q

State before:
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 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
q : ℕ
q_in_L : q ∈ L
h7 : q ∣ m
h8 : m ∣ n
⊢ p ≤ q
Tactic:
have q_dvd_n : q ∣ n := dvd_trans h7 h8
State after:
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 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
q : ℕ
q_in_L : q ∈ L
h7 : q ∣ m
h8 : m ∣ n
q_dvd_n : q ∣ n
⊢ p ≤ q

State before:
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 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
q : ℕ
q_in_L : q ∈ L
h7 : q ∣ m
h8 : m ∣ n
q_dvd_n : q ∣ n
⊢ p ≤ q
Tactic:
have ap_L : all_prime L := ndpl_L.left
State after:
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 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
q : ℕ
q_in_L : q ∈ L
h7 : q ∣ m
h8 : m ∣ n
q_dvd_n : q ∣ n
ap_L : all_prime L
⊢ p ≤ q

State before:
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 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
q : ℕ
q_in_L : q ∈ L
h7 : q ∣ m
h8 : m ∣ n
q_dvd_n : q ∣ n
ap_L : all_prime L
⊢ p ≤ q
Tactic:
define at ap_L
State after:
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 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
q : ℕ
q_in_L : q ∈ L
h7 : q ∣ m
h8 : m ∣ n
q_dvd_n : q ∣ n
ap_L : ∀ p ∈ L, prime p
⊢ p ≤ q

State before:
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 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
q : ℕ
q_in_L : q ∈ L
h7 : q ∣ m
h8 : m ∣ n
q_dvd_n : q ∣ n
ap_L : ∀ p ∈ L, prime p
⊢ p ≤ q
Tactic:
have q_prime_factor : prime_factor q n :=
  And.intro (ap_L q q_in_L) q_dvd_n
State after:
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 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
q : ℕ
q_in_L : q ∈ L
h7 : q ∣ m
h8 : m ∣ n
q_dvd_n : q ∣ n
ap_L : ∀ p ∈ L, prime p
q_prime_factor : prime_factor q n
⊢ p ≤ q

State before:
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 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
q : ℕ
q_in_L : q ∈ L
h7 : q ∣ m
h8 : m ∣ n
q_dvd_n : q ∣ n
ap_L : ∀ p ∈ L, prime p
q_prime_factor : prime_factor q n
⊢ p ≤ q
Tactic:
show p ≤ q from p_least q q_prime_factor
State after:
no goals

State before:
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 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
q : ℕ
q_in_L : q ∈ L
h7 : q ∣ m
⊢ m ∣ n
Tactic:
apply Exists.intro p
State after:
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 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
q : ℕ
q_in_L : q ∈ L
h7 : q ∣ m
⊢ n = m * p

State before:
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 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
q : ℕ
q_in_L : q ∈ L
h7 : q ∣ m
⊢ n = m * p
Tactic:
rewrite [n_eq_pm]
State after:
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 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
q : ℕ
q_in_L : q ∈ L
h7 : q ∣ m
⊢ p * m = m * p

State before:
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 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
q : ℕ
q_in_L : q ∈ L
h7 : q ∣ m
⊢ p * m = m * p
Tactic:
ring
State after:
no goals

State before:
case neg.right
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 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
⊢ prod (p :: L) = n
Tactic:
rewrite [prod_cons, h6.right, n_eq_pm]
State after:
case neg.right
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 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
⊢ p * m = p * m

State before:
case neg.right
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 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
⊢ p * m = p * m
Tactic:
rfl
State after:
no goals