-- Mathlib/Data/Nat/Choose/Factorization.lean
theorem factorization_choose_le_log : (choose n k).factorization p ≤ log p n

Proof state:
case neg
p n k : ℕ
h : ¬(n.choose k).factorization p = 0
hp : Prime p
hkn : k ≤ n
⊢ (n.choose k).factorization p ≤ log p n

Tactic:
rw [factorization_def _ hp, @padicValNat_def _ ⟨hp⟩ _ (choose_pos hkn)]

Result:
case neg
p n k : ℕ
h : ¬(n.choose k).factorization p = 0
hp : Prime p
hkn : k ≤ n
⊢ multiplicity p (n.choose k) ≤ log p n

Proof state:
case neg
p n k : ℕ
h : ¬(n.choose k).factorization p = 0
hp : Prime p
hkn : k ≤ n
⊢ multiplicity p (n.choose k) ≤ log p n

Tactic:
rw [← Nat.cast_le (α := ℕ∞), ← FiniteMultiplicity.emultiplicity_eq_multiplicity]

Result:
case neg
p n k : ℕ
h : ¬(n.choose k).factorization p = 0
hp : Prime p
hkn : k ≤ n
⊢ emultiplicity p (n.choose k) ≤ ↑(log p n)

case neg
p n k : ℕ
h : ¬(n.choose k).factorization p = 0
hp : Prime p
hkn : k ≤ n
⊢ FiniteMultiplicity p (n.choose k)

Proof state:
case neg
p n k : ℕ
h : ¬(n.choose k).factorization p = 0
hp : Prime p
hkn : k ≤ n
⊢ FiniteMultiplicity p (n.choose k)

Tactic:
apply Nat.finiteMultiplicity_iff.2 ⟨hp.ne_one, choose_pos hkn⟩

Result:
no goals

Proof state:
case neg
p n k : ℕ
h : ¬(n.choose k).factorization p = 0
⊢ (n.choose k).factorization p ≤ log p n

Tactic:
have hp : p.Prime := Not.imp_symm (choose n k).factorization_eq_zero_of_non_prime h

Result:
case neg
p n k : ℕ
h : ¬(n.choose k).factorization p = 0
hp : Prime p
⊢ (n.choose k).factorization p ≤ log p n

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

Tactic:
simp [h]

Result:
no goals

Proof state:
p n k : ℕ
⊢ (n.choose k).factorization p ≤ log p n

Tactic:
by_cases h : (choose n k).factorization p = 0

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

case neg
p n k : ℕ
h : ¬(n.choose k).factorization p = 0
⊢ (n.choose k).factorization p ≤ log p n

Proof state:
p n k : ℕ
h : ¬(n.choose k).factorization p = 0
hp : Prime p
⊢ k ≤ n

Tactic:
refine le_of_not_lt fun hnk => h ?_

Result:
p n k : ℕ
h : ¬(n.choose k).factorization p = 0
hp : Prime p
hnk : n < k
⊢ (n.choose k).factorization p = 0

Proof state:
case neg
p n k : ℕ
h : ¬(n.choose k).factorization p = 0
hp : Prime p
⊢ (n.choose k).factorization p ≤ log p n

Tactic:
have hkn : k ≤ n := by
  refine le_of_not_lt fun hnk => h ?_
  simp [choose_eq_zero_of_lt hnk]

Result:
case neg
p n k : ℕ
h : ¬(n.choose k).factorization p = 0
hp : Prime p
hkn : k ≤ n
⊢ (n.choose k).factorization p ≤ log p n

Proof state:
case neg
p n k : ℕ
h : ¬(n.choose k).factorization p = 0
hp : Prime p
hkn : k ≤ n
⊢ (Finset.filter (fun i => p ^ i ≤ k % p ^ i + (n - k) % p ^ i) (Finset.Ico 1 (log p n + 1))).card ≤ log p n

Tactic:
exact (Finset.card_filter_le _ _).trans (le_of_eq (Nat.card_Ico _ _))

Result:
no goals

Proof state:
p n k : ℕ
h : ¬(n.choose k).factorization p = 0
hp : Prime p
hnk : n < k
⊢ (n.choose k).factorization p = 0

Tactic:
simp [choose_eq_zero_of_lt hnk]

Result:
no goals

Proof state:
case neg
p n k : ℕ
h : ¬(n.choose k).factorization p = 0
hp : Prime p
hkn : k ≤ n
⊢ emultiplicity p (n.choose k) ≤ ↑(log p n)

Tactic:
simp only [hp.emultiplicity_choose hkn (lt_add_one _), Nat.cast_le]

Result:
case neg
p n k : ℕ
h : ¬(n.choose k).factorization p = 0
hp : Prime p
hkn : k ≤ n
⊢ (Finset.filter (fun i => p ^ i ≤ k % p ^ i + (n - k) % p ^ i) (Finset.Ico 1 (log p n + 1))).card ≤ log p n