-- Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean
theorem roth_lower_bound_explicit (hN : 4096 ≤ N) :
    (N : ℝ) * exp (-4 * √(log N)) < rothNumberNat N

Proof state:
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 : rexp (-4 * √(log ↑N)) = rexp (-2 * √(log ↑N)) * rexp (-2 * √(log ↑N))
⊢ rexp (-4 * √(log ↑N)) ≤ ↑N ^ (-(2 / ↑n)) * (rexp (2 - ↑n) / ↑n)

Tactic:
rw [this]

Result:
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 : rexp (-4 * √(log ↑N)) = rexp (-2 * √(log ↑N)) * rexp (-2 * √(log ↑N))
⊢ rexp (-2 * √(log ↑N)) * rexp (-2 * √(log ↑N)) ≤ ↑N ^ (-(2 / ↑n)) * (rexp (2 - ↑n) / ↑n)

Proof state:
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
⊢ rexp (-4 * √(log ↑N)) ≤ ↑N ^ (-(2 / ↑n)) * (rexp (2 - ↑n) / ↑n)

Tactic:
have : exp (-4 * √(log N)) = exp (-2 * √(log N)) * exp (-2 * √(log N)) := by
  rw [← exp_add, ← add_mul]
  norm_num

Result:
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 : rexp (-4 * √(log ↑N)) = rexp (-2 * √(log ↑N)) * rexp (-2 * √(log ↑N))
⊢ rexp (-4 * √(log ↑N)) ≤ ↑N ^ (-(2 / ↑n)) * (rexp (2 - ↑n) / ↑n)

Proof state:
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 : rexp (-4 * √(log ↑N)) = rexp (-2 * √(log ↑N)) * rexp (-2 * √(log ↑N))
⊢ rexp (-2 * √(log ↑N)) * rexp (-2 * √(log ↑N)) ≤ ↑N ^ (-(2 / ↑n)) * (rexp (2 - ↑n) / ↑n)

Tactic:
refine mul_le_mul ?_ (exp_neg_two_mul_le <| Real.sqrt_pos.2 <| log_pos ?_).le (exp_pos _).le <|
    rpow_nonneg (cast_nonneg _) _

Result:
case refine_1
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 : rexp (-4 * √(log ↑N)) = rexp (-2 * √(log ↑N)) * rexp (-2 * √(log ↑N))
⊢ rexp (-2 * √(log ↑N)) ≤ ↑N ^ (-(2 / ↑n))

case refine_2
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 : rexp (-4 * √(log ↑N)) = rexp (-2 * √(log ↑N)) * rexp (-2 * √(log ↑N))
⊢ 1 < ↑N

Proof state:
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
⊢ ↑N * rexp (-4 * √(log ↑N)) < ↑(rothNumberNat N)

Tactic:
have hn₂ : 2 < n := three_le_nValue <| hN.trans' <| by norm_num1

Result:
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 < n
⊢ ↑N * rexp (-4 * √(log ↑N)) < ↑(rothNumberNat N)

Proof state:
case refine_1
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 : rexp (-4 * √(log ↑N)) = rexp (-2 * √(log ↑N)) * rexp (-2 * √(log ↑N))
⊢ 2 * √(log ↑N) ≤ 2 * ↑n

Tactic:
exact mul_le_mul_of_nonneg_left (le_ceil _) zero_le_two

Result:
no goals

Proof state:
N : ℕ
hN : 4096 ≤ N
⊢ ↑N * rexp (-4 * √(log ↑N)) < ↑(rothNumberNat N)

Tactic:
let n := nValue N

Result:
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
⊢ ↑N * rexp (-4 * √(log ↑N)) < ↑(rothNumberNat N)

Proof state:
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
⊢ ↑N * rexp (-4 * √(log ↑N)) < ↑(rothNumberNat N)

Tactic:
have hN₀ : 0 < (N : ℝ) := cast_pos.2 (hN.trans' <| by norm_num1)

Result:
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
⊢ ↑N * rexp (-4 * √(log ↑N)) < ↑(rothNumberNat N)

Proof state:
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 < n
⊢ ↑N * rexp (-4 * √(log ↑N)) < ↑(rothNumberNat N)

Tactic:
have : (2 * dValue N - 1) ^ n ≤ N := le_N (hN.trans' <| by norm_num1)

Result:
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 * rexp (-4 * √(log ↑N)) < ↑(rothNumberNat N)

Proof state:
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
⊢ succ 0 ≤ 4096

Tactic:
norm_num1

Result:
no goals

Proof state:
case refine_1
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 : rexp (-4 * √(log ↑N)) = rexp (-2 * √(log ↑N)) * rexp (-2 * √(log ↑N))
⊢ 1 < ↑N

Tactic:
rw [one_lt_cast]

Result:
case refine_1
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 : rexp (-4 * √(log ↑N)) = rexp (-2 * √(log ↑N)) * rexp (-2 * √(log ↑N))
⊢ 1 < N

Proof state:
case h.a
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 - 2 ≠ 0

case h.hab
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 ^ (↑(nValue N))⁻¹ / rexp 1 < ↑(dValue N)

Tactic:
exacts [(tsub_pos_of_lt hn₂).ne', bound hN]

Result:
no goals

Proof state:
case refine_1
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 : rexp (-4 * √(log ↑N)) = rexp (-2 * √(log ↑N)) * rexp (-2 * √(log ↑N))
⊢ 0 < √(log ↑N)

Tactic:
refine Real.sqrt_pos.2 (log_pos ?_)

Result:
case refine_1
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 : rexp (-4 * √(log ↑N)) = rexp (-2 * √(log ↑N)) * rexp (-2 * √(log ↑N))
⊢ 1 < ↑N

Proof state:
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
⊢ 2 ≤ 4096

Tactic:
norm_num1

Result:
no goals

Proof state:
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 ^ (↑(nValue N))⁻¹ / rexp 1) ^ (n - 2) / ↑n < ↑(dValue N) ^ (n - 2) / ↑n

Tactic:
gcongr

Result:
case h.a
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 - 2 ≠ 0

case h.hab
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 ^ (↑(nValue N))⁻¹ / rexp 1 < ↑(dValue N)

Proof state:
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
⊢ 64 ≤ 4096

Tactic:
norm_num1

Result:
no goals

Proof state:
case refine_1
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 : rexp (-4 * √(log ↑N)) = rexp (-2 * √(log ↑N)) * rexp (-2 * √(log ↑N))
⊢ rexp (-2 * √(log ↑N)) ≤ ↑N ^ (-(2 / ↑n))

Tactic:
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]

Result:
case refine_1
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 : rexp (-4 * √(log ↑N)) = rexp (-2 * √(log ↑N)) * rexp (-2 * √(log ↑N))
⊢ 2 * √(log ↑N) ≤ 2 * ↑n

case refine_1
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 : rexp (-4 * √(log ↑N)) = rexp (-2 * √(log ↑N)) * rexp (-2 * √(log ↑N))
⊢ 0 < √(log ↑N)

Proof state:
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 * rexp (-4 * √(log ↑N)) ≤ ↑N * (↑N ^ (2 / ↑n) * (rexp (↑n - 2) * ↑n))⁻¹

Tactic:
refine mul_le_mul_of_nonneg_left ?_ (cast_nonneg _)

Result:
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
⊢ rexp (-4 * √(log ↑N)) ≤ (↑N ^ (2 / ↑n) * (rexp (↑n - 2) * ↑n))⁻¹