α : Type ?u.793471
β : Type ?u.793474
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
⊢ ↑N * exp (-4 * Real.sqrt (log ↑N)) < ↑(↑rothNumberNat N)
α : Type ?u.793471
β : Type ?u.793474
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ ↑N * exp (-4 * Real.sqrt (log ↑N)) < ↑(↑rothNumberNat N)
let n := nValue N
α : Type ?u.793471
β : Type ?u.793474
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
⊢ ↑N * exp (-4 * Real.sqrt (log ↑N)) < ↑(↑rothNumberNat N)
α : Type ?u.793471
β : Type ?u.793474
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
⊢ ↑N * exp (-4 * Real.sqrt (log ↑N)) < ↑(↑rothNumberNat N)
have hn : 0 < (n : ℝ) := cast_pos.2 (nValue_pos <| hN.trans' <| by norm_num1)
α : Type ?u.793471
β : Type ?u.793474
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
⊢ ↑N * exp (-4 * Real.sqrt (log ↑N)) < ↑(↑rothNumberNat N)
α : Type ?u.793471
β : Type ?u.793474
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
⊢ ↑N * exp (-4 * Real.sqrt (log ↑N)) < ↑(↑rothNumberNat N)
have hd : 0 < dValue N := dValue_pos (hN.trans' <| by norm_num1)
α : Type ?u.793471
β : Type ?u.793474
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
⊢ ↑N * exp (-4 * Real.sqrt (log ↑N)) < ↑(↑rothNumberNat N)
α : Type ?u.793471
β : Type ?u.793474
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
⊢ ↑N * exp (-4 * Real.sqrt (log ↑N)) < ↑(↑rothNumberNat N)
have hN₀ : 0 < (N : ℝ) := cast_pos.2 (hN.trans' <| by norm_num1)
α : Type ?u.793471
β : Type ?u.793474
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 ≤ n
⊢ ↑N * exp (-4 * Real.sqrt (log ↑N)) < ↑(↑rothNumberNat N)
α : Type ?u.793471
β : Type ?u.793474
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
⊢ ↑N * exp (-4 * Real.sqrt (log ↑N)) < ↑(↑rothNumberNat N)
have hn₂ : 2 ≤ n := two_le_nValue (hN.trans' <| by norm_num1)
α : Type ?u.793471
β : Type ?u.793474
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 ≤ n
this : (2 * dValue N - 1) ^ n ≤ N
⊢ ↑N * exp (-4 * Real.sqrt (log ↑N)) < ↑(↑rothNumberNat N)
α : Type ?u.793471
β : Type ?u.793474
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 ≤ n
⊢ ↑N * exp (-4 * Real.sqrt (log ↑N)) < ↑(↑rothNumberNat N)
have : (2 * dValue N - 1) ^ n ≤ N := le_N (hN.trans' <| by norm_num1)
α : Type ?u.793471
β : Type ?u.793474
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 ≤ n
this : (2 * dValue N - 1) ^ n ≤ N
⊢ ↑N * exp (-4 * Real.sqrt (log ↑N)) < ↑(dValue N) ^ (↑n - 2) / ↑n
α : Type ?u.793471
β : Type ?u.793474
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 ≤ n
this : (2 * dValue N - 1) ^ n ≤ N
⊢ ↑N * exp (-4 * Real.sqrt (log ↑N)) < ↑(↑rothNumberNat N)
refine' ((bound_aux hd.ne' hn₂).trans <| cast_le.2 <| rothNumberNat.mono this).trans_lt' _
α : Type ?u.793471
β : Type ?u.793474
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 ≤ n
this : (2 * dValue N - 1) ^ n ≤ N
⊢ ↑N * exp (-4 * Real.sqrt (log ↑N)) < ↑(dValue N) ^ (n - 2) / ↑n
α : Type ?u.793471
β : Type ?u.793474
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 ≤ n
this : (2 * dValue N - 1) ^ n ≤ N
⊢ ↑N * exp (-4 * Real.sqrt (log ↑N)) < ↑(dValue N) ^ (↑n - 2) / ↑n
conv_rhs => rw [← cast_two, ← cast_sub hn₂, rpow_nat_cast]
case refine'_1
α : Type ?u.793471
β : Type ?u.793474
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 ≤ n
this : (2 * dValue N - 1) ^ n ≤ N
⊢ 0 ≤ ↑N ^ (1 / ↑(nValue N)) / exp 1

case refine'_2
α : Type ?u.793471
β : Type ?u.793474
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 ≤ n
this : (2 * dValue N - 1) ^ n ≤ N
⊢ 0 < n - 2

case refine'_3
α : Type ?u.793471
β : Type ?u.793474
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 ≤ n
this : (2 * dValue N - 1) ^ n ≤ N
⊢ ↑N * exp (-4 * Real.sqrt (log ↑N)) ≤ (↑N ^ (1 / ↑(nValue N)) / exp 1) ^ (n - 2) / ↑n
α : Type ?u.793471
β : Type ?u.793474
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 ≤ n
this : (2 * dValue N - 1) ^ n ≤ N
⊢ ↑N * exp (-4 * Real.sqrt (log ↑N)) < ↑(dValue N) ^ (n - 2) / ↑n
refine' (div_lt_div_of_lt hn <| pow_lt_pow_of_lt_left (bound hN) _ _).trans_le' _
case refine'_3
α : Type ?u.793471
β : Type ?u.793474
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 ≤ n
this : (2 * dValue N - 1) ^ n ≤ N
⊢ ↑N * exp (-4 * Real.sqrt (log ↑N)) ≤ ↑N * (↑N ^ (2 / ↑n) * (exp (↑n - 2) * ↑n))⁻¹
case refine'_3
α : Type ?u.793471
β : Type ?u.793474
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 ≤ n
this : (2 * dValue N - 1) ^ n ≤ N
⊢ ↑N * exp (-4 * Real.sqrt (log ↑N)) ≤ (↑N ^ (1 / ↑(nValue N)) / exp 1) ^ (n - 2) / ↑n
rw [← rpow_nat_cast, div_rpow (rpow_nonneg_of_nonneg hN₀.le _) (exp_pos _).le, ← rpow_mul hN₀.le,
  mul_comm (_ / _), mul_one_div, cast_sub hn₂, cast_two, same_sub_div hn.ne', exp_one_rpow,
  div_div, rpow_sub hN₀, rpow_one, div_div, div_eq_mul_inv]
case refine'_3
α : Type ?u.793471
β : Type ?u.793474
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 ≤ n
this : (2 * dValue N - 1) ^ n ≤ N
⊢ exp (-4 * Real.sqrt (log ↑N)) ≤ (↑N ^ (2 / ↑n) * (exp (↑n - 2) * ↑n))⁻¹
case refine'_3
α : Type ?u.793471
β : Type ?u.793474
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 ≤ n
this : (2 * dValue N - 1) ^ n ≤ N
⊢ ↑N * exp (-4 * Real.sqrt (log ↑N)) ≤ ↑N * (↑N ^ (2 / ↑n) * (exp (↑n - 2) * ↑n))⁻¹
refine' mul_le_mul_of_nonneg_left _ (cast_nonneg _)
case refine'_3
α : Type ?u.793471
β : Type ?u.793474
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 ≤ n
this : (2 * dValue N - 1) ^ n ≤ N
⊢ exp (-4 * Real.sqrt (log ↑N)) ≤ ↑N ^ (-(2 / ↑n)) * (exp (2 - ↑n) / ↑n)
case refine'_3
α : Type ?u.793471
β : Type ?u.793474
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 ≤ n
this : (2 * dValue N - 1) ^ n ≤ N
⊢ exp (-4 * Real.sqrt (log ↑N)) ≤ (↑N ^ (2 / ↑n) * (exp (↑n - 2) * ↑n))⁻¹
rw [mul_inv, mul_inv, ← exp_neg, ← rpow_neg (cast_nonneg _), neg_sub, ← div_eq_mul_inv]
case refine'_3
α : Type ?u.793471
β : Type ?u.793474
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 ≤ n
this✝ : (2 * dValue N - 1) ^ n ≤ N
this : exp (-4 * Real.sqrt (log ↑N)) = exp (-2 * Real.sqrt (log ↑N)) * exp (-2 * Real.sqrt (log ↑N))
⊢ exp (-4 * Real.sqrt (log ↑N)) ≤ ↑N ^ (-(2 / ↑n)) * (exp (2 - ↑n) / ↑n)
case refine'_3
α : Type ?u.793471
β : Type ?u.793474
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 ≤ n
this : (2 * dValue N - 1) ^ n ≤ N
⊢ exp (-4 * Real.sqrt (log ↑N)) ≤ ↑N ^ (-(2 / ↑n)) * (exp (2 - ↑n) / ↑n)
have : exp (-4 * sqrt (log N)) = exp (-2 * sqrt (log N)) * exp (-2 * sqrt (log N)) := by
  rw [← exp_add, ← add_mul]
  norm_num
case refine'_3
α : Type ?u.793471
β : Type ?u.793474
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 ≤ n
this✝ : (2 * dValue N - 1) ^ n ≤ N
this : exp (-4 * Real.sqrt (log ↑N)) = exp (-2 * Real.sqrt (log ↑N)) * exp (-2 * Real.sqrt (log ↑N))
⊢ exp (-2 * Real.sqrt (log ↑N)) * exp (-2 * Real.sqrt (log ↑N)) ≤ ↑N ^ (-(2 / ↑n)) * (exp (2 - ↑n) / ↑n)
case refine'_3
α : Type ?u.793471
β : Type ?u.793474
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 ≤ n
this✝ : (2 * dValue N - 1) ^ n ≤ N
this : exp (-4 * Real.sqrt (log ↑N)) = exp (-2 * Real.sqrt (log ↑N)) * exp (-2 * Real.sqrt (log ↑N))
⊢ exp (-4 * Real.sqrt (log ↑N)) ≤ ↑N ^ (-(2 / ↑n)) * (exp (2 - ↑n) / ↑n)
rw [this]
case refine'_3.refine'_1
α : Type ?u.793471
β : Type ?u.793474
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 ≤ n
this✝ : (2 * dValue N - 1) ^ n ≤ N
this : exp (-4 * Real.sqrt (log ↑N)) = exp (-2 * Real.sqrt (log ↑N)) * exp (-2 * Real.sqrt (log ↑N))
⊢ exp (-2 * Real.sqrt (log ↑N)) ≤ ↑N ^ (-(2 / ↑n))

case refine'_3.refine'_2
α : Type ?u.793471
β : Type ?u.793474
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 ≤ n
this✝ : (2 * dValue N - 1) ^ n ≤ N
this : exp (-4 * Real.sqrt (log ↑N)) = exp (-2 * Real.sqrt (log ↑N)) * exp (-2 * Real.sqrt (log ↑N))
⊢ 1 < ↑N
case refine'_3
α : Type ?u.793471
β : Type ?u.793474
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 ≤ n
this✝ : (2 * dValue N - 1) ^ n ≤ N
this : exp (-4 * Real.sqrt (log ↑N)) = exp (-2 * Real.sqrt (log ↑N)) * exp (-2 * Real.sqrt (log ↑N))
⊢ exp (-2 * Real.sqrt (log ↑N)) * exp (-2 * Real.sqrt (log ↑N)) ≤ ↑N ^ (-(2 / ↑n)) * (exp (2 - ↑n) / ↑n)
refine' mul_le_mul _ (exp_neg_two_mul_le <| Real.sqrt_pos.2 <| log_pos _).le (exp_pos _).le <|
    rpow_nonneg_of_nonneg (cast_nonneg _) _
no goals
α : Type ?u.793471
β : Type ?u.793474
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
⊢ 2 ≤ 4096
norm_num1
no goals
α : Type ?u.793471
β : Type ?u.793474
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
⊢ 8 ≤ 4096
norm_num1
no goals
α : Type ?u.793471
β : Type ?u.793474
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
⊢ succ 0 ≤ 4096
norm_num1
no goals
α : Type ?u.793471
β : Type ?u.793474
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
⊢ 3 ≤ 4096
norm_num1
no goals
α : Type ?u.793471
β : Type ?u.793474
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 ≤ n
⊢ 2 ≤ 4096
norm_num1
no goals
case refine'_1
α : Type ?u.793471
β : Type ?u.793474
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 ≤ n
this : (2 * dValue N - 1) ^ n ≤ N
⊢ 0 ≤ ↑N ^ (1 / ↑(nValue N)) / exp 1
exact div_nonneg (rpow_nonneg_of_nonneg (cast_nonneg _) _) (exp_pos _).le
no goals
case refine'_2
α : Type ?u.793471
β : Type ?u.793474
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 ≤ n
this : (2 * dValue N - 1) ^ n ≤ N
⊢ 0 < n - 2
exact tsub_pos_of_lt (three_le_nValue <| hN.trans' <| by norm_num1)
no goals
α : Type ?u.793471
β : Type ?u.793474
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 ≤ n
this : (2 * dValue N - 1) ^ n ≤ N
⊢ 64 ≤ 4096
norm_num1
α : Type ?u.793471
β : Type ?u.793474
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 ≤ n
this : (2 * dValue N - 1) ^ n ≤ N
⊢ exp (-4 * Real.sqrt (log ↑N)) = exp ((-2 + -2) * Real.sqrt (log ↑N))
α : Type ?u.793471
β : Type ?u.793474
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 ≤ n
this : (2 * dValue N - 1) ^ n ≤ N
⊢ exp (-4 * Real.sqrt (log ↑N)) = exp (-2 * Real.sqrt (log ↑N)) * exp (-2 * Real.sqrt (log ↑N))
rw [← exp_add, ← add_mul]
no goals
α : Type ?u.793471
β : Type ?u.793474
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 ≤ n
this : (2 * dValue N - 1) ^ n ≤ N
⊢ exp (-4 * Real.sqrt (log ↑N)) = exp ((-2 + -2) * Real.sqrt (log ↑N))
norm_num
case refine'_3.refine'_1
α : Type ?u.793471
β : Type ?u.793474
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 ≤ n
this✝ : (2 * dValue N - 1) ^ n ≤ N
this : exp (-4 * Real.sqrt (log ↑N)) = exp (-2 * Real.sqrt (log ↑N)) * exp (-2 * Real.sqrt (log ↑N))
⊢ 2 * Real.sqrt (log ↑N) ≤ 2 * ↑n

case refine'_3.refine'_1
α : Type ?u.793471
β : Type ?u.793474
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 ≤ n
this✝ : (2 * dValue N - 1) ^ n ≤ N
this : exp (-4 * Real.sqrt (log ↑N)) = exp (-2 * Real.sqrt (log ↑N)) * exp (-2 * Real.sqrt (log ↑N))
⊢ 0 < Real.sqrt (log ↑N)
case refine'_3.refine'_1
α : Type ?u.793471
β : Type ?u.793474
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 ≤ n
this✝ : (2 * dValue N - 1) ^ n ≤ N
this : exp (-4 * Real.sqrt (log ↑N)) = exp (-2 * Real.sqrt (log ↑N)) * exp (-2 * Real.sqrt (log ↑N))
⊢ exp (-2 * Real.sqrt (log ↑N)) ≤ ↑N ^ (-(2 / ↑n))
rw [← le_log_iff_exp_le (rpow_pos_of_pos hN₀ _), log_rpow hN₀, ← le_div_iff, mul_div_assoc,
  div_sqrt, neg_mul, neg_le_neg_iff, div_mul_eq_mul_div, div_le_iff hn]
case refine'_3.refine'_1
α : Type ?u.793471
β : Type ?u.793474
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 ≤ n
this✝ : (2 * dValue N - 1) ^ n ≤ N
this : exp (-4 * Real.sqrt (log ↑N)) = exp (-2 * Real.sqrt (log ↑N)) * exp (-2 * Real.sqrt (log ↑N))
⊢ 1 < ↑N
case refine'_3.refine'_1
α : Type ?u.793471
β : Type ?u.793474
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 ≤ n
this✝ : (2 * dValue N - 1) ^ n ≤ N
this : exp (-4 * Real.sqrt (log ↑N)) = exp (-2 * Real.sqrt (log ↑N)) * exp (-2 * Real.sqrt (log ↑N))
⊢ 0 < Real.sqrt (log ↑N)
refine' Real.sqrt_pos.2 (log_pos _)
case refine'_3.refine'_1
α : Type ?u.793471
β : Type ?u.793474
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 ≤ n
this✝ : (2 * dValue N - 1) ^ n ≤ N
this : exp (-4 * Real.sqrt (log ↑N)) = exp (-2 * Real.sqrt (log ↑N)) * exp (-2 * Real.sqrt (log ↑N))
⊢ 1 < N
case refine'_3.refine'_1
α : Type ?u.793471
β : Type ?u.793474
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 ≤ n
this✝ : (2 * dValue N - 1) ^ n ≤ N
this : exp (-4 * Real.sqrt (log ↑N)) = exp (-2 * Real.sqrt (log ↑N)) * exp (-2 * Real.sqrt (log ↑N))
⊢ 1 < ↑N
rw [one_lt_cast]
no goals
case refine'_3.refine'_1
α : Type ?u.793471
β : Type ?u.793474
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 ≤ n
this✝ : (2 * dValue N - 1) ^ n ≤ N
this : exp (-4 * Real.sqrt (log ↑N)) = exp (-2 * Real.sqrt (log ↑N)) * exp (-2 * Real.sqrt (log ↑N))
⊢ 1 < N
exact hN.trans_lt' (by norm_num1)
no goals
case refine'_3.refine'_1
α : Type ?u.793471
β : Type ?u.793474
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 ≤ n
this✝ : (2 * dValue N - 1) ^ n ≤ N
this : exp (-4 * Real.sqrt (log ↑N)) = exp (-2 * Real.sqrt (log ↑N)) * exp (-2 * Real.sqrt (log ↑N))
⊢ 2 * Real.sqrt (log ↑N) ≤ 2 * ↑n
exact mul_le_mul_of_nonneg_left (le_ceil _) zero_le_two
no goals
α : Type ?u.793471
β : Type ?u.793474
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 ≤ n
this✝ : (2 * dValue N - 1) ^ n ≤ N
this : exp (-4 * Real.sqrt (log ↑N)) = exp (-2 * Real.sqrt (log ↑N)) * exp (-2 * Real.sqrt (log ↑N))
⊢ 1 < 4096
norm_num1
case refine'_3.refine'_2
α : Type ?u.793471
β : Type ?u.793474
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 ≤ n
this✝ : (2 * dValue N - 1) ^ n ≤ N
this : exp (-4 * Real.sqrt (log ↑N)) = exp (-2 * Real.sqrt (log ↑N)) * exp (-2 * Real.sqrt (log ↑N))
⊢ 1 < N
case refine'_3.refine'_2
α : Type ?u.793471
β : Type ?u.793474
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 ≤ n
this✝ : (2 * dValue N - 1) ^ n ≤ N
this : exp (-4 * Real.sqrt (log ↑N)) = exp (-2 * Real.sqrt (log ↑N)) * exp (-2 * Real.sqrt (log ↑N))
⊢ 1 < ↑N
rw [one_lt_cast]
no goals
case refine'_3.refine'_2
α : Type ?u.793471
β : Type ?u.793474
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 ≤ n
this✝ : (2 * dValue N - 1) ^ n ≤ N
this : exp (-4 * Real.sqrt (log ↑N)) = exp (-2 * Real.sqrt (log ↑N)) * exp (-2 * Real.sqrt (log ↑N))
⊢ 1 < N
exact hN.trans_lt' (by norm_num1)
no goals
α : Type ?u.793471
β : Type ?u.793474
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 ≤ n
this✝ : (2 * dValue N - 1) ^ n ≤ N
this : exp (-4 * Real.sqrt (log ↑N)) = exp (-2 * Real.sqrt (log ↑N)) * exp (-2 * Real.sqrt (log ↑N))
⊢ 1 < 4096
norm_num1