case pos
n p : ℕ
hp : Prime p
⊢ p ^ ↑(factorization n) p ∣ n

case neg
n p : ℕ
hp : ¬Prime p
⊢ p ^ ↑(factorization n) p ∣ n
n p : ℕ
⊢ p ^ ↑(factorization n) p ∣ n
by_cases hp : p.Prime
case pos
n p : ℕ
hp : Prime p
⊢ p ^ ↑(factorization n) p ∣ n
case pos
n p : ℕ
hp : Prime p
⊢ p ^ ↑(factorization n) p ∣ n

case neg
n p : ℕ
hp : ¬Prime p
⊢ p ^ ↑(factorization n) p ∣ n
case neg => simp [hp]
case pos
n p : ℕ
hp : Prime p
⊢ p ^ count p (factors n) ∣ n
case pos
n p : ℕ
hp : Prime p
⊢ p ^ ↑(factorization n) p ∣ n
rw [← factors_count_eq]
case pos
n p : ℕ
hp : Prime p
⊢ factors (p ^ count p (factors n)) <+~ factors n
case pos
n p : ℕ
hp : Prime p
⊢ p ^ count p (factors n) ∣ n
apply dvd_of_factors_subperm (pow_ne_zero _ hp.ne_zero)
case pos
n p : ℕ
hp : Prime p
⊢ ∀ (x : ℕ), x ∈ replicate (count p (factors n)) p → count x (replicate (count p (factors n)) p) ≤ count x (factors n)
case pos
n p : ℕ
hp : Prime p
⊢ factors (p ^ count p (factors n)) <+~ factors n
rw [hp.factors_pow, List.subperm_ext_iff]
case pos
n p : ℕ
hp : Prime p
q : ℕ
hq : q ∈ replicate (count p (factors n)) p
⊢ count q (replicate (count p (factors n)) p) ≤ count q (factors n)
case pos
n p : ℕ
hp : Prime p
⊢ ∀ (x : ℕ), x ∈ replicate (count p (factors n)) p → count x (replicate (count p (factors n)) p) ≤ count x (factors n)
intro q hq
no goals
case pos
n p : ℕ
hp : Prime p
q : ℕ
hq : q ∈ replicate (count p (factors n)) p
⊢ count q (replicate (count p (factors n)) p) ≤ count q (factors n)
simp [List.eq_of_mem_replicate hq]
no goals
n p : ℕ
hp : ¬Prime p
⊢ p ^ ↑(factorization n) p ∣ n
simp [hp]