rw [mul_eq_one_iff' (Nat.one_le_pow' (n - q) 2) (Nat.one_le_two_pow (m - p))] at hfac
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hfac : 3 ^ (n - q) * 2 ^ (m - p) = 1
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
hdvd2 : 2 ^ p ∣ 3 ^ (n - q) * 2 ^ m
⊢ m = p ∧ n = q
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hfac : (2 + 1) ^ (n - q) = 1 ∧ 2 ^ (m - p) = 1
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
hdvd2 : 2 ^ p ∣ 3 ^ (n - q) * 2 ^ m
⊢ m = p ∧ n = q