rw [Nat.factorization_mul, Nat.factorization_mul] at h
m n q p : ℕ
h : Nat.factorization (2 ^ m * 3 ^ n) = Nat.factorization (2 ^ p * 3 ^ q)
⊢ m = p ∧ n = q
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

case ha
m n q p : ℕ
h : Nat.factorization (2 ^ m) + Nat.factorization (3 ^ n) = Nat.factorization (2 ^ p * 3 ^ q)
⊢ 2 ^ p ≠ 0

case hb
m n q p : ℕ
h : Nat.factorization (2 ^ m) + Nat.factorization (3 ^ n) = Nat.factorization (2 ^ p * 3 ^ q)
⊢ 3 ^ q ≠ 0

case ha
m n q p : ℕ
h : Nat.factorization (2 ^ m * 3 ^ n) = Nat.factorization (2 ^ p * 3 ^ q)
⊢ 2 ^ m ≠ 0

case hb
m n q p : ℕ
h : Nat.factorization (2 ^ m * 3 ^ n) = Nat.factorization (2 ^ p * 3 ^ q)
⊢ 3 ^ n ≠ 0