-- 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
hz₂₄ : LT.lt (α := ℕ) 0 139887
⊢ 3.141592 < π
have hz₂₅ : (HMul.hMul (α := ℕ) 2 64690 + 128757) * HPow.hPow (α := ℕ) (β := ℕ) 139887 2 ≤
  HPow.hPow (α := ℕ) (β := ℕ) 279437 2 * 64690
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]