apply_fun (λ e => Nat.log 2 e) at h2
case intro
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
h2 : 2 ^ (m - p) = 1
h3 : 3 ^ (n - q) = 1
hdvd2 : 2 ^ p ∣ 2 ^ m * 3 ^ (n - q)
⊢ m = p ∧ n = q
case intro
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
h3 : 3 ^ (n - q) = 1
hdvd2 : 2 ^ p ∣ 2 ^ m * 3 ^ (n - q)
h2 : Nat.log 2 (2 ^ (m - p)) = Nat.log 2 1
⊢ m = p ∧ n = q