have h2 : ∑ i ∈ Finset.range n, i < k := by
  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]
  rw [h, multiplicity.Finset.prod Int.prime_two, Nat.cast_sum]
  apply Finset.sum_congr rfl; intro i hi
  rw [multiplicity.multiplicity_sub_of_gt,
      multiplicity.multiplicity_pow_self_of_prime Int.prime_two]
  rwa [multiplicity.multiplicity_pow_self_of_prime Int.prime_two,
       multiplicity.multiplicity_pow_self_of_prime Int.prime_two,
    PartENat.coe_lt_coe, ← Finset.mem_range]
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
⊢ n < 6
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
h2 : ∑ i ∈ Finset.range n, i < k
⊢ n < 6