rw [pow_dvd_pow_iff (by simp) (by simp)]
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hfac : 2 ^ m * 3 ^ n / 3 ^ q = 2 ^ p
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
⊢ 3 ^ q ∣ 3 ^ n
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hfac : 2 ^ m * 3 ^ n / 3 ^ q = 2 ^ p
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
⊢ q ≤ n