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 10 ≤
    2 - HPow.hPow (β := ℕ) (3.141592 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 10 1)) 2
hz :
  (HDiv.hDiv (α := ℝ) (↑11482 : ℝ) (↑8119 : ℝ)).sqrtTwoAddSeries 9 ≤
    2 - HPow.hPow (β := ℕ) (3.141592 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 10 1)) 2
hb : LT.lt (α := ℕ) 0 1
hd : LT.lt (α := ℕ) 0 8119
h : (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 8119 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 11482 2 * 1
hz₁ :
  (HDiv.hDiv (α := ℝ) (↑7792 : ℝ) (↑4217 : ℝ)).sqrtTwoAddSeries 8 ≤
    2 - HPow.hPow (β := ℕ) (3.141592 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 10 1)) 2
hz₂ : LT.lt (α := ℕ) 0 8119
hz₃ : LT.lt (α := ℕ) 0 4217
hz₄ :
  (HMul.hMul (α := ℕ) 2 8119 + 11482) * HPow.hPow (α := ℕ) (β := ℕ) 4217 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 7792 2 * 8119
hb₁ : LT.lt (α := ℕ) 0 1
hd₁ : LT.lt (α := ℕ) 0 8119
h₁ : (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 8119 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 11482 2 * 1
hz₅ :
  (HDiv.hDiv (α := ℝ) (↑54055 : ℝ) (↑27557 : ℝ)).sqrtTwoAddSeries 7 ≤
    2 - HPow.hPow (β := ℕ) (3.141592 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 10 1)) 2
hz₆ : LT.lt (α := ℕ) 0 4217
hz₇ : LT.lt (α := ℕ) 0 27557
hz₈ :
  (HMul.hMul (α := ℕ) 2 4217 + 7792) * HPow.hPow (α := ℕ) (β := ℕ) 27557 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 54055 2 * 4217
hz₉ : LT.lt (α := ℕ) 0 8119
hz₁₀ : LT.lt (α := ℕ) 0 4217
hz₁₁ :
  (HMul.hMul (α := ℕ) 2 8119 + 11482) * HPow.hPow (α := ℕ) (β := ℕ) 4217 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 7792 2 * 8119
hb₂ : LT.lt (α := ℕ) 0 1
hd₂ : LT.lt (α := ℕ) 0 8119
h₂ : (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 8119 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 11482 2 * 1
hz₁₂ :
  (HDiv.hDiv (α := ℝ) (↑128757 : ℝ) (↑64690 : ℝ)).sqrtTwoAddSeries 6 ≤
    2 - HPow.hPow (β := ℕ) (3.141592 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 10 1)) 2
hz₁₃ : LT.lt (α := ℕ) 0 27557
hz₁₄ : LT.lt (α := ℕ) 0 64690
hz₁₅ :
  (HMul.hMul (α := ℕ) 2 27557 + 54055) * HPow.hPow (α := ℕ) (β := ℕ) 64690 2 ≤
    HPow.hPow (α := ℕ) (β := ℕ) 128757 2 * 27557
hz₁₆ : LT.lt (α := ℕ) 0 4217
hz₁₇ : LT.lt (α := ℕ) 0 27557
hz₁₈ :
  (HMul.hMul (α := ℕ) 2 4217 + 7792) * HPow.hPow (α := ℕ) (β := ℕ) 27557 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 54055 2 * 4217
hz₁₉ : LT.lt (α := ℕ) 0 8119
hz₂₀ : LT.lt (α := ℕ) 0 4217
hz₂₁ :
  (HMul.hMul (α := ℕ) 2 8119 + 11482) * HPow.hPow (α := ℕ) (β := ℕ) 4217 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 7792 2 * 8119
hb₃ : LT.lt (α := ℕ) 0 1
hd₃ : LT.lt (α := ℕ) 0 8119
h₃ : (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 8119 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 11482 2 * 1
hz₂₂ :
  (HDiv.hDiv (α := ℝ) (↑279437 : ℝ) (↑139887 : ℝ)).sqrtTwoAddSeries 5 ≤
    2 - HPow.hPow (β := ℕ) (3.141592 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 10 1)) 2
hz₂₃ : LT.lt (α := ℕ) 0 64690
⊢ 3.141592 < π
have hz₂₄ : LT.lt (α := ℕ) 0 139887
Tactic: pi_lower_bound [
    11482/8119, 7792/4217, 54055/27557, 2-623/64690, 2-337/139887, 2-208/345307, 2-167/1108925,
    2-64/1699893, 2-31/3293535, 2-48/20398657]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
⊢ π < 3.141593
have h : 2 -
    HPow.hPow (β := ℕ)
      ((3.141593 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 11) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 11 1)) 2 ≤
  (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries 11
Tactic: pi_upper_bound [
    35839/25342, 49143/26596, 145729/74292, 294095/147759, 2-137/56868, 2-471/781921, 2-153/1015961,
    2-157/4170049, 2-28/2974805, 2-9/3824747, 2-7/11899211]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
h :
  2 -
      HPow.hPow (β := ℕ)
        ((3.141593 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 11) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 11 1)) 2 ≤
    (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries 11
⊢ π < 3.141593
have h₂ : 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 11 ≤ 3.141593
Tactic: pi_upper_bound [
    35839/25342, 49143/26596, 145729/74292, 294095/147759, 2-137/56868, 2-471/781921, 2-153/1015961,
    2-157/4170049, 2-28/2974805, 2-9/3824747, 2-7/11899211]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
h :
  2 -
      HPow.hPow (β := ℕ)
        ((3.141593 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 11) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 11 1)) 2 ≤
    (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries 11
h₂ : 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 11 ≤ 3.141593
⊢ π < 3.141593
have h₁ : 2 -
    HPow.hPow (β := ℕ)
      ((3.141593 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 11) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 11 1)) 2 ≤
  (HDiv.hDiv (α := ℝ) (↑35839 : ℝ) (↑25342 : ℝ)).sqrtTwoAddSeries 10
Tactic: pi_upper_bound [
    35839/25342, 49143/26596, 145729/74292, 294095/147759, 2-137/56868, 2-471/781921, 2-153/1015961,
    2-157/4170049, 2-28/2974805, 2-9/3824747, 2-7/11899211]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
h :
  2 -
      HPow.hPow (β := ℕ)
        ((3.141593 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 11) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 11 1)) 2 ≤
    (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries 11
h₂ : 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 11 ≤ 3.141593
h₁ :
  2 -
      HPow.hPow (β := ℕ)
        ((3.141593 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 11) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 11 1)) 2 ≤
    (HDiv.hDiv (α := ℝ) (↑35839 : ℝ) (↑25342 : ℝ)).sqrtTwoAddSeries 10
⊢ π < 3.141593
have h₃ : LT.lt (α := ℕ) 0 25342
Tactic: pi_upper_bound [
    35839/25342, 49143/26596, 145729/74292, 294095/147759, 2-137/56868, 2-471/781921, 2-153/1015961,
    2-157/4170049, 2-28/2974805, 2-9/3824747, 2-7/11899211]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
h :
  2 -
      HPow.hPow (β := ℕ)
        ((3.141593 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 11) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 11 1)) 2 ≤
    (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries 11
h₂ : 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 11 ≤ 3.141593
h₁ :
  2 -
      HPow.hPow (β := ℕ)
        ((3.141593 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 11) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 11 1)) 2 ≤
    (HDiv.hDiv (α := ℝ) (↑35839 : ℝ) (↑25342 : ℝ)).sqrtTwoAddSeries 10
h₃ : LT.lt (α := ℕ) 0 25342
⊢ π < 3.141593
have h₄ : LT.lt (α := ℕ) 0 1
Tactic: pi_upper_bound [
    35839/25342, 49143/26596, 145729/74292, 294095/147759, 2-137/56868, 2-471/781921, 2-153/1015961,
    2-157/4170049, 2-28/2974805, 2-9/3824747, 2-7/11899211]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
h :
  2 -
      HPow.hPow (β := ℕ)
        ((3.141593 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 11) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 11 1)) 2 ≤
    (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries 11
h₂ : 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 11 ≤ 3.141593
h₁ :
  2 -
      HPow.hPow (β := ℕ)
        ((3.141593 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 11) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 11 1)) 2 ≤
    (HDiv.hDiv (α := ℝ) (↑35839 : ℝ) (↑25342 : ℝ)).sqrtTwoAddSeries 10
h₃ : LT.lt (α := ℕ) 0 25342
h₄ : LT.lt (α := ℕ) 0 1
⊢ π < 3.141593
have h₅ : HPow.hPow (α := ℕ) (β := ℕ) 35839 2 * 1 ≤ (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 25342 2
Tactic: pi_upper_bound [
    35839/25342, 49143/26596, 145729/74292, 294095/147759, 2-137/56868, 2-471/781921, 2-153/1015961,
    2-157/4170049, 2-28/2974805, 2-9/3824747, 2-7/11899211]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
h :
  2 -
      HPow.hPow (β := ℕ)
        ((3.141593 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 11) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 11 1)) 2 ≤
    (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries 11
h₂ : 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 11 ≤ 3.141593
h₁ :
  2 -
      HPow.hPow (β := ℕ)
        ((3.141593 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 11) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 11 1)) 2 ≤
    (HDiv.hDiv (α := ℝ) (↑35839 : ℝ) (↑25342 : ℝ)).sqrtTwoAddSeries 10
h₃ : LT.lt (α := ℕ) 0 25342
h₄ : LT.lt (α := ℕ) 0 1
h₅ : HPow.hPow (α := ℕ) (β := ℕ) 35839 2 * 1 ≤ (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 25342 2
h₆ : 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 11 ≤ 3.141593
⊢ π < 3.141593
have h₇ : 2 -
    HPow.hPow (β := ℕ)
      ((3.141593 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 11) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 11 1)) 2 ≤
  (HDiv.hDiv (α := ℝ) (↑49143 : ℝ) (↑26596 : ℝ)).sqrtTwoAddSeries 9
Tactic: pi_upper_bound [
    35839/25342, 49143/26596, 145729/74292, 294095/147759, 2-137/56868, 2-471/781921, 2-153/1015961,
    2-157/4170049, 2-28/2974805, 2-9/3824747, 2-7/11899211]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
h :
  2 -
      HPow.hPow (β := ℕ)
        ((3.141593 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 11) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 11 1)) 2 ≤
    (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries 11
h₂ : 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 11 ≤ 3.141593
h₁ :
  2 -
      HPow.hPow (β := ℕ)
        ((3.141593 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 11) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 11 1)) 2 ≤
    (HDiv.hDiv (α := ℝ) (↑35839 : ℝ) (↑25342 : ℝ)).sqrtTwoAddSeries 10
h₃ : LT.lt (α := ℕ) 0 25342
h₄ : LT.lt (α := ℕ) 0 1
h₅ : HPow.hPow (α := ℕ) (β := ℕ) 35839 2 * 1 ≤ (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 25342 2
h₆ : 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 11 ≤ 3.141593
h₇ :
  2 -
      HPow.hPow (β := ℕ)
        ((3.141593 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 11) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 11 1)) 2 ≤
    (HDiv.hDiv (α := ℝ) (↑49143 : ℝ) (↑26596 : ℝ)).sqrtTwoAddSeries 9
⊢ π < 3.141593
have h₈ : LT.lt (α := ℕ) 0 26596
Tactic: pi_upper_bound [
    35839/25342, 49143/26596, 145729/74292, 294095/147759, 2-137/56868, 2-471/781921, 2-153/1015961,
    2-157/4170049, 2-28/2974805, 2-9/3824747, 2-7/11899211]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
h :
  2 -
      HPow.hPow (β := ℕ)
        ((3.141593 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 11) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 11 1)) 2 ≤
    (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries 11
h₂ : 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 11 ≤ 3.141593
h₁ :
  2 -
      HPow.hPow (β := ℕ)
        ((3.141593 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 11) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 11 1)) 2 ≤
    (HDiv.hDiv (α := ℝ) (↑35839 : ℝ) (↑25342 : ℝ)).sqrtTwoAddSeries 10
h₃ : LT.lt (α := ℕ) 0 25342
h₄ : LT.lt (α := ℕ) 0 1
h₅ : HPow.hPow (α := ℕ) (β := ℕ) 35839 2 * 1 ≤ (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 25342 2
h₆ : 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 11 ≤ 3.141593
h₇ :
  2 -
      HPow.hPow (β := ℕ)
        ((3.141593 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 11) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 11 1)) 2 ≤
    (HDiv.hDiv (α := ℝ) (↑49143 : ℝ) (↑26596 : ℝ)).sqrtTwoAddSeries 9
h₈ : LT.lt (α := ℕ) 0 26596
h₉ : LT.lt (α := ℕ) 0 25342
⊢ π < 3.141593
have h₁₀ : HPow.hPow (α := ℕ) (β := ℕ) 49143 2 * 25342 ≤ (HMul.hMul (α := ℕ) 2 25342 + 35839) * HPow.hPow (α := ℕ) (β := ℕ) 26596 2
Tactic: pi_upper_bound [
    35839/25342, 49143/26596, 145729/74292, 294095/147759, 2-137/56868, 2-471/781921, 2-153/1015961,
    2-157/4170049, 2-28/2974805, 2-9/3824747, 2-7/11899211]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
h :
  2 -
      HPow.hPow (β := ℕ)
        ((3.141593 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 11) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 11 1)) 2 ≤
    (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries 11
h₂ : 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 11 ≤ 3.141593
h₁ :
  2 -
      HPow.hPow (β := ℕ)
        ((3.141593 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 11) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 11 1)) 2 ≤
    (HDiv.hDiv (α := ℝ) (↑35839 : ℝ) (↑25342 : ℝ)).sqrtTwoAddSeries 10
h₃ : LT.lt (α := ℕ) 0 25342
h₄ : LT.lt (α := ℕ) 0 1
h₅ : HPow.hPow (α := ℕ) (β := ℕ) 35839 2 * 1 ≤ (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 25342 2
h₆ : 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 11 ≤ 3.141593
h₇ :
  2 -
      HPow.hPow (β := ℕ)
        ((3.141593 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 11) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 11 1)) 2 ≤
    (HDiv.hDiv (α := ℝ) (↑49143 : ℝ) (↑26596 : ℝ)).sqrtTwoAddSeries 9
h₈ : LT.lt (α := ℕ) 0 26596
h₉ : LT.lt (α := ℕ) 0 25342
h₁₀ :
  HPow.hPow (α := ℕ) (β := ℕ) 49143 2 * 25342 ≤
    (HMul.hMul (α := ℕ) 2 25342 + 35839) * HPow.hPow (α := ℕ) (β := ℕ) 26596 2
h₁₁ : LT.lt (α := ℕ) 0 25342
h₁₂ : LT.lt (α := ℕ) 0 1
h₁₃ : HPow.hPow (α := ℕ) (β := ℕ) 35839 2 * 1 ≤ (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 25342 2
h₁₄ : 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 11 ≤ 3.141593
⊢ π < 3.141593
have h₁₅ : 2 -
    HPow.hPow (β := ℕ)
      ((3.141593 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 11) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 11 1)) 2 ≤
  (HDiv.hDiv (α := ℝ) (↑145729 : ℝ) (↑74292 : ℝ)).sqrtTwoAddSeries 8
Tactic: pi_upper_bound [
    35839/25342, 49143/26596, 145729/74292, 294095/147759, 2-137/56868, 2-471/781921, 2-153/1015961,
    2-157/4170049, 2-28/2974805, 2-9/3824747, 2-7/11899211]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
h :
  2 -
      HPow.hPow (β := ℕ)
        ((3.141593 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 11) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 11 1)) 2 ≤
    (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries 11
h₂ : 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 11 ≤ 3.141593
h₁ :
  2 -
      HPow.hPow (β := ℕ)
        ((3.141593 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 11) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 11 1)) 2 ≤
    (HDiv.hDiv (α := ℝ) (↑35839 : ℝ) (↑25342 : ℝ)).sqrtTwoAddSeries 10
h₃ : LT.lt (α := ℕ) 0 25342
h₄ : LT.lt (α := ℕ) 0 1
h₅ : HPow.hPow (α := ℕ) (β := ℕ) 35839 2 * 1 ≤ (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 25342 2
h₆ : 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 11 ≤ 3.141593
h₇ :
  2 -
      HPow.hPow (β := ℕ)
        ((3.141593 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 11) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 11 1)) 2 ≤
    (HDiv.hDiv (α := ℝ) (↑49143 : ℝ) (↑26596 : ℝ)).sqrtTwoAddSeries 9
h₈ : LT.lt (α := ℕ) 0 26596
h₉ : LT.lt (α := ℕ) 0 25342
h₁₀ :
  HPow.hPow (α := ℕ) (β := ℕ) 49143 2 * 25342 ≤
    (HMul.hMul (α := ℕ) 2 25342 + 35839) * HPow.hPow (α := ℕ) (β := ℕ) 26596 2
h₁₁ : LT.lt (α := ℕ) 0 25342
h₁₂ : LT.lt (α := ℕ) 0 1
h₁₃ : HPow.hPow (α := ℕ) (β := ℕ) 35839 2 * 1 ≤ (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 25342 2
h₁₄ : 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 11 ≤ 3.141593
h₁₅ :
  2 -
      HPow.hPow (β := ℕ)
        ((3.141593 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 11) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 11 1)) 2 ≤
    (HDiv.hDiv (α := ℝ) (↑145729 : ℝ) (↑74292 : ℝ)).sqrtTwoAddSeries 8
⊢ π < 3.141593
have h₁₆ : LT.lt (α := ℕ) 0 74292
Tactic: pi_upper_bound [
    35839/25342, 49143/26596, 145729/74292, 294095/147759, 2-137/56868, 2-471/781921, 2-153/1015961,
    2-157/4170049, 2-28/2974805, 2-9/3824747, 2-7/11899211]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
h :
  2 -
      HPow.hPow (β := ℕ)
        ((3.141593 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 11) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 11 1)) 2 ≤
    (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries 11
h₂ : 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 11 ≤ 3.141593
h₁ :
  2 -
      HPow.hPow (β := ℕ)
        ((3.141593 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 11) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 11 1)) 2 ≤
    (HDiv.hDiv (α := ℝ) (↑35839 : ℝ) (↑25342 : ℝ)).sqrtTwoAddSeries 10
h₃ : LT.lt (α := ℕ) 0 25342
h₄ : LT.lt (α := ℕ) 0 1
h₅ : HPow.hPow (α := ℕ) (β := ℕ) 35839 2 * 1 ≤ (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 25342 2
h₆ : 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 11 ≤ 3.141593
h₇ :
  2 -
      HPow.hPow (β := ℕ)
        ((3.141593 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 11) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 11 1)) 2 ≤
    (HDiv.hDiv (α := ℝ) (↑49143 : ℝ) (↑26596 : ℝ)).sqrtTwoAddSeries 9
h₈ : LT.lt (α := ℕ) 0 26596
h₉ : LT.lt (α := ℕ) 0 25342
h₁₀ :
  HPow.hPow (α := ℕ) (β := ℕ) 49143 2 * 25342 ≤
    (HMul.hMul (α := ℕ) 2 25342 + 35839) * HPow.hPow (α := ℕ) (β := ℕ) 26596 2
h₁₁ : LT.lt (α := ℕ) 0 25342
h₁₂ : LT.lt (α := ℕ) 0 1
h₁₃ : HPow.hPow (α := ℕ) (β := ℕ) 35839 2 * 1 ≤ (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 25342 2
h₁₄ : 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 11 ≤ 3.141593
h₁₅ :
  2 -
      HPow.hPow (β := ℕ)
        ((3.141593 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 11) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 11 1)) 2 ≤
    (HDiv.hDiv (α := ℝ) (↑145729 : ℝ) (↑74292 : ℝ)).sqrtTwoAddSeries 8
h₁₆ : LT.lt (α := ℕ) 0 74292
h₁₇ : LT.lt (α := ℕ) 0 26596
⊢ π < 3.141593
have h₁₈ : HPow.hPow (α := ℕ) (β := ℕ) 145729 2 * 26596 ≤
  (HMul.hMul (α := ℕ) 2 26596 + 49143) * HPow.hPow (α := ℕ) (β := ℕ) 74292 2
Tactic: pi_upper_bound [
    35839/25342, 49143/26596, 145729/74292, 294095/147759, 2-137/56868, 2-471/781921, 2-153/1015961,
    2-157/4170049, 2-28/2974805, 2-9/3824747, 2-7/11899211]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
h :
  2 -
      HPow.hPow (β := ℕ)
        ((3.141593 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 11) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 11 1)) 2 ≤
    (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries 11
h₂ : 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 11 ≤ 3.141593
h₁ :
  2 -
      HPow.hPow (β := ℕ)
        ((3.141593 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 11) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 11 1)) 2 ≤
    (HDiv.hDiv (α := ℝ) (↑35839 : ℝ) (↑25342 : ℝ)).sqrtTwoAddSeries 10
h₃ : LT.lt (α := ℕ) 0 25342
h₄ : LT.lt (α := ℕ) 0 1
h₅ : HPow.hPow (α := ℕ) (β := ℕ) 35839 2 * 1 ≤ (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 25342 2
h₆ : 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 11 ≤ 3.141593
h₇ :
  2 -
      HPow.hPow (β := ℕ)
        ((3.141593 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 11) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 11 1)) 2 ≤
    (HDiv.hDiv (α := ℝ) (↑49143 : ℝ) (↑26596 : ℝ)).sqrtTwoAddSeries 9
h₈ : LT.lt (α := ℕ) 0 26596
h₉ : LT.lt (α := ℕ) 0 25342
h₁₀ :
  HPow.hPow (α := ℕ) (β := ℕ) 49143 2 * 25342 ≤
    (HMul.hMul (α := ℕ) 2 25342 + 35839) * HPow.hPow (α := ℕ) (β := ℕ) 26596 2
h₁₁ : LT.lt (α := ℕ) 0 25342
h₁₂ : LT.lt (α := ℕ) 0 1
h₁₃ : HPow.hPow (α := ℕ) (β := ℕ) 35839 2 * 1 ≤ (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 25342 2
h₁₄ : 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 11 ≤ 3.141593
h₁₅ :
  2 -
      HPow.hPow (β := ℕ)
        ((3.141593 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 11) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 11 1)) 2 ≤
    (HDiv.hDiv (α := ℝ) (↑145729 : ℝ) (↑74292 : ℝ)).sqrtTwoAddSeries 8
h₁₆ : LT.lt (α := ℕ) 0 74292
h₁₇ : LT.lt (α := ℕ) 0 26596
h₁₈ :
  HPow.hPow (α := ℕ) (β := ℕ) 145729 2 * 26596 ≤
    (HMul.hMul (α := ℕ) 2 26596 + 49143) * HPow.hPow (α := ℕ) (β := ℕ) 74292 2
h₁₉ : LT.lt (α := ℕ) 0 26596
h₂₀ : LT.lt (α := ℕ) 0 25342
h₂₁ :
  HPow.hPow (α := ℕ) (β := ℕ) 49143 2 * 25342 ≤
    (HMul.hMul (α := ℕ) 2 25342 + 35839) * HPow.hPow (α := ℕ) (β := ℕ) 26596 2
h₂₂ : LT.lt (α := ℕ) 0 25342
h₂₃ : LT.lt (α := ℕ) 0 1
h₂₄ : HPow.hPow (α := ℕ) (β := ℕ) 35839 2 * 1 ≤ (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 25342 2
h₂₅ : 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 11 ≤ 3.141593
⊢ π < 3.141593
have h₂₆ : 2 -
    HPow.hPow (β := ℕ)
      ((3.141593 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 11) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 11 1)) 2 ≤
  (HDiv.hDiv (α := ℝ) (↑294095 : ℝ) (↑147759 : ℝ)).sqrtTwoAddSeries 7
Tactic: pi_upper_bound [
    35839/25342, 49143/26596, 145729/74292, 294095/147759, 2-137/56868, 2-471/781921, 2-153/1015961,
    2-157/4170049, 2-28/2974805, 2-9/3824747, 2-7/11899211]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
h :
  2 -
      HPow.hPow (β := ℕ)
        ((3.141593 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 11) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 11 1)) 2 ≤
    (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries 11
h₂ : 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 11 ≤ 3.141593
h₁ :
  2 -
      HPow.hPow (β := ℕ)
        ((3.141593 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 11) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 11 1)) 2 ≤
    (HDiv.hDiv (α := ℝ) (↑35839 : ℝ) (↑25342 : ℝ)).sqrtTwoAddSeries 10
h₃ : LT.lt (α := ℕ) 0 25342
h₄ : LT.lt (α := ℕ) 0 1
h₅ : HPow.hPow (α := ℕ) (β := ℕ) 35839 2 * 1 ≤ (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 25342 2
h₆ : 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 11 ≤ 3.141593
h₇ :
  2 -
      HPow.hPow (β := ℕ)
        ((3.141593 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 11) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 11 1)) 2 ≤
    (HDiv.hDiv (α := ℝ) (↑49143 : ℝ) (↑26596 : ℝ)).sqrtTwoAddSeries 9
h₈ : LT.lt (α := ℕ) 0 26596
h₉ : LT.lt (α := ℕ) 0 25342
h₁₀ :
  HPow.hPow (α := ℕ) (β := ℕ) 49143 2 * 25342 ≤
    (HMul.hMul (α := ℕ) 2 25342 + 35839) * HPow.hPow (α := ℕ) (β := ℕ) 26596 2
h₁₁ : LT.lt (α := ℕ) 0 25342
h₁₂ : LT.lt (α := ℕ) 0 1
h₁₃ : HPow.hPow (α := ℕ) (β := ℕ) 35839 2 * 1 ≤ (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 25342 2
h₁₄ : 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 11 ≤ 3.141593
h₁₅ :
  2 -
      HPow.hPow (β := ℕ)
        ((3.141593 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 11) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 11 1)) 2 ≤
    (HDiv.hDiv (α := ℝ) (↑145729 : ℝ) (↑74292 : ℝ)).sqrtTwoAddSeries 8
h₁₆ : LT.lt (α := ℕ) 0 74292
h₁₇ : LT.lt (α := ℕ) 0 26596
h₁₈ :
  HPow.hPow (α := ℕ) (β := ℕ) 145729 2 * 26596 ≤
    (HMul.hMul (α := ℕ) 2 26596 + 49143) * HPow.hPow (α := ℕ) (β := ℕ) 74292 2
h₁₉ : LT.lt (α := ℕ) 0 26596
h₂₀ : LT.lt (α := ℕ) 0 25342
h₂₁ :
  HPow.hPow (α := ℕ) (β := ℕ) 49143 2 * 25342 ≤
    (HMul.hMul (α := ℕ) 2 25342 + 35839) * HPow.hPow (α := ℕ) (β := ℕ) 26596 2
h₂₂ : LT.lt (α := ℕ) 0 25342
h₂₃ : LT.lt (α := ℕ) 0 1
h₂₄ : HPow.hPow (α := ℕ) (β := ℕ) 35839 2 * 1 ≤ (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 25342 2
h₂₅ : 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 11 ≤ 3.141593
h₂₆ :
  2 -
      HPow.hPow (β := ℕ)
        ((3.141593 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 11) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 11 1)) 2 ≤
    (HDiv.hDiv (α := ℝ) (↑294095 : ℝ) (↑147759 : ℝ)).sqrtTwoAddSeries 7
⊢ π < 3.141593
have h₂₇ : LT.lt (α := ℕ) 0 147759
Tactic: pi_upper_bound [
    35839/25342, 49143/26596, 145729/74292, 294095/147759, 2-137/56868, 2-471/781921, 2-153/1015961,
    2-157/4170049, 2-28/2974805, 2-9/3824747, 2-7/11899211]