suffices multiplicity 2 (k ! : ℤ) = ↑(∑ i ∈ Finset.range n, i : ℕ) by
  rw [← PartENat.coe_lt_coe, ← this]; change multiplicity ((2 : ℕ) : ℤ) _ < _
  simp_rw [multiplicity.Int.natCast_multiplicity,
           Nat.multiplicity_two_factorial_lt hk.lt.ne.symm]
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
⊢ ∑ i ∈ Finset.range n, i < k
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
⊢ multiplicity 2 ↑k ! = ↑(∑ i ∈ Finset.range n, i)