-- Mathlib/Data/Nat/Choose/Factorization.lean
theorem factorization_choose_of_lt_three_mul (hp' : p ≠ 2) (hk : p ≤ k) (hk' : p ≤ n - k)
    (hn : n < 3 * p) : (choose n k).factorization p = 0

Proof state:
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
⊢ (n.choose k).factorization p = 0

Tactic:
simp [choose_eq_zero_of_lt hnk]

Result:
no goals

Proof state:
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
⊢ (n.choose k).factorization p = 0

Tactic:
rcases em' p.Prime with hp | hp

Result:
case inl
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
hp : ¬Prime p
⊢ (n.choose k).factorization p = 0

case inr
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
hp : Prime p
⊢ (n.choose k).factorization p = 0

Proof state:
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

Tactic:
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]

Result:
no goals

Proof state:
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

Tactic:
calc
  n < 3 * p := hn
  _ ≤ p * p := mul_le_mul_right' this p
  _ = p ^ 2 := (sq p).symm
  _ ≤ p ^ i := pow_right_mono₀ hp.one_lt.le hi

Result:
no goals

Proof state:
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

Tactic:
have : 3 ≤ p := lt_of_le_of_ne hp.two_le hp'.symm

Result:
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

Proof state:
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

Tactic:
rw [pow_one, ← add_lt_add_iff_left (2 * p), ← succ_mul, two_mul, add_add_add_comm]

Result:
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

Proof state:
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

Tactic:
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])

Result:
no goals

Proof state:
case inl
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
hp : ¬Prime p
⊢ (n.choose k).factorization p = 0

Tactic:
exact factorization_eq_zero_of_non_prime (choose n k) hp

Result:
no goals

Proof state:
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

Tactic:
intro i hi

Result:
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

Proof state:
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
⊢ emultiplicity p (n.choose k) = 0

Tactic:
simp only [hp.emultiplicity_choose hkn (lt_add_one _), cast_eq_zero, Finset.card_eq_zero,
  Finset.filter_eq_empty_iff, not_le]

Result:
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

Proof state:
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
⊢ (n.choose k).factorization p = 0

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

Result:
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
⊢ emultiplicity p (n.choose k) = 0

Proof state:
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

Tactic:
rwa [div_add_mod, div_add_mod, add_tsub_cancel_of_le hkn]

Result:
no goals

Proof state:
case inr
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
hp : Prime p
⊢ (n.choose k).factorization p = 0

Tactic:
rcases lt_or_le n k with hnk | hkn

Result:
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
⊢ (n.choose k).factorization p = 0

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
⊢ (n.choose k).factorization p = 0

Proof state:
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

Tactic:
replace hn : n < p ^ i := by
  have : 3 ≤ p := lt_of_le_of_ne hp.two_le hp'.symm
  calc
    n < 3 * p := hn
    _ ≤ p * p := mul_le_mul_right' this p
    _ = p ^ 2 := (sq p).symm
    _ ≤ p ^ i := pow_right_mono₀ hp.one_lt.le hi

Result:
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

Proof state:
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

Tactic:
rcases eq_or_lt_of_le (Finset.mem_Ico.mp hi).1 with (rfl | hi)

Result:
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

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