simp_rw [Finsupp.add_apply, Finsupp.smul_apply, Nat.prime_three.factorization_self,
  nsmul_one, Nat.factorization_eq_zero_of_not_dvd this, smul_zero, zero_add] at h
case right
m n q p : ℕ
h : ↑(m • Nat.factorization 2 + n • Nat.factorization 3) 3 = ↑(p • Nat.factorization 2 + q • Nat.factorization 3) 3
this : ¬3 ∣ 2
⊢ n = q
case right
m n q p : ℕ
this : ¬3 ∣ 2
h : ↑n = ↑q
⊢ n = q