have hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n := by
  exact dvd_mul_of_dvd_right (pow_dvd_pow 3 h₂) (2 ^ m)
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hfac : 2 ^ m * 3 ^ n = 2 ^ p * 3 ^ q
⊢ m = p ∧ n = q
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hfac : 2 ^ m * 3 ^ n = 2 ^ p * 3 ^ q
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
⊢ m = p ∧ n = q