case inl
p : ℕ
⊢ count p (factors 0) = ↑(factorization 0) p

case inr
n p : ℕ
hn0 : n > 0
⊢ count p (factors n) = ↑(factorization n) p
n p : ℕ
⊢ count p (factors n) = ↑(factorization n) p
rcases n.eq_zero_or_pos with (rfl | hn0)
case pos
n p : ℕ
hn0 : n > 0
pp : Prime p
⊢ count p (factors n) = ↑(factorization n) p

case neg
n p : ℕ
hn0 : n > 0
pp : ¬Prime p
⊢ count p (factors n) = ↑(factorization n) p
case inr
n p : ℕ
hn0 : n > 0
⊢ count p (factors n) = ↑(factorization n) p
by_cases pp : p.Prime
case pos
n p : ℕ
hn0 : n > 0
pp : Prime p
⊢ count p (factors n) = ↑(factorization n) p
case pos
n p : ℕ
hn0 : n > 0
pp : Prime p
⊢ count p (factors n) = ↑(factorization n) p

case neg
n p : ℕ
hn0 : n > 0
pp : ¬Prime p
⊢ count p (factors n) = ↑(factorization n) p
case neg =>
  rw [count_eq_zero_of_not_mem (mt prime_of_mem_factors pp)]
  simp [factorization, pp]
case pos
n p : ℕ
hn0 : n > 0
pp : Prime p
⊢ count p (factors n) = padicValNat p n
case pos
n p : ℕ
hn0 : n > 0
pp : Prime p
⊢ count p (factors n) = ↑(factorization n) p
simp only [factorization, coe_mk, pp, if_true]
case pos
n p : ℕ
hn0 : n > 0
pp : Prime p
⊢ ↑(count p (factors n)) = ↑(Multiset.count (↑normalize p) (UniqueFactorizationMonoid.normalizedFactors n))
case pos
n p : ℕ
hn0 : n > 0
pp : Prime p
⊢ count p (factors n) = padicValNat p n
rw [← PartENat.natCast_inj, padicValNat_def' pp.ne_one hn0,
  UniqueFactorizationMonoid.multiplicity_eq_count_normalizedFactors pp hn0.ne']
no goals
case pos
n p : ℕ
hn0 : n > 0
pp : Prime p
⊢ ↑(count p (factors n)) = ↑(Multiset.count (↑normalize p) (UniqueFactorizationMonoid.normalizedFactors n))
simp [factors_eq]
no goals
case inl
p : ℕ
⊢ count p (factors 0) = ↑(factorization 0) p
simp [factorization, count]
n p : ℕ
hn0 : n > 0
pp : ¬Prime p
⊢ 0 = ↑(factorization n) p
n p : ℕ
hn0 : n > 0
pp : ¬Prime p
⊢ count p (factors n) = ↑(factorization n) p
rw [count_eq_zero_of_not_mem (mt prime_of_mem_factors pp)]
no goals
n p : ℕ
hn0 : n > 0
pp : ¬Prime p
⊢ 0 = ↑(factorization n) p
simp [factorization, pp]