awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
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
⊢ HPow.hPow (β := ℕ) (3 * log 2 * (69 / 50)) 2 ≤ 12 * log 2
have nlinarith₁₆ : 12 * log 2 < HPow.hPow (β := ℕ) (3 * log 2 * (69 / 50)) 2 → GT.gt (α := ℝ) 324194088061593686976 0
Tactic: nlinarith [log_two_lt_d9, log_two_gt_d9]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
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
⊢ HPow.hPow (β := ℕ) (3 * log 2 * (69 / 50)) 2 ≤ 12 * log 2
have nlinarith₁₇ : 12 * log 2 < HPow.hPow (β := ℕ) (3 * log 2 * (69 / 50)) 2 → GT.gt (α := ℝ) 71415000000 0
Tactic: nlinarith [log_two_lt_d9, log_two_gt_d9]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
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
⊢ HPow.hPow (β := ℕ) (3 * log 2 * (69 / 50)) 2 ≤ 12 * log 2
have nlinarith₁₈ : 12 * log 2 < HPow.hPow (β := ℕ) (3 * log 2 * (69 / 50)) 2 → GT.gt (α := ℝ) 1115859375 0
Tactic: nlinarith [log_two_lt_d9, log_two_gt_d9]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
N : ℕ
hN : 4096 ≤ N
⊢ √(log (HPow.hPow (α := ℝ) (β := ℕ) 2 12)) ≤ √(log (↑N : ℝ))
have a : HPow.hPow (α := ℝ) (β := ℕ) 2 12 ≤ (↑N : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
N : ℕ
hN : 4096 ≤ N
⊢ log (2 / (1 - 2 / rexp 1)) * (69 / 50) ≤ √(log (↑N : ℝ))
have _ : log (2 / (1 - 2 / rexp 1)) * (69 / 50) ≤ log (HPow.hPow (α := ℝ) (β := ℕ) 2 3) * (69 / 50)
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
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
N : ℕ
hN : 4096 ≤ N
_ : log (2 / (1 - 2 / rexp 1)) * (69 / 50) ≤ log (HPow.hPow (α := ℝ) (β := ℕ) 2 3) * (69 / 50)
⊢ log (2 / (1 - 2 / rexp 1)) * (69 / 50) ≤ √(log (↑N : ℝ))
have _₁ : log (HPow.hPow (α := ℝ) (β := ℕ) 2 3) * (69 / 50) ≤ √(log (HPow.hPow (α := ℝ) (β := ℕ) 2 12))
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
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
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 (2 / (1 - 2 / rexp 1)) * (69 / 50) ≤ √(log (↑N : ℝ))
have _₂ : √(log (HPow.hPow (α := ℝ) (β := ℕ) 2 12)) ≤ √(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
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (hypothesis)
Goal:
x : ℝ
hx : 0 < x
⊢ rexp (-2 * x) < rexp (HSub.hSub (α := ℝ) 2 (↑⌈x⌉₊ : ℝ)) / (↑⌈x⌉₊ : ℝ)
have h₁ : (↑⌈x⌉₊ : ℝ) < x + 1
Tactic: have h₁ := ceil_lt_add_one hx.le
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
x : ℝ
hx : 0 < x
h₁ : (↑⌈x⌉₊ : ℝ) < x + 1
⊢ 1 - x ≤ HSub.hSub (α := ℝ) 2 (↑⌈x⌉₊ : ℝ)
have linarith : HSub.hSub (α := ℝ) 2 (↑⌈x⌉₊ : ℝ) < 1 - x → (↑⌈x⌉₊ : ℝ) - (x + 1) + (HSub.hSub (α := ℝ) 2 (↑⌈x⌉₊ : ℝ) - (1 - x)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (hypothesis)
Goal:
x : ℝ
hx : 0 < x
h₁ : (↑⌈x⌉₊ : ℝ) < x + 1
⊢ rexp (-2 * x) < rexp (HSub.hSub (α := ℝ) 2 (↑⌈x⌉₊ : ℝ)) / (↑⌈x⌉₊ : ℝ)
have h₂ : 1 - x ≤ HSub.hSub (α := ℝ) 2 (↑⌈x⌉₊ : ℝ)
Tactic: have h₂ : 1 - x ≤ 2 - ⌈x⌉₊ := by linarith
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
x : ℝ
hx : 0 < x
h₁ : (↑⌈x⌉₊ : ℝ) < x + 1
h₂ : 1 - x ≤ HSub.hSub (α := ℝ) 2 (↑⌈x⌉₊ : ℝ)
⊢ rexp (1 - x) / (x + 1) ≤ rexp (HSub.hSub (α := ℝ) 2 (↑⌈x⌉₊ : ℝ)) / (x + 1)
have hc : 0 ≤ x + 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
x : ℝ
hx : 0 < x
h₁ : (↑⌈x⌉₊ : ℝ) < x + 1
h₂ : 1 - x ≤ HSub.hSub (α := ℝ) 2 (↑⌈x⌉₊ : ℝ)
⊢ rexp (HSub.hSub (α := ℝ) 2 (↑⌈x⌉₊ : ℝ)) / (x + 1) < rexp (HSub.hSub (α := ℝ) 2 (↑⌈x⌉₊ : ℝ)) / (↑⌈x⌉₊ : ℝ)
have ha : 0 < rexp (HSub.hSub (α := ℝ) 2 (↑⌈x⌉₊ : ℝ))
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
x : ℝ
hx : 0 < x
h₁ : (↑⌈x⌉₊ : ℝ) < x + 1
h₂ : 1 - x ≤ HSub.hSub (α := ℝ) 2 (↑⌈x⌉₊ : ℝ)
ha : 0 < rexp (HSub.hSub (α := ℝ) 2 (↑⌈x⌉₊ : ℝ))
⊢ rexp (HSub.hSub (α := ℝ) 2 (↑⌈x⌉₊ : ℝ)) / (x + 1) < rexp (HSub.hSub (α := ℝ) 2 (↑⌈x⌉₊ : ℝ)) / (↑⌈x⌉₊ : ℝ)
have hc : LT.lt (α := ℝ) 0 (↑⌈x⌉₊ : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
x : ℝ
hx : 0 < x
h₁ : (↑⌈x⌉₊ : ℝ) < x + 1
h₂ : 1 - x ≤ HSub.hSub (α := ℝ) 2 (↑⌈x⌉₊ : ℝ)
⊢ rexp (-2 * x) < rexp (HSub.hSub (α := ℝ) 2 (↑⌈x⌉₊ : ℝ)) / (↑⌈x⌉₊ : ℝ)
have _ : rexp (-2 * x) ≤ rexp (1 - x) / (x + 1)
Tactic: calc
    _ ≤ exp (1 - x) / (x + 1) := ?_
    _ ≤ exp (2 - ⌈x⌉₊) / (x + 1) := by gcongr
    _ < _ := by gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
x : ℝ
hx : 0 < x
h₁ : (↑⌈x⌉₊ : ℝ) < x + 1
h₂ : 1 - x ≤ HSub.hSub (α := ℝ) 2 (↑⌈x⌉₊ : ℝ)
⊢ rexp (-2 * x) ≤ rexp (1 - x) / (x + 1)
have rw : x + 1 ≤ rexp (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]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
x : ℝ
hx : 2 / (1 - 2 / rexp 1) ≤ x
⊢ x / rexp 1 < (↑⌊x / 2⌋₊ : ℝ)
have apply : x / rexp 1 ≤ x / 2 - 1
Tactic: apply lt_of_le_of_lt _ (sub_one_lt_floor _)
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
x : ℝ
hx : 2 / (1 - 2 / rexp 1) ≤ x
⊢ 0 < 1 - 2 / rexp 1
have rw : 2 < rexp 1
Tactic: rw [sub_pos, div_lt_one (exp_pos _)]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (hypothesis)
Goal:
x : ℝ
hx : 2 / (1 - 2 / rexp 1) ≤ x
⊢ x / rexp 1 ≤ x / 2 - 1
have this : 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
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
x : ℝ
hx : 2 / (1 - 2 / rexp 1) ≤ x
this : 0 < 1 - 2 / rexp 1
⊢ x / rexp 1 ≤ x / 2 - 1
have rwa : LT.lt (α := ℝ) 0 2
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]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
x : ℝ
hx : 2 / (1 - 2 / rexp 1) ≤ x
this : 0 < 1 - 2 / rexp 1
rwa : LT.lt (α := ℝ) 0 2
⊢ x / rexp 1 ≤ x / 2 - 1
have rwa₁ : Ne (α := ℝ) 2 0
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]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
x : ℝ
hx : 50 / 19 ≤ x
⊢ (↑⌈x⌉₊ : ℝ) < 1.38 * x
have refine : x + 1 ≤ 1.38 * x
Tactic: refine (ceil_lt_add_one <| hx.trans' <| by norm_num).trans_le ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
x : ℝ
hx : 50 / 19 ≤ x
⊢ x + 1 ≤ 1.38 * x
have rw : 1 ≤ HSub.hSub (α := ℝ) 1.38 1 * x
Tactic: rw [← le_sub_iff_add_le', ← sub_one_mul]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (hypothesis)
Goal:
x : ℝ
hx : 50 / 19 ≤ x
⊢ 1 ≤ HSub.hSub (α := ℝ) 1.38 1 * x
have this : 1.38 = 69 / 50
Tactic: have : (1.38 : ℝ) = 69 / 50 := by norm_num
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
x : ℝ
hx : 50 / 19 ≤ x
this : 1.38 = 69 / 50
⊢ 1 ≤ HSub.hSub (α := ℝ) 1.38 1 * x
have rwa : 0 < 50 / 19
Tactic: rwa [this, show (69 / 50 - 1 : ℝ) = (50 / 19)⁻¹ by norm_num1, ←
    div_eq_inv_mul, one_le_div]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
N : ℕ
hN : 64 ≤ N
⊢ 3 ≤ nValue N
have rw : 2 < √(log (↑N : ℝ))
Tactic: rw [nValue, ← lt_iff_add_one_le, lt_ceil, cast_two]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
N : ℕ
hN : 64 ≤ N
⊢ 2 < √(log (↑N : ℝ))
have h : HPow.hPow (α := ℝ) (β := ℕ) 2 2 < log (↑N : ℝ)
Tactic: apply lt_sqrt_of_sq_lt
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
N : ℕ
hN : 64 ≤ N
⊢ HPow.hPow (α := ℝ) (β := ℝ) 2 (↑6 : ℝ) ≤ (↑N : ℝ)
have rw : HPow.hPow (α := ℝ) (β := ℕ) 2 6 ≤ (↑N : ℝ)
Tactic: rw [rpow_natCast]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (hypothesis)
Goal:
N : ℕ
hN : 64 ≤ N
⊢ HPow.hPow (α := ℝ) (β := ℕ) 2 2 < log (↑N : ℝ)
have this : HPow.hPow (α := ℝ) (β := ℝ) 2 (↑6 : ℝ) ≤ (↑N : ℝ)
Tactic: have : (2 : ℝ) ^ ((6 : ℕ) : ℝ) ≤ N := by
    rw [rpow_natCast]
    exact (cast_le.2 hN).trans' (by norm_num1)
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
N : ℕ
hN : 64 ≤ N
this : HPow.hPow (α := ℝ) (β := ℝ) 2 (↑6 : ℝ) ≤ (↑N : ℝ)
⊢ HPow.hPow (α := ℝ) (β := ℕ) 2 2 < log (↑N : ℝ)
have apply : HPow.hPow (α := ℝ) (β := ℕ) 2 2 < log (HPow.hPow (α := ℝ) (β := ℝ) 2 (↑6 : ℝ))
Tactic: apply lt_of_lt_of_le _ (log_le_log (rpow_pos_of_pos zero_lt_two _) this)
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
N : ℕ
hN : 64 ≤ N
this : HPow.hPow (α := ℝ) (β := ℝ) 2 (↑6 : ℝ) ≤ (↑N : ℝ)
⊢ HPow.hPow (α := ℝ) (β := ℕ) 2 2 < log (HPow.hPow (α := ℝ) (β := ℝ) 2 (↑6 : ℝ))
have rw : HPow.hPow (α := ℝ) (β := ℕ) 2 2 / (↑6 : ℝ) < log 2
Tactic: rw [log_rpow zero_lt_two, ← div_lt_iff₀']
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
N : ℕ
hN : 64 ≤ N
this : HPow.hPow (α := ℝ) (β := ℝ) 2 (↑6 : ℝ) ≤ (↑N : ℝ)
rw : HPow.hPow (α := ℝ) (β := ℕ) 2 2 / (↑6 : ℝ) < log 2
⊢ HPow.hPow (α := ℝ) (β := ℕ) 2 2 < log (HPow.hPow (α := ℝ) (β := ℝ) 2 (↑6 : ℝ))
have rw₁ : LT.lt (α := ℝ) 0 (↑6 : ℝ)
Tactic: rw [log_rpow zero_lt_two, ← div_lt_iff₀']
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (hypothesis)
Goal:
N : ℕ
hN₃ : 8 ≤ N
⊢ 0 < dValue N
have hN₀ : LT.lt (α := ℝ) 0 (↑N : ℝ)
Tactic: have hN₀ : 0 < (N : ℝ) := cast_pos.2 (succ_pos'.trans_le hN₃)
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
N : ℕ
hN₃ : 8 ≤ N
hN₀ : LT.lt (α := ℝ) 0 (↑N : ℝ)
⊢ 0 < dValue N
have rw : log 2 * (↑(nValue N) : ℝ) ≤ log (↑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₀]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
N : ℕ
hN₃ : 8 ≤ N
hN₀ : LT.lt (α := ℝ) 0 (↑N : ℝ)
rw : log 2 * (↑(nValue N) : ℝ) ≤ log (↑N : ℝ)
⊢ 0 < dValue N
have rw₁ : LT.lt (α := ℝ) 0 (↑(nValue 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₀]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
N : ℕ
hN₃ : 8 ≤ N
hN₀ : LT.lt (α := ℝ) 0 (↑N : ℝ)
rw : log 2 * (↑(nValue N) : ℝ) ≤ log (↑N : ℝ)
rw₁ : LT.lt (α := ℝ) 0 (↑(nValue N) : ℝ)
⊢ 0 < dValue N
have rw₂ : HPow.hPow (α := ℝ) (β := ℝ) (↑N : ℝ) (↑(nValue N) : ℝ)⁻¹ ≠ 0
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₀]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
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
⊢ 0 < dValue N
have rw₃ : 0 < HPow.hPow (α := ℝ) (β := ℝ) (↑N : ℝ) (↑(nValue N) : ℝ)⁻¹ / 2
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₀]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
N : ℕ
hN₃ : 8 ≤ N
hN₀ : LT.lt (α := ℝ) 0 (↑N : ℝ)
⊢ (↑(nValue N) : ℝ) ≤ 2 * √(log (↑N : ℝ))
have apply : √(log (↑N : ℝ)) + 1 ≤ 2 * √(log (↑N : ℝ))
Tactic: apply (ceil_lt_add_one <| sqrt_nonneg _).le.trans
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
N : ℕ
hN₃ : 8 ≤ N
hN₀ : LT.lt (α := ℝ) 0 (↑N : ℝ)
⊢ √(log (↑N : ℝ)) + 1 ≤ 2 * √(log (↑N : ℝ))
have rw : 1 ≤ √(log (↑N : ℝ))
Tactic: rw [two_mul, add_le_add_iff_left]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
N : ℕ
hN₃ : 8 ≤ N
hN₀ : LT.lt (α := ℝ) 0 (↑N : ℝ)
⊢ 1 ≤ √(log (↑N : ℝ))
have h : HPow.hPow (α := ℝ) (β := ℕ) 1 2 ≤ log (↑N : ℝ)
Tactic: apply le_sqrt_of_sq_le
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
N : ℕ
hN₃ : 8 ≤ N
hN₀ : LT.lt (α := ℝ) 0 (↑N : ℝ)
⊢ HPow.hPow (α := ℝ) (β := ℕ) 1 2 ≤ log (↑N : ℝ)
have h : rexp 1 ≤ (↑N : ℝ)
Tactic: rw [one_pow, le_log_iff_exp_le hN₀]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (hypothesis)
Goal:
N : ℕ
hN₃ : 8 ≤ N
hN₀ : LT.lt (α := ℝ) 0 (↑N : ℝ)
⊢ log 2 * (↑(nValue N) : ℝ) ≤ log (↑N : ℝ)
have this : (↑(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₃)
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
N : ℕ
hN₃ : 8 ≤ N
hN₀ : LT.lt (α := ℝ) 0 (↑N : ℝ)
this : (↑(nValue N) : ℝ) ≤ 2 * √(log (↑N : ℝ))
⊢ log 2 * (↑(nValue N) : ℝ) ≤ log (↑N : ℝ)
have apply : log 2 * (2 * √(log (↑N : ℝ))) ≤ log (↑N : ℝ)
Tactic: apply (mul_le_mul_of_nonneg_left this <| log_nonneg one_le_two).trans _
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
N : ℕ
hN₃ : 8 ≤ N
hN₀ : LT.lt (α := ℝ) 0 (↑N : ℝ)
this : (↑(nValue N) : ℝ) ≤ 2 * √(log (↑N : ℝ))
⊢ log 2 * (2 * √(log (↑N : ℝ))) ≤ log (↑N : ℝ)
have rw : log 2 * 2 ≤ √(log (↑N : ℝ))
Tactic: rw [← mul_assoc, ← le_div_iff₀ (Real.sqrt_pos.2 <| log_pos <| one_lt_cast.2 _), div_sqrt]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
N : ℕ
hN₃ : 8 ≤ N
hN₀ : LT.lt (α := ℝ) 0 (↑N : ℝ)
this : (↑(nValue N) : ℝ) ≤ 2 * √(log (↑N : ℝ))
rw : log 2 * 2 ≤ √(log (↑N : ℝ))
⊢ log 2 * (2 * √(log (↑N : ℝ))) ≤ log (↑N : ℝ)
have rw₁ : 1 < N
Tactic: rw [← mul_assoc, ← le_div_iff₀ (Real.sqrt_pos.2 <| log_pos <| one_lt_cast.2 _), div_sqrt]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
N : ℕ
hN₃ : 8 ≤ N
hN₀ : LT.lt (α := ℝ) 0 (↑N : ℝ)
this : (↑(nValue N) : ℝ) ≤ 2 * √(log (↑N : ℝ))
⊢ log 2 * 2 ≤ √(log (↑N : ℝ))
have apply : √(log 8) ≤ √(log (↑N : ℝ))
Tactic: apply log_two_mul_two_le_sqrt_log_eight.trans
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
N : ℕ
hN₃ : 8 ≤ N
hN₀ : LT.lt (α := ℝ) 0 (↑N : ℝ)
this : (↑(nValue N) : ℝ) ≤ 2 * √(log (↑N : ℝ))
⊢ √(log 8) ≤ √(log (↑N : ℝ))
have h : log 8 ≤ log (↑N : ℝ)
Tactic: apply Real.sqrt_le_sqrt
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (hypothesis)
Goal:
N : ℕ
hN : 2 ≤ N
⊢ (2 * dValue N - 1) ^ nValue N ≤ N
have this : (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 _ _) _
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
N : ℕ
hN : 2 ≤ N
this : (2 * dValue N - 1) ^ nValue N ≤ (2 * dValue N) ^ nValue N
⊢ (2 * dValue N - 1) ^ nValue N ≤ N
have apply : (2 * dValue N) ^ nValue N ≤ N
Tactic: apply this.trans