-- Module: Mathlib.Analysis.Real.Pi.Bounds
Goal:
h :
  2 -
      HPow.hPow (β := ℕ) ((3.15 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1))
        2 ≤
    (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries 4
h₂ : 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4 ≤ 3.15
h₁ :
  2 -
      HPow.hPow (β := ℕ) ((3.15 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1))
        2 ≤
    (HDiv.hDiv (α := ℝ) (↑41 : ℝ) (↑29 : ℝ)).sqrtTwoAddSeries 3
h₃ : LT.lt (α := ℕ) 0 29
h₄ : LT.lt (α := ℕ) 0 1
h₅ : HPow.hPow (α := ℕ) (β := ℕ) 41 2 * 1 ≤ (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 29 2
h₆ : 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4 ≤ 3.15
h₇ :
  2 -
      HPow.hPow (β := ℕ) ((3.15 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1))
        2 ≤
    (HDiv.hDiv (α := ℝ) (↑109 : ℝ) (↑59 : ℝ)).sqrtTwoAddSeries 2
h₈ : LT.lt (α := ℕ) 0 59
h₉ : LT.lt (α := ℕ) 0 29
h₁₀ : HPow.hPow (α := ℕ) (β := ℕ) 109 2 * 29 ≤ (HMul.hMul (α := ℕ) 2 29 + 41) * HPow.hPow (α := ℕ) (β := ℕ) 59 2
h₁₁ : LT.lt (α := ℕ) 0 29
h₁₂ : LT.lt (α := ℕ) 0 1
h₁₃ : HPow.hPow (α := ℕ) (β := ℕ) 41 2 * 1 ≤ (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 29 2
h₁₄ : 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4 ≤ 3.15
h₁₅ :
  2 -
      HPow.hPow (β := ℕ) ((3.15 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1))
        2 ≤
    (HDiv.hDiv (α := ℝ) (↑865 : ℝ) (↑441 : ℝ)).sqrtTwoAddSeries 1
h₁₆ : LT.lt (α := ℕ) 0 441
h₁₇ : LT.lt (α := ℕ) 0 59
h₁₈ : HPow.hPow (α := ℕ) (β := ℕ) 865 2 * 59 ≤ (HMul.hMul (α := ℕ) 2 59 + 109) * HPow.hPow (α := ℕ) (β := ℕ) 441 2
h₁₉ : LT.lt (α := ℕ) 0 59
h₂₀ : LT.lt (α := ℕ) 0 29
h₂₁ : HPow.hPow (α := ℕ) (β := ℕ) 109 2 * 29 ≤ (HMul.hMul (α := ℕ) 2 29 + 41) * HPow.hPow (α := ℕ) (β := ℕ) 59 2
h₂₂ : LT.lt (α := ℕ) 0 29
h₂₃ : LT.lt (α := ℕ) 0 1
h₂₄ : HPow.hPow (α := ℕ) (β := ℕ) 41 2 * 1 ≤ (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 29 2
h₂₅ : 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4 ≤ 3.15
h₂₆ :
  2 -
      HPow.hPow (β := ℕ) ((3.15 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1))
        2 ≤
    (HDiv.hDiv (α := ℝ) (↑412 : ℝ) (↑207 : ℝ)).sqrtTwoAddSeries 0
h₂₇ : LT.lt (α := ℕ) 0 207
h₂₈ : LT.lt (α := ℕ) 0 441
h₂₉ : HPow.hPow (α := ℕ) (β := ℕ) 412 2 * 441 ≤ (HMul.hMul (α := ℕ) 2 441 + 865) * HPow.hPow (α := ℕ) (β := ℕ) 207 2
h₃₀ : LT.lt (α := ℕ) 0 441
h₃₁ : LT.lt (α := ℕ) 0 59
h₃₂ : HPow.hPow (α := ℕ) (β := ℕ) 865 2 * 59 ≤ (HMul.hMul (α := ℕ) 2 59 + 109) * HPow.hPow (α := ℕ) (β := ℕ) 441 2
h₃₃ : LT.lt (α := ℕ) 0 59
h₃₄ : LT.lt (α := ℕ) 0 29
h₃₅ : HPow.hPow (α := ℕ) (β := ℕ) 109 2 * 29 ≤ (HMul.hMul (α := ℕ) 2 29 + 41) * HPow.hPow (α := ℕ) (β := ℕ) 59 2
h₃₆ : LT.lt (α := ℕ) 0 29
h₃₇ : LT.lt (α := ℕ) 0 1
h₃₈ : HPow.hPow (α := ℕ) (β := ℕ) 41 2 * 1 ≤ (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 29 2
h₃₉ : 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4 ≤ 3.15
h₄₀ :
  2 ≤
    HDiv.hDiv (α := ℝ) 412 207 +
      HPow.hPow (β := ℕ) ((3.15 - (HPow.hPow (α := ℝ) (β := ℕ) 4 4)⁻¹) / HPow.hPow (α := ℝ) (β := ℕ) 2 5) 2
h₄₁ : LT.lt (α := ℕ) 0 207
h₄₂ : LT.lt (α := ℕ) 0 441
h₄₃ : HPow.hPow (α := ℕ) (β := ℕ) 412 2 * 441 ≤ (HMul.hMul (α := ℕ) 2 441 + 865) * HPow.hPow (α := ℕ) (β := ℕ) 207 2
h₄₄ : LT.lt (α := ℕ) 0 441
h₄₅ : LT.lt (α := ℕ) 0 59
h₄₆ : HPow.hPow (α := ℕ) (β := ℕ) 865 2 * 59 ≤ (HMul.hMul (α := ℕ) 2 59 + 109) * HPow.hPow (α := ℕ) (β := ℕ) 441 2
h₄₇ : LT.lt (α := ℕ) 0 59
h₄₈ : LT.lt (α := ℕ) 0 29
h₄₉ : HPow.hPow (α := ℕ) (β := ℕ) 109 2 * 29 ≤ (HMul.hMul (α := ℕ) 2 29 + 41) * HPow.hPow (α := ℕ) (β := ℕ) 59 2
h₅₀ : LT.lt (α := ℕ) 0 29
h₅₁ : LT.lt (α := ℕ) 0 1
h₅₂ : HPow.hPow (α := ℕ) (β := ℕ) 41 2 * 1 ≤ (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 29 2
h₅₃ : 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 4 ≤ 3.15
⊢ π < 3.15

Tactic:
pi_upper_bound [41 / 29, 109 / 59, 865 / 441, 412 / 207]