-- Mathlib/Data/Nat/Factorization/Defs.lean
theorem primeFactorsList_count_eq {n p : ℕ} : n.primeFactorsList.count p = n.factorization p

Proof state:
case inr
n p : ℕ
hn0 : n > 0
pp : Prime p
⊢ count p n.primeFactorsList = n.factorization p

Tactic:
simp only [factorization_def _ pp]

Result:
case inr
n p : ℕ
hn0 : n > 0
pp : Prime p
⊢ count p n.primeFactorsList = padicValNat p n

Proof state:
case inr.a
n p : ℕ
hn0 : n > 0
pp : Prime p
h : replicate (count p n.primeFactorsList + 1) p <+~ n.primeFactorsList
this : count p (replicate (count p n.primeFactorsList + 1) p) ≤ count p n.primeFactorsList
⊢ False

Tactic:
simp at this

Result:
no goals

Proof state:
n p : ℕ
hn0 : n > 0
pp : ¬Prime p
⊢ 0 = n.factorization p

Tactic:
simp [factorization, pp]

Result:
no goals

Proof state:
n p : ℕ
⊢ count p n.primeFactorsList = n.factorization p

Tactic:
rcases n.eq_zero_or_pos with (rfl | hn0)

Result:
case inl
p : ℕ
⊢ count p (primeFactorsList 0) = (factorization 0) p

case inr
n p : ℕ
hn0 : n > 0
⊢ count p n.primeFactorsList = n.factorization p

Proof state:
case inr.a
n p : ℕ
hn0 : n > 0
pp : Prime p
⊢ padicValNat p n ≤ count p n.primeFactorsList

Tactic:
rw [← Nat.lt_add_one_iff, lt_iff_not_ge, ge_iff_le,
  le_padicValNat_iff_replicate_subperm_primeFactorsList pp hn0.ne']

Result:
case inr.a
n p : ℕ
hn0 : n > 0
pp : Prime p
⊢ ¬replicate (count p n.primeFactorsList + 1) p <+~ n.primeFactorsList

Proof state:
case inl
p : ℕ
⊢ count p (primeFactorsList 0) = (factorization 0) p

Tactic:
simp [factorization, count]

Result:
no goals

Proof state:
case inr
n p : ℕ
hn0 : n > 0
pp : Prime p
⊢ count p n.primeFactorsList = padicValNat p n

Tactic:
apply _root_.le_antisymm

Result:
case inr.a
n p : ℕ
hn0 : n > 0
pp : Prime p
⊢ count p n.primeFactorsList ≤ padicValNat p n

case inr.a
n p : ℕ
hn0 : n > 0
pp : Prime p
⊢ padicValNat p n ≤ count p n.primeFactorsList

Proof state:
case inr.a
n p : ℕ
hn0 : n > 0
pp : Prime p
⊢ count p n.primeFactorsList ≤ padicValNat p n

Tactic:
rw [le_padicValNat_iff_replicate_subperm_primeFactorsList pp hn0.ne']

Result:
case inr.a
n p : ℕ
hn0 : n > 0
pp : Prime p
⊢ replicate (count p n.primeFactorsList) p <+~ n.primeFactorsList

Proof state:
case inr.a
n p : ℕ
hn0 : n > 0
pp : Prime p
h : replicate (count p n.primeFactorsList + 1) p <+~ n.primeFactorsList
⊢ False

Tactic:
have := h.count_le p

Result:
case inr.a
n p : ℕ
hn0 : n > 0
pp : Prime p
h : replicate (count p n.primeFactorsList + 1) p <+~ n.primeFactorsList
this : count p (replicate (count p n.primeFactorsList + 1) p) ≤ count p n.primeFactorsList
⊢ False

Proof state:
n p : ℕ
hn0 : n > 0
pp : ¬Prime p
⊢ count p n.primeFactorsList = n.factorization p

Tactic:
rw [count_eq_zero_of_not_mem (mt prime_of_mem_primeFactorsList pp)]

Result:
n p : ℕ
hn0 : n > 0
pp : ¬Prime p
⊢ 0 = n.factorization p

Proof state:
case inr.a
n p : ℕ
hn0 : n > 0
pp : Prime p
⊢ ¬replicate (count p n.primeFactorsList + 1) p <+~ n.primeFactorsList

Tactic:
intro h

Result:
case inr.a
n p : ℕ
hn0 : n > 0
pp : Prime p
h : replicate (count p n.primeFactorsList + 1) p <+~ n.primeFactorsList
⊢ False

Proof state:
case inr
n p : ℕ
hn0 : n > 0
⊢ count p n.primeFactorsList = n.factorization p

Tactic:
if pp : p.Prime then ?_ else
  rw [count_eq_zero_of_not_mem (mt prime_of_mem_primeFactorsList pp)]
  simp [factorization, pp]

Result:
case inr
n p : ℕ
hn0 : n > 0
pp : Prime p
⊢ count p n.primeFactorsList = n.factorization p

Proof state:
case inr.a
n p : ℕ
hn0 : n > 0
pp : Prime p
⊢ replicate (count p n.primeFactorsList) p <+~ n.primeFactorsList

Tactic:
exact List.le_count_iff_replicate_sublist.mp le_rfl |>.subperm

Result:
no goals