rw [h3, h4] at hpq
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
h1 : p ∈ List.replicate k r
h3 : p = r
h2 : q ∈ List.replicate k r
h4 : q = r
⊢ False
case intro.intro.intro.intro
n p q : ℕ
hp : p.Prime
hq : q.Prime
r : ℕ
hpq : r ≠ r
k : ℕ
h0 : r ^ k ≠ 0
hpn : p ∣ r ^ k
hqn : q ∣ r ^ k
hr : r.Prime
hk : 0 < k
h1 : p ∈ List.replicate k r
h3 : p = r
h2 : q ∈ List.replicate k r
h4 : q = r
⊢ False