case refine'_1
α : Type ?u.651487
β : Type ?u.651490
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
⊢ 0 < 2 / (1 - 2 / exp 1)

case refine'_2
α : Type ?u.651487
β : Type ?u.651490
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
⊢ log 8 * (69 / 50) ≤ Real.sqrt (log ↑N)
α : Type ?u.651487
β : Type ?u.651490
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
⊢ log (2 / (1 - 2 / exp 1)) * (69 / 50) ≤ Real.sqrt (log ↑N)
refine' (mul_le_mul_of_nonneg_right ((log_le_log _ <| by norm_num1).2
    two_div_one_sub_two_div_e_le_eight) <| by norm_num1).trans _
case refine'_2
α : Type ?u.651487
β : Type ?u.651490
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
l8 : log 8 = ↑3 * log 2
⊢ log 8 * (69 / 50) ≤ Real.sqrt (log ↑N)
case refine'_2
α : Type ?u.651487
β : Type ?u.651490
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
⊢ log 8 * (69 / 50) ≤ Real.sqrt (log ↑N)
have l8 : log 8 = (3 : ℕ) * log 2 := by
  rw [← log_rpow zero_lt_two, rpow_nat_cast]
  norm_num
case refine'_2
α : Type ?u.651487
β : Type ?u.651490
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
l8 : log 8 = ↑3 * log 2
⊢ ↑3 * log 2 * (69 / 50) ≤ Real.sqrt (log ↑N)
case refine'_2
α : Type ?u.651487
β : Type ?u.651490
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
l8 : log 8 = ↑3 * log 2
⊢ log 8 * (69 / 50) ≤ Real.sqrt (log ↑N)
rw [l8]
α : Type ?u.651487
β : Type ?u.651490
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
l8 : log 8 = ↑3 * log 2
⊢ (↑3 * log 2 * (69 / 50)) ^ 2 ≤ ↑12 * log 2
case refine'_2
α : Type ?u.651487
β : Type ?u.651490
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
l8 : log 8 = ↑3 * log 2
⊢ ↑3 * log 2 * (69 / 50) ≤ Real.sqrt (log ↑N)
apply le_sqrt_of_sq_le (le_trans _ this)
α : Type ?u.651487
β : Type ?u.651490
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
l8 : log 8 = ↑3 * log 2
⊢ (↑3 * (69 / 50)) ^ 2 * log 2 * log 2 ≤ ↑12 * log 2
α : Type ?u.651487
β : Type ?u.651490
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
l8 : log 8 = ↑3 * log 2
⊢ (↑3 * log 2 * (69 / 50)) ^ 2 ≤ ↑12 * log 2
rw [mul_right_comm, mul_pow, sq (log 2), ← mul_assoc]
α : Type ?u.651487
β : Type ?u.651490
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
l8 : log 8 = ↑3 * log 2
⊢ (↑3 * (69 / 50)) ^ 2 * log 2 ≤ ↑12
α : Type ?u.651487
β : Type ?u.651490
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
l8 : log 8 = ↑3 * log 2
⊢ (↑3 * (69 / 50)) ^ 2 * log 2 * log 2 ≤ ↑12 * log 2
apply mul_le_mul_of_nonneg_right _ (log_nonneg one_le_two)
α : Type ?u.651487
β : Type ?u.651490
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
l8 : log 8 = ↑3 * log 2
⊢ log 2 ≤ ↑12 / (↑3 * (69 / 50)) ^ 2

α : Type ?u.651487
β : Type ?u.651490
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
l8 : log 8 = ↑3 * log 2
⊢ 0 < (↑3 * (69 / 50)) ^ 2
α : Type ?u.651487
β : Type ?u.651490
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
l8 : log 8 = ↑3 * log 2
⊢ (↑3 * (69 / 50)) ^ 2 * log 2 ≤ ↑12
rw [← le_div_iff']
no goals
α : Type ?u.651487
β : Type ?u.651490
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
l8 : log 8 = ↑3 * log 2
⊢ 0 < (↑3 * (69 / 50)) ^ 2
exact sq_pos_of_ne_zero _ (by norm_num1)
α : Type ?u.651487
β : Type ?u.651490
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 2 ^ 12 ≤ ↑N

case h
α : Type ?u.651487
β : Type ?u.651490
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 0 < 2 ^ ↑12

case h₁
α : Type ?u.651487
β : Type ?u.651490
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 0 < ↑N
α : Type ?u.651487
β : Type ?u.651490
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ ↑12 * log 2 ≤ log ↑N
rw [← log_rpow zero_lt_two, log_le_log, rpow_nat_cast]
case h₁
α : Type ?u.651487
β : Type ?u.651490
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 0 < N
case h₁
α : Type ?u.651487
β : Type ?u.651490
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 0 < ↑N
rw [cast_pos]
no goals
case h₁
α : Type ?u.651487
β : Type ?u.651490
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 0 < N
exact hN.trans_lt' (by norm_num1)
α : Type ?u.651487
β : Type ?u.651490
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 4096 ≤ ↑N
α : Type ?u.651487
β : Type ?u.651490
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 2 ^ 12 ≤ ↑N
norm_num1
no goals
α : Type ?u.651487
β : Type ?u.651490
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 4096 ≤ ↑N
exact_mod_cast hN
no goals
case h
α : Type ?u.651487
β : Type ?u.651490
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 0 < 2 ^ ↑12
exact rpow_pos_of_pos zero_lt_two _
no goals
α : Type ?u.651487
β : Type ?u.651490
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 0 < 4096
norm_num1
no goals
α : Type ?u.651487
β : Type ?u.651490
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
⊢ 0 < 8
norm_num1
no goals
α : Type ?u.651487
β : Type ?u.651490
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
⊢ 0 ≤ 69 / 50
norm_num1
case refine'_1
α : Type ?u.651487
β : Type ?u.651490
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
⊢ 0 < 1 - 2 / exp 1
case refine'_1
α : Type ?u.651487
β : Type ?u.651490
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
⊢ 0 < 2 / (1 - 2 / exp 1)
refine' div_pos zero_lt_two _
case refine'_1
α : Type ?u.651487
β : Type ?u.651490
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
⊢ 2 < exp 1
case refine'_1
α : Type ?u.651487
β : Type ?u.651490
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
⊢ 0 < 1 - 2 / exp 1
rw [sub_pos, div_lt_one (exp_pos _)]
no goals
case refine'_1
α : Type ?u.651487
β : Type ?u.651490
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
⊢ 2 < exp 1
exact exp_one_gt_d9.trans_le' (by norm_num1)
no goals
α : Type ?u.651487
β : Type ?u.651490
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
⊢ 2 ≤ 2.7182818283
norm_num1
α : Type ?u.651487
β : Type ?u.651490
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
⊢ log 8 = log (2 ^ 3)
α : Type ?u.651487
β : Type ?u.651490
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
⊢ log 8 = ↑3 * log 2
rw [← log_rpow zero_lt_two, rpow_nat_cast]
no goals
α : Type ?u.651487
β : Type ?u.651490
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
⊢ log 8 = log (2 ^ 3)
norm_num
no goals
α : Type ?u.651487
β : Type ?u.651490
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
l8 : log 8 = ↑3 * log 2
⊢ log 2 ≤ ↑12 / (↑3 * (69 / 50)) ^ 2
exact log_two_lt_d9.le.trans (by norm_num1)
no goals
α : Type ?u.651487
β : Type ?u.651490
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
l8 : log 8 = ↑3 * log 2
⊢ 0.6931471808 ≤ ↑12 / (↑3 * (69 / 50)) ^ 2
norm_num1
no goals
α : Type ?u.651487
β : Type ?u.651490
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
l8 : log 8 = ↑3 * log 2
⊢ ↑3 * (69 / 50) ≠ 0
norm_num1