-- Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean
theorem le_sqrt_log (hN : 4096 ≤ N) : log (2 / (1 - 2 / exp 1)) * (69 / 50) ≤ √(log ↑N)

Proof state:
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

Tactic:
apply mul_le_mul_of_nonneg_right _ (log_nonneg one_le_two)

Result:
N : ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
l8 : log 8 = ↑3 * log 2
⊢ (↑3 * (69 / 50)) ^ 2 * log 2 ≤ ↑12

Proof state:
case refine_1
N : ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
⊢ 0 < 2 / (1 - 2 / rexp 1)

Tactic:
refine div_pos zero_lt_two ?_

Result:
case refine_1
N : ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
⊢ 0 < 1 - 2 / rexp 1

Proof state:
N : ℕ
hN : 4096 ≤ N
⊢ log (2 / (1 - 2 / rexp 1)) * (69 / 50) ≤ √(log ↑N)

Tactic:
have : (12 : ℕ) * log 2 ≤ log N := by
  rw [← log_rpow zero_lt_two, rpow_natCast]
  exact log_le_log (by positivity) (mod_cast hN)

Result:
N : ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
⊢ log (2 / (1 - 2 / rexp 1)) * (69 / 50) ≤ √(log ↑N)

Proof state:
case refine_2
N : ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
l8 : log 8 = ↑3 * log 2
⊢ ↑3 * log 2 * (69 / 50) ≤ √(log ↑N)

Tactic:
apply le_sqrt_of_sq_le (le_trans _ this)

Result:
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

Proof state:
N : ℕ
hN : 4096 ≤ N
⊢ log (2 ^ 12) ≤ log ↑N

Tactic:
exact log_le_log (by positivity) (mod_cast hN)

Result:
no goals

Proof state:
case refine_2
N : ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
l8 : log 8 = ↑3 * log 2
⊢ log 8 * (69 / 50) ≤ √(log ↑N)

Tactic:
rw [l8]

Result:
case refine_2
N : ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
l8 : log 8 = ↑3 * log 2
⊢ ↑3 * log 2 * (69 / 50) ≤ √(log ↑N)

Proof state:
N : ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
⊢ log 8 = log (2 ^ 3)

Tactic:
norm_num

Result:
no goals

Proof state:
case refine_1
N : ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
⊢ 2 < rexp 1

Tactic:
exact exp_one_gt_d9.trans_le' (by norm_num1)

Result:
no goals

Proof state:
N : ℕ
hN : 4096 ≤ N
⊢ 0 < 2 ^ 12

Tactic:
positivity

Result:
no goals

Proof state:
N : ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
l8 : log 8 = ↑3 * log 2
⊢ 0.6931471808 ≤ ↑12 / (↑3 * (69 / 50)) ^ 2

Tactic:
norm_num1

Result:
no goals

Proof state:
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

Tactic:
rw [mul_right_comm, mul_pow, sq (log 2), ← mul_assoc]

Result:
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

Proof state:
case refine_2
N : ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
⊢ log 8 * (69 / 50) ≤ √(log ↑N)

Tactic:
have l8 : log 8 = (3 : ℕ) * log 2 := by
  rw [← log_rpow zero_lt_two, rpow_natCast]
  norm_num

Result:
case refine_2
N : ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
l8 : log 8 = ↑3 * log 2
⊢ log 8 * (69 / 50) ≤ √(log ↑N)

Proof state:
N : ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
l8 : log 8 = ↑3 * log 2
⊢ log 2 ≤ ↑12 / (↑3 * (69 / 50)) ^ 2

Tactic:
exact log_two_lt_d9.le.trans (by norm_num1)

Result:
no goals

Proof state:
N : ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
⊢ log (2 / (1 - 2 / rexp 1)) * (69 / 50) ≤ √(log ↑N)

Tactic:
refine (mul_le_mul_of_nonneg_right (log_le_log ?_ two_div_one_sub_two_div_e_le_eight) <| by
  norm_num1).trans ?_

Result:
case refine_1
N : ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
⊢ 0 < 2 / (1 - 2 / rexp 1)

case refine_2
N : ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
⊢ log 8 * (69 / 50) ≤ √(log ↑N)

Proof state:
N : ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
⊢ log 8 = ↑3 * log 2

Tactic:
rw [← log_rpow zero_lt_two, rpow_natCast]

Result:
N : ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
⊢ log 8 = log (2 ^ 3)

Proof state:
N : ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
l8 : log 8 = ↑3 * log 2
⊢ 0 < (↑3 * (69 / 50)) ^ 2

Tactic:
exact sq_pos_of_ne_zero (by norm_num1)

Result:
no goals

Proof state:
N : ℕ
hN : 4096 ≤ N
⊢ ↑12 * log 2 ≤ log ↑N

Tactic:
rw [← log_rpow zero_lt_two, rpow_natCast]

Result:
N : ℕ
hN : 4096 ≤ N
⊢ log (2 ^ 12) ≤ log ↑N

Proof state:
N : ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
l8 : log 8 = ↑3 * log 2
⊢ ↑3 * (69 / 50) ≠ 0

Tactic:
norm_num1

Result:
no goals

Proof state:
N : ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
l8 : log 8 = ↑3 * log 2
⊢ (↑3 * (69 / 50)) ^ 2 * log 2 ≤ ↑12

Tactic:
rw [← le_div_iff₀']

Result:
N : ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
l8 : log 8 = ↑3 * log 2
⊢ log 2 ≤ ↑12 / (↑3 * (69 / 50)) ^ 2

N : ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
l8 : log 8 = ↑3 * log 2
⊢ 0 < (↑3 * (69 / 50)) ^ 2

Proof state:
N : ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
⊢ 0 ≤ 69 / 50

Tactic:
norm_num1

Result:
no goals

Proof state:
case refine_1
N : ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
⊢ 0 < 1 - 2 / rexp 1

Tactic:
rw [sub_pos, div_lt_one (exp_pos _)]

Result:
case refine_1
N : ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
⊢ 2 < rexp 1

Proof state:
N : ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
⊢ 2 ≤ 2.7182818283

Tactic:
norm_num1

Result:
no goals