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