-- Mathlib/Data/Nat/Multiplicity.lean
theorem emultiplicity_choose' {p n k b : ℕ} (hp : p.Prime) (hnb : log p (n + k) < b) :
    emultiplicity p (choose (n + k) k) = #{i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i}

Proof state:
p n k b : ℕ
hp : Prime p
hnb : log p (n + k) < b
h₁ :
  emultiplicity p ((n + k).choose k) + emultiplicity p (k ! * n !) =
    ↑(#(filter (fun i => p ^ i ≤ k % p ^ i + n % p ^ i) (Ico 1 b))) + emultiplicity p (k ! * n !)
⊢ emultiplicity p (k ! * n !) ≠ ⊤

Tactic:
apply finiteMultiplicity_iff_emultiplicity_ne_top.1

Result:
p n k b : ℕ
hp : Prime p
hnb : log p (n + k) < b
h₁ :
  emultiplicity p ((n + k).choose k) + emultiplicity p (k ! * n !) =
    ↑(#(filter (fun i => p ^ i ≤ k % p ^ i + n % p ^ i) (Ico 1 b))) + emultiplicity p (k ! * n !)
⊢ FiniteMultiplicity p (k ! * n !)

Proof state:
p n k b : ℕ
hp : Prime p
hnb : log p (n + k) < b
⊢ emultiplicity p ((n + k).choose k * k ! * n !) =
    ↑(#(filter (fun i => p ^ i ≤ k % p ^ i + n % p ^ i) (Ico 1 b))) + emultiplicity p (k ! * n !)

Tactic:
have := (add_tsub_cancel_right n k) ▸ choose_mul_factorial_mul_factorial (le_add_left k n)

Result:
p n k b : ℕ
hp : Prime p
hnb : log p (n + k) < b
this : (n + k).choose k * k ! * n ! = (n + k)!
⊢ emultiplicity p ((n + k).choose k * k ! * n !) =
    ↑(#(filter (fun i => p ^ i ≤ k % p ^ i + n % p ^ i) (Ico 1 b))) + emultiplicity p (k ! * n !)

Proof state:
p n k b : ℕ
hp : Prime p
hnb : log p (n + k) < b
⊢ emultiplicity p ((n + k).choose k) = ↑(#(filter (fun i => p ^ i ≤ k % p ^ i + n % p ^ i) (Ico 1 b)))

Tactic:
have h₁ :
    emultiplicity p (choose (n + k) k) + emultiplicity p (k ! * n !) =
      #{i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i} + emultiplicity p (k ! * n !) := by
  rw [← hp.emultiplicity_mul, ← mul_assoc]
  have := (add_tsub_cancel_right n k) ▸ choose_mul_factorial_mul_factorial (le_add_left k n)
  rw [this, hp.emultiplicity_factorial hnb, hp.emultiplicity_mul,
    hp.emultiplicity_factorial ((log_mono_right (le_add_left k n)).trans_lt hnb),
    hp.emultiplicity_factorial ((log_mono_right (le_add_left n k)).trans_lt
    (add_comm n k ▸ hnb)), multiplicity_choose_aux hp (le_add_left k n)]
  simp [add_comm]

Result:
p n k b : ℕ
hp : Prime p
hnb : log p (n + k) < b
h₁ :
  emultiplicity p ((n + k).choose k) + emultiplicity p (k ! * n !) =
    ↑(#(filter (fun i => p ^ i ≤ k % p ^ i + n % p ^ i) (Ico 1 b))) + emultiplicity p (k ! * n !)
⊢ emultiplicity p ((n + k).choose k) = ↑(#(filter (fun i => p ^ i ≤ k % p ^ i + n % p ^ i) (Ico 1 b)))

Proof state:
p n k b : ℕ
hp : Prime p
hnb : log p (n + k) < b
⊢ emultiplicity p ((n + k).choose k) + emultiplicity p (k ! * n !) =
    ↑(#(filter (fun i => p ^ i ≤ k % p ^ i + n % p ^ i) (Ico 1 b))) + emultiplicity p (k ! * n !)

Tactic:
rw [← hp.emultiplicity_mul, ← mul_assoc]

Result:
p n k b : ℕ
hp : Prime p
hnb : log p (n + k) < b
⊢ emultiplicity p ((n + k).choose k * k ! * n !) =
    ↑(#(filter (fun i => p ^ i ≤ k % p ^ i + n % p ^ i) (Ico 1 b))) + emultiplicity p (k ! * n !)

Proof state:
p n k b : ℕ
hp : Prime p
hnb : log p (n + k) < b
h₁ :
  emultiplicity p ((n + k).choose k) + emultiplicity p (k ! * n !) =
    ↑(#(filter (fun i => p ^ i ≤ k % p ^ i + n % p ^ i) (Ico 1 b))) + emultiplicity p (k ! * n !)
⊢ emultiplicity p ((n + k).choose k) = ↑(#(filter (fun i => p ^ i ≤ k % p ^ i + n % p ^ i) (Ico 1 b)))

Tactic:
refine WithTop.add_right_cancel ?_ h₁

Result:
p n k b : ℕ
hp : Prime p
hnb : log p (n + k) < b
h₁ :
  emultiplicity p ((n + k).choose k) + emultiplicity p (k ! * n !) =
    ↑(#(filter (fun i => p ^ i ≤ k % p ^ i + n % p ^ i) (Ico 1 b))) + emultiplicity p (k ! * n !)
⊢ emultiplicity p (k ! * n !) ≠ ⊤

Proof state:
p n k b : ℕ
hp : Prime p
hnb : log p (n + k) < b
this : (n + k).choose k * k ! * n ! = (n + k)!
⊢ ↑(∑ i ∈ Ico 1 b, k / p ^ i + ∑ i ∈ Ico 1 b, (n + k - k) / p ^ i +
        #(filter (fun i => p ^ i ≤ k % p ^ i + (n + k - k) % p ^ i) (Ico 1 b))) =
    ↑(#(filter (fun i => p ^ i ≤ k % p ^ i + n % p ^ i) (Ico 1 b))) +
      (↑(∑ i ∈ Ico 1 b, k / p ^ i) + ↑(∑ i ∈ Ico 1 b, n / p ^ i))

Tactic:
simp [add_comm]

Result:
no goals

Proof state:
p n k b : ℕ
hp : Prime p
hnb : log p (n + k) < b
h₁ :
  emultiplicity p ((n + k).choose k) + emultiplicity p (k ! * n !) =
    ↑(#(filter (fun i => p ^ i ≤ k % p ^ i + n % p ^ i) (Ico 1 b))) + emultiplicity p (k ! * n !)
⊢ FiniteMultiplicity p (k ! * n !)

Tactic:
exact Nat.finiteMultiplicity_iff.2 ⟨hp.ne_one, mul_pos (factorial_pos k) (factorial_pos n)⟩

Result:
no goals

Proof state:
p n k b : ℕ
hp : Prime p
hnb : log p (n + k) < b
this : (n + k).choose k * k ! * n ! = (n + k)!
⊢ emultiplicity p ((n + k).choose k * k ! * n !) =
    ↑(#(filter (fun i => p ^ i ≤ k % p ^ i + n % p ^ i) (Ico 1 b))) + emultiplicity p (k ! * n !)

Tactic:
rw [this, hp.emultiplicity_factorial hnb, hp.emultiplicity_mul,
  hp.emultiplicity_factorial ((log_mono_right (le_add_left k n)).trans_lt hnb),
  hp.emultiplicity_factorial ((log_mono_right (le_add_left n k)).trans_lt
  (add_comm n k ▸ hnb)), multiplicity_choose_aux hp (le_add_left k n)]

Result:
p n k b : ℕ
hp : Prime p
hnb : log p (n + k) < b
this : (n + k).choose k * k ! * n ! = (n + k)!
⊢ ↑(∑ i ∈ Ico 1 b, k / p ^ i + ∑ i ∈ Ico 1 b, (n + k - k) / p ^ i +
        #(filter (fun i => p ^ i ≤ k % p ^ i + (n + k - k) % p ^ i) (Ico 1 b))) =
    ↑(#(filter (fun i => p ^ i ≤ k % p ^ i + n % p ^ i) (Ico 1 b))) +
      (↑(∑ i ∈ Ico 1 b, k / p ^ i) + ↑(∑ i ∈ Ico 1 b, n / p ^ i))