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)
this : multiplicity 2 ↑k ! = ↑(∑ i ∈ Finset.range n, i)
⊢ multiplicity ↑2 ↑k ! < ↑k
no goals