Theorem: Imo2019P4.upper_bound (Compfiles/Imo2019P4.lean)

State before:
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
⊢ n < 6
Tactic:
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]
State after:
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
h2 : ∑ i ∈ Finset.range n, i < k
⊢ n < 6

State before:
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
h2 : ∑ i ∈ Finset.range n, i < k
⊢ n < 6
Tactic:
rw [← not_le]
State after:
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
h2 : ∑ i ∈ Finset.range n, i < k
⊢ ¬6 ≤ n

State before:
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
h2 : ∑ i ∈ Finset.range n, i < k
⊢ ¬6 ≤ n
Tactic:
intro hn
State after:
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
⊢ False

State before:
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
⊢ False
Tactic:
apply _root_.ne_of_gt _ h
State after:
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) < ↑k !

State before:
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) < ↑k !
Tactic:
calc ∏ i ∈ Finset.range n, ((2:ℤ) ^ n - (2:ℤ) ^ i) ≤ ∏ __ ∈ Finset.range n, (2:ℤ) ^ n := ?_
  _ < ↑ k ! := ?_
State after:
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_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
⊢ ∏ __ ∈ Finset.range n, 2 ^ n < ↑k !

State before:
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
⊢ ∏ __ ∈ Finset.range n, 2 ^ n < ↑k !
Tactic:
norm_cast
State after:
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 !

State before:
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 !
Tactic:
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
State after:
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)!

State before:
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)!
Tactic:
clear h h2
State after:
case calc_2
k n : ℕ
hk : k > 0
hn : 6 ≤ n
⊢ 2 ^ (n * n) < (∑ i ∈ Finset.range n, i)!

State before:
case calc_2
k n : ℕ
hk : k > 0
hn : 6 ≤ n
⊢ 2 ^ (n * n) < (∑ i ∈ Finset.range n, i)!
Tactic:
induction' n, hn using Nat.le_induction with n' hn' IH
State after:
case calc_2.base
k n : ℕ
hk : k > 0
⊢ 2 ^ (6 * 6) < (∑ i ∈ Finset.range 6, i)!

case calc_2.succ
k n : ℕ
hk : k > 0
n' : ℕ
hn' : 6 ≤ n'
IH : 2 ^ (n' * n') < (∑ i ∈ Finset.range n', i)!
⊢ 2 ^ ((n' + 1) * (n' + 1)) < (∑ i ∈ Finset.range (n' + 1), i)!

State before:
case calc_2.succ
k n : ℕ
hk : k > 0
n' : ℕ
hn' : 6 ≤ n'
IH : 2 ^ (n' * n') < (∑ i ∈ Finset.range n', i)!
⊢ 2 ^ ((n' + 1) * (n' + 1)) < (∑ i ∈ Finset.range (n' + 1), i)!
Tactic:
let A := ∑ i ∈ Finset.range n', i
State after:
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
⊢ 2 ^ ((n' + 1) * (n' + 1)) < (∑ i ∈ Finset.range (n' + 1), i)!

State before:
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
⊢ 2 ^ ((n' + 1) * (n' + 1)) < (∑ i ∈ Finset.range (n' + 1), i)!
Tactic:
have le_sum : ∑ i ∈ Finset.range 6, i ≤ A := by
  apply Finset.sum_le_sum_of_subset
  simpa using hn'
State after:
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)!

State before:
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)!
Tactic:
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]
State after:
no goals

State before:
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
⊢ ∑ i ∈ Finset.range n, i < k
Tactic:
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]
State after:
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
⊢ multiplicity 2 ↑k ! = ↑(∑ i ∈ Finset.range n, i)

State before:
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
⊢ multiplicity 2 ↑k ! = ↑(∑ i ∈ Finset.range n, i)
Tactic:
rw [h, multiplicity.Finset.prod Int.prime_two, Nat.cast_sum]
State after:
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
⊢ ∑ x ∈ Finset.range n, multiplicity 2 (2 ^ n - 2 ^ x) = ∑ x ∈ Finset.range n, ↑x

State before:
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
⊢ ∑ x ∈ Finset.range n, multiplicity 2 (2 ^ n - 2 ^ x) = ∑ x ∈ Finset.range n, ↑x
Tactic:
apply Finset.sum_congr rfl
State after:
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
⊢ ∀ x ∈ Finset.range n, multiplicity 2 (2 ^ n - 2 ^ x) = ↑x

State before:
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
⊢ ∀ x ∈ Finset.range n, multiplicity 2 (2 ^ n - 2 ^ x) = ↑x
Tactic:
intro i hi
State after:
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
i : ℕ
hi : i ∈ Finset.range n
⊢ multiplicity 2 (2 ^ n - 2 ^ i) = ↑i

State before:
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
i : ℕ
hi : i ∈ Finset.range n
⊢ multiplicity 2 (2 ^ n - 2 ^ i) = ↑i
Tactic:
rw [multiplicity.multiplicity_sub_of_gt,
    multiplicity.multiplicity_pow_self_of_prime Int.prime_two]
State after:
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
i : ℕ
hi : i ∈ Finset.range n
⊢ multiplicity 2 (2 ^ i) < multiplicity 2 (2 ^ n)

State before:
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
i : ℕ
hi : i ∈ Finset.range n
⊢ multiplicity 2 (2 ^ i) < multiplicity 2 (2 ^ n)
Tactic:
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]
State after:
no goals

State before:
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
this : multiplicity 2 ↑k ! = ↑(∑ i ∈ Finset.range n, i)
⊢ ∑ i ∈ Finset.range n, i < k
Tactic:
rw [← PartENat.coe_lt_coe, ← this]
State after:
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
this : multiplicity 2 ↑k ! = ↑(∑ i ∈ Finset.range n, i)
⊢ multiplicity 2 ↑k ! < ↑k

State before:
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
this : multiplicity 2 ↑k ! = ↑(∑ i ∈ Finset.range n, i)
⊢ multiplicity 2 ↑k ! < ↑k
Tactic:
change multiplicity ((2 : ℕ) : ℤ) _ < _
State after:
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
this : multiplicity 2 ↑k ! = ↑(∑ i ∈ Finset.range n, i)
⊢ multiplicity ↑2 ↑k ! < ↑k

State before:
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
this : multiplicity 2 ↑k ! = ↑(∑ i ∈ Finset.range n, i)
⊢ multiplicity ↑2 ↑k ! < ↑k
Tactic:
simp_rw [multiplicity.Int.natCast_multiplicity,
         Nat.multiplicity_two_factorial_lt hk.lt.ne.symm]
State after:
no goals

State before:
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
Tactic:
gcongr
State after:
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

State before:
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
Tactic:
intro i hi
State after:
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 : ℕ
hi : i ∈ Finset.range n
⊢ 0 ≤ 2 ^ n - 2 ^ i

State before:
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 : ℕ
hi : i ∈ Finset.range n
⊢ 0 ≤ 2 ^ n - 2 ^ i
Tactic:
simp only [Finset.mem_range] at hi
State after:
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 : ℕ
hi : i < n
⊢ 0 ≤ 2 ^ n - 2 ^ i

State before:
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 : ℕ
hi : i < n
⊢ 0 ≤ 2 ^ n - 2 ^ i
Tactic:
have : (2:ℤ) ^ i ≤ (2:ℤ) ^ n := by gcongr; norm_num
State after:
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 : ℕ
hi : i < n
this : 2 ^ i ≤ 2 ^ n
⊢ 0 ≤ 2 ^ n - 2 ^ i

State before:
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 : ℕ
hi : i < n
this : 2 ^ i ≤ 2 ^ n
⊢ 0 ≤ 2 ^ n - 2 ^ i
Tactic:
omega
State after:
no goals

State before:
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 : ℕ
hi : i < n
⊢ 2 ^ i ≤ 2 ^ n
Tactic:
gcongr
State after:
case ha
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 : ℕ
hi : i < n
⊢ 1 ≤ 2

State before:
case ha
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 : ℕ
hi : i < n
⊢ 1 ≤ 2
Tactic:
norm_num
State after:
no goals

State before:
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
Tactic:
apply sub_le_self
State after:
case calc_1.h1.a
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
⊢ 0 ≤ 2 ^ i✝

State before:
case calc_1.h1.a
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
⊢ 0 ≤ 2 ^ i✝
Tactic:
positivity
State after:
no goals

State before:
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
⊢ ∏ __ ∈ Finset.range n, 2 ^ n = 2 ^ (n * n)
Tactic:
rw [Finset.prod_const, Finset.card_range, ← pow_mul]
State after:
no goals

State before:
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, i)! ≤ k !
Tactic:
gcongr
State after:
no goals

State before:
case calc_2.base
k n : ℕ
hk : k > 0
⊢ 2 ^ (6 * 6) < (∑ i ∈ Finset.range 6, i)!
Tactic:
decide
State after:
no goals

State before:
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
Tactic:
apply Finset.sum_le_sum_of_subset
State after:
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'

State before:
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'
Tactic:
simpa using hn'
State after:
no goals

State before:
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)) ≤ 2 ^ (n' * n' + 4 * n')
Tactic:
gcongr <;> linarith
State after:
no goals

State before:
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' * n' + 4 * n') = 2 ^ (n' * n') * (2 ^ 4) ^ n'
Tactic:
rw [← pow_mul, ← pow_add]
State after:
no goals

State before:
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' * n') * (2 ^ 4) ^ n' < A ! * (2 ^ 4) ^ n'
Tactic:
gcongr
State after:
no goals

State before:
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
⊢ A ! * (15 + 1) ^ n' ≤ A ! * (A + 1) ^ n'
Tactic:
gcongr
State after:
case bc.hab.bc
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
⊢ 15 ≤ A

State before:
case bc.hab.bc
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
⊢ 15 ≤ A
Tactic:
exact le_sum
State after:
no goals

State before:
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
⊢ (A + n')! = (∑ i ∈ Finset.range (n' + 1), i)!
Tactic:
rw [Finset.sum_range_succ]
State after:
no goals