no goals
p a b : ℕ
hab : coprime a b
hpa : p ∈ factors a
⊢ ↑(factorization (a * b)) p = ↑(factorization a) p
rw [factorization_mul_apply_of_coprime hab, ← factors_count_eq, ← factors_count_eq,
  count_eq_zero_of_not_mem (coprime_factors_disjoint hab hpa), add_zero]