-- 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
h₂₇ : LT.lt (α := ℕ) 0 147759
h₂₈ : LT.lt (α := ℕ) 0 74292
h₂₉ :
  HPow.hPow (α := ℕ) (β := ℕ) 294095 2 * 74292 ≤
    (HMul.hMul (α := ℕ) 2 74292 + 145729) * HPow.hPow (α := ℕ) (β := ℕ) 147759 2
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 (α := ℝ) (↑113599 : ℝ) (↑56868 : ℝ)).sqrtTwoAddSeries 6
h₄₁ : LT.lt (α := ℕ) 0 56868
h₄₂ : LT.lt (α := ℕ) 0 147759
⊢ π < 3.141593
have h₄₃ : HPow.hPow (α := ℕ) (β := ℕ) 113599 2 * 147759 ≤
  (HMul.hMul (α := ℕ) 2 147759 + 294095) * HPow.hPow (α := ℕ) (β := ℕ) 56868 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]