α : Type ?u.837007
β : Type ?u.837010
n d k N : ℕ
x : Fin n → ℕ
⊢ 4 / ↑6 < log 2

α : Type ?u.837007
β : Type ?u.837010
n d k N : ℕ
x : Fin n → ℕ
⊢ 0 < ↑6
α : Type ?u.837007
β : Type ?u.837010
n d k N : ℕ
x : Fin n → ℕ
⊢ exp 4 < 64
rw [show (64 : ℝ) = 2 ^ ((6 : ℕ) : ℝ) by rw [rpow_nat_cast]; norm_num1,
  ← lt_log_iff_exp_lt (rpow_pos_of_pos zero_lt_two _), log_rpow zero_lt_two, ← div_lt_iff']
α : Type ?u.837007
β : Type ?u.837010
n d k N : ℕ
x : Fin n → ℕ
⊢ 0 < ↑6
α : Type ?u.837007
β : Type ?u.837010
n d k N : ℕ
x : Fin n → ℕ
⊢ 4 / ↑6 < log 2

α : Type ?u.837007
β : Type ?u.837010
n d k N : ℕ
x : Fin n → ℕ
⊢ 0 < ↑6
exact log_two_gt_d9.trans_le' (by norm_num1)
no goals
α : Type ?u.837007
β : Type ?u.837010
n d k N : ℕ
x : Fin n → ℕ
⊢ 0 < ↑6
norm_num
α : Type ?u.837007
β : Type ?u.837010
n d k N : ℕ
x : Fin n → ℕ
⊢ 64 = 2 ^ 6
α : Type ?u.837007
β : Type ?u.837010
n d k N : ℕ
x : Fin n → ℕ
⊢ 64 = 2 ^ ↑6
rw [rpow_nat_cast]
no goals
α : Type ?u.837007
β : Type ?u.837010
n d k N : ℕ
x : Fin n → ℕ
⊢ 64 = 2 ^ 6
norm_num1
no goals
α : Type ?u.837007
β : Type ?u.837010
n d k N : ℕ
x : Fin n → ℕ
⊢ 4 / ↑6 ≤ 0.6931471803
norm_num1