-- 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
h₄₃ :
  HPow.hPow (α := ℕ) (β := ℕ) 113599 2 * 147759 ≤
    (HMul.hMul (α := ℕ) 2 147759 + 294095) * HPow.hPow (α := ℕ) (β := ℕ) 56868 2
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 (α := ℝ) (↑1563371 : ℝ) (↑781921 : ℝ)).sqrtTwoAddSeries 5
h₅₈ : LT.lt (α := ℕ) 0 781921
h₅₉ : LT.lt (α := ℕ) 0 56868
h₆₀ :
  HPow.hPow (α := ℕ) (β := ℕ) 1563371 2 * 56868 ≤
    (HMul.hMul (α := ℕ) 2 56868 + 113599) * HPow.hPow (α := ℕ) (β := ℕ) 781921 2
h₆₁ : LT.lt (α := ℕ) 0 56868
h₆₂ : LT.lt (α := ℕ) 0 147759
h₆₃ :
  HPow.hPow (α := ℕ) (β := ℕ) 113599 2 * 147759 ≤
    (HMul.hMul (α := ℕ) 2 147759 + 294095) * HPow.hPow (α := ℕ) (β := ℕ) 56868 2
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 (α := ℝ) (↑2031769 : ℝ) (↑1015961 : ℝ)).sqrtTwoAddSeries 4
h₇₈ : LT.lt (α := ℕ) 0 1015961
h₇₉ : LT.lt (α := ℕ) 0 781921
h₈₀ :
  HPow.hPow (α := ℕ) (β := ℕ) 2031769 2 * 781921 ≤
    (HMul.hMul (α := ℕ) 2 781921 + 1563371) * HPow.hPow (α := ℕ) (β := ℕ) 1015961 2
h₈₁ : LT.lt (α := ℕ) 0 781921
h₈₂ : LT.lt (α := ℕ) 0 56868
h₈₃ :
  HPow.hPow (α := ℕ) (β := ℕ) 1563371 2 * 56868 ≤
    (HMul.hMul (α := ℕ) 2 56868 + 113599) * HPow.hPow (α := ℕ) (β := ℕ) 781921 2
h₈₄ : LT.lt (α := ℕ) 0 56868
h₈₅ : LT.lt (α := ℕ) 0 147759
h₈₆ :
  HPow.hPow (α := ℕ) (β := ℕ) 113599 2 * 147759 ≤
    (HMul.hMul (α := ℕ) 2 147759 + 294095) * HPow.hPow (α := ℕ) (β := ℕ) 56868 2
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 (α := ℝ) (↑8339941 : ℝ) (↑4170049 : ℝ)).sqrtTwoAddSeries 3
h₁₀₁ : LT.lt (α := ℕ) 0 4170049
h₁₀₂ : LT.lt (α := ℕ) 0 1015961
⊢ π < 3.141593
have h₁₀₃ : HPow.hPow (α := ℕ) (β := ℕ) 8339941 2 * 1015961 ≤
  (HMul.hMul (α := ℕ) 2 1015961 + 2031769) * HPow.hPow (α := ℕ) (β := ℕ) 4170049 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]