-- Mathlib/Data/Nat/Multiplicity.lean
theorem emultiplicity_choose_prime_pow_add_emultiplicity (hp : p.Prime) (hkn : k ≤ p ^ n)
    (hk0 : k ≠ 0) : emultiplicity p (choose (p ^ n) k) + emultiplicity p k = n :=
  le_antisymm
    (by
      have hdisj :
        Disjoint {i ∈ Ico 1 n.succ | p ^ i ≤ k % p ^ i + (p ^ n - k) % p ^ i}
          {i ∈ Ico 1 n.succ | p ^ i ∣ k}

Proof state:
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
⊢ emultiplicity p (p ^ n) ≤ emultiplicity p ((p ^ n).choose k) + emultiplicity p k

Tactic:
exact emultiplicity_le_emultiplicity_choose_add hp _ _

Result:
no goals

Proof state:
case a
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 n.succ))
    (filter (fun i => p ^ i ∣ k) (Ico 1 n.succ))
⊢ ↑(#(filter (fun i => p ^ i ≤ k % p ^ i + (p ^ n - k) % p ^ i) (Ico 1 (log p (p ^ n)).succ)) +
        #(filter (fun i => p ^ i ∣ k) (Ico 1 (log p (p ^ n)).succ))) ≤
    n

Tactic:
rw [log_pow hp.one_lt, ← card_union_of_disjoint hdisj, filter_union_right]

Result:
case a
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 n.succ))
    (filter (fun i => p ^ i ∣ k) (Ico 1 n.succ))
⊢ ↑(#(filter (fun x => p ^ x ≤ k % p ^ x + (p ^ n - k) % p ^ x ∨ p ^ x ∣ k) (Ico 1 n.succ))) ≤ n

Proof state:
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
⊢ ↑n ≤ emultiplicity p ((p ^ n).choose k) + emultiplicity p k

Tactic:
rw [← hp.emultiplicity_pow_self]

Result:
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
⊢ emultiplicity p (p ^ n) ≤ emultiplicity p ((p ^ n).choose k) + emultiplicity p k

Proof state:
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 n.succ))
    (filter (fun i => p ^ i ∣ k) (Ico 1 n.succ))
⊢ ↑(#(filter (fun i => p ^ i ≤ k % p ^ i + (p ^ n - k) % p ^ i) (Ico 1 (log p (p ^ n)).succ)) +
        #(filter (fun i => p ^ i ∣ k) (Ico 1 (log p (p ^ n)).succ))) ≤
    ↑n

Tactic:
apply WithTop.coe_mono

Result:
case a
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 n.succ))
    (filter (fun i => p ^ i ∣ k) (Ico 1 n.succ))
⊢ ↑(#(filter (fun i => p ^ i ≤ k % p ^ i + (p ^ n - k) % p ^ i) (Ico 1 (log p (p ^ n)).succ)) +
        #(filter (fun i => p ^ i ∣ k) (Ico 1 (log p (p ^ n)).succ))) ≤
    n

Proof state:
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 n.succ))
    (filter (fun i => p ^ i ∣ k) (Ico 1 n.succ))

Tactic:
simp +contextual [disjoint_right, *, dvd_iff_mod_eq_zero,
  Nat.mod_lt _ (pow_pos hp.pos _)]

Result:
no goals

Proof state:
case a
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 n.succ))
    (filter (fun i => p ^ i ∣ k) (Ico 1 n.succ))
filter_le_Ico :
  #(filter (fun x => p ^ x ≤ k % p ^ x + (p ^ n - k) % p ^ x ∨ p ^ x ∣ k) (Ico 1 n.succ)) ≤ #(Ico 1 n.succ)
⊢ ↑(#(filter (fun x => p ^ x ≤ k % p ^ x + (p ^ n - k) % p ^ x ∨ p ^ x ∣ k) (Ico 1 n.succ))) ≤ n

Tactic:
rwa [card_Ico 1 n.succ] at filter_le_Ico

Result:
no goals

Proof state:
case a
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 n.succ))
    (filter (fun i => p ^ i ∣ k) (Ico 1 n.succ))
⊢ ↑(#(filter (fun x => p ^ x ≤ k % p ^ x + (p ^ n - k) % p ^ x ∨ p ^ x ∣ k) (Ico 1 n.succ))) ≤ n

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

Result:
case a
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 n.succ))
    (filter (fun i => p ^ i ∣ k) (Ico 1 n.succ))
filter_le_Ico :
  #(filter (fun x => p ^ x ≤ k % p ^ x + (p ^ n - k) % p ^ x ∨ p ^ x ∣ k) (Ico 1 n.succ)) ≤ #(Ico 1 n.succ)
⊢ ↑(#(filter (fun x => p ^ x ≤ k % p ^ x + (p ^ n - k) % p ^ x ∨ p ^ x ∣ k) (Ico 1 n.succ))) ≤ n

Proof state:
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 n.succ))
    (filter (fun i => p ^ i ∣ k) (Ico 1 n.succ))
⊢ emultiplicity p ((p ^ n).choose k) + emultiplicity p k ≤ ↑n

Tactic:
rw [emultiplicity_choose hp hkn (lt_succ_self _),
  emultiplicity_eq_card_pow_dvd (ne_of_gt hp.one_lt) hk0.bot_lt
    (lt_succ_of_le (log_mono_right hkn)),
  ← Nat.cast_add]

Result:
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 n.succ))
    (filter (fun i => p ^ i ∣ k) (Ico 1 n.succ))
⊢ ↑(#(filter (fun i => p ^ i ≤ k % p ^ i + (p ^ n - k) % p ^ i) (Ico 1 (log p (p ^ n)).succ)) +
        #(filter (fun i => p ^ i ∣ k) (Ico 1 (log p (p ^ n)).succ))) ≤
    ↑n

Proof state:
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
⊢ emultiplicity p ((p ^ n).choose k) + emultiplicity p k ≤ ↑n

Tactic:
have hdisj :
  Disjoint {i ∈ Ico 1 n.succ | p ^ i ≤ k % p ^ i + (p ^ n - k) % p ^ i}
    {i ∈ Ico 1 n.succ | p ^ i ∣ k} := by
  simp +contextual [disjoint_right, *, dvd_iff_mod_eq_zero,
    Nat.mod_lt _ (pow_pos hp.pos _)]

Result:
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 n.succ))
    (filter (fun i => p ^ i ∣ k) (Ico 1 n.succ))
⊢ emultiplicity p ((p ^ n).choose k) + emultiplicity p k ≤ ↑n