have h3 : p*q ≠ 0 := by
  apply Nat.mul_ne_zero h1 h2
p q : ℕ
hp : Nat.Prime p
hq : Nat.Prime q
h1 : p ≠ 0
h2 : q ≠ 0
⊢ p * q ≠ 0
p q : ℕ
hp : Nat.Prime p
hq : Nat.Prime q
h1 : p ≠ 0
h2 : q ≠ 0
h3 : p * q ≠ 0
⊢ p * q ≠ 0