awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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) ^ nValue N ≤ N
have suffices : HMul.hMul (α := ℝ) 2 (↑(dValue N) : ℝ) ^ nValue N ≤ (↑N : ℝ)
Tactic: suffices ((2 * dValue N) ^ nValue N : ℝ) ≤ N from mod_cast this
-- 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
i : HMul.hMul (α := ℝ) 2 (↑(dValue N) : ℝ) ≤ HPow.hPow (α := ℝ) (β := ℝ) (↑N : ℝ) (↑(nValue N) : ℝ)⁻¹
⊢ HMul.hMul (α := ℝ) 2 (↑(dValue N) : ℝ) ^ nValue N ≤ (↑N : ℝ)
have rw : HPow.hPow (β := ℝ) (HMul.hMul (α := ℝ) 2 (↑(dValue N) : ℝ)) (↑(nValue N) : ℝ) ≤ (↑N : ℝ)
Tactic: rw [← rpow_natCast]
-- 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
i : HMul.hMul (α := ℝ) 2 (↑(dValue N) : ℝ) ≤ HPow.hPow (α := ℝ) (β := ℝ) (↑N : ℝ) (↑(nValue N) : ℝ)⁻¹
⊢ HPow.hPow (β := ℝ) (HMul.hMul (α := ℝ) 2 (↑(dValue N) : ℝ)) (↑(nValue N) : ℝ) ≤ (↑N : ℝ)
have apply : HPow.hPow (β := ℝ) (HPow.hPow (α := ℝ) (β := ℝ) (↑N : ℝ) (↑(nValue N) : ℝ)⁻¹) (↑(nValue N) : ℝ) ≤ (↑N : ℝ)
Tactic: apply (rpow_le_rpow (mul_nonneg zero_le_two (cast_nonneg _)) i (cast_nonneg _)).trans
-- 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
i : HMul.hMul (α := ℝ) 2 (↑(dValue N) : ℝ) ≤ HPow.hPow (α := ℝ) (β := ℝ) (↑N : ℝ) (↑(nValue N) : ℝ)⁻¹
⊢ HPow.hPow (β := ℝ) (HPow.hPow (α := ℝ) (β := ℝ) (↑N : ℝ) (↑(nValue N) : ℝ)⁻¹) (↑(nValue N) : ℝ) ≤ (↑N : ℝ)
have rw : Ne (α := ℝ) (↑(nValue N) : ℝ) 0
Tactic: rw [← rpow_mul (cast_nonneg _), inv_mul_cancel₀, rpow_one]
-- 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
i : HMul.hMul (α := ℝ) 2 (↑(dValue N) : ℝ) ≤ HPow.hPow (α := ℝ) (β := ℝ) (↑N : ℝ) (↑(nValue N) : ℝ)⁻¹
⊢ Ne (α := ℝ) (↑(nValue N) : ℝ) 0
have rw : nValue N ≠ 0
Tactic: rw [cast_ne_zero]
-- 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
⊢ HMul.hMul (α := ℝ) 2 (↑(dValue N) : ℝ) ^ nValue N ≤ (↑N : ℝ)
have suffices : HMul.hMul (α := ℝ) 2 (↑(dValue N) : ℝ) ≤ HPow.hPow (α := ℝ) (β := ℝ) (↑N : ℝ) (↑(nValue 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'
-- 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
⊢ HMul.hMul (α := ℝ) 2 (↑(dValue N) : ℝ) ≤ HPow.hPow (α := ℝ) (β := ℝ) (↑N : ℝ) (↑(nValue N) : ℝ)⁻¹
have rw : (↑(dValue N) : ℝ) ≤ HPow.hPow (α := ℝ) (β := ℝ) (↑N : ℝ) (↑(nValue N) : ℝ)⁻¹ / 2
Tactic: rw [← le_div_iff₀']
-- 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
rw : (↑(dValue N) : ℝ) ≤ HPow.hPow (α := ℝ) (β := ℝ) (↑N : ℝ) (↑(nValue N) : ℝ)⁻¹ / 2
⊢ HMul.hMul (α := ℝ) 2 (↑(dValue N) : ℝ) ≤ HPow.hPow (α := ℝ) (β := ℝ) (↑N : ℝ) (↑(nValue N) : ℝ)⁻¹
have rw₁ : LT.lt (α := ℝ) 0 2
Tactic: rw [← le_div_iff₀']
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
N : ℕ
hN : 4096 ≤ N
⊢ HPow.hPow (α := ℝ) (β := ℝ) (↑N : ℝ) (↑(nValue N) : ℝ)⁻¹ / rexp 1 < (↑(dValue N) : ℝ)
have apply : 2 / (1 - 2 / rexp 1) ≤ HPow.hPow (α := ℝ) (β := ℝ) (↑N : ℝ) (↑(nValue N) : ℝ)⁻¹
Tactic: apply div_lt_floor _
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
N : ℕ
hN : 4096 ≤ N
⊢ 2 / (1 - 2 / rexp 1) ≤ HPow.hPow (α := ℝ) (β := ℝ) (↑N : ℝ) (↑(nValue N) : ℝ)⁻¹
have rw : log (2 / (1 - 2 / rexp 1)) ≤ log (↑N : ℝ) / (↑⌈√(log (↑N : ℝ))⌉₊ : ℝ)
Tactic: rw [← log_le_log_iff, log_rpow, mul_comm, ← div_eq_mul_inv, nValue]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
N : ℕ
hN : 4096 ≤ N
rw : log (2 / (1 - 2 / rexp 1)) ≤ log (↑N : ℝ) / (↑⌈√(log (↑N : ℝ))⌉₊ : ℝ)
⊢ 2 / (1 - 2 / rexp 1) ≤ HPow.hPow (α := ℝ) (β := ℝ) (↑N : ℝ) (↑(nValue N) : ℝ)⁻¹
have hx : LT.lt (α := ℝ) 0 (↑N : ℝ)
Tactic: rw [← log_le_log_iff, log_rpow, mul_comm, ← div_eq_mul_inv, nValue]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
N : ℕ
hN : 4096 ≤ N
rw : log (2 / (1 - 2 / rexp 1)) ≤ log (↑N : ℝ) / (↑⌈√(log (↑N : ℝ))⌉₊ : ℝ)
hx : LT.lt (α := ℝ) 0 (↑N : ℝ)
⊢ 2 / (1 - 2 / rexp 1) ≤ HPow.hPow (α := ℝ) (β := ℝ) (↑N : ℝ) (↑(nValue N) : ℝ)⁻¹
have h : 0 < 2 / (1 - 2 / rexp 1)
Tactic: rw [← log_le_log_iff, log_rpow, mul_comm, ← div_eq_mul_inv, nValue]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
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)
⊢ 2 / (1 - 2 / rexp 1) ≤ HPow.hPow (α := ℝ) (β := ℝ) (↑N : ℝ) (↑(nValue N) : ℝ)⁻¹
have h₁ : 0 < HPow.hPow (α := ℝ) (β := ℝ) (↑N : ℝ) (↑(nValue N) : ℝ)⁻¹
Tactic: rw [← log_le_log_iff, log_rpow, mul_comm, ← div_eq_mul_inv, nValue]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
N : ℕ
hN : 4096 ≤ N
⊢ log (2 / (1 - 2 / rexp 1)) ≤ log (↑N : ℝ) / (↑⌈√(log (↑N : ℝ))⌉₊ : ℝ)
have grw : log (2 / (1 - 2 / rexp 1)) ≤ log (↑N : ℝ) / (1.38 * √(log (↑N : ℝ)))
Tactic: grw [ceil_lt_mul]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
N : ℕ
hN : 4096 ≤ N
grw : log (2 / (1 - 2 / rexp 1)) ≤ log (↑N : ℝ) / (1.38 * √(log (↑N : ℝ)))
⊢ log (2 / (1 - 2 / rexp 1)) ≤ log (↑N : ℝ) / (↑⌈√(log (↑N : ℝ))⌉₊ : ℝ)
have h₂ : LT.lt (α := ℝ) 0 (↑⌈√(log (↑N : ℝ))⌉₊ : ℝ)
Tactic: grw [ceil_lt_mul]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
N : ℕ
hN : 4096 ≤ N
grw : log (2 / (1 - 2 / rexp 1)) ≤ log (↑N : ℝ) / (1.38 * √(log (↑N : ℝ)))
h₂ : LT.lt (α := ℝ) 0 (↑⌈√(log (↑N : ℝ))⌉₊ : ℝ)
⊢ log (2 / (1 - 2 / rexp 1)) ≤ log (↑N : ℝ) / (↑⌈√(log (↑N : ℝ))⌉₊ : ℝ)
have grw₁ : 50 / 19 ≤ √(log (↑N : ℝ))
Tactic: grw [ceil_lt_mul]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
N : ℕ
hN : 4096 ≤ N
⊢ log (2 / (1 - 2 / rexp 1)) ≤ log (↑N : ℝ) / (1.38 * √(log (↑N : ℝ)))
have rw : log (2 / (1 - 2 / rexp 1)) * 1.38 ≤ √(log (↑N : ℝ))
Tactic: rw [mul_comm, ← div_div, div_sqrt, le_div_iff₀]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
N : ℕ
hN : 4096 ≤ N
rw : log (2 / (1 - 2 / rexp 1)) * 1.38 ≤ √(log (↑N : ℝ))
⊢ log (2 / (1 - 2 / rexp 1)) ≤ log (↑N : ℝ) / (1.38 * √(log (↑N : ℝ)))
have rw₁ : LT.lt (α := ℝ) 0 1.38
Tactic: rw [mul_comm, ← div_div, div_sqrt, le_div_iff₀]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
N : ℕ
hN : 4096 ≤ N
⊢ LT.lt (α := ℝ) 0 (↑⌈√(log (↑N : ℝ))⌉₊ : ℝ)
have h₂ : 0 < log (↑N : ℝ)
Tactic: rw [cast_pos, lt_ceil, cast_zero, Real.sqrt_pos]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
N : ℕ
hN : 4096 ≤ N
⊢ 0 < log (↑N : ℝ)
have h₂ : LT.lt (α := ℝ) 1 (↑N : ℝ)
Tactic: refine log_pos ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
N : ℕ
hN : 4096 ≤ N
⊢ LT.lt (α := ℝ) 1 (↑N : ℝ)
have h₂ : 1 < N
Tactic: rw [one_lt_cast]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
N : ℕ
hN : 4096 ≤ N
⊢ 50 / 19 ≤ √(log (↑N : ℝ))
have h : HPow.hPow (β := ℕ) (50 / 19) 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 : 4096 ≤ N
⊢ (↑12 : ℝ) * log 2 ≤ log (↑N : ℝ)
have rw : log (HPow.hPow (α := ℝ) (β := ℕ) 2 12) ≤ log (↑N : ℝ)
Tactic: rw [← log_rpow zero_lt_two, rpow_natCast]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (hypothesis)
Goal:
N : ℕ
hN : 4096 ≤ N
⊢ HPow.hPow (β := ℕ) (50 / 19) 2 ≤ log (↑N : ℝ)
have this : (↑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)
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
N : ℕ
hN : 4096 ≤ N
this : (↑12 : ℝ) * log 2 ≤ log (↑N : ℝ)
⊢ HPow.hPow (β := ℕ) (50 / 19) 2 ≤ log (↑N : ℝ)
have h : HPow.hPow (β := ℕ) (50 / 19) 2 ≤ (↑12 : ℝ) * log 2
Tactic: refine le_trans ?_ this
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
N : ℕ
hN : 4096 ≤ N
this : (↑12 : ℝ) * log 2 ≤ log (↑N : ℝ)
⊢ HPow.hPow (β := ℕ) (50 / 19) 2 ≤ (↑12 : ℝ) * log 2
have h : HPow.hPow (β := ℕ) (50 / 19) 2 / (↑12 : ℝ) ≤ log 2
Tactic: rw [← div_le_iff₀']
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
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 ≤ (↑12 : ℝ) * log 2
have h₁ : LT.lt (α := ℝ) 0 (↑12 : ℝ)
Tactic: rw [← div_le_iff₀']
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
N : ℕ
hN : 4096 ≤ N
⊢ LT.lt (α := ℝ) 0 (↑N : ℝ)
have hx : 0 < N
Tactic: rw [cast_pos]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
N : ℕ
hN : 4096 ≤ N
⊢ 0 < 2 / (1 - 2 / rexp 1)
have h : 0 < 1 - 2 / rexp 1
Tactic: refine div_pos zero_lt_two ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
N : ℕ
hN : 4096 ≤ N
⊢ 0 < 1 - 2 / rexp 1
have h : 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:
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
⊢ (↑N : ℝ) * rexp (-4 * √(log (↑N : ℝ))) < (↑((rothNumberNat : (a : ℕ) → ℕ) N) : ℝ)
have hn : LT.lt (α := ℝ) 0 (↑n : ℝ)
Tactic: have hn : 0 < (n : ℝ) := cast_pos.2 (nValue_pos <| hN.trans' <| by norm_num1)
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (hypothesis)
Goal:
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : LT.lt (α := ℝ) 0 (↑n : ℝ)
⊢ (↑N : ℝ) * rexp (-4 * √(log (↑N : ℝ))) < (↑((rothNumberNat : (a : ℕ) → ℕ) N) : ℝ)
have hd : 0 < dValue N
Tactic: have hd : 0 < dValue N := dValue_pos (hN.trans' <| by norm_num1)
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (hypothesis)
Goal:
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : LT.lt (α := ℝ) 0 (↑n : ℝ)
hd : 0 < dValue N
⊢ (↑N : ℝ) * rexp (-4 * √(log (↑N : ℝ))) < (↑((rothNumberNat : (a : ℕ) → ℕ) N) : ℝ)
have hN₀ : LT.lt (α := ℝ) 0 (↑N : ℝ)
Tactic: have hN₀ : 0 < (N : ℝ) := cast_pos.2 (hN.trans' <| by norm_num1)
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (hypothesis)
Goal:
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : LT.lt (α := ℝ) 0 (↑n : ℝ)
hd : 0 < dValue N
hN₀ : LT.lt (α := ℝ) 0 (↑N : ℝ)
⊢ (↑N : ℝ) * rexp (-4 * √(log (↑N : ℝ))) < (↑((rothNumberNat : (a : ℕ) → ℕ) N) : ℝ)
have hn₂ : 2 < n
Tactic: have hn₂ : 2 < n := three_le_nValue <| hN.trans' <| by norm_num1
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (hypothesis)
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
⊢ (↑N : ℝ) * rexp (-4 * √(log (↑N : ℝ))) < (↑((rothNumberNat : (a : ℕ) → ℕ) N) : ℝ)
have this : (2 * dValue N - 1) ^ n ≤ N
Tactic: have : (2 * dValue N - 1) ^ n ≤ N := le_N (hN.trans' <| by norm_num1)
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
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) ^ (n - 2) / (↑n : ℝ) <
    HPow.hPow (α := ℝ) (↑(dValue N) : ℝ) (n - 2) / (↑n : ℝ)
have h : n - 2 ≠ 0
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
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
⊢ (HPow.hPow (α := ℝ) (β := ℝ) (↑N : ℝ) (↑(nValue N) : ℝ)⁻¹ / rexp 1) ^ (n - 2) / (↑n : ℝ) <
    HPow.hPow (α := ℝ) (↑(dValue N) : ℝ) (n - 2) / (↑n : ℝ)
have h₁ : HPow.hPow (α := ℝ) (β := ℝ) (↑N : ℝ) (↑(nValue N) : ℝ)⁻¹ / rexp 1 < (↑(dValue N) : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
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 : ℝ))) < (↑((rothNumberNat : (a : ℕ) → ℕ) N) : ℝ)
have _ : (↑N : ℝ) * rexp (-4 * √(log (↑N : ℝ))) ≤
  (HPow.hPow (α := ℝ) (β := ℝ) (↑N : ℝ) (↑(nValue N) : ℝ)⁻¹ / rexp 1) ^ (n - 2) / (↑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
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
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 : ℝ)
have rw : (↑N : ℝ) * rexp (-4 * √(log (↑N : ℝ))) ≤
  (↑N : ℝ) *
    (HPow.hPow (α := ℝ) (↑N : ℝ) (HDiv.hDiv (α := ℝ) 2 (↑n : ℝ)) * (rexp (HSub.hSub (α := ℝ) (↑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]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
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 : ℝ))) ≤
    (↑N : ℝ) *
      (HPow.hPow (α := ℝ) (↑N : ℝ) (HDiv.hDiv (α := ℝ) 2 (↑n : ℝ)) *
          (rexp (HSub.hSub (α := ℝ) (↑n : ℝ) 2) * (↑n : ℝ)))⁻¹
have hbc : rexp (-4 * √(log (↑N : ℝ))) ≤
  (HPow.hPow (α := ℝ) (↑N : ℝ) (HDiv.hDiv (α := ℝ) 2 (↑n : ℝ)) * (rexp (HSub.hSub (α := ℝ) (↑n : ℝ) 2) * (↑n : ℝ)))⁻¹
Tactic: gcongr _ * ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
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 : ℝ))) ≤
    (HPow.hPow (α := ℝ) (↑N : ℝ) (HDiv.hDiv (α := ℝ) 2 (↑n : ℝ)) * (rexp (HSub.hSub (α := ℝ) (↑n : ℝ) 2) * (↑n : ℝ)))⁻¹
have hbc : rexp (-4 * √(log (↑N : ℝ))) ≤
  HPow.hPow (α := ℝ) (↑N : ℝ) (-HDiv.hDiv (α := ℝ) 2 (↑n : ℝ)) * (rexp (HSub.hSub (α := ℝ) 2 (↑n : ℝ)) / (↑n : ℝ))
Tactic: rw [mul_inv, mul_inv, ← exp_neg, ← rpow_neg (cast_nonneg _), neg_sub, ← div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
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 : ℝ)))
have rw : rexp (-4 * √(log (↑N : ℝ))) = rexp (HAdd.hAdd (α := ℝ) (-2) (-2) * √(log (↑N : ℝ)))
Tactic: rw [← exp_add, ← add_mul]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (hypothesis)
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 : ℝ))) ≤
    HPow.hPow (α := ℝ) (↑N : ℝ) (-HDiv.hDiv (α := ℝ) 2 (↑n : ℝ)) * (rexp (HSub.hSub (α := ℝ) 2 (↑n : ℝ)) / (↑n : ℝ))
have this₁ : 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
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
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 : ℝ)))
⊢ rexp (-4 * √(log (↑N : ℝ))) ≤
    HPow.hPow (α := ℝ) (↑N : ℝ) (-HDiv.hDiv (α := ℝ) 2 (↑n : ℝ)) * (rexp (HSub.hSub (α := ℝ) 2 (↑n : ℝ)) / (↑n : ℝ))
have hbc : rexp (-2 * √(log (↑N : ℝ))) * rexp (-2 * √(log (↑N : ℝ))) ≤
  HPow.hPow (α := ℝ) (↑N : ℝ) (-HDiv.hDiv (α := ℝ) 2 (↑n : ℝ)) * (rexp (HSub.hSub (α := ℝ) 2 (↑n : ℝ)) / (↑n : ℝ))
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
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 : ℝ)))
⊢ rexp (-2 * √(log (↑N : ℝ))) * rexp (-2 * √(log (↑N : ℝ))) ≤
    HPow.hPow (α := ℝ) (↑N : ℝ) (-HDiv.hDiv (α := ℝ) 2 (↑n : ℝ)) * (rexp (HSub.hSub (α := ℝ) 2 (↑n : ℝ)) / (↑n : ℝ))
have hbc : rexp (-2 * √(log (↑N : ℝ))) ≤ HPow.hPow (α := ℝ) (↑N : ℝ) (-HDiv.hDiv (α := ℝ) 2 (↑n : ℝ))
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
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 : ℝ))
⊢ rexp (-2 * √(log (↑N : ℝ))) * rexp (-2 * √(log (↑N : ℝ))) ≤
    HPow.hPow (α := ℝ) (↑N : ℝ) (-HDiv.hDiv (α := ℝ) 2 (↑n : ℝ)) * (rexp (HSub.hSub (α := ℝ) 2 (↑n : ℝ)) / (↑n : ℝ))
have hbc₁ : rexp (-2 * √(log (↑N : ℝ))) ≤ rexp (HSub.hSub (α := ℝ) 2 (↑n : ℝ)) / (↑n : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
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 : ℝ)))
⊢ rexp (-2 * √(log (↑N : ℝ))) ≤ HPow.hPow (α := ℝ) (↑N : ℝ) (-HDiv.hDiv (α := ℝ) 2 (↑n : ℝ))
have hbc : 2 * √(log (↑N : ℝ)) ≤ HMul.hMul (α := ℝ) 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]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
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 : ℝ)
⊢ rexp (-2 * √(log (↑N : ℝ))) ≤ HPow.hPow (α := ℝ) (↑N : ℝ) (-HDiv.hDiv (α := ℝ) 2 (↑n : ℝ))
have hbc₁ : 0 < √(log (↑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]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
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 : ℝ)))
⊢ 2 * √(log (↑N : ℝ)) ≤ HMul.hMul (α := ℝ) 2 (↑n : ℝ)
have hbc : √(log (↑N : ℝ)) ≤ (↑n : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
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 : ℝ)))
⊢ 0 < √(log (↑N : ℝ))
have hbc : LT.lt (α := ℝ) 1 (↑N : ℝ)
Tactic: refine Real.sqrt_pos.2 (log_pos ?_)
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
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 : ℝ)))
⊢ LT.lt (α := ℝ) 1 (↑N : ℝ)
have hbc : 1 < N
Tactic: rw [one_lt_cast]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
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 : ℝ)))
⊢ rexp (-2 * √(log (↑N : ℝ))) ≤ rexp (HSub.hSub (α := ℝ) 2 (↑n : ℝ)) / (↑n : ℝ)
have hbc : LT.lt (α := ℝ) 1 (↑N : ℝ)
Tactic: refine (exp_neg_two_mul_le <| Real.sqrt_pos.2 <| log_pos ?_).le
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
⊢ 64 = HPow.hPow (α := ℝ) (β := ℝ) 2 (↑6 : ℝ)
have rw : 64 = HPow.hPow (α := ℝ) (β := ℕ) 2 6
Tactic: rw [rpow_natCast]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
⊢ rexp 4 < 64
have rw : HDiv.hDiv (α := ℝ) 4 (↑6 : ℝ) < log 2
Tactic: rw [show (64 : ℝ) = 2 ^ ((6 : ℕ) : ℝ) by rw [rpow_natCast]; norm_num1,
    ← lt_log_iff_exp_lt (rpow_pos_of_pos zero_lt_two _), log_rpow zero_lt_two, ← div_lt_iff₀']
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
rw : HDiv.hDiv (α := ℝ) 4 (↑6 : ℝ) < log 2
⊢ rexp 4 < 64
have rw₁ : LT.lt (α := ℝ) 0 (↑6 : ℝ)
Tactic: rw [show (64 : ℝ) = 2 ^ ((6 : ℕ) : ℝ) by rw [rpow_natCast]; norm_num1,
    ← lt_log_iff_exp_lt (rpow_pos_of_pos zero_lt_two _), log_rpow zero_lt_two, ← div_lt_iff₀']
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
⊢ 4096 = HPow.hPow (α := ℝ) (β := ℕ) 2 12
have norm_cast : 4096 = HPow.hPow (α := ℕ) (β := ℕ) 2 12
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
⊢ 4096 < rexp 16
have rw : 12 * log 2 < 16
Tactic: rw [← log_lt_iff_lt_exp (show (0 : ℝ) < 4096 by simp), show (4096 : ℝ) = 2 ^ 12 by norm_cast,
    ← rpow_natCast, log_rpow zero_lt_two, cast_ofNat]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
⊢ 12 * log 2 < 16
have linarith : 16 ≤ 12 * log 2 → 156250000 / 156250000 = 1
Tactic: linarith [log_two_lt_d9]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
linarith : 16 ≤ 12 * log 2 → 156250000 / 156250000 = 1
⊢ 12 * log 2 < 16
have linarith₁ : 16 ≤ 12 * log 2 → HMul.hMul (α := ℝ) 1 156250000 = 156250000
Tactic: linarith [log_two_lt_d9]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
linarith : 16 ≤ 12 * log 2 → 156250000 / 156250000 = 1
linarith₁ : 16 ≤ 12 * log 2 → HMul.hMul (α := ℝ) 1 156250000 = 156250000
⊢ 12 * log 2 < 16
have linarith₂ : 16 ≤ 12 * log 2 → GT.gt (α := ℝ) 156250000 0
Tactic: linarith [log_two_lt_d9]