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

State before:
n : ℕ
h : 2 ≤ n
⊢ ∃ p, prime_factor p n ∧ ∀ (q : ℕ), prime_factor q n → p ≤ q
Tactic:
set S : Set Nat := {p : Nat | prime_factor p n}
State after:
n : ℕ
h : 2 ≤ n
S : Set ℕ := {p | prime_factor p n}
⊢ ∃ p, prime_factor p n ∧ ∀ (q : ℕ), prime_factor q n → p ≤ q

State before:
n : ℕ
h : 2 ≤ n
S : Set ℕ := {p | prime_factor p n}
⊢ ∃ p, prime_factor p n ∧ ∀ (q : ℕ), prime_factor q n → p ≤ q
Tactic:
have h2 : ∃ (p : Nat), p ∈ S := exists_prime_factor n h
State after:
n : ℕ
h : 2 ≤ n
S : Set ℕ := {p | prime_factor p n}
h2 : ∃ p, p ∈ S
⊢ ∃ p, prime_factor p n ∧ ∀ (q : ℕ), prime_factor q n → p ≤ q

State before:
n : ℕ
h : 2 ≤ n
S : Set ℕ := {p | prime_factor p n}
h2 : ∃ p, p ∈ S
⊢ ∃ p, prime_factor p n ∧ ∀ (q : ℕ), prime_factor q n → p ≤ q
Tactic:
show ∃ (p : Nat), prime_factor p n ∧
  ∀ (q : Nat), prime_factor q n → p ≤ q from well_ord_princ S h2
State after:
no goals