-- Module: Mathlib.Analysis.Real.Pi.Bounds
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
hz₂₂ : HDiv.hDiv (α := ℝ) 1447 727 ≤ 2 - HPow.hPow (β := ℕ) (3.14 / HPow.hPow (α := ℝ) (β := ℕ) 2 5) 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 < π

Tactic:
pi_lower_bound [338 / 239, 704 / 381, 1940 / 989, 1447 / 727]