[GOAL]
m n b : ℕ
hm : m ≠ 1
hn : 0 < n
hb : log m n < b
⊢ multiplicity m n = ↑(card (Ico 1 (Part.get (multiplicity m n) (_ : multiplicity.Finite m n) + 1)))
[PROOFSTEP]
simp
[GOAL]
m n b : ℕ
hm : m ≠ 1
hn : 0 < n
hb : log m n < b
i : ℕ
⊢ i ∈ Ico 1 (Part.get (multiplicity m n) (_ : multiplicity.Finite m n) + 1) ↔ i ∈ filter (fun i => m ^ i ∣ n) (Ico 1 b)
[PROOFSTEP]
rw [mem_filter, mem_Ico, mem_Ico, lt_succ_iff, ← @PartENat.coe_le_coe i, PartENat.natCast_get, ←
  pow_dvd_iff_le_multiplicity, and_right_comm]
[GOAL]
m n b : ℕ
hm : m ≠ 1
hn : 0 < n
hb : log m n < b
i : ℕ
⊢ 1 ≤ i ∧ m ^ i ∣ n ↔ (1 ≤ i ∧ m ^ i ∣ n) ∧ i < b
[PROOFSTEP]
refine' (and_iff_left_of_imp fun h => lt_of_le_of_lt _ hb).symm
[GOAL]
m n b : ℕ
hm : m ≠ 1
hn : 0 < n
hb : log m n < b
i : ℕ
h : 1 ≤ i ∧ m ^ i ∣ n
⊢ i ≤ log m n
[PROOFSTEP]
cases' m with m
[GOAL]
case zero
n b : ℕ
hn : 0 < n
i : ℕ
hm : zero ≠ 1
hb : log zero n < b
h : 1 ≤ i ∧ zero ^ i ∣ n
⊢ i ≤ log zero n
[PROOFSTEP]
rw [zero_eq, zero_pow, zero_dvd_iff] at h 
[GOAL]
case zero
n b : ℕ
hn : 0 < n
i : ℕ
hm : zero ≠ 1
hb : log zero n < b
h : 1 ≤ i ∧ n = 0
⊢ i ≤ log zero n
case zero n b : ℕ hn : 0 < n i : ℕ hm : zero ≠ 1 hb : log zero n < b h : 1 ≤ i ∧ 0 ^ i ∣ n ⊢ 0 < i
[PROOFSTEP]
exacts [(hn.ne' h.2).elim, h.1]
[GOAL]
case succ
n b : ℕ
hn : 0 < n
i m : ℕ
hm : succ m ≠ 1
hb : log (succ m) n < b
h : 1 ≤ i ∧ succ m ^ i ∣ n
⊢ i ≤ log (succ m) n
[PROOFSTEP]
exact le_log_of_pow_le (one_lt_iff_ne_zero_and_ne_one.2 ⟨m.succ_ne_zero, hm⟩) (le_of_dvd hn h.2)
[GOAL]
p : ℕ
hp : Prime p
b : ℕ
x✝ : log p 0 < b
⊢ multiplicity p 0! = ↑(∑ i in Ico 1 b, 0 / p ^ i)
[PROOFSTEP]
simp [Ico, hp.multiplicity_one]
[GOAL]
p : ℕ
hp : Prime p
n b : ℕ
hb : log p (n + 1) < b
⊢ multiplicity p (n + 1)! = multiplicity p n ! + multiplicity p (n + 1)
[PROOFSTEP]
rw [factorial_succ, hp.multiplicity_mul, add_comm]
[GOAL]
p : ℕ
hp : Prime p
n b : ℕ
hb : log p (n + 1) < b
⊢ multiplicity p n ! + multiplicity p (n + 1) =
    ↑(∑ i in Ico 1 b, n / p ^ i) + ↑(card (filter (fun i => p ^ i ∣ n + 1) (Ico 1 b)))
[PROOFSTEP]
rw [multiplicity_factorial hp ((log_mono_right <| le_succ _).trans_lt hb), ←
  multiplicity_eq_card_pow_dvd hp.ne_one (succ_pos _) hb]
[GOAL]
p : ℕ
hp : Prime p
n b : ℕ
hb : log p (n + 1) < b
⊢ ↑(∑ i in Ico 1 b, n / p ^ i) + ↑(card (filter (fun i => p ^ i ∣ n + 1) (Ico 1 b))) =
    ↑(∑ i in Ico 1 b, (n / p ^ i + if p ^ i ∣ n + 1 then 1 else 0))
[PROOFSTEP]
rw [sum_add_distrib, sum_boole]
[GOAL]
p : ℕ
hp : Prime p
n b : ℕ
hb : log p (n + 1) < b
⊢ ↑(∑ i in Ico 1 b, n / p ^ i) + ↑(card (filter (fun i => p ^ i ∣ n + 1) (Ico 1 b))) =
    ↑(∑ x in Ico 1 b, n / p ^ x + ↑(card (filter (fun x => p ^ x ∣ n + 1) (Ico 1 b))))
[PROOFSTEP]
simp
[GOAL]
n p : ℕ
hp : Prime p
⊢ multiplicity p (p * (n + 1))! = multiplicity p (p * n)! + multiplicity p (n + 1) + 1
[PROOFSTEP]
have hp' := hp.prime
[GOAL]
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
⊢ multiplicity p (p * (n + 1))! = multiplicity p (p * n)! + multiplicity p (n + 1) + 1
[PROOFSTEP]
have h0 : 2 ≤ p := hp.two_le
[GOAL]
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
⊢ multiplicity p (p * (n + 1))! = multiplicity p (p * n)! + multiplicity p (n + 1) + 1
[PROOFSTEP]
have h1 : 1 ≤ p * n + 1 := Nat.le_add_left _ _
[GOAL]
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
⊢ multiplicity p (p * (n + 1))! = multiplicity p (p * n)! + multiplicity p (n + 1) + 1
[PROOFSTEP]
have h2 : p * n + 1 ≤ p * (n + 1)
[GOAL]
case h2
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
⊢ p * n + 1 ≤ p * (n + 1)
[PROOFSTEP]
linarith
[GOAL]
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
⊢ multiplicity p (p * (n + 1))! = multiplicity p (p * n)! + multiplicity p (n + 1) + 1
[PROOFSTEP]
have h3 : p * n + 1 ≤ p * (n + 1) + 1
[GOAL]
case h3
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
⊢ p * n + 1 ≤ p * (n + 1) + 1
[PROOFSTEP]
linarith
[GOAL]
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
⊢ multiplicity p (p * (n + 1))! = multiplicity p (p * n)! + multiplicity p (n + 1) + 1
[PROOFSTEP]
have hm : multiplicity p (p * n)! ≠ ⊤ :=
  by
  rw [Ne.def, eq_top_iff_not_finite, Classical.not_not, finite_nat_iff]
  exact ⟨hp.ne_one, factorial_pos _⟩
[GOAL]
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
⊢ multiplicity p (p * n)! ≠ ⊤
[PROOFSTEP]
rw [Ne.def, eq_top_iff_not_finite, Classical.not_not, finite_nat_iff]
[GOAL]
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
⊢ p ≠ 1 ∧ 0 < (p * n)!
[PROOFSTEP]
exact ⟨hp.ne_one, factorial_pos _⟩
[GOAL]
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
hm : multiplicity p (p * n)! ≠ ⊤
⊢ multiplicity p (p * (n + 1))! = multiplicity p (p * n)! + multiplicity p (n + 1) + 1
[PROOFSTEP]
revert hm
[GOAL]
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
⊢ multiplicity p (p * n)! ≠ ⊤ → multiplicity p (p * (n + 1))! = multiplicity p (p * n)! + multiplicity p (n + 1) + 1
[PROOFSTEP]
have h4 : ∀ m ∈ Ico (p * n + 1) (p * (n + 1)), multiplicity p m = 0 :=
  by
  intro m hm
  rw [multiplicity_eq_zero, ← not_dvd_iff_between_consec_multiples _ hp.pos]
  rw [mem_Ico] at hm 
  exact ⟨n, lt_of_succ_le hm.1, hm.2⟩
[GOAL]
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
⊢ ∀ (m : ℕ), m ∈ Ico (p * n + 1) (p * (n + 1)) → multiplicity p m = 0
[PROOFSTEP]
intro m hm
[GOAL]
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
m : ℕ
hm : m ∈ Ico (p * n + 1) (p * (n + 1))
⊢ multiplicity p m = 0
[PROOFSTEP]
rw [multiplicity_eq_zero, ← not_dvd_iff_between_consec_multiples _ hp.pos]
[GOAL]
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
m : ℕ
hm : m ∈ Ico (p * n + 1) (p * (n + 1))
⊢ ∃ k, p * k < m ∧ m < p * (k + 1)
[PROOFSTEP]
rw [mem_Ico] at hm 
[GOAL]
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
m : ℕ
hm : p * n + 1 ≤ m ∧ m < p * (n + 1)
⊢ ∃ k, p * k < m ∧ m < p * (k + 1)
[PROOFSTEP]
exact ⟨n, lt_of_succ_le hm.1, hm.2⟩
[GOAL]
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
h4 : ∀ (m : ℕ), m ∈ Ico (p * n + 1) (p * (n + 1)) → multiplicity p m = 0
⊢ multiplicity p (p * n)! ≠ ⊤ → multiplicity p (p * (n + 1))! = multiplicity p (p * n)! + multiplicity p (n + 1) + 1
[PROOFSTEP]
simp_rw [← prod_Ico_id_eq_factorial, multiplicity.Finset.prod hp', ← sum_Ico_consecutive _ h1 h3, add_assoc]
[GOAL]
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
h4 : ∀ (m : ℕ), m ∈ Ico (p * n + 1) (p * (n + 1)) → multiplicity p m = 0
⊢ ∑ x in Ico 1 (p * n + 1), multiplicity p x ≠ ⊤ →
    ∑ x in Ico 1 (p * n + 1), multiplicity p x + ∑ x in Ico (p * n + 1) (p * (n + 1) + 1), multiplicity p x =
      ∑ x in Ico 1 (p * n + 1), multiplicity p x + (multiplicity p (n + 1) + 1)
[PROOFSTEP]
intro h
[GOAL]
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
h4 : ∀ (m : ℕ), m ∈ Ico (p * n + 1) (p * (n + 1)) → multiplicity p m = 0
h : ∑ x in Ico 1 (p * n + 1), multiplicity p x ≠ ⊤
⊢ ∑ x in Ico 1 (p * n + 1), multiplicity p x + ∑ x in Ico (p * n + 1) (p * (n + 1) + 1), multiplicity p x =
    ∑ x in Ico 1 (p * n + 1), multiplicity p x + (multiplicity p (n + 1) + 1)
[PROOFSTEP]
rw [PartENat.add_left_cancel_iff h, sum_Ico_succ_top h2, multiplicity.mul hp', hp.multiplicity_self, sum_congr rfl h4,
  sum_const_zero, zero_add, add_comm (1 : PartENat)]
[GOAL]
n p : ℕ
hp : Prime p
⊢ multiplicity p (p * n)! = multiplicity p n ! + ↑n
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
p : ℕ
hp : Prime p
⊢ multiplicity p (p * zero)! = multiplicity p zero ! + ↑zero
[PROOFSTEP]
simp
[GOAL]
case succ
p : ℕ
hp : Prime p
n : ℕ
ih : multiplicity p (p * n)! = multiplicity p n ! + ↑n
⊢ multiplicity p (p * succ n)! = multiplicity p (succ n)! + ↑(succ n)
[PROOFSTEP]
simp only [succ_eq_add_one, multiplicity.mul, hp, hp.prime, ih, multiplicity_factorial_mul_succ, ← add_assoc,
  Nat.cast_one, Nat.cast_add, factorial_succ]
[GOAL]
case succ
p : ℕ
hp : Prime p
n : ℕ
ih : multiplicity p (p * n)! = multiplicity p n ! + ↑n
⊢ multiplicity p n ! + ↑n + multiplicity p (n + 1) + 1 = multiplicity p (n + 1) + multiplicity p n ! + ↑n + 1
[PROOFSTEP]
congr 1
[GOAL]
case succ.e_a
p : ℕ
hp : Prime p
n : ℕ
ih : multiplicity p (p * n)! = multiplicity p n ! + ↑n
⊢ multiplicity p n ! + ↑n + multiplicity p (n + 1) = multiplicity p (n + 1) + multiplicity p n ! + ↑n
[PROOFSTEP]
rw [add_comm, add_assoc]
[GOAL]
p n r b : ℕ
hp : Prime p
hbn : log p n < b
⊢ p ^ r ∣ n ! ↔ r ≤ ∑ i in Ico 1 b, n / p ^ i
[PROOFSTEP]
rw [← PartENat.coe_le_coe, ← hp.multiplicity_factorial hbn, ← pow_dvd_iff_le_multiplicity]
[GOAL]
p : ℕ
hp : Prime p
n : ℕ
⊢ multiplicity p n ! ≤ ↑(n / (p - 1))
[PROOFSTEP]
rw [hp.multiplicity_factorial (lt_succ_self _), PartENat.coe_le_coe]
[GOAL]
p : ℕ
hp : Prime p
n : ℕ
⊢ ∑ i in Ico 1 (succ (log p n)), n / p ^ i ≤ n / (p - 1)
[PROOFSTEP]
exact Nat.geom_sum_Ico_le hp.two_le _ _
[GOAL]
p n b k : ℕ
hp : Prime p
hkn : k ≤ n
⊢ ∑ i in Ico 1 b, n / p ^ i = ∑ i in Ico 1 b, (k + (n - k)) / p ^ i
[PROOFSTEP]
simp only [add_tsub_cancel_of_le hkn]
[GOAL]
p n b k : ℕ
hp : Prime p
hkn : k ≤ n
⊢ ∑ i in Ico 1 b, (k + (n - k)) / p ^ i =
    ∑ i in Ico 1 b, (k / p ^ i + (n - k) / p ^ i + if p ^ i ≤ k % p ^ i + (n - k) % p ^ i then 1 else 0)
[PROOFSTEP]
simp only [Nat.add_div (pow_pos hp.pos _)]
[GOAL]
p n b k : ℕ
hp : Prime p
hkn : k ≤ n
⊢ ∑ i in Ico 1 b, (k / p ^ i + (n - k) / p ^ i + if p ^ i ≤ k % p ^ i + (n - k) % p ^ i then 1 else 0) =
    ∑ i in Ico 1 b, k / p ^ i + ∑ i in Ico 1 b, (n - k) / p ^ i +
      card (filter (fun i => p ^ i ≤ k % p ^ i + (n - k) % p ^ i) (Ico 1 b))
[PROOFSTEP]
simp [sum_add_distrib, sum_boole]
[GOAL]
p n k b : ℕ
hp : Prime p
hkn : k ≤ n
hnb : log p n < b
⊢ multiplicity p (choose n k) = ↑(card (filter (fun i => p ^ i ≤ k % p ^ i + (n - k) % p ^ i) (Ico 1 b)))
[PROOFSTEP]
have h₁ :
  multiplicity p (choose n k) + multiplicity p (k ! * (n - k)!) =
    ((Finset.Ico 1 b).filter fun i => p ^ i ≤ k % p ^ i + (n - k) % p ^ i).card + multiplicity p (k ! * (n - k)!) :=
  by
  rw [← hp.multiplicity_mul, ← mul_assoc, choose_mul_factorial_mul_factorial hkn, hp.multiplicity_factorial hnb,
    hp.multiplicity_mul, hp.multiplicity_factorial ((log_mono_right hkn).trans_lt hnb),
    hp.multiplicity_factorial (lt_of_le_of_lt (log_mono_right tsub_le_self) hnb), multiplicity_choose_aux hp hkn]
  simp [add_comm]
[GOAL]
p n k b : ℕ
hp : Prime p
hkn : k ≤ n
hnb : log p n < b
⊢ multiplicity p (choose n k) + multiplicity p (k ! * (n - k)!) =
    ↑(card (filter (fun i => p ^ i ≤ k % p ^ i + (n - k) % p ^ i) (Ico 1 b))) + multiplicity p (k ! * (n - k)!)
[PROOFSTEP]
rw [← hp.multiplicity_mul, ← mul_assoc, choose_mul_factorial_mul_factorial hkn, hp.multiplicity_factorial hnb,
  hp.multiplicity_mul, hp.multiplicity_factorial ((log_mono_right hkn).trans_lt hnb),
  hp.multiplicity_factorial (lt_of_le_of_lt (log_mono_right tsub_le_self) hnb), multiplicity_choose_aux hp hkn]
[GOAL]
p n k b : ℕ
hp : Prime p
hkn : k ≤ n
hnb : log p n < b
⊢ ↑(∑ i in Ico 1 b, k / p ^ i + ∑ i in Ico 1 b, (n - k) / p ^ i +
        card (filter (fun i => p ^ i ≤ k % p ^ i + (n - k) % p ^ i) (Ico 1 b))) =
    ↑(card (filter (fun i => p ^ i ≤ k % p ^ i + (n - k) % p ^ i) (Ico 1 b))) +
      (↑(∑ i in Ico 1 b, k / p ^ i) + ↑(∑ i in Ico 1 b, (n - k) / p ^ i))
[PROOFSTEP]
simp [add_comm]
[GOAL]
p n k b : ℕ
hp : Prime p
hkn : k ≤ n
hnb : log p n < b
h₁ :
  multiplicity p (choose n k) + multiplicity p (k ! * (n - k)!) =
    ↑(card (filter (fun i => p ^ i ≤ k % p ^ i + (n - k) % p ^ i) (Ico 1 b))) + multiplicity p (k ! * (n - k)!)
⊢ multiplicity p (choose n k) = ↑(card (filter (fun i => p ^ i ≤ k % p ^ i + (n - k) % p ^ i) (Ico 1 b)))
[PROOFSTEP]
refine (PartENat.add_right_cancel_iff ?_).1 h₁
[GOAL]
p n k b : ℕ
hp : Prime p
hkn : k ≤ n
hnb : log p n < b
h₁ :
  multiplicity p (choose n k) + multiplicity p (k ! * (n - k)!) =
    ↑(card (filter (fun i => p ^ i ≤ k % p ^ i + (n - k) % p ^ i) (Ico 1 b))) + multiplicity p (k ! * (n - k)!)
⊢ multiplicity p (k ! * (n - k)!) ≠ ⊤
[PROOFSTEP]
apply PartENat.ne_top_iff_dom.2
[GOAL]
p n k b : ℕ
hp : Prime p
hkn : k ≤ n
hnb : log p n < b
h₁ :
  multiplicity p (choose n k) + multiplicity p (k ! * (n - k)!) =
    ↑(card (filter (fun i => p ^ i ≤ k % p ^ i + (n - k) % p ^ i) (Ico 1 b))) + multiplicity p (k ! * (n - k)!)
⊢ (multiplicity p (k ! * (n - k)!)).Dom
[PROOFSTEP]
exact finite_nat_iff.2 ⟨hp.ne_one, mul_pos (factorial_pos k) (factorial_pos (n - k))⟩
[GOAL]
p : ℕ
hp : Prime p
x✝ : ℕ
⊢ multiplicity p x✝ ≤ multiplicity p (choose x✝ 0) + multiplicity p 0
[PROOFSTEP]
simp
[GOAL]
p : ℕ
hp : Prime p
n✝ : ℕ
⊢ multiplicity p 0 ≤ multiplicity p (choose 0 (n✝ + 1)) + multiplicity p (n✝ + 1)
[PROOFSTEP]
simp
[GOAL]
p : ℕ
hp : Prime p
n k : ℕ
⊢ multiplicity p (n + 1) ≤ multiplicity p (choose (n + 1) (k + 1)) + multiplicity p (k + 1)
[PROOFSTEP]
rw [← hp.multiplicity_mul]
[GOAL]
p : ℕ
hp : Prime p
n k : ℕ
⊢ multiplicity p (n + 1) ≤ multiplicity p (choose (n + 1) (k + 1) * (k + 1))
[PROOFSTEP]
refine' multiplicity_le_multiplicity_of_dvd_right _
[GOAL]
p : ℕ
hp : Prime p
n k : ℕ
⊢ n + 1 ∣ choose (n + 1) (k + 1) * (k + 1)
[PROOFSTEP]
rw [← succ_mul_choose_eq]
[GOAL]
p : ℕ
hp : Prime p
n k : ℕ
⊢ n + 1 ∣ succ n * choose n k
[PROOFSTEP]
exact dvd_mul_right _ _
[GOAL]
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
⊢ multiplicity p (choose (p ^ n) k) + multiplicity p k ≤ ↑n
[PROOFSTEP]
have hdisj :
  Disjoint ((Ico 1 n.succ).filter fun i => p ^ i ≤ k % p ^ i + (p ^ n - k) % p ^ i)
    ((Ico 1 n.succ).filter fun i => p ^ i ∣ k) :=
  by simp (config := { contextual := true }) [disjoint_right, *, dvd_iff_mod_eq_zero, Nat.mod_lt _ (pow_pos hp.pos _)]
[GOAL]
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
⊢ Disjoint (filter (fun i => p ^ i ≤ k % p ^ i + (p ^ n - k) % p ^ i) (Ico 1 (succ n)))
    (filter (fun i => p ^ i ∣ k) (Ico 1 (succ n)))
[PROOFSTEP]
simp (config := { contextual := true }) [disjoint_right, *, dvd_iff_mod_eq_zero, Nat.mod_lt _ (pow_pos hp.pos _)]
[GOAL]
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
hdisj :
  Disjoint (filter (fun i => p ^ i ≤ k % p ^ i + (p ^ n - k) % p ^ i) (Ico 1 (succ n)))
    (filter (fun i => p ^ i ∣ k) (Ico 1 (succ n)))
⊢ multiplicity p (choose (p ^ n) k) + multiplicity p k ≤ ↑n
[PROOFSTEP]
rw [multiplicity_choose hp hkn (lt_succ_self _),
  multiplicity_eq_card_pow_dvd (ne_of_gt hp.one_lt) hk0.bot_lt (lt_succ_of_le (log_mono_right hkn)), ← Nat.cast_add,
  PartENat.coe_le_coe, log_pow hp.one_lt, ← card_disjoint_union hdisj, filter_union_right]
[GOAL]
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
hdisj :
  Disjoint (filter (fun i => p ^ i ≤ k % p ^ i + (p ^ n - k) % p ^ i) (Ico 1 (succ n)))
    (filter (fun i => p ^ i ∣ k) (Ico 1 (succ n)))
⊢ card (filter (fun x => p ^ x ≤ k % p ^ x + (p ^ n - k) % p ^ x ∨ p ^ x ∣ k) (Ico 1 (succ n))) ≤ n
[PROOFSTEP]
have filter_le_Ico := (Ico 1 n.succ).card_filter_le fun x => p ^ x ≤ k % p ^ x + (p ^ n - k) % p ^ x ∨ p ^ x ∣ k
[GOAL]
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
hdisj :
  Disjoint (filter (fun i => p ^ i ≤ k % p ^ i + (p ^ n - k) % p ^ i) (Ico 1 (succ n)))
    (filter (fun i => p ^ i ∣ k) (Ico 1 (succ n)))
filter_le_Ico :
  card (filter (fun x => p ^ x ≤ k % p ^ x + (p ^ n - k) % p ^ x ∨ p ^ x ∣ k) (Ico 1 (succ n))) ≤ card (Ico 1 (succ n))
⊢ card (filter (fun x => p ^ x ≤ k % p ^ x + (p ^ n - k) % p ^ x ∨ p ^ x ∣ k) (Ico 1 (succ n))) ≤ n
[PROOFSTEP]
rwa [card_Ico 1 n.succ] at filter_le_Ico 
[GOAL]
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
⊢ ↑n ≤ multiplicity p (choose (p ^ n) k) + multiplicity p k
[PROOFSTEP]
rw [← hp.multiplicity_pow_self]
[GOAL]
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
⊢ multiplicity p (p ^ n) ≤ multiplicity p (choose (p ^ n) k) + multiplicity p k
[PROOFSTEP]
exact multiplicity_le_multiplicity_choose_add hp _ _
[GOAL]
p n k : ℕ
hp : Prime p
hk : k ≠ 0
hkp : k ≠ p ^ n
⊢ p ∣ choose (p ^ n) k
[PROOFSTEP]
obtain hkp | hkp := hkp.symm.lt_or_lt
[GOAL]
case inl
p n k : ℕ
hp : Prime p
hk : k ≠ 0
hkp✝ : k ≠ p ^ n
hkp : p ^ n < k
⊢ p ∣ choose (p ^ n) k
[PROOFSTEP]
simp [choose_eq_zero_of_lt hkp]
[GOAL]
case inr
p n k : ℕ
hp : Prime p
hk : k ≠ 0
hkp✝ : k ≠ p ^ n
hkp : k < p ^ n
⊢ p ∣ choose (p ^ n) k
[PROOFSTEP]
refine' multiplicity_ne_zero.1 fun h => hkp.not_le <| Nat.le_of_dvd hk.bot_lt _
[GOAL]
case inr
p n k : ℕ
hp : Prime p
hk : k ≠ 0
hkp✝ : k ≠ p ^ n
hkp : k < p ^ n
h : multiplicity p (choose (p ^ n) k) = 0
⊢ p ^ n ∣ k
[PROOFSTEP]
have H := hp.multiplicity_choose_prime_pow_add_multiplicity hkp.le hk
[GOAL]
case inr
p n k : ℕ
hp : Prime p
hk : k ≠ 0
hkp✝ : k ≠ p ^ n
hkp : k < p ^ n
h : multiplicity p (choose (p ^ n) k) = 0
H : multiplicity p (choose (p ^ n) k) + multiplicity p k = ↑n
⊢ p ^ n ∣ k
[PROOFSTEP]
rw [h, zero_add, eq_coe_iff] at H 
[GOAL]
case inr
p n k : ℕ
hp : Prime p
hk : k ≠ 0
hkp✝ : k ≠ p ^ n
hkp : k < p ^ n
h : multiplicity p (choose (p ^ n) k) = 0
H : p ^ n ∣ k ∧ ¬p ^ (n + 1) ∣ k
⊢ p ^ n ∣ k
[PROOFSTEP]
exact H.1
[GOAL]
p n k : ℕ
hp : Prime p
⊢ p ∣ choose (p ^ n) k ↔ k ≠ 0 ∧ k ≠ p ^ n
[PROOFSTEP]
refine' ⟨fun h => ⟨_, _⟩, fun h => dvd_choose_pow hp h.1 h.2⟩
[GOAL]
case refine'_1
p n k : ℕ
hp : Prime p
h : p ∣ choose (p ^ n) k
⊢ k ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
case refine'_2
p n k : ℕ
hp : Prime p
h : p ∣ choose (p ^ n) k
⊢ k ≠ p ^ n
[PROOFSTEP]
rintro rfl
[GOAL]
case refine'_1
p n : ℕ
hp : Prime p
h : p ∣ choose (p ^ n) 0
⊢ False
[PROOFSTEP]
simp [hp.ne_one] at h 
[GOAL]
case refine'_2
p n : ℕ
hp : Prime p
h : p ∣ choose (p ^ n) (p ^ n)
⊢ False
[PROOFSTEP]
simp [hp.ne_one] at h 
[GOAL]
⊢ ∀ {n : ℕ}, n ≠ 0 → multiplicity 2 n ! < ↑n
[PROOFSTEP]
have h2 := prime_two.prime
[GOAL]
h2 : _root_.Prime 2
⊢ ∀ {n : ℕ}, n ≠ 0 → multiplicity 2 n ! < ↑n
[PROOFSTEP]
refine' binaryRec _ _
[GOAL]
case refine'_1
h2 : _root_.Prime 2
⊢ 0 ≠ 0 → multiplicity 2 0! < ↑0
[PROOFSTEP]
exact fun h => False.elim <| h rfl
[GOAL]
case refine'_2
h2 : _root_.Prime 2
⊢ ∀ (b : Bool) (n : ℕ), (n ≠ 0 → multiplicity 2 n ! < ↑n) → bit b n ≠ 0 → multiplicity 2 (bit b n)! < ↑(bit b n)
[PROOFSTEP]
intro b n ih h
[GOAL]
case refine'_2
h2 : _root_.Prime 2
b : Bool
n : ℕ
ih : n ≠ 0 → multiplicity 2 n ! < ↑n
h : bit b n ≠ 0
⊢ multiplicity 2 (bit b n)! < ↑(bit b n)
[PROOFSTEP]
by_cases hn : n = 0
[GOAL]
case pos
h2 : _root_.Prime 2
b : Bool
n : ℕ
ih : n ≠ 0 → multiplicity 2 n ! < ↑n
h : bit b n ≠ 0
hn : n = 0
⊢ multiplicity 2 (bit b n)! < ↑(bit b n)
[PROOFSTEP]
subst hn
[GOAL]
case pos
h2 : _root_.Prime 2
b : Bool
ih : 0 ≠ 0 → multiplicity 2 0! < ↑0
h : bit b 0 ≠ 0
⊢ multiplicity 2 (bit b 0)! < ↑(bit b 0)
[PROOFSTEP]
simp only [ne_eq, bit_eq_zero, true_and, Bool.not_eq_false] at h 
[GOAL]
case pos
h2 : _root_.Prime 2
b : Bool
ih : 0 ≠ 0 → multiplicity 2 0! < ↑0
h : b = true
⊢ multiplicity 2 (bit b 0)! < ↑(bit b 0)
[PROOFSTEP]
simp only [h, bit_true, bit1_zero, factorial, mul_one, Nat.isUnit_iff, cast_one]
[GOAL]
case pos
h2 : _root_.Prime 2
b : Bool
ih : 0 ≠ 0 → multiplicity 2 0! < ↑0
h : b = true
⊢ multiplicity 2 (succ 0) < 1
[PROOFSTEP]
rw [Prime.multiplicity_one]
[GOAL]
case pos
h2 : _root_.Prime 2
b : Bool
ih : 0 ≠ 0 → multiplicity 2 0! < ↑0
h : b = true
⊢ 0 < 1
case pos h2 : _root_.Prime 2 b : Bool ih : 0 ≠ 0 → multiplicity 2 0! < ↑0 h : b = true ⊢ Prime 2
[PROOFSTEP]
simp only [zero_lt_one]
[GOAL]
case pos
h2 : _root_.Prime 2
b : Bool
ih : 0 ≠ 0 → multiplicity 2 0! < ↑0
h : b = true
⊢ Prime 2
[PROOFSTEP]
decide
[GOAL]
case neg
h2 : _root_.Prime 2
b : Bool
n : ℕ
ih : n ≠ 0 → multiplicity 2 n ! < ↑n
h : bit b n ≠ 0
hn : ¬n = 0
⊢ multiplicity 2 (bit b n)! < ↑(bit b n)
[PROOFSTEP]
have : multiplicity 2 (2 * n)! < (2 * n : ℕ) :=
  by
  rw [prime_two.multiplicity_factorial_mul]
  refine' (PartENat.add_lt_add_right (ih hn) (PartENat.natCast_ne_top _)).trans_le _
  rw [two_mul]
  norm_cast
[GOAL]
h2 : _root_.Prime 2
b : Bool
n : ℕ
ih : n ≠ 0 → multiplicity 2 n ! < ↑n
h : bit b n ≠ 0
hn : ¬n = 0
⊢ multiplicity 2 (2 * n)! < ↑(2 * n)
[PROOFSTEP]
rw [prime_two.multiplicity_factorial_mul]
[GOAL]
h2 : _root_.Prime 2
b : Bool
n : ℕ
ih : n ≠ 0 → multiplicity 2 n ! < ↑n
h : bit b n ≠ 0
hn : ¬n = 0
⊢ multiplicity 2 n ! + ↑n < ↑(2 * n)
[PROOFSTEP]
refine' (PartENat.add_lt_add_right (ih hn) (PartENat.natCast_ne_top _)).trans_le _
[GOAL]
h2 : _root_.Prime 2
b : Bool
n : ℕ
ih : n ≠ 0 → multiplicity 2 n ! < ↑n
h : bit b n ≠ 0
hn : ¬n = 0
⊢ ↑n + ↑n ≤ ↑(2 * n)
[PROOFSTEP]
rw [two_mul]
[GOAL]
h2 : _root_.Prime 2
b : Bool
n : ℕ
ih : n ≠ 0 → multiplicity 2 n ! < ↑n
h : bit b n ≠ 0
hn : ¬n = 0
⊢ ↑n + ↑n ≤ ↑(n + n)
[PROOFSTEP]
norm_cast
[GOAL]
case neg
h2 : _root_.Prime 2
b : Bool
n : ℕ
ih : n ≠ 0 → multiplicity 2 n ! < ↑n
h : bit b n ≠ 0
hn : ¬n = 0
this : multiplicity 2 (2 * n)! < ↑(2 * n)
⊢ multiplicity 2 (bit b n)! < ↑(bit b n)
[PROOFSTEP]
cases b
[GOAL]
case neg.false
h2 : _root_.Prime 2
n : ℕ
ih : n ≠ 0 → multiplicity 2 n ! < ↑n
hn : ¬n = 0
this : multiplicity 2 (2 * n)! < ↑(2 * n)
h : bit false n ≠ 0
⊢ multiplicity 2 (bit false n)! < ↑(bit false n)
[PROOFSTEP]
simpa [bit0_eq_two_mul n]
[GOAL]
case neg.true
h2 : _root_.Prime 2
n : ℕ
ih : n ≠ 0 → multiplicity 2 n ! < ↑n
hn : ¬n = 0
this : multiplicity 2 (2 * n)! < ↑(2 * n)
h : bit true n ≠ 0
⊢ multiplicity 2 (bit true n)! < ↑(bit true n)
[PROOFSTEP]
suffices multiplicity 2 (2 * n + 1) + multiplicity 2 (2 * n)! < ↑(2 * n) + 1 by
  simpa [succ_eq_add_one, multiplicity.mul, h2, prime_two, Nat.bit1_eq_succ_bit0, bit0_eq_two_mul n]
[GOAL]
h2 : _root_.Prime 2
n : ℕ
ih : n ≠ 0 → multiplicity 2 n ! < ↑n
hn : ¬n = 0
this✝ : multiplicity 2 (2 * n)! < ↑(2 * n)
h : bit true n ≠ 0
this : multiplicity 2 (2 * n + 1) + multiplicity 2 (2 * n)! < ↑(2 * n) + 1
⊢ multiplicity 2 (bit true n)! < ↑(bit true n)
[PROOFSTEP]
simpa [succ_eq_add_one, multiplicity.mul, h2, prime_two, Nat.bit1_eq_succ_bit0, bit0_eq_two_mul n]
[GOAL]
case neg.true
h2 : _root_.Prime 2
n : ℕ
ih : n ≠ 0 → multiplicity 2 n ! < ↑n
hn : ¬n = 0
this : multiplicity 2 (2 * n)! < ↑(2 * n)
h : bit true n ≠ 0
⊢ multiplicity 2 (2 * n + 1) + multiplicity 2 (2 * n)! < ↑(2 * n) + 1
[PROOFSTEP]
rw [multiplicity_eq_zero.2 (two_not_dvd_two_mul_add_one n), zero_add]
[GOAL]
case neg.true
h2 : _root_.Prime 2
n : ℕ
ih : n ≠ 0 → multiplicity 2 n ! < ↑n
hn : ¬n = 0
this : multiplicity 2 (2 * n)! < ↑(2 * n)
h : bit true n ≠ 0
⊢ multiplicity 2 (2 * n)! < ↑(2 * n) + 1
[PROOFSTEP]
refine' this.trans _
[GOAL]
case neg.true
h2 : _root_.Prime 2
n : ℕ
ih : n ≠ 0 → multiplicity 2 n ! < ↑n
hn : ¬n = 0
this : multiplicity 2 (2 * n)! < ↑(2 * n)
h : bit true n ≠ 0
⊢ ↑(2 * n) < ↑(2 * n) + 1
[PROOFSTEP]
exact_mod_cast lt_succ_self _
