simp_rw [Nat.factorization_pow] at h
m n q p : ℕ
h : Nat.factorization (2 ^ m) + Nat.factorization (3 ^ n) = Nat.factorization (2 ^ p) + Nat.factorization (3 ^ q)
⊢ m = p ∧ n = q
m n q p : ℕ
h : m • Nat.factorization 2 + n • Nat.factorization 3 = p • Nat.factorization 2 + q • Nat.factorization 3
⊢ m = p ∧ n = q