calc 2 ^ ((n' + 1) * (n' + 1))
    ≤ 2 ^ (n' * n' + 4 * n') := by gcongr <;> linarith
  _ = 2 ^ (n' * n') * (2 ^ 4) ^ n' := by rw [← pow_mul, ← pow_add]
  _ < A ! * (2 ^ 4) ^ n' := by gcongr
  _ = A ! * (15 + 1) ^ n' := rfl
  _ ≤ A ! * (A + 1) ^ n' := by gcongr; exact le_sum
  _ ≤ (A + n')! := Nat.factorial_mul_pow_le_factorial
  _ = (∑ i ∈ Finset.range (n' + 1), i)! := by rw [Finset.sum_range_succ]
case calc_2.succ
k n : ℕ
hk : k > 0
n' : ℕ
hn' : 6 ≤ n'
IH : 2 ^ (n' * n') < (∑ i ∈ Finset.range n', i)!
A : ℕ := ∑ i ∈ Finset.range n', i
le_sum : ∑ i ∈ Finset.range 6, i ≤ A
⊢ 2 ^ ((n' + 1) * (n' + 1)) < (∑ i ∈ Finset.range (n' + 1), i)!
no goals