case inl
p b : ℕ
hb : 0 ≤ p ^ b
⊢ ↑(factorization 0) p ≤ b

case inr
n p b : ℕ
hb : n ≤ p ^ b
hn : n ≠ 0
⊢ ↑(factorization n) p ≤ b
n p b : ℕ
hb : n ≤ p ^ b
⊢ ↑(factorization n) p ≤ b
rcases eq_or_ne n 0 with (rfl | hn)
case pos
n p b : ℕ
hb : n ≤ p ^ b
hn : n ≠ 0
pp : Prime p
⊢ ↑(factorization n) p ≤ b

case neg
n p b : ℕ
hb : n ≤ p ^ b
hn : n ≠ 0
pp : ¬Prime p
⊢ ↑(factorization n) p ≤ b
case inr
n p b : ℕ
hb : n ≤ p ^ b
hn : n ≠ 0
⊢ ↑(factorization n) p ≤ b
by_cases pp : p.Prime
no goals
case inl
p b : ℕ
hb : 0 ≤ p ^ b
⊢ ↑(factorization 0) p ≤ b
simp
no goals
case pos
n p b : ℕ
hb : n ≤ p ^ b
hn : n ≠ 0
pp : Prime p
⊢ ↑(factorization n) p ≤ b
exact (pow_le_iff_le_right pp.two_le).1 (le_trans (ord_proj_le p hn) hb)
no goals
case neg
n p b : ℕ
hb : n ≤ p ^ b
hn : n ≠ 0
pp : ¬Prime p
⊢ ↑(factorization n) p ≤ b
simp [factorization_eq_zero_of_non_prime n pp]