calc ∏ __ ∈ Finset.range n, 2 ^ n = 2 ^ (n * n) := by
       rw [Finset.prod_const, Finset.card_range, ← pow_mul]
  _ < (∑ i ∈ Finset.range n, i)! := ?_
  _ ≤ k ! := by gcongr
case calc_2
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
h2 : ∑ i ∈ Finset.range n, i < k
hn : 6 ≤ n
⊢ ∏ i ∈ Finset.range n, 2 ^ n < k !
case calc_2
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
h2 : ∑ i ∈ Finset.range n, i < k
hn : 6 ≤ n
⊢ 2 ^ (n * n) < (∑ i ∈ Finset.range n, i)!