rw [← hrk] at hqn hpn h0
case intro.intro.intro.intro
n p q : ℕ
hp : p.Prime
hq : q.Prime
hpq : p ≠ q
hpn : p ∣ n
hqn : q ∣ n
h0 : n ≠ 0
r k : ℕ
hr : r.Prime
hk : 0 < k
hrk : r ^ k = n
⊢ False
case intro.intro.intro.intro
n p q : ℕ
hp : p.Prime
hq : q.Prime
hpq : p ≠ q
r k : ℕ
h0 : r ^ k ≠ 0
hpn : p ∣ r ^ k
hqn : q ∣ r ^ k
hr : r.Prime
hk : 0 < k
hrk : r ^ k = n
⊢ False