apply Finset.sum_le_sum_of_subset
k n : ℕ
hk : k > 0
n' : ℕ
hn' : 6 ≤ n'
IH : 2 ^ (n' * n') < (∑ i ∈ Finset.range n', i)!
A : ℕ := ∑ i ∈ Finset.range n', i
⊢ ∑ i ∈ Finset.range 6, i ≤ A
case h
k n : ℕ
hk : k > 0
n' : ℕ
hn' : 6 ≤ n'
IH : 2 ^ (n' * n') < (∑ i ∈ Finset.range n', i)!
A : ℕ := ∑ i ∈ Finset.range n', i
⊢ Finset.range 6 ⊆ Finset.range n'