awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
pi_lower_bound :
  (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries 4 ≤
    2 - HPow.hPow (β := ℕ) (3.14 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1)) 2
hz :
  (HDiv.hDiv (α := ℝ) (↑338 : ℝ) (↑239 : ℝ)).sqrtTwoAddSeries 3 ≤
    2 - HPow.hPow (β := ℕ) (3.14 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1)) 2
hb : LT.lt (α := ℕ) 0 1
hd : LT.lt (α := ℕ) 0 239
h : (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 239 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 338 2 * 1
hz₁ :
  (HDiv.hDiv (α := ℝ) (↑704 : ℝ) (↑381 : ℝ)).sqrtTwoAddSeries 2 ≤
    2 - HPow.hPow (β := ℕ) (3.14 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1)) 2
hz₂ : LT.lt (α := ℕ) 0 239
hz₃ : LT.lt (α := ℕ) 0 381
hz₄ : (HMul.hMul (α := ℕ) 2 239 + 338) * HPow.hPow (α := ℕ) (β := ℕ) 381 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 704 2 * 239
hb₁ : LT.lt (α := ℕ) 0 1
hd₁ : LT.lt (α := ℕ) 0 239
h₁ : (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 239 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 338 2 * 1
hz₅ :
  (HDiv.hDiv (α := ℝ) (↑1940 : ℝ) (↑989 : ℝ)).sqrtTwoAddSeries 1 ≤
    2 - HPow.hPow (β := ℕ) (3.14 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1)) 2
hz₆ : LT.lt (α := ℕ) 0 381
hz₇ : LT.lt (α := ℕ) 0 989
hz₈ : (HMul.hMul (α := ℕ) 2 381 + 704) * HPow.hPow (α := ℕ) (β := ℕ) 989 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 1940 2 * 381
hz₉ : LT.lt (α := ℕ) 0 239
hz₁₀ : LT.lt (α := ℕ) 0 381
hz₁₁ : (HMul.hMul (α := ℕ) 2 239 + 338) * HPow.hPow (α := ℕ) (β := ℕ) 381 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 704 2 * 239
hb₂ : LT.lt (α := ℕ) 0 1
hd₂ : LT.lt (α := ℕ) 0 239
h₂ : (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 239 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 338 2 * 1
hz₁₂ :
  (HDiv.hDiv (α := ℝ) (↑1447 : ℝ) (↑727 : ℝ)).sqrtTwoAddSeries 0 ≤
    2 - HPow.hPow (β := ℕ) (3.14 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1)) 2
hz₁₃ : LT.lt (α := ℕ) 0 989
⊢ 3.14 < π
have hz₁₄ : LT.lt (α := ℕ) 0 727
Tactic: pi_lower_bound [338 / 239, 704 / 381, 1940 / 989, 1447 / 727]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
pi_lower_bound :
  (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries 4 ≤
    2 - HPow.hPow (β := ℕ) (3.14 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1)) 2
hz :
  (HDiv.hDiv (α := ℝ) (↑338 : ℝ) (↑239 : ℝ)).sqrtTwoAddSeries 3 ≤
    2 - HPow.hPow (β := ℕ) (3.14 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1)) 2
hb : LT.lt (α := ℕ) 0 1
hd : LT.lt (α := ℕ) 0 239
h : (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 239 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 338 2 * 1
hz₁ :
  (HDiv.hDiv (α := ℝ) (↑704 : ℝ) (↑381 : ℝ)).sqrtTwoAddSeries 2 ≤
    2 - HPow.hPow (β := ℕ) (3.14 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1)) 2
hz₂ : LT.lt (α := ℕ) 0 239
hz₃ : LT.lt (α := ℕ) 0 381
hz₄ : (HMul.hMul (α := ℕ) 2 239 + 338) * HPow.hPow (α := ℕ) (β := ℕ) 381 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 704 2 * 239
hb₁ : LT.lt (α := ℕ) 0 1
hd₁ : LT.lt (α := ℕ) 0 239
h₁ : (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 239 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 338 2 * 1
hz₅ :
  (HDiv.hDiv (α := ℝ) (↑1940 : ℝ) (↑989 : ℝ)).sqrtTwoAddSeries 1 ≤
    2 - HPow.hPow (β := ℕ) (3.14 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1)) 2
hz₆ : LT.lt (α := ℕ) 0 381
hz₇ : LT.lt (α := ℕ) 0 989
hz₈ : (HMul.hMul (α := ℕ) 2 381 + 704) * HPow.hPow (α := ℕ) (β := ℕ) 989 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 1940 2 * 381
hz₉ : LT.lt (α := ℕ) 0 239
hz₁₀ : LT.lt (α := ℕ) 0 381
hz₁₁ : (HMul.hMul (α := ℕ) 2 239 + 338) * HPow.hPow (α := ℕ) (β := ℕ) 381 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 704 2 * 239
hb₂ : LT.lt (α := ℕ) 0 1
hd₂ : LT.lt (α := ℕ) 0 239
h₂ : (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 239 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 338 2 * 1
hz₁₂ :
  (HDiv.hDiv (α := ℝ) (↑1447 : ℝ) (↑727 : ℝ)).sqrtTwoAddSeries 0 ≤
    2 - HPow.hPow (β := ℕ) (3.14 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1)) 2
hz₁₃ : LT.lt (α := ℕ) 0 989
hz₁₄ : LT.lt (α := ℕ) 0 727
⊢ 3.14 < π
have hz₁₅ : (HMul.hMul (α := ℕ) 2 989 + 1940) * HPow.hPow (α := ℕ) (β := ℕ) 727 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 1447 2 * 989
Tactic: pi_lower_bound [338 / 239, 704 / 381, 1940 / 989, 1447 / 727]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
pi_lower_bound :
  (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries 4 ≤
    2 - HPow.hPow (β := ℕ) (3.14 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1)) 2
hz :
  (HDiv.hDiv (α := ℝ) (↑338 : ℝ) (↑239 : ℝ)).sqrtTwoAddSeries 3 ≤
    2 - HPow.hPow (β := ℕ) (3.14 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1)) 2
hb : LT.lt (α := ℕ) 0 1
hd : LT.lt (α := ℕ) 0 239
h : (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 239 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 338 2 * 1
hz₁ :
  (HDiv.hDiv (α := ℝ) (↑704 : ℝ) (↑381 : ℝ)).sqrtTwoAddSeries 2 ≤
    2 - HPow.hPow (β := ℕ) (3.14 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1)) 2
hz₂ : LT.lt (α := ℕ) 0 239
hz₃ : LT.lt (α := ℕ) 0 381
hz₄ : (HMul.hMul (α := ℕ) 2 239 + 338) * HPow.hPow (α := ℕ) (β := ℕ) 381 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 704 2 * 239
hb₁ : LT.lt (α := ℕ) 0 1
hd₁ : LT.lt (α := ℕ) 0 239
h₁ : (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 239 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 338 2 * 1
hz₅ :
  (HDiv.hDiv (α := ℝ) (↑1940 : ℝ) (↑989 : ℝ)).sqrtTwoAddSeries 1 ≤
    2 - HPow.hPow (β := ℕ) (3.14 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1)) 2
hz₆ : LT.lt (α := ℕ) 0 381
hz₇ : LT.lt (α := ℕ) 0 989
hz₈ : (HMul.hMul (α := ℕ) 2 381 + 704) * HPow.hPow (α := ℕ) (β := ℕ) 989 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 1940 2 * 381
hz₉ : LT.lt (α := ℕ) 0 239
hz₁₀ : LT.lt (α := ℕ) 0 381
hz₁₁ : (HMul.hMul (α := ℕ) 2 239 + 338) * HPow.hPow (α := ℕ) (β := ℕ) 381 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 704 2 * 239
hb₂ : LT.lt (α := ℕ) 0 1
hd₂ : LT.lt (α := ℕ) 0 239
h₂ : (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 239 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 338 2 * 1
hz₁₂ :
  (HDiv.hDiv (α := ℝ) (↑1447 : ℝ) (↑727 : ℝ)).sqrtTwoAddSeries 0 ≤
    2 - HPow.hPow (β := ℕ) (3.14 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1)) 2
hz₁₃ : LT.lt (α := ℕ) 0 989
hz₁₄ : LT.lt (α := ℕ) 0 727
hz₁₅ : (HMul.hMul (α := ℕ) 2 989 + 1940) * HPow.hPow (α := ℕ) (β := ℕ) 727 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 1447 2 * 989
hz₁₆ : LT.lt (α := ℕ) 0 381
hz₁₇ : LT.lt (α := ℕ) 0 989
hz₁₈ : (HMul.hMul (α := ℕ) 2 381 + 704) * HPow.hPow (α := ℕ) (β := ℕ) 989 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 1940 2 * 381
hz₁₉ : LT.lt (α := ℕ) 0 239
hz₂₀ : LT.lt (α := ℕ) 0 381
hz₂₁ : (HMul.hMul (α := ℕ) 2 239 + 338) * HPow.hPow (α := ℕ) (β := ℕ) 381 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 704 2 * 239
hb₃ : LT.lt (α := ℕ) 0 1
hd₃ : LT.lt (α := ℕ) 0 239
h₃ : (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 239 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 338 2 * 1
⊢ 3.14 < π
have hz₂₂ : HDiv.hDiv (α := ℝ) 1447 727 ≤ 2 - HPow.hPow (β := ℕ) (3.14 / HPow.hPow (α := ℝ) (β := ℕ) 2 5) 2
Tactic: pi_lower_bound [338 / 239, 704 / 381, 1940 / 989, 1447 / 727]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
⊢ π < 3.15
have h : 2 -
    HPow.hPow (β := ℕ) ((3.15 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1))
      2 ≤
  (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries 4
Tactic: pi_upper_bound [41 / 29, 109 / 59, 865 / 441, 412 / 207]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
h :
  2 -
      HPow.hPow (β := ℕ) ((3.15 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1))
        2 ≤
    (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries 4
⊢ π < 3.15
have h₂ : 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4 ≤ 3.15
Tactic: pi_upper_bound [41 / 29, 109 / 59, 865 / 441, 412 / 207]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
h :
  2 -
      HPow.hPow (β := ℕ) ((3.15 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1))
        2 ≤
    (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries 4
h₂ : 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4 ≤ 3.15
⊢ π < 3.15
have h₁ : 2 -
    HPow.hPow (β := ℕ) ((3.15 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1))
      2 ≤
  (HDiv.hDiv (α := ℝ) (↑41 : ℝ) (↑29 : ℝ)).sqrtTwoAddSeries 3
Tactic: pi_upper_bound [41 / 29, 109 / 59, 865 / 441, 412 / 207]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
h :
  2 -
      HPow.hPow (β := ℕ) ((3.15 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1))
        2 ≤
    (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries 4
h₂ : 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4 ≤ 3.15
h₁ :
  2 -
      HPow.hPow (β := ℕ) ((3.15 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1))
        2 ≤
    (HDiv.hDiv (α := ℝ) (↑41 : ℝ) (↑29 : ℝ)).sqrtTwoAddSeries 3
⊢ π < 3.15
have h₃ : LT.lt (α := ℕ) 0 29
Tactic: pi_upper_bound [41 / 29, 109 / 59, 865 / 441, 412 / 207]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
h :
  2 -
      HPow.hPow (β := ℕ) ((3.15 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1))
        2 ≤
    (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries 4
h₂ : 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4 ≤ 3.15
h₁ :
  2 -
      HPow.hPow (β := ℕ) ((3.15 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1))
        2 ≤
    (HDiv.hDiv (α := ℝ) (↑41 : ℝ) (↑29 : ℝ)).sqrtTwoAddSeries 3
h₃ : LT.lt (α := ℕ) 0 29
⊢ π < 3.15
have h₄ : LT.lt (α := ℕ) 0 1
Tactic: pi_upper_bound [41 / 29, 109 / 59, 865 / 441, 412 / 207]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
h :
  2 -
      HPow.hPow (β := ℕ) ((3.15 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1))
        2 ≤
    (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries 4
h₂ : 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4 ≤ 3.15
h₁ :
  2 -
      HPow.hPow (β := ℕ) ((3.15 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1))
        2 ≤
    (HDiv.hDiv (α := ℝ) (↑41 : ℝ) (↑29 : ℝ)).sqrtTwoAddSeries 3
h₃ : LT.lt (α := ℕ) 0 29
h₄ : LT.lt (α := ℕ) 0 1
⊢ π < 3.15
have h₅ : HPow.hPow (α := ℕ) (β := ℕ) 41 2 * 1 ≤ (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 29 2
Tactic: pi_upper_bound [41 / 29, 109 / 59, 865 / 441, 412 / 207]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
h :
  2 -
      HPow.hPow (β := ℕ) ((3.15 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1))
        2 ≤
    (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries 4
h₂ : 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4 ≤ 3.15
h₁ :
  2 -
      HPow.hPow (β := ℕ) ((3.15 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1))
        2 ≤
    (HDiv.hDiv (α := ℝ) (↑41 : ℝ) (↑29 : ℝ)).sqrtTwoAddSeries 3
h₃ : LT.lt (α := ℕ) 0 29
h₄ : LT.lt (α := ℕ) 0 1
h₅ : HPow.hPow (α := ℕ) (β := ℕ) 41 2 * 1 ≤ (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 29 2
h₆ : 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4 ≤ 3.15
⊢ π < 3.15
have h₇ : 2 -
    HPow.hPow (β := ℕ) ((3.15 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1))
      2 ≤
  (HDiv.hDiv (α := ℝ) (↑109 : ℝ) (↑59 : ℝ)).sqrtTwoAddSeries 2
Tactic: pi_upper_bound [41 / 29, 109 / 59, 865 / 441, 412 / 207]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
h :
  2 -
      HPow.hPow (β := ℕ) ((3.15 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1))
        2 ≤
    (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries 4
h₂ : 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4 ≤ 3.15
h₁ :
  2 -
      HPow.hPow (β := ℕ) ((3.15 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1))
        2 ≤
    (HDiv.hDiv (α := ℝ) (↑41 : ℝ) (↑29 : ℝ)).sqrtTwoAddSeries 3
h₃ : LT.lt (α := ℕ) 0 29
h₄ : LT.lt (α := ℕ) 0 1
h₅ : HPow.hPow (α := ℕ) (β := ℕ) 41 2 * 1 ≤ (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 29 2
h₆ : 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4 ≤ 3.15
h₇ :
  2 -
      HPow.hPow (β := ℕ) ((3.15 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1))
        2 ≤
    (HDiv.hDiv (α := ℝ) (↑109 : ℝ) (↑59 : ℝ)).sqrtTwoAddSeries 2
⊢ π < 3.15
have h₈ : LT.lt (α := ℕ) 0 59
Tactic: pi_upper_bound [41 / 29, 109 / 59, 865 / 441, 412 / 207]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
h :
  2 -
      HPow.hPow (β := ℕ) ((3.15 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1))
        2 ≤
    (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries 4
h₂ : 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4 ≤ 3.15
h₁ :
  2 -
      HPow.hPow (β := ℕ) ((3.15 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1))
        2 ≤
    (HDiv.hDiv (α := ℝ) (↑41 : ℝ) (↑29 : ℝ)).sqrtTwoAddSeries 3
h₃ : LT.lt (α := ℕ) 0 29
h₄ : LT.lt (α := ℕ) 0 1
h₅ : HPow.hPow (α := ℕ) (β := ℕ) 41 2 * 1 ≤ (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 29 2
h₆ : 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4 ≤ 3.15
h₇ :
  2 -
      HPow.hPow (β := ℕ) ((3.15 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1))
        2 ≤
    (HDiv.hDiv (α := ℝ) (↑109 : ℝ) (↑59 : ℝ)).sqrtTwoAddSeries 2
h₈ : LT.lt (α := ℕ) 0 59
h₉ : LT.lt (α := ℕ) 0 29
⊢ π < 3.15
have h₁₀ : HPow.hPow (α := ℕ) (β := ℕ) 109 2 * 29 ≤ (HMul.hMul (α := ℕ) 2 29 + 41) * HPow.hPow (α := ℕ) (β := ℕ) 59 2
Tactic: pi_upper_bound [41 / 29, 109 / 59, 865 / 441, 412 / 207]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
h :
  2 -
      HPow.hPow (β := ℕ) ((3.15 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1))
        2 ≤
    (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries 4
h₂ : 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4 ≤ 3.15
h₁ :
  2 -
      HPow.hPow (β := ℕ) ((3.15 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1))
        2 ≤
    (HDiv.hDiv (α := ℝ) (↑41 : ℝ) (↑29 : ℝ)).sqrtTwoAddSeries 3
h₃ : LT.lt (α := ℕ) 0 29
h₄ : LT.lt (α := ℕ) 0 1
h₅ : HPow.hPow (α := ℕ) (β := ℕ) 41 2 * 1 ≤ (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 29 2
h₆ : 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4 ≤ 3.15
h₇ :
  2 -
      HPow.hPow (β := ℕ) ((3.15 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1))
        2 ≤
    (HDiv.hDiv (α := ℝ) (↑109 : ℝ) (↑59 : ℝ)).sqrtTwoAddSeries 2
h₈ : LT.lt (α := ℕ) 0 59
h₉ : LT.lt (α := ℕ) 0 29
h₁₀ : HPow.hPow (α := ℕ) (β := ℕ) 109 2 * 29 ≤ (HMul.hMul (α := ℕ) 2 29 + 41) * HPow.hPow (α := ℕ) (β := ℕ) 59 2
h₁₁ : LT.lt (α := ℕ) 0 29
h₁₂ : LT.lt (α := ℕ) 0 1
h₁₃ : HPow.hPow (α := ℕ) (β := ℕ) 41 2 * 1 ≤ (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 29 2
h₁₄ : 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4 ≤ 3.15
⊢ π < 3.15
have h₁₅ : 2 -
    HPow.hPow (β := ℕ) ((3.15 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1))
      2 ≤
  (HDiv.hDiv (α := ℝ) (↑865 : ℝ) (↑441 : ℝ)).sqrtTwoAddSeries 1
Tactic: pi_upper_bound [41 / 29, 109 / 59, 865 / 441, 412 / 207]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
h :
  2 -
      HPow.hPow (β := ℕ) ((3.15 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1))
        2 ≤
    (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries 4
h₂ : 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4 ≤ 3.15
h₁ :
  2 -
      HPow.hPow (β := ℕ) ((3.15 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1))
        2 ≤
    (HDiv.hDiv (α := ℝ) (↑41 : ℝ) (↑29 : ℝ)).sqrtTwoAddSeries 3
h₃ : LT.lt (α := ℕ) 0 29
h₄ : LT.lt (α := ℕ) 0 1
h₅ : HPow.hPow (α := ℕ) (β := ℕ) 41 2 * 1 ≤ (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 29 2
h₆ : 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4 ≤ 3.15
h₇ :
  2 -
      HPow.hPow (β := ℕ) ((3.15 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1))
        2 ≤
    (HDiv.hDiv (α := ℝ) (↑109 : ℝ) (↑59 : ℝ)).sqrtTwoAddSeries 2
h₈ : LT.lt (α := ℕ) 0 59
h₉ : LT.lt (α := ℕ) 0 29
h₁₀ : HPow.hPow (α := ℕ) (β := ℕ) 109 2 * 29 ≤ (HMul.hMul (α := ℕ) 2 29 + 41) * HPow.hPow (α := ℕ) (β := ℕ) 59 2
h₁₁ : LT.lt (α := ℕ) 0 29
h₁₂ : LT.lt (α := ℕ) 0 1
h₁₃ : HPow.hPow (α := ℕ) (β := ℕ) 41 2 * 1 ≤ (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 29 2
h₁₄ : 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4 ≤ 3.15
h₁₅ :
  2 -
      HPow.hPow (β := ℕ) ((3.15 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1))
        2 ≤
    (HDiv.hDiv (α := ℝ) (↑865 : ℝ) (↑441 : ℝ)).sqrtTwoAddSeries 1
⊢ π < 3.15
have h₁₆ : LT.lt (α := ℕ) 0 441
Tactic: pi_upper_bound [41 / 29, 109 / 59, 865 / 441, 412 / 207]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
h :
  2 -
      HPow.hPow (β := ℕ) ((3.15 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1))
        2 ≤
    (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries 4
h₂ : 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4 ≤ 3.15
h₁ :
  2 -
      HPow.hPow (β := ℕ) ((3.15 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1))
        2 ≤
    (HDiv.hDiv (α := ℝ) (↑41 : ℝ) (↑29 : ℝ)).sqrtTwoAddSeries 3
h₃ : LT.lt (α := ℕ) 0 29
h₄ : LT.lt (α := ℕ) 0 1
h₅ : HPow.hPow (α := ℕ) (β := ℕ) 41 2 * 1 ≤ (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 29 2
h₆ : 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4 ≤ 3.15
h₇ :
  2 -
      HPow.hPow (β := ℕ) ((3.15 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1))
        2 ≤
    (HDiv.hDiv (α := ℝ) (↑109 : ℝ) (↑59 : ℝ)).sqrtTwoAddSeries 2
h₈ : LT.lt (α := ℕ) 0 59
h₉ : LT.lt (α := ℕ) 0 29
h₁₀ : HPow.hPow (α := ℕ) (β := ℕ) 109 2 * 29 ≤ (HMul.hMul (α := ℕ) 2 29 + 41) * HPow.hPow (α := ℕ) (β := ℕ) 59 2
h₁₁ : LT.lt (α := ℕ) 0 29
h₁₂ : LT.lt (α := ℕ) 0 1
h₁₃ : HPow.hPow (α := ℕ) (β := ℕ) 41 2 * 1 ≤ (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 29 2
h₁₄ : 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4 ≤ 3.15
h₁₅ :
  2 -
      HPow.hPow (β := ℕ) ((3.15 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1))
        2 ≤
    (HDiv.hDiv (α := ℝ) (↑865 : ℝ) (↑441 : ℝ)).sqrtTwoAddSeries 1
h₁₆ : LT.lt (α := ℕ) 0 441
h₁₇ : LT.lt (α := ℕ) 0 59
⊢ π < 3.15
have h₁₈ : HPow.hPow (α := ℕ) (β := ℕ) 865 2 * 59 ≤ (HMul.hMul (α := ℕ) 2 59 + 109) * HPow.hPow (α := ℕ) (β := ℕ) 441 2
Tactic: pi_upper_bound [41 / 29, 109 / 59, 865 / 441, 412 / 207]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
h :
  2 -
      HPow.hPow (β := ℕ) ((3.15 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1))
        2 ≤
    (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries 4
h₂ : 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4 ≤ 3.15
h₁ :
  2 -
      HPow.hPow (β := ℕ) ((3.15 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1))
        2 ≤
    (HDiv.hDiv (α := ℝ) (↑41 : ℝ) (↑29 : ℝ)).sqrtTwoAddSeries 3
h₃ : LT.lt (α := ℕ) 0 29
h₄ : LT.lt (α := ℕ) 0 1
h₅ : HPow.hPow (α := ℕ) (β := ℕ) 41 2 * 1 ≤ (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 29 2
h₆ : 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4 ≤ 3.15
h₇ :
  2 -
      HPow.hPow (β := ℕ) ((3.15 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1))
        2 ≤
    (HDiv.hDiv (α := ℝ) (↑109 : ℝ) (↑59 : ℝ)).sqrtTwoAddSeries 2
h₈ : LT.lt (α := ℕ) 0 59
h₉ : LT.lt (α := ℕ) 0 29
h₁₀ : HPow.hPow (α := ℕ) (β := ℕ) 109 2 * 29 ≤ (HMul.hMul (α := ℕ) 2 29 + 41) * HPow.hPow (α := ℕ) (β := ℕ) 59 2
h₁₁ : LT.lt (α := ℕ) 0 29
h₁₂ : LT.lt (α := ℕ) 0 1
h₁₃ : HPow.hPow (α := ℕ) (β := ℕ) 41 2 * 1 ≤ (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 29 2
h₁₄ : 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4 ≤ 3.15
h₁₅ :
  2 -
      HPow.hPow (β := ℕ) ((3.15 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1))
        2 ≤
    (HDiv.hDiv (α := ℝ) (↑865 : ℝ) (↑441 : ℝ)).sqrtTwoAddSeries 1
h₁₆ : LT.lt (α := ℕ) 0 441
h₁₇ : LT.lt (α := ℕ) 0 59
h₁₈ : HPow.hPow (α := ℕ) (β := ℕ) 865 2 * 59 ≤ (HMul.hMul (α := ℕ) 2 59 + 109) * HPow.hPow (α := ℕ) (β := ℕ) 441 2
h₁₉ : LT.lt (α := ℕ) 0 59
h₂₀ : LT.lt (α := ℕ) 0 29
h₂₁ : HPow.hPow (α := ℕ) (β := ℕ) 109 2 * 29 ≤ (HMul.hMul (α := ℕ) 2 29 + 41) * HPow.hPow (α := ℕ) (β := ℕ) 59 2
h₂₂ : LT.lt (α := ℕ) 0 29
h₂₃ : LT.lt (α := ℕ) 0 1
h₂₄ : HPow.hPow (α := ℕ) (β := ℕ) 41 2 * 1 ≤ (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 29 2
h₂₅ : 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4 ≤ 3.15
⊢ π < 3.15
have h₂₆ : 2 -
    HPow.hPow (β := ℕ) ((3.15 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1))
      2 ≤
  (HDiv.hDiv (α := ℝ) (↑412 : ℝ) (↑207 : ℝ)).sqrtTwoAddSeries 0
Tactic: pi_upper_bound [41 / 29, 109 / 59, 865 / 441, 412 / 207]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
h :
  2 -
      HPow.hPow (β := ℕ) ((3.15 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1))
        2 ≤
    (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries 4
h₂ : 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4 ≤ 3.15
h₁ :
  2 -
      HPow.hPow (β := ℕ) ((3.15 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1))
        2 ≤
    (HDiv.hDiv (α := ℝ) (↑41 : ℝ) (↑29 : ℝ)).sqrtTwoAddSeries 3
h₃ : LT.lt (α := ℕ) 0 29
h₄ : LT.lt (α := ℕ) 0 1
h₅ : HPow.hPow (α := ℕ) (β := ℕ) 41 2 * 1 ≤ (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 29 2
h₆ : 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4 ≤ 3.15
h₇ :
  2 -
      HPow.hPow (β := ℕ) ((3.15 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1))
        2 ≤
    (HDiv.hDiv (α := ℝ) (↑109 : ℝ) (↑59 : ℝ)).sqrtTwoAddSeries 2
h₈ : LT.lt (α := ℕ) 0 59
h₉ : LT.lt (α := ℕ) 0 29
h₁₀ : HPow.hPow (α := ℕ) (β := ℕ) 109 2 * 29 ≤ (HMul.hMul (α := ℕ) 2 29 + 41) * HPow.hPow (α := ℕ) (β := ℕ) 59 2
h₁₁ : LT.lt (α := ℕ) 0 29
h₁₂ : LT.lt (α := ℕ) 0 1
h₁₃ : HPow.hPow (α := ℕ) (β := ℕ) 41 2 * 1 ≤ (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 29 2
h₁₄ : 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4 ≤ 3.15
h₁₅ :
  2 -
      HPow.hPow (β := ℕ) ((3.15 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1))
        2 ≤
    (HDiv.hDiv (α := ℝ) (↑865 : ℝ) (↑441 : ℝ)).sqrtTwoAddSeries 1
h₁₆ : LT.lt (α := ℕ) 0 441
h₁₇ : LT.lt (α := ℕ) 0 59
h₁₈ : HPow.hPow (α := ℕ) (β := ℕ) 865 2 * 59 ≤ (HMul.hMul (α := ℕ) 2 59 + 109) * HPow.hPow (α := ℕ) (β := ℕ) 441 2
h₁₉ : LT.lt (α := ℕ) 0 59
h₂₀ : LT.lt (α := ℕ) 0 29
h₂₁ : HPow.hPow (α := ℕ) (β := ℕ) 109 2 * 29 ≤ (HMul.hMul (α := ℕ) 2 29 + 41) * HPow.hPow (α := ℕ) (β := ℕ) 59 2
h₂₂ : LT.lt (α := ℕ) 0 29
h₂₃ : LT.lt (α := ℕ) 0 1
h₂₄ : HPow.hPow (α := ℕ) (β := ℕ) 41 2 * 1 ≤ (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 29 2
h₂₅ : 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4 ≤ 3.15
h₂₆ :
  2 -
      HPow.hPow (β := ℕ) ((3.15 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1))
        2 ≤
    (HDiv.hDiv (α := ℝ) (↑412 : ℝ) (↑207 : ℝ)).sqrtTwoAddSeries 0
⊢ π < 3.15
have h₂₇ : LT.lt (α := ℕ) 0 207
Tactic: pi_upper_bound [41 / 29, 109 / 59, 865 / 441, 412 / 207]