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
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
⊢ multiplicity p (choose (p ^ n) k) + multiplicity p k ≤ ↑n
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 _)]
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
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
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]
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
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
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
no goals
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
rwa [card_Ico 1 n.succ] at filter_le_Ico
no goals
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)))
simp (config := { contextual := true }) [disjoint_right, *, dvd_iff_mod_eq_zero,
  Nat.mod_lt _ (pow_pos hp.pos _)]
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
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
⊢ ↑n ≤ multiplicity p (choose (p ^ n) k) + multiplicity p k
rw [← hp.multiplicity_pow_self]
no goals
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
exact multiplicity_le_multiplicity_choose_add hp _ _