-- Module: Mathlib.Analysis.Real.Pi.Bounds
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
h₁₀₃ :
  HPow.hPow (α := ℕ) (β := ℕ) 8339941 2 * 1015961 ≤
    (HMul.hMul (α := ℕ) 2 1015961 + 2031769) * HPow.hPow (α := ℕ) (β := ℕ) 4170049 2
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 (α := ℝ) (↑5949582 : ℝ) (↑2974805 : ℝ)).sqrtTwoAddSeries 2
h₁₂₇ : LT.lt (α := ℕ) 0 2974805
h₁₂₈ : LT.lt (α := ℕ) 0 4170049
h₁₂₉ :
  HPow.hPow (α := ℕ) (β := ℕ) 5949582 2 * 4170049 ≤
    (HMul.hMul (α := ℕ) 2 4170049 + 8339941) * HPow.hPow (α := ℕ) (β := ℕ) 2974805 2
h₁₃₀ : LT.lt (α := ℕ) 0 4170049
h₁₃₁ : LT.lt (α := ℕ) 0 1015961
h₁₃₂ :
  HPow.hPow (α := ℕ) (β := ℕ) 8339941 2 * 1015961 ≤
    (HMul.hMul (α := ℕ) 2 1015961 + 2031769) * HPow.hPow (α := ℕ) (β := ℕ) 4170049 2
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 (α := ℝ) (↑7649485 : ℝ) (↑3824747 : ℝ)).sqrtTwoAddSeries 1
h₁₅₆ : LT.lt (α := ℕ) 0 3824747
h₁₅₇ : LT.lt (α := ℕ) 0 2974805
h₁₅₈ :
  HPow.hPow (α := ℕ) (β := ℕ) 7649485 2 * 2974805 ≤
    (HMul.hMul (α := ℕ) 2 2974805 + 5949582) * HPow.hPow (α := ℕ) (β := ℕ) 3824747 2
h₁₅₉ : LT.lt (α := ℕ) 0 2974805
h₁₆₀ : LT.lt (α := ℕ) 0 4170049
h₁₆₁ :
  HPow.hPow (α := ℕ) (β := ℕ) 5949582 2 * 4170049 ≤
    (HMul.hMul (α := ℕ) 2 4170049 + 8339941) * HPow.hPow (α := ℕ) (β := ℕ) 2974805 2
h₁₆₂ : LT.lt (α := ℕ) 0 4170049
h₁₆₃ : LT.lt (α := ℕ) 0 1015961
h₁₆₄ :
  HPow.hPow (α := ℕ) (β := ℕ) 8339941 2 * 1015961 ≤
    (HMul.hMul (α := ℕ) 2 1015961 + 2031769) * HPow.hPow (α := ℕ) (β := ℕ) 4170049 2
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 (α := ℝ) (↑23798415 : ℝ) (↑11899211 : ℝ)).sqrtTwoAddSeries 0
h₁₈₈ : LT.lt (α := ℕ) 0 11899211
h₁₈₉ : LT.lt (α := ℕ) 0 3824747
h₁₉₀ :
  HPow.hPow (α := ℕ) (β := ℕ) 23798415 2 * 3824747 ≤
    (HMul.hMul (α := ℕ) 2 3824747 + 7649485) * HPow.hPow (α := ℕ) (β := ℕ) 11899211 2
h₁₉₁ : LT.lt (α := ℕ) 0 3824747
h₁₉₂ : LT.lt (α := ℕ) 0 2974805
h₁₉₃ :
  HPow.hPow (α := ℕ) (β := ℕ) 7649485 2 * 2974805 ≤
    (HMul.hMul (α := ℕ) 2 2974805 + 5949582) * HPow.hPow (α := ℕ) (β := ℕ) 3824747 2
h₁₉₄ : LT.lt (α := ℕ) 0 2974805
h₁₉₅ : LT.lt (α := ℕ) 0 4170049
h₁₉₆ :
  HPow.hPow (α := ℕ) (β := ℕ) 5949582 2 * 4170049 ≤
    (HMul.hMul (α := ℕ) 2 4170049 + 8339941) * HPow.hPow (α := ℕ) (β := ℕ) 2974805 2
h₁₉₇ : LT.lt (α := ℕ) 0 4170049
h₁₉₈ : LT.lt (α := ℕ) 0 1015961
h₁₉₉ :
  HPow.hPow (α := ℕ) (β := ℕ) 8339941 2 * 1015961 ≤
    (HMul.hMul (α := ℕ) 2 1015961 + 2031769) * HPow.hPow (α := ℕ) (β := ℕ) 4170049 2
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 ≤
    HDiv.hDiv (α := ℝ) 23798415 11899211 +
      HPow.hPow (β := ℕ) ((3.141593 - (HPow.hPow (α := ℝ) (β := ℕ) 4 11)⁻¹) / HPow.hPow (α := ℝ) (β := ℕ) 2 12) 2
h₂₂₃ : LT.lt (α := ℕ) 0 11899211
h₂₂₄ : LT.lt (α := ℕ) 0 3824747
h₂₂₅ :
  HPow.hPow (α := ℕ) (β := ℕ) 23798415 2 * 3824747 ≤
    (HMul.hMul (α := ℕ) 2 3824747 + 7649485) * HPow.hPow (α := ℕ) (β := ℕ) 11899211 2
h₂₂₆ : LT.lt (α := ℕ) 0 3824747
h₂₂₇ : LT.lt (α := ℕ) 0 2974805
h₂₂₈ :
  HPow.hPow (α := ℕ) (β := ℕ) 7649485 2 * 2974805 ≤
    (HMul.hMul (α := ℕ) 2 2974805 + 5949582) * HPow.hPow (α := ℕ) (β := ℕ) 3824747 2
h₂₂₉ : LT.lt (α := ℕ) 0 2974805
h₂₃₀ : LT.lt (α := ℕ) 0 4170049
h₂₃₁ :
  HPow.hPow (α := ℕ) (β := ℕ) 5949582 2 * 4170049 ≤
    (HMul.hMul (α := ℕ) 2 4170049 + 8339941) * HPow.hPow (α := ℕ) (β := ℕ) 2974805 2
h₂₃₂ : LT.lt (α := ℕ) 0 4170049
h₂₃₃ : LT.lt (α := ℕ) 0 1015961
h₂₃₄ :
  HPow.hPow (α := ℕ) (β := ℕ) 8339941 2 * 1015961 ≤
    (HMul.hMul (α := ℕ) 2 1015961 + 2031769) * HPow.hPow (α := ℕ) (β := ℕ) 4170049 2
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
⊢ π < 3.141593

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]