Theorem: Nat.Prime.eq_of_dvd_of_prime (LeanCourse/MIL/C05_Elementary_Number_Theory/S03_Infinitely_Many_Primes.lean)

State before:
p q : ℕ
prime_p : Nat.Prime p
prime_q : Nat.Prime q
h : p ∣ q
⊢ p = q
Tactic:
sorry
State after:
no goals