no goals
R : Type ?u.553992
m n : ℕ
m0 : m ≠ 0
n0 : n ≠ 0
⊢ ↑Ω (m * n) = ↑Ω m + ↑Ω n
rw [cardFactors_apply, cardFactors_apply, cardFactors_apply, ← Multiset.coe_card, ← factors_eq,
  UniqueFactorizationMonoid.normalizedFactors_mul m0 n0, factors_eq, factors_eq,
  Multiset.card_add, Multiset.coe_card, Multiset.coe_card]