case intro
n : ℕ+
hn : n ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ ↑n
⊢ ∃ p, Prime p ∧ p ∣ n
n : ℕ+
hn : n ≠ 1
⊢ ∃ p, Prime p ∧ p ∣ n
obtain ⟨p, hp⟩ := Nat.exists_prime_and_dvd (mt coe_eq_one_iff.mp hn)
case intro
n : ℕ+
hn : n ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ ↑n
⊢ Prime { val := p, property := (_ : 0 < p) } ∧ { val := p, property := (_ : 0 < p) } ∣ n
case intro
n : ℕ+
hn : n ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ ↑n
⊢ ∃ p, Prime p ∧ p ∣ n
exists (⟨p, Nat.Prime.pos hp.left⟩ : ℕ+)
case intro
n : ℕ+
hn : n ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ ↑n
⊢ Prime { val := p, property := (_ : 0 < p) } ∧ ↑{ val := p, property := (_ : 0 < p) } ∣ ↑n
case intro
n : ℕ+
hn : n ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ ↑n
⊢ Prime { val := p, property := (_ : 0 < p) } ∧ { val := p, property := (_ : 0 < p) } ∣ n
rw [dvd_iff]
no goals
case intro
n : ℕ+
hn : n ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ ↑n
⊢ Prime { val := p, property := (_ : 0 < p) } ∧ ↑{ val := p, property := (_ : 0 < p) } ∣ ↑n
apply hp