case pos
p n k : ℕ
h : ↑(factorization (choose n k)) p = 0
⊢ ↑(factorization (choose n k)) p ≤ log p n

case neg
p n k : ℕ
h : ¬↑(factorization (choose n k)) p = 0
⊢ ↑(factorization (choose n k)) p ≤ log p n
p n k : ℕ
⊢ ↑(factorization (choose n k)) p ≤ log p n
by_cases h : (choose n k).factorization p = 0
case neg
p n k : ℕ
h : ¬↑(factorization (choose n k)) p = 0
hp : Prime p
⊢ ↑(factorization (choose n k)) p ≤ log p n
case neg
p n k : ℕ
h : ¬↑(factorization (choose n k)) p = 0
⊢ ↑(factorization (choose n k)) p ≤ log p n
have hp : p.Prime := Not.imp_symm (choose n k).factorization_eq_zero_of_non_prime h
case neg
p n k : ℕ
h : ¬↑(factorization (choose n k)) p = 0
hp : Prime p
hkn : k ≤ n
⊢ ↑(factorization (choose n k)) p ≤ log p n
case neg
p n k : ℕ
h : ¬↑(factorization (choose n k)) p = 0
hp : Prime p
⊢ ↑(factorization (choose n k)) p ≤ log p n
have hkn : k ≤ n := by
  refine' le_of_not_lt fun hnk => h _
  simp [choose_eq_zero_of_lt hnk]
case neg
p n k : ℕ
h : ¬↑(factorization (choose n k)) p = 0
hp : Prime p
hkn : k ≤ n
⊢ Part.get (multiplicity p (choose n k)) (_ : multiplicity.Finite p (choose n k)) ≤ log p n
case neg
p n k : ℕ
h : ¬↑(factorization (choose n k)) p = 0
hp : Prime p
hkn : k ≤ n
⊢ ↑(factorization (choose n k)) p ≤ log p n
rw [factorization_def _ hp, @padicValNat_def _ ⟨hp⟩ _ (choose_pos hkn)]
case neg
p n k : ℕ
h : ¬↑(factorization (choose n k)) p = 0
hp : Prime p
hkn : k ≤ n
⊢ Finset.card (Finset.filter (fun i => p ^ i ≤ k % p ^ i + (n - k) % p ^ i) (Finset.Ico 1 (log p n + 1))) ≤ log p n
case neg
p n k : ℕ
h : ¬↑(factorization (choose n k)) p = 0
hp : Prime p
hkn : k ≤ n
⊢ Part.get (multiplicity p (choose n k)) (_ : multiplicity.Finite p (choose n k)) ≤ log p n
simp only [hp.multiplicity_choose hkn (lt_add_one _), PartENat.get_natCast]
no goals
case neg
p n k : ℕ
h : ¬↑(factorization (choose n k)) p = 0
hp : Prime p
hkn : k ≤ n
⊢ Finset.card (Finset.filter (fun i => p ^ i ≤ k % p ^ i + (n - k) % p ^ i) (Finset.Ico 1 (log p n + 1))) ≤ log p n
refine (Finset.card_filter_le _ _).trans (le_of_eq (Nat.card_Ico _ _))
no goals
case pos
p n k : ℕ
h : ↑(factorization (choose n k)) p = 0
⊢ ↑(factorization (choose n k)) p ≤ log p n
simp [h]
p n k : ℕ
h : ¬↑(factorization (choose n k)) p = 0
hp : Prime p
hnk : n < k
⊢ ↑(factorization (choose n k)) p = 0
p n k : ℕ
h : ¬↑(factorization (choose n k)) p = 0
hp : Prime p
⊢ k ≤ n
refine' le_of_not_lt fun hnk => h _
no goals
p n k : ℕ
h : ¬↑(factorization (choose n k)) p = 0
hp : Prime p
hnk : n < k
⊢ ↑(factorization (choose n k)) p = 0
simp [choose_eq_zero_of_lt hnk]