case intro.intro
n : ℤ
hn : natAbs n ≠ 1
p : ℕ
pp : Nat.Prime p
pd : p ∣ natAbs n
⊢ ∃ p, Prime p ∧ p ∣ n
n : ℤ
hn : natAbs n ≠ 1
⊢ ∃ p, Prime p ∧ p ∣ n
obtain ⟨p, pp, pd⟩ := Nat.exists_prime_and_dvd hn
no goals
case intro.intro
n : ℤ
hn : natAbs n ≠ 1
p : ℕ
pp : Nat.Prime p
pd : p ∣ natAbs n
⊢ ∃ p, Prime p ∧ p ∣ n
exact ⟨p, Nat.prime_iff_prime_int.mp pp, Int.coe_nat_dvd_left.mpr pd⟩