awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
⊢ LT.lt (α := ℝ) 0 2.7182818283

Tactic:
norm_num
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
⊢ 0 < rexp 1

Tactic:
exact exp_one_gt_d9.trans' (by norm_num)

Premises used: Real.exp_one_gt_d9, LT.lt.trans'
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 4096 ≤ N
hbc : 0 < 2 / (1 - 2 / rexp 1)
hbc₁ : 2 / (1 - 2 / rexp 1) ≤ HPow.hPow (α := ℝ) (β := ℕ) 2 3
⊢ log (2 / (1 - 2 / rexp 1)) * (69 / 50) ≤ log (HPow.hPow (α := ℝ) (β := ℕ) 2 3) * (69 / 50)

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 4096 ≤ N
hbc : 0 < 2 * rexp 1 / (rexp 1 - 2)
⊢ 0 < 2 / (1 - 2 / rexp 1)

Tactic:
field_simp
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 4096 ≤ N
⊢ 0 < 2 * rexp 1 / (rexp 1 - 2)

Tactic:
simp (disch := positivity) [exp_one_gt_two]

Premises used: Real.exp_one_gt_two
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 4096 ≤ N
hbc : 2 / (1 - 2 / rexp 1) ≤ 8
⊢ 2 / (1 - 2 / rexp 1) ≤ HPow.hPow (α := ℝ) (β := ℕ) 2 3

Tactic:
norm_num1
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 4096 ≤ N
⊢ 2 / (1 - 2 / rexp 1) ≤ 8

Tactic:
two_div_one_sub_two_div_e_le_eight

Premises used: Behrend.two_div_one_sub_two_div_e_le_eight
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 4096 ≤ N
⊢ 2 / (1 - 2 / rexp 1) ≤ 8

Tactic:
exact two_div_one_sub_two_div_e_le_eight

Premises used: Behrend.two_div_one_sub_two_div_e_le_eight
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 4096 ≤ N
simp : 3 * log 2 * (69 / 50) ≤ √(12 * log 2)
⊢ log (HPow.hPow (α := ℝ) (β := ℕ) 2 3) * (69 / 50) ≤ √(log (HPow.hPow (α := ℝ) (β := ℕ) 2 12))

Tactic:
simp only [Real.log_pow, Nat.cast_ofNat]

Premises used: Nat.cast_ofNat, Real.log_pow
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 4096 ≤ N
h : HPow.hPow (β := ℕ) (3 * log 2 * (69 / 50)) 2 ≤ 12 * log 2
⊢ 3 * log 2 * (69 / 50) ≤ √(12 * log 2)

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
nlinarith : 12 * log 2 < HPow.hPow (β := ℕ) (3 * log 2 * (69 / 50)) 2 → 10000000000 / 10000000000 = 1
nlinarith₁ : 12 * log 2 < HPow.hPow (β := ℕ) (3 * log 2 * (69 / 50)) 2 → HMul.hMul (α := ℝ) 1 10000000000 = 10000000000
nlinarith₂ : 12 * log 2 < HPow.hPow (β := ℕ) (3 * log 2 * (69 / 50)) 2 → GT.gt (α := ℝ) 10000000000 0
nlinarith₃ : 12 * log 2 < HPow.hPow (β := ℕ) (3 * log 2 * (69 / 50)) 2 → 156250000 / 156250000 = 1
nlinarith₄ : 12 * log 2 < HPow.hPow (β := ℕ) (3 * log 2 * (69 / 50)) 2 → HMul.hMul (α := ℝ) 1 156250000 = 156250000
nlinarith₅ : 12 * log 2 < HPow.hPow (β := ℕ) (3 * log 2 * (69 / 50)) 2 → GT.gt (α := ℝ) 156250000 0
nlinarith₆ : 12 * log 2 < HPow.hPow (β := ℕ) (3 * log 2 * (69 / 50)) 2 → HMul.hMul (α := ℝ) 1 2500 = 2500
nlinarith₇ : 12 * log 2 < HPow.hPow (β := ℕ) (3 * log 2 * (69 / 50)) 2 → HMul.hMul (α := ℝ) 1 1 = 1
nlinarith₈ : 12 * log 2 < HPow.hPow (β := ℕ) (3 * log 2 * (69 / 50)) 2 → 50 / 50 = 1
nlinarith₉ nlinarith₁₀ : 12 * log 2 < HPow.hPow (β := ℕ) (3 * log 2 * (69 / 50)) 2 → HMul.hMul (α := ℝ) 1 50 = 50
nlinarith₁₁ : 12 * log 2 < HPow.hPow (β := ℕ) (3 * log 2 * (69 / 50)) 2 → 1 * HPow.hPow (α := ℝ) (β := ℕ) 50 2 = 2500
nlinarith₁₂ : 12 * log 2 < HPow.hPow (β := ℕ) (3 * log 2 * (69 / 50)) 2 → GT.gt (α := ℝ) 2500 0
nlinarith₁₃ :
  12 * log 2 < HPow.hPow (β := ℕ) (3 * log 2 * (69 / 50)) 2 →
    7812499994420703125 *
                (HMul.hMul (α := ℝ) 1 12 * (2500 * log 2) -
                  1 * HPow.hPow (β := ℕ) (HMul.hMul (α := ℝ) 1 3 * (1 * log 2) * HMul.hMul (α := ℝ) 1 69) 2) +
              20748421620975173471424 * (156250000 * log 2 - HMul.hMul (α := ℝ) 1 108304247) +
            324194088061593686976 * (HMul.hMul (α := ℝ) 1 6931471803 - 10000000000 * log 2) +
          71415000000 *
            (0 -
              (0 - HPow.hPow (β := ℕ) (HMul.hMul (α := ℝ) 1 3 * (1 * log 2) * HMul.hMul (α := ℝ) 1 69) 2) *
                (156250000 * log 2 - HMul.hMul (α := ℝ) 1 108304247)) +
        1115859375 *
          (0 -
            (HMul.hMul (α := ℝ) 1 12 * (2500 * log 2) -
                1 * HPow.hPow (β := ℕ) (HMul.hMul (α := ℝ) 1 3 * (1 * log 2) * HMul.hMul (α := ℝ) 1 69) 2) *
              (HMul.hMul (α := ℝ) 1 6931471803 - 10000000000 * log 2)) =
      0
nlinarith₁₄ : 12 * log 2 < HPow.hPow (β := ℕ) (3 * log 2 * (69 / 50)) 2 → GT.gt (α := ℝ) 7812499994420703125 0
nlinarith₁₅ : 12 * log 2 < HPow.hPow (β := ℕ) (3 * log 2 * (69 / 50)) 2 → GT.gt (α := ℝ) 20748421620975173471424 0
nlinarith₁₆ : 12 * log 2 < HPow.hPow (β := ℕ) (3 * log 2 * (69 / 50)) 2 → GT.gt (α := ℝ) 324194088061593686976 0
nlinarith₁₇ : 12 * log 2 < HPow.hPow (β := ℕ) (3 * log 2 * (69 / 50)) 2 → GT.gt (α := ℝ) 71415000000 0
nlinarith₁₈ : 12 * log 2 < HPow.hPow (β := ℕ) (3 * log 2 * (69 / 50)) 2 → GT.gt (α := ℝ) 1115859375 0
⊢ HPow.hPow (β := ℕ) (3 * log 2 * (69 / 50)) 2 ≤ 12 * log 2

Tactic:
nlinarith [log_two_lt_d9, log_two_gt_d9]

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

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

Tactic:
mod_cast hN

Premises used: congrArg, cast, Nat.cast_le._simp_1, LE.le, Nat.cast, congrFun', OfNat.ofNat, Eq.symm, Eq.trans, Nat.cast_pow._simp_1
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 4096 ≤ N
⊢ HPow.hPow (α := ℝ) (β := ℕ) 2 12 ≤ (↑N : ℝ)

Tactic:
exact mod_cast hN
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 4096 ≤ N
_ : log (2 / (1 - 2 / rexp 1)) * (69 / 50) ≤ log (HPow.hPow (α := ℝ) (β := ℕ) 2 3) * (69 / 50)
_₁ : log (HPow.hPow (α := ℝ) (β := ℕ) 2 3) * (69 / 50) ≤ √(log (HPow.hPow (α := ℝ) (β := ℕ) 2 12))
_₂ : √(log (HPow.hPow (α := ℝ) (β := ℕ) 2 12)) ≤ √(log (↑N : ℝ))
⊢ log (2 / (1 - 2 / rexp 1)) * (69 / 50) ≤ √(log (↑N : ℝ))

Tactic:
calc
    _ ≤ log (2 ^ 3) * (69 / 50) := by
      gcongr
      · field_simp
        simp (disch := positivity) [exp_one_gt_two]
      · norm_num1
        exact two_div_one_sub_two_div_e_le_eight
    _ ≤ √(log (2 ^ 12)) := by
      simp only [Real.log_pow, Nat.cast_ofNat]
      apply le_sqrt_of_sq_le
      nlinarith [log_two_lt_d9, log_two_gt_d9]
    _ ≤ √(log ↑N) := by
      gcongr
      exact mod_cast hN

Premises used: HDiv.hDiv, Nat.cast, Real.log, HPow.hPow, OfNat.ofNat
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
x : ℝ
hx : 0 < x
⊢ (↑⌈x⌉₊ : ℝ) < x + 1

Tactic:
have h₁ := ceil_lt_add_one hx.le
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
x : ℝ
hx : 0 < x
h₁ : (↑⌈x⌉₊ : ℝ) < x + 1
linarith :
  HSub.hSub (α := ℝ) 2 (↑⌈x⌉₊ : ℝ) < 1 - x → (↑⌈x⌉₊ : ℝ) - (x + 1) + (HSub.hSub (α := ℝ) 2 (↑⌈x⌉₊ : ℝ) - (1 - x)) = 0
⊢ 1 - x ≤ HSub.hSub (α := ℝ) 2 (↑⌈x⌉₊ : ℝ)

Tactic:
linarith
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
x : ℝ
hx : 0 < x
h₁ : (↑⌈x⌉₊ : ℝ) < x + 1
⊢ 1 - x ≤ HSub.hSub (α := ℝ) 2 (↑⌈x⌉₊ : ℝ)

Tactic:
have h₂ : 1 - x ≤ 2 - ⌈x⌉₊ := by linarith
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
x : ℝ
hx : 0 < x
h₁ : (↑⌈x⌉₊ : ℝ) < x + 1
h₂ : 1 - x ≤ HSub.hSub (α := ℝ) 2 (↑⌈x⌉₊ : ℝ)
⊢ rexp (-2 * x) ≤ rexp (1 - x) / (x + 1)

Tactic:
?_
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
x : ℝ
hx : 0 < x
h₁ : (↑⌈x⌉₊ : ℝ) < x + 1
h₂ : 1 - x ≤ HSub.hSub (α := ℝ) 2 (↑⌈x⌉₊ : ℝ)
hc : 0 ≤ x + 1
⊢ rexp (1 - x) / (x + 1) ≤ rexp (HSub.hSub (α := ℝ) 2 (↑⌈x⌉₊ : ℝ)) / (x + 1)

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
x : ℝ
hx : 0 < x
h₁ : (↑⌈x⌉₊ : ℝ) < x + 1
h₂ : 1 - x ≤ HSub.hSub (α := ℝ) 2 (↑⌈x⌉₊ : ℝ)
ha : 0 < rexp (HSub.hSub (α := ℝ) 2 (↑⌈x⌉₊ : ℝ))
hc : LT.lt (α := ℝ) 0 (↑⌈x⌉₊ : ℝ)
⊢ rexp (HSub.hSub (α := ℝ) 2 (↑⌈x⌉₊ : ℝ)) / (x + 1) < rexp (HSub.hSub (α := ℝ) 2 (↑⌈x⌉₊ : ℝ)) / (↑⌈x⌉₊ : ℝ)

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
x : ℝ
hx : 0 < x
h₁ : (↑⌈x⌉₊ : ℝ) < x + 1
h₂ : 1 - x ≤ HSub.hSub (α := ℝ) 2 (↑⌈x⌉₊ : ℝ)
_ : rexp (-2 * x) ≤ rexp (1 - x) / (x + 1)
⊢ rexp (-2 * x) < rexp (HSub.hSub (α := ℝ) 2 (↑⌈x⌉₊ : ℝ)) / (↑⌈x⌉₊ : ℝ)

Tactic:
calc
    _ ≤ exp (1 - x) / (x + 1) := ?_
    _ ≤ exp (2 - ⌈x⌉₊) / (x + 1) := by gcongr
    _ < _ := by gcongr

Premises used: HSub.hSub, Real.exp, Nat.cast, HAdd.hAdd, Nat.ceil, OfNat.ofNat
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
x : ℝ
hx : 0 < x
h₁ : (↑⌈x⌉₊ : ℝ) < x + 1
h₂ : 1 - x ≤ HSub.hSub (α := ℝ) 2 (↑⌈x⌉₊ : ℝ)
rw : x + 1 ≤ rexp (x + 1)
⊢ rexp (-2 * x) ≤ rexp (1 - x) / (x + 1)

Tactic:
rw [le_div_iff₀ (add_pos hx zero_lt_one), ← le_div_iff₀' (exp_pos _), ← exp_sub, neg_mul,
    sub_neg_eq_add, two_mul, sub_add_add_cancel, add_comm _ x]

Premises used: le_div_iff₀', add_pos, two_mul, add_comm, zero_lt_one, sub_add_add_cancel, neg_mul, Real.exp_sub, le_div_iff₀, sub_neg_eq_add, Real.exp_pos
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
x : ℝ
hx : 0 < x
h₁ : (↑⌈x⌉₊ : ℝ) < x + 1
h₂ : 1 - x ≤ HSub.hSub (α := ℝ) 2 (↑⌈x⌉₊ : ℝ)
⊢ x + 1 ≤ rexp (x + 1)

Tactic:
le_trans (le_add_of_nonneg_right zero_le_one) (add_one_le_exp _)

Premises used: zero_le_one, le_add_of_nonneg_right, Real.add_one_le_exp, le_trans
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
x : ℝ
hx : 0 < x
h₁ : (↑⌈x⌉₊ : ℝ) < x + 1
h₂ : 1 - x ≤ HSub.hSub (α := ℝ) 2 (↑⌈x⌉₊ : ℝ)
⊢ x + 1 ≤ rexp (x + 1)

Tactic:
exact le_trans (le_add_of_nonneg_right zero_le_one) (add_one_le_exp _)

Premises used: zero_le_one, le_add_of_nonneg_right, Real.add_one_le_exp, le_trans
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
x : ℝ
hx : 2 / (1 - 2 / rexp 1) ≤ x
apply : x / rexp 1 ≤ x / 2 - 1
⊢ x / rexp 1 < (↑⌊x / 2⌋₊ : ℝ)

Tactic:
apply lt_of_le_of_lt _ (sub_one_lt_floor _)

Premises used: lt_of_le_of_lt, Nat.sub_one_lt_floor
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
x : ℝ
hx : 2 / (1 - 2 / rexp 1) ≤ x
rw : 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:
x : ℝ
hx : 2 / (1 - 2 / rexp 1) ≤ x
⊢ 2 < rexp 1

Tactic:
exp_one_gt_two

Premises used: Real.exp_one_gt_two
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
x : ℝ
hx : 2 / (1 - 2 / rexp 1) ≤ x
⊢ 2 < rexp 1

Tactic:
exact exp_one_gt_two

Premises used: Real.exp_one_gt_two
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
x : ℝ
hx : 2 / (1 - 2 / rexp 1) ≤ x
⊢ 0 < 1 - 2 / rexp 1

Tactic:
have : 0 < 1 - 2 / exp 1 := by
    rw [sub_pos, div_lt_one (exp_pos _)]
    exact exp_one_gt_two
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
x : ℝ
hx : 2 / (1 - 2 / rexp 1) ≤ x
this : 0 < 1 - 2 / rexp 1
rwa : LT.lt (α := ℝ) 0 2
rwa₁ : Ne (α := ℝ) 2 0
⊢ x / rexp 1 ≤ x / 2 - 1

Tactic:
rwa [le_sub_comm, div_eq_mul_one_div x, div_eq_mul_one_div x, ← mul_sub, div_sub', ←
    div_eq_mul_one_div, mul_div_assoc', one_le_div, ← div_le_iff₀ this]

Premises used: div_le_iff₀, mul_sub, mul_div_assoc', div_eq_mul_one_div, div_sub', one_le_div, le_sub_comm
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
x : ℝ
hx : 2 / (1 - 2 / rexp 1) ≤ x
this : 0 < 1 - 2 / rexp 1
⊢ LT.lt (α := ℝ) 0 2

Tactic:
zero_lt_two

Premises used: zero_lt_two
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
x : ℝ
hx : 2 / (1 - 2 / rexp 1) ≤ x
this : 0 < 1 - 2 / rexp 1
⊢ LT.lt (α := ℝ) 0 2

Tactic:
exact zero_lt_two

Premises used: zero_lt_two
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
x : ℝ
hx : 2 / (1 - 2 / rexp 1) ≤ x
this : 0 < 1 - 2 / rexp 1
⊢ Ne (α := ℝ) 2 0

Tactic:
two_ne_zero

Premises used: two_ne_zero
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
x : ℝ
hx : 2 / (1 - 2 / rexp 1) ≤ x
this : 0 < 1 - 2 / rexp 1
⊢ Ne (α := ℝ) 2 0

Tactic:
exact two_ne_zero

Premises used: two_ne_zero
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
x : ℝ
hx : 50 / 19 ≤ x
⊢ 0 ≤ 50 / 19

Tactic:
norm_num
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
x : ℝ
hx : 50 / 19 ≤ x
refine : x + 1 ≤ 1.38 * x
⊢ (↑⌈x⌉₊ : ℝ) < 1.38 * x

Tactic:
refine (ceil_lt_add_one <| hx.trans' <| by norm_num).trans_le ?_

Premises used: Nat.ceil_lt_add_one, LT.lt.trans_le, LE.le.trans'
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
x : ℝ
hx : 50 / 19 ≤ x
rw : 1 ≤ HSub.hSub (α := ℝ) 1.38 1 * x
⊢ x + 1 ≤ 1.38 * x

Tactic:
rw [← le_sub_iff_add_le', ← sub_one_mul]

Premises used: le_sub_iff_add_le', sub_one_mul
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
x : ℝ
hx : 50 / 19 ≤ x
⊢ 1.38 = 69 / 50

Tactic:
norm_num
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
x : ℝ
hx : 50 / 19 ≤ x
⊢ 1.38 = 69 / 50

Tactic:
have : (1.38 : ℝ) = 69 / 50 := by norm_num
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
x : ℝ
hx : 50 / 19 ≤ x
this : 1.38 = 69 / 50
⊢ 69 / 50 - 1 = (50 / 19)⁻¹

Tactic:
norm_num1
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
x : ℝ
hx : 50 / 19 ≤ x
this : 1.38 = 69 / 50
rwa : 0 < 50 / 19
⊢ 1 ≤ HSub.hSub (α := ℝ) 1.38 1 * x

Tactic:
rwa [this, show (69 / 50 - 1 : ℝ) = (50 / 19)⁻¹ by norm_num1, ←
    div_eq_inv_mul, one_le_div]

Premises used: div_eq_inv_mul, one_le_div
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
x : ℝ
hx : 50 / 19 ≤ x
this : 1.38 = 69 / 50
⊢ 0 < 50 / 19

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

Tactic:
ceil_pos.2 <| Real.sqrt_pos.2 <| log_pos <| one_lt_cast.2 <| hN

Premises used: Iff.mpr, Nat.ceil_pos, Real.log_pos, Real.sqrt_pos, Nat.one_lt_cast, Behrend.nValue
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 64 ≤ N
rw : 2 < √(log (↑N : ℝ))
⊢ 3 ≤ nValue N

Tactic:
rw [nValue, ← lt_iff_add_one_le, lt_ceil, cast_two]

Premises used: Nat.lt_iff_add_one_le, Nat.lt_ceil, Behrend.nValue, Nat.cast_two
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 64 ≤ N
h : HPow.hPow (α := ℝ) (β := ℕ) 2 2 < log (↑N : ℝ)
⊢ 2 < √(log (↑N : ℝ))

Tactic:
apply lt_sqrt_of_sq_lt

Premises used: Real.lt_sqrt_of_sq_lt
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 64 ≤ N
rw : HPow.hPow (α := ℝ) (β := ℕ) 2 6 ≤ (↑N : ℝ)
⊢ HPow.hPow (α := ℝ) (β := ℝ) 2 (↑6 : ℝ) ≤ (↑N : ℝ)

Tactic:
rw [rpow_natCast]

Premises used: Real.rpow_natCast
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 64 ≤ N
⊢ HPow.hPow (α := ℝ) (β := ℕ) 2 6 ≤ (↑64 : ℝ)

Tactic:
norm_num1
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 64 ≤ N
⊢ HPow.hPow (α := ℝ) (β := ℕ) 2 6 ≤ (↑N : ℝ)

Tactic:
exact (cast_le.2 hN).trans' (by norm_num1)

Premises used: Iff.mpr, Nat.cast_le, LE.le.trans'
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 64 ≤ N
⊢ HPow.hPow (α := ℝ) (β := ℝ) 2 (↑6 : ℝ) ≤ (↑N : ℝ)

Tactic:
have : (2 : ℝ) ^ ((6 : ℕ) : ℝ) ≤ N := by
    rw [rpow_natCast]
    exact (cast_le.2 hN).trans' (by norm_num1)
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 64 ≤ N
this : HPow.hPow (α := ℝ) (β := ℝ) 2 (↑6 : ℝ) ≤ (↑N : ℝ)
apply : HPow.hPow (α := ℝ) (β := ℕ) 2 2 < log (HPow.hPow (α := ℝ) (β := ℝ) 2 (↑6 : ℝ))
⊢ HPow.hPow (α := ℝ) (β := ℕ) 2 2 < log (↑N : ℝ)

Tactic:
apply lt_of_lt_of_le _ (log_le_log (rpow_pos_of_pos zero_lt_two _) this)

Premises used: Real.rpow_pos_of_pos, Real.log_le_log, zero_lt_two, lt_of_lt_of_le
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 64 ≤ N
this : HPow.hPow (α := ℝ) (β := ℝ) 2 (↑6 : ℝ) ≤ (↑N : ℝ)
rw : HPow.hPow (α := ℝ) (β := ℕ) 2 2 / (↑6 : ℝ) < log 2
rw₁ : LT.lt (α := ℝ) 0 (↑6 : ℝ)
⊢ HPow.hPow (α := ℝ) (β := ℕ) 2 2 < log (HPow.hPow (α := ℝ) (β := ℝ) 2 (↑6 : ℝ))

Tactic:
rw [log_rpow zero_lt_two, ← div_lt_iff₀']

Premises used: Real.log_rpow, div_lt_iff₀', zero_lt_two
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 64 ≤ N
this : HPow.hPow (α := ℝ) (β := ℝ) 2 (↑6 : ℝ) ≤ (↑N : ℝ)
⊢ HPow.hPow (α := ℝ) (β := ℕ) 2 2 / (↑6 : ℝ) ≤ 0.6931471803

Tactic:
norm_num1
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 64 ≤ N
this : HPow.hPow (α := ℝ) (β := ℝ) 2 (↑6 : ℝ) ≤ (↑N : ℝ)
⊢ HPow.hPow (α := ℝ) (β := ℕ) 2 2 / (↑6 : ℝ) < log 2

Tactic:
exact log_two_gt_d9.trans_le' (by norm_num1)

Premises used: Real.log_two_gt_d9, LT.lt.trans_le'
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 64 ≤ N
this : HPow.hPow (α := ℝ) (β := ℝ) 2 (↑6 : ℝ) ≤ (↑N : ℝ)
⊢ LT.lt (α := ℝ) 0 (↑6 : ℝ)

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

Tactic:
have hN₀ : 0 < (N : ℝ) := cast_pos.2 (succ_pos'.trans_le hN₃)
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN₃ : 8 ≤ N
hN₀ : LT.lt (α := ℝ) 0 (↑N : ℝ)
rw : log 2 * (↑(nValue N) : ℝ) ≤ log (↑N : ℝ)
rw₁ : LT.lt (α := ℝ) 0 (↑(nValue N) : ℝ)
rw₂ : HPow.hPow (α := ℝ) (β := ℝ) (↑N : ℝ) (↑(nValue N) : ℝ)⁻¹ ≠ 0
rw₃ : 0 < HPow.hPow (α := ℝ) (β := ℝ) (↑N : ℝ) (↑(nValue N) : ℝ)⁻¹ / 2
⊢ 0 < dValue N

Tactic:
rw [dValue, floor_pos, ← log_le_log_iff zero_lt_one, log_one, log_div _ two_ne_zero, log_rpow hN₀,
    inv_mul_eq_div, sub_nonneg, le_div_iff₀]

Premises used: Behrend.dValue, Real.log_rpow, inv_mul_eq_div, Real.log_one, Real.log_div, two_ne_zero, zero_lt_one, Real.log_le_log_iff, le_div_iff₀, sub_nonneg, Nat.floor_pos
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN₃ : 8 ≤ N
hN₀ : LT.lt (α := ℝ) 0 (↑N : ℝ)
apply : √(log (↑N : ℝ)) + 1 ≤ 2 * √(log (↑N : ℝ))
⊢ (↑(nValue N) : ℝ) ≤ 2 * √(log (↑N : ℝ))

Tactic:
apply (ceil_lt_add_one <| sqrt_nonneg _).le.trans

Premises used: Nat.ceil_lt_add_one, LT.lt.le, LE.le.trans, Real.sqrt_nonneg
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN₃ : 8 ≤ N
hN₀ : LT.lt (α := ℝ) 0 (↑N : ℝ)
rw : 1 ≤ √(log (↑N : ℝ))
⊢ √(log (↑N : ℝ)) + 1 ≤ 2 * √(log (↑N : ℝ))

Tactic:
rw [two_mul, add_le_add_iff_left]

Premises used: add_le_add_iff_left, two_mul
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN₃ : 8 ≤ N
hN₀ : LT.lt (α := ℝ) 0 (↑N : ℝ)
h : HPow.hPow (α := ℝ) (β := ℕ) 1 2 ≤ log (↑N : ℝ)
⊢ 1 ≤ √(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₃ : 8 ≤ N
hN₀ : LT.lt (α := ℝ) 0 (↑N : ℝ)
h : rexp 1 ≤ (↑N : ℝ)
⊢ HPow.hPow (α := ℝ) (β := ℕ) 1 2 ≤ log (↑N : ℝ)

Tactic:
rw [one_pow, le_log_iff_exp_le hN₀]

Premises used: one_pow, Real.le_log_iff_exp_le
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN₃ : 8 ≤ N
hN₀ : LT.lt (α := ℝ) 0 (↑N : ℝ)
⊢ LE.le (α := ℝ) 2.7182818286 (↑8 : ℝ)

Tactic:
norm_num
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN₃ : 8 ≤ N
hN₀ : LT.lt (α := ℝ) 0 (↑N : ℝ)
⊢ rexp 1 ≤ (↑N : ℝ)

Tactic:
exact (exp_one_lt_d9.le.trans <| by norm_num).trans (cast_le.2 hN₃)

Premises used: Iff.mpr, LT.lt.le, Real.exp_one_lt_d9, Nat.cast_le, LE.le.trans
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN₃ : 8 ≤ N
hN₀ : LT.lt (α := ℝ) 0 (↑N : ℝ)
⊢ (↑(nValue N) : ℝ) ≤ 2 * √(log (↑N : ℝ))

Tactic:
have : (nValue N : ℝ) ≤ 2 * √(log N) := by
      apply (ceil_lt_add_one <| sqrt_nonneg _).le.trans
      rw [two_mul, add_le_add_iff_left]
      apply le_sqrt_of_sq_le
      rw [one_pow, le_log_iff_exp_le hN₀]
      exact (exp_one_lt_d9.le.trans <| by norm_num).trans (cast_le.2 hN₃)
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN₃ : 8 ≤ N
hN₀ : LT.lt (α := ℝ) 0 (↑N : ℝ)
this : (↑(nValue N) : ℝ) ≤ 2 * √(log (↑N : ℝ))
apply : log 2 * (2 * √(log (↑N : ℝ))) ≤ log (↑N : ℝ)
⊢ log 2 * (↑(nValue N) : ℝ) ≤ log (↑N : ℝ)

Tactic:
apply (mul_le_mul_of_nonneg_left this <| log_nonneg one_le_two).trans _

Premises used: Real.log_nonneg, one_le_two, LE.le.trans, mul_le_mul_of_nonneg_left
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN₃ : 8 ≤ N
hN₀ : LT.lt (α := ℝ) 0 (↑N : ℝ)
this : (↑(nValue N) : ℝ) ≤ 2 * √(log (↑N : ℝ))
rw : log 2 * 2 ≤ √(log (↑N : ℝ))
rw₁ : 1 < N
⊢ log 2 * (2 * √(log (↑N : ℝ))) ≤ log (↑N : ℝ)

Tactic:
rw [← mul_assoc, ← le_div_iff₀ (Real.sqrt_pos.2 <| log_pos <| one_lt_cast.2 _), div_sqrt]

Premises used: Iff.mpr, mul_assoc, Real.log_pos, Real.div_sqrt, Real.sqrt_pos, Nat.one_lt_cast, le_div_iff₀
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN₃ : 8 ≤ N
hN₀ : LT.lt (α := ℝ) 0 (↑N : ℝ)
this : (↑(nValue N) : ℝ) ≤ 2 * √(log (↑N : ℝ))
apply : √(log 8) ≤ √(log (↑N : ℝ))
⊢ log 2 * 2 ≤ √(log (↑N : ℝ))

Tactic:
apply log_two_mul_two_le_sqrt_log_eight.trans

Premises used: Behrend.log_two_mul_two_le_sqrt_log_eight, LE.le.trans
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN₃ : 8 ≤ N
hN₀ : LT.lt (α := ℝ) 0 (↑N : ℝ)
this : (↑(nValue N) : ℝ) ≤ 2 * √(log (↑N : ℝ))
h : log 8 ≤ log (↑N : ℝ)
⊢ √(log 8) ≤ √(log (↑N : ℝ))

Tactic:
apply Real.sqrt_le_sqrt

Premises used: Real.sqrt_le_sqrt
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN₃ : 8 ≤ N
hN₀ : LT.lt (α := ℝ) 0 (↑N : ℝ)
this : (↑(nValue N) : ℝ) ≤ 2 * √(log (↑N : ℝ))
⊢ LT.lt (α := ℝ) 0 8

Tactic:
simp
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN₃ : 8 ≤ N
hN₀ : LT.lt (α := ℝ) 0 (↑N : ℝ)
this : (↑(nValue N) : ℝ) ≤ 2 * √(log (↑N : ℝ))
⊢ log 8 ≤ log (↑N : ℝ)

Tactic:
exact log_le_log (by simp) (mod_cast hN₃)

Premises used: Real.log_le_log
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN₃ : 8 ≤ N
hN₀ : LT.lt (α := ℝ) 0 (↑N : ℝ)
this : (↑(nValue N) : ℝ) ≤ 2 * √(log (↑N : ℝ))
⊢ LT.lt (α := ℕ) 1 8

Tactic:
simp
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN₃ : 8 ≤ N
hN₀ : LT.lt (α := ℝ) 0 (↑N : ℝ)
this : (↑(nValue N) : ℝ) ≤ 2 * √(log (↑N : ℝ))
⊢ 1 < N

Tactic:
exact hN₃.trans_lt' (by simp)

Premises used: LE.le.trans_lt'
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN₃ : 8 ≤ N
hN₀ : LT.lt (α := ℝ) 0 (↑N : ℝ)
⊢ LE.le (α := ℕ) 2 8

Tactic:
simp
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN₃ : 8 ≤ N
hN₀ : LT.lt (α := ℝ) 0 (↑N : ℝ)
⊢ LT.lt (α := ℝ) 0 (↑(nValue N) : ℝ)

Tactic:
exact cast_pos.2 (nValue_pos <| hN₃.trans' <| by simp)

Premises used: Iff.mpr, Nat.cast_pos, Behrend.nValue_pos, LE.le.trans'
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN₃ : 8 ≤ N
hN₀ : LT.lt (α := ℝ) 0 (↑N : ℝ)
⊢ HPow.hPow (α := ℝ) (β := ℝ) (↑N : ℝ) (↑(nValue N) : ℝ)⁻¹ ≠ 0

Tactic:
(rpow_pos_of_pos hN₀ _).ne'

Premises used: Real.rpow_pos_of_pos, LT.lt.ne'
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN₃ : 8 ≤ N
hN₀ : LT.lt (α := ℝ) 0 (↑N : ℝ)
⊢ HPow.hPow (α := ℝ) (β := ℝ) (↑N : ℝ) (↑(nValue N) : ℝ)⁻¹ ≠ 0

Tactic:
exact (rpow_pos_of_pos hN₀ _).ne'

Premises used: Real.rpow_pos_of_pos, LT.lt.ne'
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN₃ : 8 ≤ N
hN₀ : LT.lt (α := ℝ) 0 (↑N : ℝ)
⊢ 0 < HPow.hPow (α := ℝ) (β := ℝ) (↑N : ℝ) (↑(nValue N) : ℝ)⁻¹ / 2

Tactic:
div_pos (rpow_pos_of_pos hN₀ _) zero_lt_two

Premises used: Real.rpow_pos_of_pos, div_pos, zero_lt_two
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN₃ : 8 ≤ N
hN₀ : LT.lt (α := ℝ) 0 (↑N : ℝ)
⊢ 0 < HPow.hPow (α := ℝ) (β := ℝ) (↑N : ℝ) (↑(nValue N) : ℝ)⁻¹ / 2

Tactic:
exact div_pos (rpow_pos_of_pos hN₀ _) zero_lt_two

Premises used: Real.rpow_pos_of_pos, div_pos, zero_lt_two
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
N : ℕ
hN : 2 ≤ N
⊢ (2 * dValue N - 1) ^ nValue N ≤ (2 * dValue N) ^ nValue N

Tactic:
have : (2 * dValue N - 1) ^ nValue N ≤ (2 * dValue N) ^ nValue N :=
    Nat.pow_le_pow_left (Nat.sub_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
apply : (2 * dValue N) ^ nValue N ≤ N
⊢ (2 * dValue N - 1) ^ nValue N ≤ N

Tactic:
apply this.trans

Premises used: LE.le.trans