α : Type ?u.738856
β : Type ?u.738859
n d k N : ℕ
x : Fin n → ℕ
hN : 3 ≤ N
⊢ ↑1 ^ 2 < log ↑N
α : Type ?u.738856
β : Type ?u.738859
n d k N : ℕ
x : Fin n → ℕ
hN : 3 ≤ N
⊢ 2 ≤ nValue N
refine' succ_le_of_lt (lt_ceil.2 <| lt_sqrt_of_sq_lt _)
α : Type ?u.738856
β : Type ?u.738859
n d k N : ℕ
x : Fin n → ℕ
hN : 3 ≤ N
⊢ exp 1 < ↑N

α : Type ?u.738856
β : Type ?u.738859
n d k N : ℕ
x : Fin n → ℕ
hN : 3 ≤ N
⊢ 0 < ↑N
α : Type ?u.738856
β : Type ?u.738859
n d k N : ℕ
x : Fin n → ℕ
hN : 3 ≤ N
⊢ ↑1 ^ 2 < log ↑N
rw [cast_one, one_pow, lt_log_iff_exp_lt]
α : Type ?u.738856
β : Type ?u.738859
n d k N : ℕ
x : Fin n → ℕ
hN : 3 ≤ N
⊢ exp 1 < ↑3

α : Type ?u.738856
β : Type ?u.738859
n d k N : ℕ
x : Fin n → ℕ
hN : 3 ≤ N
⊢ 0 < ↑N
α : Type ?u.738856
β : Type ?u.738859
n d k N : ℕ
x : Fin n → ℕ
hN : 3 ≤ N
⊢ exp 1 < ↑N

α : Type ?u.738856
β : Type ?u.738859
n d k N : ℕ
x : Fin n → ℕ
hN : 3 ≤ N
⊢ 0 < ↑N
refine' lt_of_lt_of_le _ (cast_le.2 hN)
α : Type ?u.738856
β : Type ?u.738859
n d k N : ℕ
x : Fin n → ℕ
hN : 3 ≤ N
⊢ 0 < N
α : Type ?u.738856
β : Type ?u.738859
n d k N : ℕ
x : Fin n → ℕ
hN : 3 ≤ N
⊢ 0 < ↑N
rw [cast_pos]
no goals
α : Type ?u.738856
β : Type ?u.738859
n d k N : ℕ
x : Fin n → ℕ
hN : 3 ≤ N
⊢ 0 < N
exact (zero_lt_succ _).trans_le hN
no goals
α : Type ?u.738856
β : Type ?u.738859
n d k N : ℕ
x : Fin n → ℕ
hN : 3 ≤ N
⊢ exp 1 < ↑3
exact exp_one_lt_d9.trans_le (by norm_num)
no goals
α : Type ?u.738856
β : Type ?u.738859
n d k N : ℕ
x : Fin n → ℕ
hN : 3 ≤ N
⊢ 2.7182818286 ≤ ↑3
norm_num