Theorem: Aux.primeDivisors_nonempty (PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/AuxResults.lean)

State before:
n : ℕ
hn : 2 ≤ n
⊢ n.primeFactors.Nonempty
Tactic:
unfold Finset.Nonempty
State after:
n : ℕ
hn : 2 ≤ n
⊢ ∃ x, x ∈ n.primeFactors

State before:
n : ℕ
hn : 2 ≤ n
⊢ ∃ x, x ∈ n.primeFactors
Tactic:
simp_rw[Nat.mem_primeFactors_of_ne_zero (by positivity)]
State after:
n : ℕ
hn : 2 ≤ n
⊢ ∃ x, x.Prime ∧ x ∣ n

State before:
n : ℕ
hn : 2 ≤ n
⊢ ∃ x, x.Prime ∧ x ∣ n
Tactic:
apply Nat.exists_prime_and_dvd (by linarith)
State after:
no goals

State before:
n : ℕ
hn : 2 ≤ n
⊢ ?m.33651 ≠ 0
Tactic:
positivity
State after:
no goals

State before:
n : ℕ
hn : 2 ≤ n
⊢ n ≠ 1
Tactic:
linarith
State after:
no goals