obtain ⟨m, ⟨h1, ⟨h2, h3⟩⟩⟩ := h
n : ℕ
hn : n ≥ 2
h : ∃ m ≥ 2, m ≠ n ∧ m ∣ n
p✝ : Prime n
ngt0 : 0 < n
p : n.Prime
⊢ False
case intro.intro.intro
n : ℕ
hn : n ≥ 2
p✝ : Prime n
ngt0 : 0 < n
p : n.Prime
m : ℕ
h1 : m ≥ 2
h2 : m ≠ n
h3 : m ∣ n
⊢ False