-- 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
h₄₃ :
  HPow.hPow (α := ℕ) (β := ℕ) 43947 2 * 24713 ≤
    (HMul.hMul (α := ℕ) 2 24713 + 49188) * HPow.hPow (α := ℕ) (β := ℕ) 22000 2
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 (α := ℝ) (↑235667 : ℝ) (↑117869 : ℝ)).sqrtTwoAddSeries 3
h₅₈ : LT.lt (α := ℕ) 0 117869
h₅₉ : LT.lt (α := ℕ) 0 22000
h₆₀ :
  HPow.hPow (α := ℕ) (β := ℕ) 235667 2 * 22000 ≤
    (HMul.hMul (α := ℕ) 2 22000 + 43947) * HPow.hPow (α := ℕ) (β := ℕ) 117869 2
h₆₁ : LT.lt (α := ℕ) 0 22000
h₆₂ : LT.lt (α := ℕ) 0 24713
h₆₃ :
  HPow.hPow (α := ℕ) (β := ℕ) 43947 2 * 24713 ≤
    (HMul.hMul (α := ℕ) 2 24713 + 49188) * HPow.hPow (α := ℕ) (β := ℕ) 22000 2
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 (α := ℝ) (↑624137 : ℝ) (↑312092 : ℝ)).sqrtTwoAddSeries 2
h₇₈ : LT.lt (α := ℕ) 0 312092
h₇₉ : LT.lt (α := ℕ) 0 117869
h₈₀ :
  HPow.hPow (α := ℕ) (β := ℕ) 624137 2 * 117869 ≤
    (HMul.hMul (α := ℕ) 2 117869 + 235667) * HPow.hPow (α := ℕ) (β := ℕ) 312092 2
h₈₁ : LT.lt (α := ℕ) 0 117869
h₈₂ : LT.lt (α := ℕ) 0 22000
h₈₃ :
  HPow.hPow (α := ℕ) (β := ℕ) 235667 2 * 22000 ≤
    (HMul.hMul (α := ℕ) 2 22000 + 43947) * HPow.hPow (α := ℕ) (β := ℕ) 117869 2
h₈₄ : LT.lt (α := ℕ) 0 22000
h₈₅ : LT.lt (α := ℕ) 0 24713
h₈₆ :
  HPow.hPow (α := ℕ) (β := ℕ) 43947 2 * 24713 ≤
    (HMul.hMul (α := ℕ) 2 24713 + 49188) * HPow.hPow (α := ℕ) (β := ℕ) 22000 2
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 (α := ℝ) (↑903049 : ℝ) (↑451533 : ℝ)).sqrtTwoAddSeries 1
h₁₀₁ : LT.lt (α := ℕ) 0 451533
h₁₀₂ : LT.lt (α := ℕ) 0 312092
h₁₀₃ :
  HPow.hPow (α := ℕ) (β := ℕ) 903049 2 * 312092 ≤
    (HMul.hMul (α := ℕ) 2 312092 + 624137) * HPow.hPow (α := ℕ) (β := ℕ) 451533 2
h₁₀₄ : LT.lt (α := ℕ) 0 312092
h₁₀₅ : LT.lt (α := ℕ) 0 117869
h₁₀₆ :
  HPow.hPow (α := ℕ) (β := ℕ) 624137 2 * 117869 ≤
    (HMul.hMul (α := ℕ) 2 117869 + 235667) * HPow.hPow (α := ℕ) (β := ℕ) 312092 2
h₁₀₇ : LT.lt (α := ℕ) 0 117869
h₁₀₈ : LT.lt (α := ℕ) 0 22000
h₁₀₉ :
  HPow.hPow (α := ℕ) (β := ℕ) 235667 2 * 22000 ≤
    (HMul.hMul (α := ℕ) 2 22000 + 43947) * HPow.hPow (α := ℕ) (β := ℕ) 117869 2
h₁₁₀ : LT.lt (α := ℕ) 0 22000
h₁₁₁ : LT.lt (α := ℕ) 0 24713
h₁₁₂ :
  HPow.hPow (α := ℕ) (β := ℕ) 43947 2 * 24713 ≤
    (HMul.hMul (α := ℕ) 2 24713 + 49188) * HPow.hPow (α := ℕ) (β := ℕ) 22000 2
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
⊢ π < 3.1416
have h₁₂₆ : 2 -
    HPow.hPow (β := ℕ) ((3.1416 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 9) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 9 1))
      2 ≤
  (HDiv.hDiv (α := ℝ) (↑849938 : ℝ) (↑424971 : ℝ)).sqrtTwoAddSeries 0
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]