awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 2 ≤ N
this : (2 * dValue N - 1) ^ nValue N ≤ (2 * dValue N) ^ nValue N
suffices : HMul.hMul (α := ℝ) 2 (↑(dValue N) : ℝ) ^ nValue N ≤ (↑N : ℝ)
⊢ (2 * dValue N) ^ nValue N ≤ N

Tactic:
suffices ((2 * dValue N) ^ nValue N : ℝ) ≤ N from mod_cast this
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 2 ≤ N
this : (2 * dValue N - 1) ^ nValue N ≤ (2 * dValue N) ^ nValue N
i : HMul.hMul (α := ℝ) 2 (↑(dValue N) : ℝ) ≤ HPow.hPow (α := ℝ) (β := ℝ) (↑N : ℝ) (↑(nValue N) : ℝ)⁻¹
rw : HPow.hPow (β := ℝ) (HMul.hMul (α := ℝ) 2 (↑(dValue N) : ℝ)) (↑(nValue N) : ℝ) ≤ (↑N : ℝ)
⊢ HMul.hMul (α := ℝ) 2 (↑(dValue N) : ℝ) ^ nValue N ≤ (↑N : ℝ)

Tactic:
rw [← rpow_natCast]

Premises used: Real.rpow_natCast
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 2 ≤ N
this : (2 * dValue N - 1) ^ nValue N ≤ (2 * dValue N) ^ nValue N
i : HMul.hMul (α := ℝ) 2 (↑(dValue N) : ℝ) ≤ HPow.hPow (α := ℝ) (β := ℝ) (↑N : ℝ) (↑(nValue N) : ℝ)⁻¹
apply : HPow.hPow (β := ℝ) (HPow.hPow (α := ℝ) (β := ℝ) (↑N : ℝ) (↑(nValue N) : ℝ)⁻¹) (↑(nValue N) : ℝ) ≤ (↑N : ℝ)
⊢ HPow.hPow (β := ℝ) (HMul.hMul (α := ℝ) 2 (↑(dValue N) : ℝ)) (↑(nValue N) : ℝ) ≤ (↑N : ℝ)

Tactic:
apply (rpow_le_rpow (mul_nonneg zero_le_two (cast_nonneg _)) i (cast_nonneg _)).trans

Premises used: mul_nonneg, Nat.cast_nonneg, Real.rpow_le_rpow, zero_le_two, LE.le.trans
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 2 ≤ N
this : (2 * dValue N - 1) ^ nValue N ≤ (2 * dValue N) ^ nValue N
i : HMul.hMul (α := ℝ) 2 (↑(dValue N) : ℝ) ≤ HPow.hPow (α := ℝ) (β := ℝ) (↑N : ℝ) (↑(nValue N) : ℝ)⁻¹
rw : Ne (α := ℝ) (↑(nValue N) : ℝ) 0
⊢ HPow.hPow (β := ℝ) (HPow.hPow (α := ℝ) (β := ℝ) (↑N : ℝ) (↑(nValue N) : ℝ)⁻¹) (↑(nValue N) : ℝ) ≤ (↑N : ℝ)

Tactic:
rw [← rpow_mul (cast_nonneg _), inv_mul_cancel₀, rpow_one]

Premises used: Nat.cast_nonneg, Real.rpow_one, Real.rpow_mul, inv_mul_cancel₀
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 2 ≤ N
this : (2 * dValue N - 1) ^ nValue N ≤ (2 * dValue N) ^ nValue N
i : HMul.hMul (α := ℝ) 2 (↑(dValue N) : ℝ) ≤ HPow.hPow (α := ℝ) (β := ℝ) (↑N : ℝ) (↑(nValue N) : ℝ)⁻¹
rw : nValue N ≠ 0
⊢ Ne (α := ℝ) (↑(nValue N) : ℝ) 0

Tactic:
rw [cast_ne_zero]

Premises used: Nat.cast_ne_zero
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 2 ≤ N
this : (2 * dValue N - 1) ^ nValue N ≤ (2 * dValue N) ^ nValue N
i : HMul.hMul (α := ℝ) 2 (↑(dValue N) : ℝ) ≤ HPow.hPow (α := ℝ) (β := ℝ) (↑N : ℝ) (↑(nValue N) : ℝ)⁻¹
⊢ nValue N ≠ 0

Tactic:
apply (nValue_pos hN).ne'

Premises used: Behrend.nValue_pos, LT.lt.ne'
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 2 ≤ N
this : (2 * dValue N - 1) ^ nValue N ≤ (2 * dValue N) ^ nValue N
suffices : HMul.hMul (α := ℝ) 2 (↑(dValue N) : ℝ) ≤ HPow.hPow (α := ℝ) (β := ℝ) (↑N : ℝ) (↑(nValue N) : ℝ)⁻¹
⊢ HMul.hMul (α := ℝ) 2 (↑(dValue N) : ℝ) ^ nValue N ≤ (↑N : ℝ)

Tactic:
suffices i : (2 * dValue N : ℝ) ≤ (N : ℝ) ^ (nValue N : ℝ)⁻¹ by
    rw [← rpow_natCast]
    apply (rpow_le_rpow (mul_nonneg zero_le_two (cast_nonneg _)) i (cast_nonneg _)).trans
    rw [← rpow_mul (cast_nonneg _), inv_mul_cancel₀, rpow_one]
    rw [cast_ne_zero]
    apply (nValue_pos hN).ne'
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 2 ≤ N
this : (2 * dValue N - 1) ^ nValue N ≤ (2 * dValue N) ^ nValue N
rw : (↑(dValue N) : ℝ) ≤ HPow.hPow (α := ℝ) (β := ℝ) (↑N : ℝ) (↑(nValue N) : ℝ)⁻¹ / 2
rw₁ : LT.lt (α := ℝ) 0 2
⊢ HMul.hMul (α := ℝ) 2 (↑(dValue N) : ℝ) ≤ HPow.hPow (α := ℝ) (β := ℝ) (↑N : ℝ) (↑(nValue N) : ℝ)⁻¹

Tactic:
rw [← le_div_iff₀']

Premises used: le_div_iff₀'
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 2 ≤ N
this : (2 * dValue N - 1) ^ nValue N ≤ (2 * dValue N) ^ nValue N
⊢ 0 ≤ HPow.hPow (α := ℝ) (β := ℝ) (↑N : ℝ) (↑(nValue N) : ℝ)⁻¹ / 2

Tactic:
positivity
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 2 ≤ N
this : (2 * dValue N - 1) ^ nValue N ≤ (2 * dValue N) ^ nValue N
⊢ (↑(dValue N) : ℝ) ≤ HPow.hPow (α := ℝ) (β := ℝ) (↑N : ℝ) (↑(nValue N) : ℝ)⁻¹ / 2

Tactic:
exact floor_le (by positivity)

Premises used: Nat.floor_le
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 2 ≤ N
this : (2 * dValue N - 1) ^ nValue N ≤ (2 * dValue N) ^ nValue N
⊢ LT.lt (α := ℝ) 0 2

Tactic:
apply zero_lt_two

Premises used: zero_lt_two
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 4096 ≤ N
apply : 2 / (1 - 2 / rexp 1) ≤ HPow.hPow (α := ℝ) (β := ℝ) (↑N : ℝ) (↑(nValue N) : ℝ)⁻¹
⊢ HPow.hPow (α := ℝ) (β := ℝ) (↑N : ℝ) (↑(nValue N) : ℝ)⁻¹ / rexp 1 < (↑(dValue N) : ℝ)

Tactic:
apply div_lt_floor _

Premises used: Behrend.div_lt_floor
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 4096 ≤ N
rw : log (2 / (1 - 2 / rexp 1)) ≤ log (↑N : ℝ) / (↑⌈√(log (↑N : ℝ))⌉₊ : ℝ)
hx : LT.lt (α := ℝ) 0 (↑N : ℝ)
h : 0 < 2 / (1 - 2 / rexp 1)
h₁ : 0 < HPow.hPow (α := ℝ) (β := ℝ) (↑N : ℝ) (↑(nValue N) : ℝ)⁻¹
⊢ 2 / (1 - 2 / rexp 1) ≤ HPow.hPow (α := ℝ) (β := ℝ) (↑N : ℝ) (↑(nValue N) : ℝ)⁻¹

Tactic:
rw [← log_le_log_iff, log_rpow, mul_comm, ← div_eq_mul_inv, nValue]

Premises used: Real.log_rpow, div_eq_mul_inv, Real.log_le_log_iff, mul_comm, Behrend.nValue
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 4096 ≤ N
grw : log (2 / (1 - 2 / rexp 1)) ≤ log (↑N : ℝ) / (1.38 * √(log (↑N : ℝ)))
h₂ : LT.lt (α := ℝ) 0 (↑⌈√(log (↑N : ℝ))⌉₊ : ℝ)
grw₁ : 50 / 19 ≤ √(log (↑N : ℝ))
⊢ log (2 / (1 - 2 / rexp 1)) ≤ log (↑N : ℝ) / (↑⌈√(log (↑N : ℝ))⌉₊ : ℝ)

Tactic:
grw [ceil_lt_mul]

Premises used: Behrend.ceil_lt_mul
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 4096 ≤ N
rw : log (2 / (1 - 2 / rexp 1)) * 1.38 ≤ √(log (↑N : ℝ))
rw₁ : LT.lt (α := ℝ) 0 1.38
⊢ log (2 / (1 - 2 / rexp 1)) ≤ log (↑N : ℝ) / (1.38 * √(log (↑N : ℝ)))

Tactic:
rw [mul_comm, ← div_div, div_sqrt, le_div_iff₀]

Premises used: Real.div_sqrt, mul_comm, div_div, le_div_iff₀
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 4096 ≤ N
⊢ log (2 / (1 - 2 / rexp 1)) * 1.38 ≤ √(log (↑N : ℝ))

Tactic:
norm_num [le_sqrt_log hN]

Premises used: Behrend.le_sqrt_log
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 4096 ≤ N
⊢ LT.lt (α := ℝ) 0 1.38

Tactic:
norm_num1
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 4096 ≤ N
h₂ : 0 < log (↑N : ℝ)
⊢ LT.lt (α := ℝ) 0 (↑⌈√(log (↑N : ℝ))⌉₊ : ℝ)

Tactic:
rw [cast_pos, lt_ceil, cast_zero, Real.sqrt_pos]

Premises used: Nat.cast_pos, Real.sqrt_pos, Nat.lt_ceil, Nat.cast_zero
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 4096 ≤ N
⊢ 0 < log (↑N : ℝ)

Tactic:
log_pos ?_

Premises used: Real.log_pos
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 4096 ≤ N
h₂ : LT.lt (α := ℝ) 1 (↑N : ℝ)
⊢ 0 < log (↑N : ℝ)

Tactic:
refine log_pos ?_
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 4096 ≤ N
h₂ : 1 < N
⊢ LT.lt (α := ℝ) 1 (↑N : ℝ)

Tactic:
rw [one_lt_cast]

Premises used: Nat.one_lt_cast
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 4096 ≤ N
⊢ LT.lt (α := ℕ) 1 4096

Tactic:
norm_num1
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 4096 ≤ N
⊢ 1 < N

Tactic:
exact hN.trans_lt' (by norm_num1)

Premises used: LE.le.trans_lt'
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 4096 ≤ N
h : HPow.hPow (β := ℕ) (50 / 19) 2 ≤ log (↑N : ℝ)
⊢ 50 / 19 ≤ √(log (↑N : ℝ))

Tactic:
apply le_sqrt_of_sq_le

Premises used: Real.le_sqrt_of_sq_le
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 4096 ≤ N
rw : log (HPow.hPow (α := ℝ) (β := ℕ) 2 12) ≤ log (↑N : ℝ)
⊢ (↑12 : ℝ) * log 2 ≤ log (↑N : ℝ)

Tactic:
rw [← log_rpow zero_lt_two, rpow_natCast]

Premises used: Real.log_rpow, zero_lt_two, Real.rpow_natCast
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 4096 ≤ N
⊢ 0 < HPow.hPow (α := ℝ) (β := ℕ) 2 12

Tactic:
positivity
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 4096 ≤ N
⊢ log (HPow.hPow (α := ℝ) (β := ℕ) 2 12) ≤ log (↑N : ℝ)

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

Premises used: Real.log_le_log
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 4096 ≤ N
⊢ (↑12 : ℝ) * log 2 ≤ 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)
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 4096 ≤ N
this : (↑12 : ℝ) * log 2 ≤ log (↑N : ℝ)
⊢ HPow.hPow (β := ℕ) (50 / 19) 2 ≤ log (↑N : ℝ)

Tactic:
le_trans ?_ this

Premises used: le_trans
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 4096 ≤ N
this : (↑12 : ℝ) * log 2 ≤ log (↑N : ℝ)
h : HPow.hPow (β := ℕ) (50 / 19) 2 ≤ (↑12 : ℝ) * log 2
⊢ HPow.hPow (β := ℕ) (50 / 19) 2 ≤ log (↑N : ℝ)

Tactic:
refine le_trans ?_ this

Premises used: le_trans
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 4096 ≤ N
this : (↑12 : ℝ) * log 2 ≤ log (↑N : ℝ)
h : HPow.hPow (β := ℕ) (50 / 19) 2 / (↑12 : ℝ) ≤ log 2
h₁ : LT.lt (α := ℝ) 0 (↑12 : ℝ)
⊢ HPow.hPow (β := ℕ) (50 / 19) 2 ≤ (↑12 : ℝ) * log 2

Tactic:
rw [← div_le_iff₀']

Premises used: div_le_iff₀'
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 4096 ≤ N
this : (↑12 : ℝ) * log 2 ≤ log (↑N : ℝ)
⊢ HPow.hPow (β := ℕ) (50 / 19) 2 / (↑12 : ℝ) ≤ 0.6931471803

Tactic:
norm_num1
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 4096 ≤ N
this : (↑12 : ℝ) * log 2 ≤ log (↑N : ℝ)
⊢ HPow.hPow (β := ℕ) (50 / 19) 2 / (↑12 : ℝ) ≤ log 2

Tactic:
exact log_two_gt_d9.le.trans' (by norm_num1)

Premises used: Real.log_two_gt_d9, LT.lt.le, LE.le.trans'
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 4096 ≤ N
this : (↑12 : ℝ) * log 2 ≤ log (↑N : ℝ)
⊢ LT.lt (α := ℝ) 0 (↑12 : ℝ)

Tactic:
norm_num1
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 4096 ≤ N
hx : 0 < N
⊢ LT.lt (α := ℝ) 0 (↑N : ℝ)

Tactic:
rw [cast_pos]

Premises used: Nat.cast_pos
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 4096 ≤ N
⊢ LT.lt (α := ℕ) 0 4096

Tactic:
norm_num1
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 4096 ≤ N
⊢ 0 < N

Tactic:
exact hN.trans_lt' (by norm_num1)

Premises used: LE.le.trans_lt'
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 4096 ≤ N
⊢ 0 < 2 / (1 - 2 / rexp 1)

Tactic:
div_pos zero_lt_two ?_

Premises used: div_pos, zero_lt_two
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 4096 ≤ N
h : 0 < 1 - 2 / rexp 1
⊢ 0 < 2 / (1 - 2 / rexp 1)

Tactic:
refine div_pos zero_lt_two ?_
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 4096 ≤ N
h : 2 < rexp 1
⊢ 0 < 1 - 2 / rexp 1

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

Premises used: sub_pos, div_lt_one, Real.exp_pos
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 4096 ≤ N
⊢ 2 < rexp 1

Tactic:
exp_one_gt_two

Premises used: Real.exp_one_gt_two
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 4096 ≤ N
⊢ 2 < rexp 1

Tactic:
exact exp_one_gt_two

Premises used: Real.exp_one_gt_two
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 4096 ≤ N
⊢ 0 < HPow.hPow (α := ℝ) (β := ℝ) (↑N : ℝ) (↑(nValue N) : ℝ)⁻¹

Tactic:
positivity
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
⊢ LE.le (α := ℕ) 2 4096

Tactic:
norm_num1
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
⊢ LT.lt (α := ℝ) 0 (↑n : ℝ)

Tactic:
have hn : 0 < (n : ℝ) := cast_pos.2 (nValue_pos <| hN.trans' <| by norm_num1)
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : LT.lt (α := ℝ) 0 (↑n : ℝ)
⊢ LE.le (α := ℕ) 8 4096

Tactic:
norm_num1
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : LT.lt (α := ℝ) 0 (↑n : ℝ)
⊢ 0 < dValue N

Tactic:
have hd : 0 < dValue N := dValue_pos (hN.trans' <| by norm_num1)
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : LT.lt (α := ℝ) 0 (↑n : ℝ)
hd : 0 < dValue N
⊢ succ 0 ≤ 4096

Tactic:
norm_num1
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : LT.lt (α := ℝ) 0 (↑n : ℝ)
hd : 0 < dValue N
⊢ LT.lt (α := ℝ) 0 (↑N : ℝ)

Tactic:
have hN₀ : 0 < (N : ℝ) := cast_pos.2 (hN.trans' <| by norm_num1)
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : LT.lt (α := ℝ) 0 (↑n : ℝ)
hd : 0 < dValue N
hN₀ : LT.lt (α := ℝ) 0 (↑N : ℝ)
⊢ LE.le (α := ℕ) 64 4096

Tactic:
norm_num1
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : LT.lt (α := ℝ) 0 (↑n : ℝ)
hd : 0 < dValue N
hN₀ : LT.lt (α := ℝ) 0 (↑N : ℝ)
⊢ 2 < n

Tactic:
have hn₂ : 2 < n := three_le_nValue <| hN.trans' <| by norm_num1
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : LT.lt (α := ℝ) 0 (↑n : ℝ)
hd : 0 < dValue N
hN₀ : LT.lt (α := ℝ) 0 (↑N : ℝ)
hn₂ : 2 < n
⊢ LE.le (α := ℕ) 2 4096

Tactic:
norm_num1
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : LT.lt (α := ℝ) 0 (↑n : ℝ)
hd : 0 < dValue N
hN₀ : LT.lt (α := ℝ) 0 (↑N : ℝ)
hn₂ : 2 < n
⊢ (2 * dValue N - 1) ^ n ≤ N

Tactic:
have : (2 * dValue N - 1) ^ n ≤ N := le_N (hN.trans' <| by norm_num1)
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : LT.lt (α := ℝ) 0 (↑n : ℝ)
hd : 0 < dValue N
hN₀ : LT.lt (α := ℝ) 0 (↑N : ℝ)
hn₂ : 2 < n
this : (2 * dValue N - 1) ^ n ≤ N
⊢ (↑N : ℝ) * rexp (-4 * √(log (↑N : ℝ))) ≤
    (HPow.hPow (α := ℝ) (β := ℝ) (↑N : ℝ) (↑(nValue N) : ℝ)⁻¹ / rexp 1) ^ (n - 2) / (↑n : ℝ)

Tactic:
?_
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : LT.lt (α := ℝ) 0 (↑n : ℝ)
hd : 0 < dValue N
hN₀ : LT.lt (α := ℝ) 0 (↑N : ℝ)
hn₂ : 2 < n
this : (2 * dValue N - 1) ^ n ≤ N
h : n - 2 ≠ 0
h₁ : HPow.hPow (α := ℝ) (β := ℝ) (↑N : ℝ) (↑(nValue N) : ℝ)⁻¹ / rexp 1 < (↑(dValue N) : ℝ)
⊢ (HPow.hPow (α := ℝ) (β := ℝ) (↑N : ℝ) (↑(nValue N) : ℝ)⁻¹ / rexp 1) ^ (n - 2) / (↑n : ℝ) <
    HPow.hPow (α := ℝ) (↑(dValue N) : ℝ) (n - 2) / (↑n : ℝ)

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : LT.lt (α := ℝ) 0 (↑n : ℝ)
hd : 0 < dValue N
hN₀ : LT.lt (α := ℝ) 0 (↑N : ℝ)
hn₂ : 2 < n
this : (2 * dValue N - 1) ^ n ≤ N
⊢ n - 2 ≠ 0

Tactic:
(tsub_pos_of_lt hn₂).ne'

Premises used: LT.lt.ne', tsub_pos_of_lt
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : LT.lt (α := ℝ) 0 (↑n : ℝ)
hd : 0 < dValue N
hN₀ : LT.lt (α := ℝ) 0 (↑N : ℝ)
hn₂ : 2 < n
this : (2 * dValue N - 1) ^ n ≤ N
⊢ HPow.hPow (α := ℝ) (β := ℝ) (↑N : ℝ) (↑(nValue N) : ℝ)⁻¹ / rexp 1 < (↑(dValue N) : ℝ)

Tactic:
bound hN

Premises used: Behrend.bound
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : LT.lt (α := ℝ) 0 (↑n : ℝ)
hd : 0 < dValue N
hN₀ : LT.lt (α := ℝ) 0 (↑N : ℝ)
hn₂ : 2 < n
this : (2 * dValue N - 1) ^ n ≤ N
⊢ n - 2 ≠ 0

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

Premises used: Behrend.bound, LT.lt.ne', tsub_pos_of_lt
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : LT.lt (α := ℝ) 0 (↑n : ℝ)
hd : 0 < dValue N
hN₀ : LT.lt (α := ℝ) 0 (↑N : ℝ)
hn₂ : 2 < n
this : (2 * dValue N - 1) ^ n ≤ N
⊢ HPow.hPow (α := ℝ) (↑(dValue N) : ℝ) (n - 2) / (↑n : ℝ) ≤
    (↑((rothNumberNat : (a : ℕ) → ℕ) ((2 * dValue N - 1) ^ n)) : ℝ)

Tactic:
bound_aux hd.ne' hn₂.le

Premises used: LT.lt.le, LT.lt.ne', Behrend.bound_aux
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : LT.lt (α := ℝ) 0 (↑n : ℝ)
hd : 0 < dValue N
hN₀ : LT.lt (α := ℝ) 0 (↑N : ℝ)
hn₂ : 2 < n
this : (2 * dValue N - 1) ^ n ≤ N
⊢ LE.le (α := ℝ) (↑((rothNumberNat : (a : ℕ) → ℕ) ((2 * dValue N - 1) ^ n)) : ℝ)
    (↑((rothNumberNat : (a : ℕ) → ℕ) N) : ℝ)

Tactic:
mod_cast rothNumberNat.mono this

Premises used: cast, rothNumberNat, Nat.cast_le._simp_1, OrderHom.mono, Eq.symm
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : LT.lt (α := ℝ) 0 (↑n : ℝ)
hd : 0 < dValue N
hN₀ : LT.lt (α := ℝ) 0 (↑N : ℝ)
hn₂ : 2 < n
this : (2 * dValue N - 1) ^ n ≤ N
_ :
  (↑N : ℝ) * rexp (-4 * √(log (↑N : ℝ))) ≤
    (HPow.hPow (α := ℝ) (β := ℝ) (↑N : ℝ) (↑(nValue N) : ℝ)⁻¹ / rexp 1) ^ (n - 2) / (↑n : ℝ)
⊢ (↑N : ℝ) * rexp (-4 * √(log (↑N : ℝ))) < (↑((rothNumberNat : (a : ℕ) → ℕ) N) : ℝ)

Tactic:
calc
    _ ≤ (N ^ (nValue N : ℝ)⁻¹ / rexp 1 : ℝ) ^ (n - 2) / n := ?_
    _ < _ := by gcongr; exacts [(tsub_pos_of_lt hn₂).ne', bound hN]
    _ ≤ rothNumberNat ((2 * dValue N - 1) ^ n) := bound_aux hd.ne' hn₂.le
    _ ≤ rothNumberNat N := mod_cast rothNumberNat.mono this

Premises used: Behrend.dValue, HMul.hMul, HSub.hSub, HDiv.hDiv, LT.lt.le, rothNumberNat, Real.exp, Nat.cast, LT.lt.ne', OrderHom.mono, Inv.inv, HPow.hPow, Behrend.bound_aux, OfNat.ofNat, Behrend.nValue, DFunLike.coe
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : LT.lt (α := ℝ) 0 (↑n : ℝ)
hd : 0 < dValue N
hN₀ : LT.lt (α := ℝ) 0 (↑N : ℝ)
hn₂ : 2 < n
this : (2 * dValue N - 1) ^ n ≤ N
rw :
  (↑N : ℝ) * rexp (-4 * √(log (↑N : ℝ))) ≤
    (↑N : ℝ) *
      (HPow.hPow (α := ℝ) (↑N : ℝ) (HDiv.hDiv (α := ℝ) 2 (↑n : ℝ)) *
          (rexp (HSub.hSub (α := ℝ) (↑n : ℝ) 2) * (↑n : ℝ)))⁻¹
⊢ (↑N : ℝ) * rexp (-4 * √(log (↑N : ℝ))) ≤
    (HPow.hPow (α := ℝ) (β := ℝ) (↑N : ℝ) (↑(nValue N) : ℝ)⁻¹ / rexp 1) ^ (n - 2) / (↑n : ℝ)

Tactic:
rw [← rpow_natCast, div_rpow (rpow_nonneg hN₀.le _) (exp_pos _).le, ← rpow_mul hN₀.le,
    inv_mul_eq_div, cast_sub hn₂.le, cast_two, same_sub_div hn.ne', exp_one_rpow,
    div_div, rpow_sub hN₀, rpow_one, div_div, div_eq_mul_inv]

Premises used: same_sub_div, Nat.cast_sub, inv_mul_eq_div, Real.exp_one_rpow, LT.lt.le, Real.div_rpow, div_eq_mul_inv, Real.rpow_one, LT.lt.ne', Real.rpow_nonneg, div_div, Real.rpow_sub, Real.rpow_mul, Nat.cast_two, Real.rpow_natCast, Real.exp_pos
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : LT.lt (α := ℝ) 0 (↑n : ℝ)
hd : 0 < dValue N
hN₀ : LT.lt (α := ℝ) 0 (↑N : ℝ)
hn₂ : 2 < n
this : (2 * dValue N - 1) ^ n ≤ N
hbc :
  rexp (-4 * √(log (↑N : ℝ))) ≤
    (HPow.hPow (α := ℝ) (↑N : ℝ) (HDiv.hDiv (α := ℝ) 2 (↑n : ℝ)) * (rexp (HSub.hSub (α := ℝ) (↑n : ℝ) 2) * (↑n : ℝ)))⁻¹
⊢ (↑N : ℝ) * rexp (-4 * √(log (↑N : ℝ))) ≤
    (↑N : ℝ) *
      (HPow.hPow (α := ℝ) (↑N : ℝ) (HDiv.hDiv (α := ℝ) 2 (↑n : ℝ)) *
          (rexp (HSub.hSub (α := ℝ) (↑n : ℝ) 2) * (↑n : ℝ)))⁻¹

Tactic:
gcongr _ * ?_
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : LT.lt (α := ℝ) 0 (↑n : ℝ)
hd : 0 < dValue N
hN₀ : LT.lt (α := ℝ) 0 (↑N : ℝ)
hn₂ : 2 < n
this : (2 * dValue N - 1) ^ n ≤ N
hbc :
  rexp (-4 * √(log (↑N : ℝ))) ≤
    HPow.hPow (α := ℝ) (↑N : ℝ) (-HDiv.hDiv (α := ℝ) 2 (↑n : ℝ)) * (rexp (HSub.hSub (α := ℝ) 2 (↑n : ℝ)) / (↑n : ℝ))
⊢ rexp (-4 * √(log (↑N : ℝ))) ≤
    (HPow.hPow (α := ℝ) (↑N : ℝ) (HDiv.hDiv (α := ℝ) 2 (↑n : ℝ)) * (rexp (HSub.hSub (α := ℝ) (↑n : ℝ) 2) * (↑n : ℝ)))⁻¹

Tactic:
rw [mul_inv, mul_inv, ← exp_neg, ← rpow_neg (cast_nonneg _), neg_sub, ← div_eq_mul_inv]

Premises used: neg_sub, Nat.cast_nonneg, mul_inv, div_eq_mul_inv, Real.exp_neg, Real.rpow_neg
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : LT.lt (α := ℝ) 0 (↑n : ℝ)
hd : 0 < dValue N
hN₀ : LT.lt (α := ℝ) 0 (↑N : ℝ)
hn₂ : 2 < n
this : (2 * dValue N - 1) ^ n ≤ N
rw : rexp (-4 * √(log (↑N : ℝ))) = rexp (HAdd.hAdd (α := ℝ) (-2) (-2) * √(log (↑N : ℝ)))
⊢ rexp (-4 * √(log (↑N : ℝ))) = rexp (-2 * √(log (↑N : ℝ))) * rexp (-2 * √(log (↑N : ℝ)))

Tactic:
rw [← exp_add, ← add_mul]

Premises used: add_mul, Real.exp_add
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : LT.lt (α := ℝ) 0 (↑n : ℝ)
hd : 0 < dValue N
hN₀ : LT.lt (α := ℝ) 0 (↑N : ℝ)
hn₂ : 2 < n
this : (2 * dValue N - 1) ^ n ≤ N
⊢ rexp (-4 * √(log (↑N : ℝ))) = rexp (HAdd.hAdd (α := ℝ) (-2) (-2) * √(log (↑N : ℝ)))

Tactic:
norm_num
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : LT.lt (α := ℝ) 0 (↑n : ℝ)
hd : 0 < dValue N
hN₀ : LT.lt (α := ℝ) 0 (↑N : ℝ)
hn₂ : 2 < n
this : (2 * dValue N - 1) ^ n ≤ N
⊢ rexp (-4 * √(log (↑N : ℝ))) = rexp (-2 * √(log (↑N : ℝ))) * rexp (-2 * √(log (↑N : ℝ)))

Tactic:
have : exp (-4 * √(log N)) = exp (-2 * √(log N)) * exp (-2 * √(log N)) := by
    rw [← exp_add, ← add_mul]
    norm_num
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : LT.lt (α := ℝ) 0 (↑n : ℝ)
hd : 0 < dValue N
hN₀ : LT.lt (α := ℝ) 0 (↑N : ℝ)
hn₂ : 2 < n
this_1 : (2 * dValue N - 1) ^ n ≤ N
this : rexp (-4 * √(log (↑N : ℝ))) = rexp (-2 * √(log (↑N : ℝ))) * rexp (-2 * √(log (↑N : ℝ)))
hbc :
  rexp (-2 * √(log (↑N : ℝ))) * rexp (-2 * √(log (↑N : ℝ))) ≤
    HPow.hPow (α := ℝ) (↑N : ℝ) (-HDiv.hDiv (α := ℝ) 2 (↑n : ℝ)) * (rexp (HSub.hSub (α := ℝ) 2 (↑n : ℝ)) / (↑n : ℝ))
⊢ rexp (-4 * √(log (↑N : ℝ))) ≤
    HPow.hPow (α := ℝ) (↑N : ℝ) (-HDiv.hDiv (α := ℝ) 2 (↑n : ℝ)) * (rexp (HSub.hSub (α := ℝ) 2 (↑n : ℝ)) / (↑n : ℝ))

Tactic:
rw [this]
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : LT.lt (α := ℝ) 0 (↑n : ℝ)
hd : 0 < dValue N
hN₀ : LT.lt (α := ℝ) 0 (↑N : ℝ)
hn₂ : 2 < n
this_1 : (2 * dValue N - 1) ^ n ≤ N
this : rexp (-4 * √(log (↑N : ℝ))) = rexp (-2 * √(log (↑N : ℝ))) * rexp (-2 * √(log (↑N : ℝ)))
hbc : rexp (-2 * √(log (↑N : ℝ))) ≤ HPow.hPow (α := ℝ) (↑N : ℝ) (-HDiv.hDiv (α := ℝ) 2 (↑n : ℝ))
hbc₁ : rexp (-2 * √(log (↑N : ℝ))) ≤ rexp (HSub.hSub (α := ℝ) 2 (↑n : ℝ)) / (↑n : ℝ)
⊢ rexp (-2 * √(log (↑N : ℝ))) * rexp (-2 * √(log (↑N : ℝ))) ≤
    HPow.hPow (α := ℝ) (↑N : ℝ) (-HDiv.hDiv (α := ℝ) 2 (↑n : ℝ)) * (rexp (HSub.hSub (α := ℝ) 2 (↑n : ℝ)) / (↑n : ℝ))

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : LT.lt (α := ℝ) 0 (↑n : ℝ)
hd : 0 < dValue N
hN₀ : LT.lt (α := ℝ) 0 (↑N : ℝ)
hn₂ : 2 < n
this_1 : (2 * dValue N - 1) ^ n ≤ N
this : rexp (-4 * √(log (↑N : ℝ))) = rexp (-2 * √(log (↑N : ℝ))) * rexp (-2 * √(log (↑N : ℝ)))
hbc : 2 * √(log (↑N : ℝ)) ≤ HMul.hMul (α := ℝ) 2 (↑n : ℝ)
hbc₁ : 0 < √(log (↑N : ℝ))
⊢ rexp (-2 * √(log (↑N : ℝ))) ≤ HPow.hPow (α := ℝ) (↑N : ℝ) (-HDiv.hDiv (α := ℝ) 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]

Premises used: div_le_iff₀, Real.rpow_pos_of_pos, Real.log_rpow, mul_div_assoc, Real.le_log_iff_exp_le, div_mul_eq_mul_div, Real.div_sqrt, neg_mul, le_div_iff₀, neg_le_neg_iff
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : LT.lt (α := ℝ) 0 (↑n : ℝ)
hd : 0 < dValue N
hN₀ : LT.lt (α := ℝ) 0 (↑N : ℝ)
hn₂ : 2 < n
this_1 : (2 * dValue N - 1) ^ n ≤ N
this : rexp (-4 * √(log (↑N : ℝ))) = rexp (-2 * √(log (↑N : ℝ))) * rexp (-2 * √(log (↑N : ℝ)))
hbc : √(log (↑N : ℝ)) ≤ (↑n : ℝ)
⊢ 2 * √(log (↑N : ℝ)) ≤ HMul.hMul (α := ℝ) 2 (↑n : ℝ)

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : LT.lt (α := ℝ) 0 (↑n : ℝ)
hd : 0 < dValue N
hN₀ : LT.lt (α := ℝ) 0 (↑N : ℝ)
hn₂ : 2 < n
this_1 : (2 * dValue N - 1) ^ n ≤ N
this : rexp (-4 * √(log (↑N : ℝ))) = rexp (-2 * √(log (↑N : ℝ))) * rexp (-2 * √(log (↑N : ℝ)))
⊢ √(log (↑N : ℝ)) ≤ (↑n : ℝ)

Tactic:
apply le_ceil

Premises used: Nat.le_ceil