α : Type ?u.838456
β : Type ?u.838459
n d k N : ℕ
x : Fin n → ℕ
⊢ 12 * log 2 < 16
α : Type ?u.838456
β : Type ?u.838459
n d k N : ℕ
x : Fin n → ℕ
⊢ 4096 < exp 16
rw [← log_lt_iff_lt_exp (show (0 : ℝ) < 4096 by norm_num), show (4096 : ℝ) = 2 ^ 12 by norm_cast,
  log_rpow zero_lt_two]
α : Type ?u.838456
β : Type ?u.838459
n d k N : ℕ
x : Fin n → ℕ
this : 12 * 0.6931471808 < 16
⊢ 12 * log 2 < 16
α : Type ?u.838456
β : Type ?u.838459
n d k N : ℕ
x : Fin n → ℕ
⊢ 12 * log 2 < 16
have : 12 * (0.6931471808 : ℝ) < 16 := by norm_num
no goals
α : Type ?u.838456
β : Type ?u.838459
n d k N : ℕ
x : Fin n → ℕ
this : 12 * 0.6931471808 < 16
⊢ 12 * log 2 < 16
linarith [log_two_lt_d9]
no goals
α : Type ?u.838456
β : Type ?u.838459
n d k N : ℕ
x : Fin n → ℕ
⊢ 0 < 4096
norm_num
no goals
α : Type ?u.838456
β : Type ?u.838459
n d k N : ℕ
x : Fin n → ℕ
⊢ 4096 = 2 ^ 12
norm_cast
no goals
α : Type ?u.838456
β : Type ?u.838459
n d k N : ℕ
x : Fin n → ℕ
⊢ 12 * 0.6931471808 < 16
norm_num