awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
linarith : HSub.hSub (α := ℝ) 8 2 * rexp 1 < HMul.hMul (α := ℝ) 8 2 → 10000000000 / 10000000000 = 1
linarith₁ : HSub.hSub (α := ℝ) 8 2 * rexp 1 < HMul.hMul (α := ℝ) 8 2 → HMul.hMul (α := ℝ) 1 10000000000 = 10000000000
linarith₂ : HSub.hSub (α := ℝ) 8 2 * rexp 1 < HMul.hMul (α := ℝ) 8 2 → GT.gt (α := ℝ) 10000000000 0
linarith₃ :
  HSub.hSub (α := ℝ) 8 2 * rexp 1 < HMul.hMul (α := ℝ) 8 2 →
    HMul.hMul (α := ℝ) 1548454849 (-1) + 5000000000 * (HSub.hSub (α := ℝ) 8 2 * rexp 1 - HMul.hMul (α := ℝ) 8 2) +
        3 * (HMul.hMul (α := ℝ) 1 27182818283 - 10000000000 * rexp 1) =
      0
⊢ HMul.hMul (α := ℝ) 8 2 ≤ HSub.hSub (α := ℝ) 8 2 * rexp 1
have linarith₄ : HSub.hSub (α := ℝ) 8 2 * rexp 1 < HMul.hMul (α := ℝ) 8 2 → GT.gt (α := ℝ) 1548454849 0
Tactic: linarith [exp_one_gt_d9]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
linarith : HSub.hSub (α := ℝ) 8 2 * rexp 1 < HMul.hMul (α := ℝ) 8 2 → 10000000000 / 10000000000 = 1
linarith₁ : HSub.hSub (α := ℝ) 8 2 * rexp 1 < HMul.hMul (α := ℝ) 8 2 → HMul.hMul (α := ℝ) 1 10000000000 = 10000000000
linarith₂ : HSub.hSub (α := ℝ) 8 2 * rexp 1 < HMul.hMul (α := ℝ) 8 2 → GT.gt (α := ℝ) 10000000000 0
linarith₃ :
  HSub.hSub (α := ℝ) 8 2 * rexp 1 < HMul.hMul (α := ℝ) 8 2 →
    HMul.hMul (α := ℝ) 1548454849 (-1) + 5000000000 * (HSub.hSub (α := ℝ) 8 2 * rexp 1 - HMul.hMul (α := ℝ) 8 2) +
        3 * (HMul.hMul (α := ℝ) 1 27182818283 - 10000000000 * rexp 1) =
      0
linarith₄ : HSub.hSub (α := ℝ) 8 2 * rexp 1 < HMul.hMul (α := ℝ) 8 2 → GT.gt (α := ℝ) 1548454849 0
⊢ HMul.hMul (α := ℝ) 8 2 ≤ HSub.hSub (α := ℝ) 8 2 * rexp 1
have linarith₅ : HSub.hSub (α := ℝ) 8 2 * rexp 1 < HMul.hMul (α := ℝ) 8 2 → GT.gt (α := ℝ) 5000000000 0
Tactic: linarith [exp_one_gt_d9]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
linarith : HSub.hSub (α := ℝ) 8 2 * rexp 1 < HMul.hMul (α := ℝ) 8 2 → 10000000000 / 10000000000 = 1
linarith₁ : HSub.hSub (α := ℝ) 8 2 * rexp 1 < HMul.hMul (α := ℝ) 8 2 → HMul.hMul (α := ℝ) 1 10000000000 = 10000000000
linarith₂ : HSub.hSub (α := ℝ) 8 2 * rexp 1 < HMul.hMul (α := ℝ) 8 2 → GT.gt (α := ℝ) 10000000000 0
linarith₃ :
  HSub.hSub (α := ℝ) 8 2 * rexp 1 < HMul.hMul (α := ℝ) 8 2 →
    HMul.hMul (α := ℝ) 1548454849 (-1) + 5000000000 * (HSub.hSub (α := ℝ) 8 2 * rexp 1 - HMul.hMul (α := ℝ) 8 2) +
        3 * (HMul.hMul (α := ℝ) 1 27182818283 - 10000000000 * rexp 1) =
      0
linarith₄ : HSub.hSub (α := ℝ) 8 2 * rexp 1 < HMul.hMul (α := ℝ) 8 2 → GT.gt (α := ℝ) 1548454849 0
linarith₅ : HSub.hSub (α := ℝ) 8 2 * rexp 1 < HMul.hMul (α := ℝ) 8 2 → GT.gt (α := ℝ) 5000000000 0
⊢ HMul.hMul (α := ℝ) 8 2 ≤ HSub.hSub (α := ℝ) 8 2 * rexp 1
have linarith₆ : HSub.hSub (α := ℝ) 8 2 * rexp 1 < HMul.hMul (α := ℝ) 8 2 → GT.gt (α := ℝ) 3 0
Tactic: linarith [exp_one_gt_d9]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
⊢ 0 < 1 - 2 / rexp 1
have rw : 2 < rexp 1
Tactic: rw [sub_pos, div_lt_one]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
rw : 2 < rexp 1
⊢ 0 < 1 - 2 / rexp 1
have rw₁ : 0 < rexp 1
Tactic: rw [sub_pos, div_lt_one]
-- 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)
have hbc : 0 < 2 / (1 - 2 / rexp 1)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
N : ℕ
hN : 4096 ≤ N
hbc : 0 < 2 / (1 - 2 / rexp 1)
⊢ log (2 / (1 - 2 / rexp 1)) * (69 / 50) ≤ log (HPow.hPow (α := ℝ) (β := ℕ) 2 3) * (69 / 50)
have hbc₁ : 2 / (1 - 2 / rexp 1) ≤ HPow.hPow (α := ℝ) (β := ℕ) 2 3
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
N : ℕ
hN : 4096 ≤ N
⊢ 0 < 2 / (1 - 2 / rexp 1)
have hbc : 0 < 2 * rexp 1 / (rexp 1 - 2)
Tactic: field_simp
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
N : ℕ
hN : 4096 ≤ N
⊢ 2 / (1 - 2 / rexp 1) ≤ HPow.hPow (α := ℝ) (β := ℕ) 2 3
have hbc : 2 / (1 - 2 / rexp 1) ≤ 8
Tactic: norm_num1
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
N : ℕ
hN : 4096 ≤ N
⊢ log (HPow.hPow (α := ℝ) (β := ℕ) 2 3) * (69 / 50) ≤ √(log (HPow.hPow (α := ℝ) (β := ℕ) 2 12))
have simp : 3 * log 2 * (69 / 50) ≤ √(12 * log 2)
Tactic: simp only [Real.log_pow, Nat.cast_ofNat]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
N : ℕ
hN : 4096 ≤ N
⊢ 3 * log 2 * (69 / 50) ≤ √(12 * log 2)
have h : HPow.hPow (β := ℕ) (3 * log 2 * (69 / 50)) 2 ≤ 12 * log 2
Tactic: apply le_sqrt_of_sq_le
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
N : ℕ
hN : 4096 ≤ N
⊢ HPow.hPow (β := ℕ) (3 * log 2 * (69 / 50)) 2 ≤ 12 * log 2
have nlinarith : 12 * log 2 < HPow.hPow (β := ℕ) (3 * log 2 * (69 / 50)) 2 → 10000000000 / 10000000000 = 1
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
⊢ HPow.hPow (β := ℕ) (3 * log 2 * (69 / 50)) 2 ≤ 12 * log 2
have nlinarith₁ : 12 * log 2 < HPow.hPow (β := ℕ) (3 * log 2 * (69 / 50)) 2 → HMul.hMul (α := ℝ) 1 10000000000 = 10000000000
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
⊢ 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 (α := ℝ) 10000000000 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
⊢ HPow.hPow (β := ℕ) (3 * log 2 * (69 / 50)) 2 ≤ 12 * log 2
have nlinarith₃ : 12 * log 2 < HPow.hPow (β := ℕ) (3 * log 2 * (69 / 50)) 2 → 156250000 / 156250000 = 1
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
⊢ HPow.hPow (β := ℕ) (3 * log 2 * (69 / 50)) 2 ≤ 12 * log 2
have nlinarith₄ : 12 * log 2 < HPow.hPow (β := ℕ) (3 * log 2 * (69 / 50)) 2 → HMul.hMul (α := ℝ) 1 156250000 = 156250000
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
⊢ 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 (α := ℝ) 156250000 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
⊢ HPow.hPow (β := ℕ) (3 * log 2 * (69 / 50)) 2 ≤ 12 * log 2
have nlinarith₆ : 12 * log 2 < HPow.hPow (β := ℕ) (3 * log 2 * (69 / 50)) 2 → HMul.hMul (α := ℝ) 1 2500 = 2500
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
⊢ HPow.hPow (β := ℕ) (3 * log 2 * (69 / 50)) 2 ≤ 12 * log 2
have nlinarith₇ : 12 * log 2 < HPow.hPow (β := ℕ) (3 * log 2 * (69 / 50)) 2 → HMul.hMul (α := ℝ) 1 1 = 1
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
⊢ HPow.hPow (β := ℕ) (3 * log 2 * (69 / 50)) 2 ≤ 12 * log 2
have nlinarith₈ : 12 * log 2 < HPow.hPow (β := ℕ) (3 * log 2 * (69 / 50)) 2 → 50 / 50 = 1
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
⊢ HPow.hPow (β := ℕ) (3 * log 2 * (69 / 50)) 2 ≤ 12 * log 2
have nlinarith₉ : 12 * log 2 < HPow.hPow (β := ℕ) (3 * log 2 * (69 / 50)) 2 → HMul.hMul (α := ℝ) 1 50 = 50
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
⊢ HPow.hPow (β := ℕ) (3 * log 2 * (69 / 50)) 2 ≤ 12 * log 2
have nlinarith₁₁ : 12 * log 2 < HPow.hPow (β := ℕ) (3 * log 2 * (69 / 50)) 2 → 1 * HPow.hPow (α := ℝ) (β := ℕ) 50 2 = 2500
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
⊢ 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 (α := ℝ) 2500 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
⊢ HPow.hPow (β := ℕ) (3 * log 2 * (69 / 50)) 2 ≤ 12 * log 2
have 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
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
⊢ 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 (α := ℝ) 7812499994420703125 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
⊢ 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 (α := ℝ) 20748421620975173471424 0
Tactic: nlinarith [log_two_lt_d9, log_two_gt_d9]