-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
h :
  2 -
      HPow.hPow (β := ℕ)
        ((3.1416 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 9) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 9 1)) 2 ≤
    (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries 9
h₂ : 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 9 ≤ 3.1416
h₁ :
  2 -
      HPow.hPow (β := ℕ)
        ((3.1416 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 9) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 9 1)) 2 ≤
    (HDiv.hDiv (α := ℝ) (↑4756 : ℝ) (↑3363 : ℝ)).sqrtTwoAddSeries 8
h₃ : LT.lt (α := ℕ) 0 3363
h₄ : LT.lt (α := ℕ) 0 1
h₅ : HPow.hPow (α := ℕ) (β := ℕ) 4756 2 * 1 ≤ (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 3363 2
h₆ : 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 9 ≤ 3.1416
h₇ :
  2 -
      HPow.hPow (β := ℕ)
        ((3.1416 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 9) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 9 1)) 2 ≤
    (HDiv.hDiv (α := ℝ) (↑14965 : ℝ) (↑8099 : ℝ)).sqrtTwoAddSeries 7
h₈ : LT.lt (α := ℕ) 0 8099
h₉ : LT.lt (α := ℕ) 0 3363
h₁₀ :
  HPow.hPow (α := ℕ) (β := ℕ) 14965 2 * 3363 ≤ (HMul.hMul (α := ℕ) 2 3363 + 4756) * HPow.hPow (α := ℕ) (β := ℕ) 8099 2
h₁₁ : LT.lt (α := ℕ) 0 3363
h₁₂ : LT.lt (α := ℕ) 0 1
h₁₃ : HPow.hPow (α := ℕ) (β := ℕ) 4756 2 * 1 ≤ (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 3363 2
h₁₄ : 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 9 ≤ 3.1416
h₁₅ :
  2 -
      HPow.hPow (β := ℕ)
        ((3.1416 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 9) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 9 1)) 2 ≤
    (HDiv.hDiv (α := ℝ) (↑21183 : ℝ) (↑10799 : ℝ)).sqrtTwoAddSeries 6
h₁₆ : LT.lt (α := ℕ) 0 10799
h₁₇ : LT.lt (α := ℕ) 0 8099
h₁₈ :
  HPow.hPow (α := ℕ) (β := ℕ) 21183 2 * 8099 ≤ (HMul.hMul (α := ℕ) 2 8099 + 14965) * HPow.hPow (α := ℕ) (β := ℕ) 10799 2
h₁₉ : LT.lt (α := ℕ) 0 8099
h₂₀ : LT.lt (α := ℕ) 0 3363
h₂₁ :
  HPow.hPow (α := ℕ) (β := ℕ) 14965 2 * 3363 ≤ (HMul.hMul (α := ℕ) 2 3363 + 4756) * HPow.hPow (α := ℕ) (β := ℕ) 8099 2
h₂₂ : LT.lt (α := ℕ) 0 3363
h₂₃ : LT.lt (α := ℕ) 0 1
h₂₄ : HPow.hPow (α := ℕ) (β := ℕ) 4756 2 * 1 ≤ (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 3363 2
h₂₅ : 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 9 ≤ 3.1416
h₂₆ :
  2 -
      HPow.hPow (β := ℕ)
        ((3.1416 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 9) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 9 1)) 2 ≤
    (HDiv.hDiv (α := ℝ) (↑49188 : ℝ) (↑24713 : ℝ)).sqrtTwoAddSeries 5
h₂₇ : LT.lt (α := ℕ) 0 24713
h₂₈ : LT.lt (α := ℕ) 0 10799
h₂₉ :
  HPow.hPow (α := ℕ) (β := ℕ) 49188 2 * 10799 ≤
    (HMul.hMul (α := ℕ) 2 10799 + 21183) * HPow.hPow (α := ℕ) (β := ℕ) 24713 2
h₃₀ : LT.lt (α := ℕ) 0 10799
h₃₁ : LT.lt (α := ℕ) 0 8099
h₃₂ :
  HPow.hPow (α := ℕ) (β := ℕ) 21183 2 * 8099 ≤ (HMul.hMul (α := ℕ) 2 8099 + 14965) * HPow.hPow (α := ℕ) (β := ℕ) 10799 2
h₃₃ : LT.lt (α := ℕ) 0 8099
h₃₄ : LT.lt (α := ℕ) 0 3363
h₃₅ :
  HPow.hPow (α := ℕ) (β := ℕ) 14965 2 * 3363 ≤ (HMul.hMul (α := ℕ) 2 3363 + 4756) * HPow.hPow (α := ℕ) (β := ℕ) 8099 2
h₃₆ : LT.lt (α := ℕ) 0 3363
h₃₇ : LT.lt (α := ℕ) 0 1
h₃₈ : HPow.hPow (α := ℕ) (β := ℕ) 4756 2 * 1 ≤ (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 3363 2
h₃₉ : 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 9 ≤ 3.1416
h₄₀ :
  2 -
      HPow.hPow (β := ℕ)
        ((3.1416 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 9) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 9 1)) 2 ≤
    (HDiv.hDiv (α := ℝ) (↑43947 : ℝ) (↑22000 : ℝ)).sqrtTwoAddSeries 4
h₄₁ : LT.lt (α := ℕ) 0 22000
h₄₂ : LT.lt (α := ℕ) 0 24713
⊢ π < 3.1416
have h₄₃ : HPow.hPow (α := ℕ) (β := ℕ) 43947 2 * 24713 ≤ (HMul.hMul (α := ℕ) 2 24713 + 49188) * HPow.hPow (α := ℕ) (β := ℕ) 22000 2
Tactic: pi_upper_bound [
    4756/3363, 14965/8099, 21183/10799, 49188/24713, 2-53/22000, 2-71/117869, 2-47/312092,
    2-17/451533, 2-4/424971]