[GOAL]
p n k : ℕ
⊢ ↑(factorization (choose n k)) p ≤ log p n
[PROOFSTEP]
by_cases h : (choose n k).factorization p = 0
[GOAL]
case pos
p n k : ℕ
h : ↑(factorization (choose n k)) p = 0
⊢ ↑(factorization (choose n k)) p ≤ log p n
[PROOFSTEP]
simp [h]
[GOAL]
case neg
p n k : ℕ
h : ¬↑(factorization (choose n k)) p = 0
⊢ ↑(factorization (choose n k)) p ≤ log p n
[PROOFSTEP]
have hp : p.Prime := Not.imp_symm (choose n k).factorization_eq_zero_of_non_prime h
[GOAL]
case neg
p n k : ℕ
h : ¬↑(factorization (choose n k)) p = 0
hp : Prime p
⊢ ↑(factorization (choose n k)) p ≤ log p n
[PROOFSTEP]
have hkn : k ≤ n := by
  refine' le_of_not_lt fun hnk => h _
  simp [choose_eq_zero_of_lt hnk]
[GOAL]
p n k : ℕ
h : ¬↑(factorization (choose n k)) p = 0
hp : Prime p
⊢ k ≤ n
[PROOFSTEP]
refine' le_of_not_lt fun hnk => h _
[GOAL]
p n k : ℕ
h : ¬↑(factorization (choose n k)) p = 0
hp : Prime p
hnk : n < k
⊢ ↑(factorization (choose n k)) p = 0
[PROOFSTEP]
simp [choose_eq_zero_of_lt hnk]
[GOAL]
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
[PROOFSTEP]
rw [factorization_def _ hp, @padicValNat_def _ ⟨hp⟩ _ (choose_pos hkn)]
[GOAL]
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
[PROOFSTEP]
simp only [hp.multiplicity_choose hkn (lt_add_one _), PartENat.get_natCast]
[GOAL]
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
[PROOFSTEP]
refine (Finset.card_filter_le _ _).trans (le_of_eq (Nat.card_Ico _ _))
[GOAL]
p n k : ℕ
p_large : n < p ^ 2
⊢ ↑(factorization (choose n k)) p ≤ 1
[PROOFSTEP]
apply factorization_choose_le_log.trans
[GOAL]
p n k : ℕ
p_large : n < p ^ 2
⊢ log p n ≤ 1
[PROOFSTEP]
rcases eq_or_ne n 0 with (rfl | hn0)
[GOAL]
case inl
p k : ℕ
p_large : 0 < p ^ 2
⊢ log p 0 ≤ 1
[PROOFSTEP]
simp
[GOAL]
case inr
p n k : ℕ
p_large : n < p ^ 2
hn0 : n ≠ 0
⊢ log p n ≤ 1
[PROOFSTEP]
exact lt_succ_iff.1 (log_lt_of_lt_pow hn0 p_large)
[GOAL]
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
⊢ ↑(factorization (choose n k)) p = 0
[PROOFSTEP]
cases' em' p.Prime with hp hp
[GOAL]
case inl
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
hp : ¬Prime p
⊢ ↑(factorization (choose n k)) p = 0
[PROOFSTEP]
exact factorization_eq_zero_of_non_prime (choose n k) hp
[GOAL]
case inr
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
hp : Prime p
⊢ ↑(factorization (choose n k)) p = 0
[PROOFSTEP]
cases' lt_or_le n k with hnk hkn
[GOAL]
case inr.inl
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
hp : Prime p
hnk : n < k
⊢ ↑(factorization (choose n k)) p = 0
[PROOFSTEP]
simp [choose_eq_zero_of_lt hnk]
[GOAL]
case inr.inr
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
hp : Prime p
hkn : k ≤ n
⊢ ↑(factorization (choose n k)) p = 0
[PROOFSTEP]
rw [factorization_def _ hp, @padicValNat_def _ ⟨hp⟩ _ (choose_pos hkn)]
[GOAL]
case inr.inr
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
hp : Prime p
hkn : k ≤ n
⊢ Part.get (multiplicity p (choose n k)) (_ : multiplicity.Finite p (choose n k)) = 0
[PROOFSTEP]
simp only [hp.multiplicity_choose hkn (lt_add_one _), PartENat.get_natCast, Finset.card_eq_zero,
  Finset.filter_eq_empty_iff, not_le]
[GOAL]
case inr.inr
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
hp : Prime p
hkn : k ≤ n
⊢ ∀ (x : ℕ), x ∈ Finset.Ico 1 (log p n + 1) → k % p ^ x + (n - k) % p ^ x < p ^ x
[PROOFSTEP]
intro i hi
[GOAL]
case inr.inr
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
hp : Prime p
hkn : k ≤ n
i : ℕ
hi : i ∈ Finset.Ico 1 (log p n + 1)
⊢ k % p ^ i + (n - k) % p ^ i < p ^ i
[PROOFSTEP]
rcases eq_or_lt_of_le (Finset.mem_Ico.mp hi).1 with (rfl | hi)
[GOAL]
case inr.inr.inl
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
hp : Prime p
hkn : k ≤ n
hi : 1 ∈ Finset.Ico 1 (log p n + 1)
⊢ k % p ^ 1 + (n - k) % p ^ 1 < p ^ 1
[PROOFSTEP]
rw [pow_one, ← add_lt_add_iff_left (2 * p), ← succ_mul, two_mul, add_add_add_comm]
[GOAL]
case inr.inr.inl
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
hp : Prime p
hkn : k ≤ n
hi : 1 ∈ Finset.Ico 1 (log p n + 1)
⊢ p + k % p + (p + (n - k) % p) < succ 2 * p
[PROOFSTEP]
exact
  lt_of_le_of_lt
    (add_le_add (add_le_add_right (le_mul_of_one_le_right' ((one_le_div_iff hp.pos).mpr hk)) (k % p))
      (add_le_add_right (le_mul_of_one_le_right' ((one_le_div_iff hp.pos).mpr hk')) ((n - k) % p)))
    (by rwa [div_add_mod, div_add_mod, add_tsub_cancel_of_le hkn])
[GOAL]
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
hp : Prime p
hkn : k ≤ n
hi : 1 ∈ Finset.Ico 1 (log p n + 1)
⊢ p * (k / p) + k % p + (p * ((n - k) / p) + (n - k) % p) < succ 2 * p
[PROOFSTEP]
rwa [div_add_mod, div_add_mod, add_tsub_cancel_of_le hkn]
[GOAL]
case inr.inr.inr
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
hp : Prime p
hkn : k ≤ n
i : ℕ
hi✝ : i ∈ Finset.Ico 1 (log p n + 1)
hi : 1 < i
⊢ k % p ^ i + (n - k) % p ^ i < p ^ i
[PROOFSTEP]
replace hn : n < p ^ i
[GOAL]
case hn
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
hp : Prime p
hkn : k ≤ n
i : ℕ
hi✝ : i ∈ Finset.Ico 1 (log p n + 1)
hi : 1 < i
⊢ n < p ^ i
case inr.inr.inr
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hp : Prime p
hkn : k ≤ n
i : ℕ
hi✝ : i ∈ Finset.Ico 1 (log p n + 1)
hi : 1 < i
hn : n < p ^ i
⊢ k % p ^ i + (n - k) % p ^ i < p ^ i
[PROOFSTEP]
have : 3 ≤ p := lt_of_le_of_ne hp.two_le hp'.symm
[GOAL]
case hn
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
hp : Prime p
hkn : k ≤ n
i : ℕ
hi✝ : i ∈ Finset.Ico 1 (log p n + 1)
hi : 1 < i
this : 3 ≤ p
⊢ n < p ^ i
[PROOFSTEP]
calc
  n < 3 * p := hn
  _ ≤ p * p := (mul_le_mul_right' this p)
  _ = p ^ 2 := (sq p).symm
  _ ≤ p ^ i := pow_le_pow hp.one_lt.le hi
[GOAL]
case inr.inr.inr
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hp : Prime p
hkn : k ≤ n
i : ℕ
hi✝ : i ∈ Finset.Ico 1 (log p n + 1)
hi : 1 < i
hn : n < p ^ i
⊢ k % p ^ i + (n - k) % p ^ i < p ^ i
[PROOFSTEP]
rwa [mod_eq_of_lt (lt_of_le_of_lt hkn hn), mod_eq_of_lt (lt_of_le_of_lt tsub_le_self hn), add_tsub_cancel_of_le hkn]
[GOAL]
p n k : ℕ
n_big : 2 < n
p_le_n : p ≤ n
big : 2 * n < 3 * p
⊢ ↑(factorization (centralBinom n)) p = 0
[PROOFSTEP]
refine' factorization_choose_of_lt_three_mul _ p_le_n (p_le_n.trans _) big
[GOAL]
case refine'_1
p n k : ℕ
n_big : 2 < n
p_le_n : p ≤ n
big : 2 * n < 3 * p
⊢ p ≠ 2
[PROOFSTEP]
rintro rfl
[GOAL]
case refine'_1
n k : ℕ
n_big : 2 < n
p_le_n : 2 ≤ n
big : 2 * n < 3 * 2
⊢ False
[PROOFSTEP]
linarith
[GOAL]
case refine'_2
p n k : ℕ
n_big : 2 < n
p_le_n : p ≤ n
big : 2 * n < 3 * p
⊢ n ≤ 2 * n - n
[PROOFSTEP]
rw [two_mul, add_tsub_cancel_left]
[GOAL]
p n k : ℕ
h : n < p
⊢ ↑(factorization n !) p = 0
[PROOFSTEP]
induction' n with n hn
[GOAL]
case zero
p n k : ℕ
h✝ : n < p
h : zero < p
⊢ ↑(factorization zero !) p = 0
[PROOFSTEP]
simp
[GOAL]
case succ
p n✝ k : ℕ
h✝ : n✝ < p
n : ℕ
hn : n < p → ↑(factorization n !) p = 0
h : succ n < p
⊢ ↑(factorization (succ n)!) p = 0
[PROOFSTEP]
rw [factorial_succ, factorization_mul n.succ_ne_zero n.factorial_ne_zero, Finsupp.coe_add, Pi.add_apply,
  hn (lt_of_succ_lt h), add_zero, factorization_eq_zero_of_lt h]
[GOAL]
p n k : ℕ
h : n < p
⊢ ↑(factorization (choose n k)) p = 0
[PROOFSTEP]
by_cases hnk : n < k
[GOAL]
case pos
p n k : ℕ
h : n < p
hnk : n < k
⊢ ↑(factorization (choose n k)) p = 0
[PROOFSTEP]
simp [choose_eq_zero_of_lt hnk]
[GOAL]
case neg
p n k : ℕ
h : n < p
hnk : ¬n < k
⊢ ↑(factorization (choose n k)) p = 0
[PROOFSTEP]
rw [choose_eq_factorial_div_factorial (le_of_not_lt hnk),
  factorization_div (factorial_mul_factorial_dvd_factorial (le_of_not_lt hnk)), Finsupp.coe_tsub, Pi.sub_apply,
  factorization_factorial_eq_zero_of_lt h, zero_tsub]
[GOAL]
p n✝ k✝ n k : ℕ
hkn : k ≤ n
⊢ ∏ p in Finset.range (n + 1), p ^ ↑(factorization (choose n k)) p = choose n k
[PROOFSTEP]
conv =>
  -- Porting note: was `nth_rw_rhs`
  rhs
  rw [← factorization_prod_pow_eq_self (choose_pos hkn).ne']
[GOAL]
p n✝ k✝ n k : ℕ
hkn : k ≤ n
| ∏ p in Finset.range (n + 1), p ^ ↑(factorization (choose n k)) p = choose n k
[PROOFSTEP]
  rhs
  rw [← factorization_prod_pow_eq_self (choose_pos hkn).ne']
[GOAL]
p n✝ k✝ n k : ℕ
hkn : k ≤ n
| ∏ p in Finset.range (n + 1), p ^ ↑(factorization (choose n k)) p = choose n k
[PROOFSTEP]
  rhs
  rw [← factorization_prod_pow_eq_self (choose_pos hkn).ne']
[GOAL]
p n✝ k✝ n k : ℕ
hkn : k ≤ n
| ∏ p in Finset.range (n + 1), p ^ ↑(factorization (choose n k)) p = choose n k
[PROOFSTEP]
rhs
[GOAL]
p n✝ k✝ n k : ℕ
hkn : k ≤ n
| choose n k
[PROOFSTEP]
rw [← factorization_prod_pow_eq_self (choose_pos hkn).ne']
[GOAL]
p n✝ k✝ n k : ℕ
hkn : k ≤ n
⊢ ∏ p in Finset.range (n + 1), p ^ ↑(factorization (choose n k)) p =
    Finsupp.prod (factorization (choose n k)) fun x x_1 => x ^ x_1
[PROOFSTEP]
rw [eq_comm]
[GOAL]
p n✝ k✝ n k : ℕ
hkn : k ≤ n
⊢ (Finsupp.prod (factorization (choose n k)) fun x x_1 => x ^ x_1) =
    ∏ p in Finset.range (n + 1), p ^ ↑(factorization (choose n k)) p
[PROOFSTEP]
apply Finset.prod_subset
[GOAL]
case h
p n✝ k✝ n k : ℕ
hkn : k ≤ n
⊢ (factorization (choose n k)).support ⊆ Finset.range (n + 1)
[PROOFSTEP]
intro p hp
[GOAL]
case h
p✝ n✝ k✝ n k : ℕ
hkn : k ≤ n
p : ℕ
hp : p ∈ (factorization (choose n k)).support
⊢ p ∈ Finset.range (n + 1)
[PROOFSTEP]
rw [Finset.mem_range]
[GOAL]
case h
p✝ n✝ k✝ n k : ℕ
hkn : k ≤ n
p : ℕ
hp : p ∈ (factorization (choose n k)).support
⊢ p < n + 1
[PROOFSTEP]
contrapose! hp
[GOAL]
case h
p✝ n✝ k✝ n k : ℕ
hkn : k ≤ n
p : ℕ
hp : n + 1 ≤ p
⊢ ¬p ∈ (factorization (choose n k)).support
[PROOFSTEP]
rw [Finsupp.mem_support_iff, Classical.not_not, factorization_choose_eq_zero_of_lt hp]
[GOAL]
case hf
p n✝ k✝ n k : ℕ
hkn : k ≤ n
⊢ ∀ (x : ℕ),
    x ∈ Finset.range (n + 1) →
      ¬x ∈ (factorization (choose n k)).support → (fun x x_1 => x ^ x_1) x (↑(factorization (choose n k)) x) = 1
[PROOFSTEP]
intro p _ h2
[GOAL]
case hf
p✝ n✝ k✝ n k : ℕ
hkn : k ≤ n
p : ℕ
a✝ : p ∈ Finset.range (n + 1)
h2 : ¬p ∈ (factorization (choose n k)).support
⊢ (fun x x_1 => x ^ x_1) p (↑(factorization (choose n k)) p) = 1
[PROOFSTEP]
simp [Classical.not_not.1 (mt Finsupp.mem_support_iff.2 h2)]
[GOAL]
p n✝ k n : ℕ
⊢ ∏ p in Finset.range (2 * n + 1), p ^ ↑(factorization (centralBinom n)) p = centralBinom n
[PROOFSTEP]
apply prod_pow_factorization_choose
[GOAL]
case hkn
p n✝ k n : ℕ
⊢ n ≤ 2 * n
[PROOFSTEP]
linarith
