rw [←Nat.div_eq_iff_eq_mul_left (by simp) hdvd3,
    Nat.mul_div_assoc (2^m)
      (by rw [pow_dvd_pow_iff (by simp) (by simp)]; exact h₂),
    Nat.pow_div h₂ (by simp)] at hfac
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
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hfac : 2 ^ m * 3 ^ (n - q) = 2 ^ p
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
⊢ m = p ∧ n = q