cases prime_q.eq_one_or_self_of_dvd _ h
p q : ℕ
prime_p : p.Prime
prime_q : q.Prime
h : p ∣ q
⊢ p = q
case inl
p q : ℕ
prime_p : p.Prime
prime_q : q.Prime
h : p ∣ q
h✝ : p = 1
⊢ p = q

case inr
p q : ℕ
prime_p : p.Prime
prime_q : q.Prime
h : p ∣ q
h✝ : p = q
⊢ p = q