gcongr
case calc_1
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 - 2 ^ i) ≤ ∏ __ ∈ Finset.range n, 2 ^ n
case calc_1.h0
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, 0 ≤ 2 ^ n - 2 ^ i

case calc_1.h1
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✝ : ℕ
a✝ : i✝ ∈ Finset.range n
⊢ 2 ^ n - 2 ^ i✝ ≤ 2 ^ n