-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
pi_lower_bound :
  (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries 10 ≤
    2 - HPow.hPow (β := ℕ) (3.141592 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 10 1)) 2
hz :
  (HDiv.hDiv (α := ℝ) (↑11482 : ℝ) (↑8119 : ℝ)).sqrtTwoAddSeries 9 ≤
    2 - HPow.hPow (β := ℕ) (3.141592 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 10 1)) 2
hb : LT.lt (α := ℕ) 0 1
hd : LT.lt (α := ℕ) 0 8119
h : (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 8119 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 11482 2 * 1
hz₁ :
  (HDiv.hDiv (α := ℝ) (↑7792 : ℝ) (↑4217 : ℝ)).sqrtTwoAddSeries 8 ≤
    2 - HPow.hPow (β := ℕ) (3.141592 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 10 1)) 2
hz₂ : LT.lt (α := ℕ) 0 8119
hz₃ : LT.lt (α := ℕ) 0 4217
hz₄ :
  (HMul.hMul (α := ℕ) 2 8119 + 11482) * HPow.hPow (α := ℕ) (β := ℕ) 4217 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 7792 2 * 8119
hb₁ : LT.lt (α := ℕ) 0 1
hd₁ : LT.lt (α := ℕ) 0 8119
h₁ : (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 8119 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 11482 2 * 1
hz₅ :
  (HDiv.hDiv (α := ℝ) (↑54055 : ℝ) (↑27557 : ℝ)).sqrtTwoAddSeries 7 ≤
    2 - HPow.hPow (β := ℕ) (3.141592 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 10 1)) 2
hz₆ : LT.lt (α := ℕ) 0 4217
hz₇ : LT.lt (α := ℕ) 0 27557
hz₈ :
  (HMul.hMul (α := ℕ) 2 4217 + 7792) * HPow.hPow (α := ℕ) (β := ℕ) 27557 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 54055 2 * 4217
hz₉ : LT.lt (α := ℕ) 0 8119
hz₁₀ : LT.lt (α := ℕ) 0 4217
hz₁₁ :
  (HMul.hMul (α := ℕ) 2 8119 + 11482) * HPow.hPow (α := ℕ) (β := ℕ) 4217 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 7792 2 * 8119
hb₂ : LT.lt (α := ℕ) 0 1
hd₂ : LT.lt (α := ℕ) 0 8119
h₂ : (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 8119 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 11482 2 * 1
hz₁₂ :
  (HDiv.hDiv (α := ℝ) (↑128757 : ℝ) (↑64690 : ℝ)).sqrtTwoAddSeries 6 ≤
    2 - HPow.hPow (β := ℕ) (3.141592 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 10 1)) 2
hz₁₃ : LT.lt (α := ℕ) 0 27557
hz₁₄ : LT.lt (α := ℕ) 0 64690
hz₁₅ :
  (HMul.hMul (α := ℕ) 2 27557 + 54055) * HPow.hPow (α := ℕ) (β := ℕ) 64690 2 ≤
    HPow.hPow (α := ℕ) (β := ℕ) 128757 2 * 27557
hz₁₆ : LT.lt (α := ℕ) 0 4217
hz₁₇ : LT.lt (α := ℕ) 0 27557
hz₁₈ :
  (HMul.hMul (α := ℕ) 2 4217 + 7792) * HPow.hPow (α := ℕ) (β := ℕ) 27557 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 54055 2 * 4217
hz₁₉ : LT.lt (α := ℕ) 0 8119
hz₂₀ : LT.lt (α := ℕ) 0 4217
hz₂₁ :
  (HMul.hMul (α := ℕ) 2 8119 + 11482) * HPow.hPow (α := ℕ) (β := ℕ) 4217 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 7792 2 * 8119
hb₃ : LT.lt (α := ℕ) 0 1
hd₃ : LT.lt (α := ℕ) 0 8119
h₃ : (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 8119 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 11482 2 * 1
hz₂₂ :
  (HDiv.hDiv (α := ℝ) (↑279437 : ℝ) (↑139887 : ℝ)).sqrtTwoAddSeries 5 ≤
    2 - HPow.hPow (β := ℕ) (3.141592 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 10 1)) 2
hz₂₃ : LT.lt (α := ℕ) 0 64690
hz₂₄ : LT.lt (α := ℕ) 0 139887
hz₂₅ :
  (HMul.hMul (α := ℕ) 2 64690 + 128757) * HPow.hPow (α := ℕ) (β := ℕ) 139887 2 ≤
    HPow.hPow (α := ℕ) (β := ℕ) 279437 2 * 64690
hz₂₆ : LT.lt (α := ℕ) 0 27557
hz₂₇ : LT.lt (α := ℕ) 0 64690
hz₂₈ :
  (HMul.hMul (α := ℕ) 2 27557 + 54055) * HPow.hPow (α := ℕ) (β := ℕ) 64690 2 ≤
    HPow.hPow (α := ℕ) (β := ℕ) 128757 2 * 27557
hz₂₉ : LT.lt (α := ℕ) 0 4217
hz₃₀ : LT.lt (α := ℕ) 0 27557
hz₃₁ :
  (HMul.hMul (α := ℕ) 2 4217 + 7792) * HPow.hPow (α := ℕ) (β := ℕ) 27557 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 54055 2 * 4217
hz₃₂ : LT.lt (α := ℕ) 0 8119
hz₃₃ : LT.lt (α := ℕ) 0 4217
hz₃₄ :
  (HMul.hMul (α := ℕ) 2 8119 + 11482) * HPow.hPow (α := ℕ) (β := ℕ) 4217 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 7792 2 * 8119
hb₄ : LT.lt (α := ℕ) 0 1
hd₄ : LT.lt (α := ℕ) 0 8119
h₄ : (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 8119 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 11482 2 * 1
hz₃₅ :
  (HDiv.hDiv (α := ℝ) (↑690406 : ℝ) (↑345307 : ℝ)).sqrtTwoAddSeries 4 ≤
    2 - HPow.hPow (β := ℕ) (3.141592 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 10 1)) 2
hz₃₆ : LT.lt (α := ℕ) 0 139887
hz₃₇ : LT.lt (α := ℕ) 0 345307
hz₃₈ :
  (HMul.hMul (α := ℕ) 2 139887 + 279437) * HPow.hPow (α := ℕ) (β := ℕ) 345307 2 ≤
    HPow.hPow (α := ℕ) (β := ℕ) 690406 2 * 139887
hz₃₉ : LT.lt (α := ℕ) 0 64690
hz₄₀ : LT.lt (α := ℕ) 0 139887
hz₄₁ :
  (HMul.hMul (α := ℕ) 2 64690 + 128757) * HPow.hPow (α := ℕ) (β := ℕ) 139887 2 ≤
    HPow.hPow (α := ℕ) (β := ℕ) 279437 2 * 64690
hz₄₂ : LT.lt (α := ℕ) 0 27557
hz₄₃ : LT.lt (α := ℕ) 0 64690
hz₄₄ :
  (HMul.hMul (α := ℕ) 2 27557 + 54055) * HPow.hPow (α := ℕ) (β := ℕ) 64690 2 ≤
    HPow.hPow (α := ℕ) (β := ℕ) 128757 2 * 27557
hz₄₅ : LT.lt (α := ℕ) 0 4217
hz₄₆ : LT.lt (α := ℕ) 0 27557
hz₄₇ :
  (HMul.hMul (α := ℕ) 2 4217 + 7792) * HPow.hPow (α := ℕ) (β := ℕ) 27557 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 54055 2 * 4217
hz₄₈ : LT.lt (α := ℕ) 0 8119
hz₄₉ : LT.lt (α := ℕ) 0 4217
hz₅₀ :
  (HMul.hMul (α := ℕ) 2 8119 + 11482) * HPow.hPow (α := ℕ) (β := ℕ) 4217 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 7792 2 * 8119
hb₅ : LT.lt (α := ℕ) 0 1
hd₅ : LT.lt (α := ℕ) 0 8119
h₅ : (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 8119 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 11482 2 * 1
hz₅₁ :
  (HDiv.hDiv (α := ℝ) (↑2217683 : ℝ) (↑1108925 : ℝ)).sqrtTwoAddSeries 3 ≤
    2 - HPow.hPow (β := ℕ) (3.141592 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 10 1)) 2
hz₅₂ : LT.lt (α := ℕ) 0 345307
hz₅₃ : LT.lt (α := ℕ) 0 1108925
hz₅₄ :
  (HMul.hMul (α := ℕ) 2 345307 + 690406) * HPow.hPow (α := ℕ) (β := ℕ) 1108925 2 ≤
    HPow.hPow (α := ℕ) (β := ℕ) 2217683 2 * 345307
hz₅₅ : LT.lt (α := ℕ) 0 139887
hz₅₆ : LT.lt (α := ℕ) 0 345307
hz₅₇ :
  (HMul.hMul (α := ℕ) 2 139887 + 279437) * HPow.hPow (α := ℕ) (β := ℕ) 345307 2 ≤
    HPow.hPow (α := ℕ) (β := ℕ) 690406 2 * 139887
hz₅₈ : LT.lt (α := ℕ) 0 64690
hz₅₉ : LT.lt (α := ℕ) 0 139887
hz₆₀ :
  (HMul.hMul (α := ℕ) 2 64690 + 128757) * HPow.hPow (α := ℕ) (β := ℕ) 139887 2 ≤
    HPow.hPow (α := ℕ) (β := ℕ) 279437 2 * 64690
hz₆₁ : LT.lt (α := ℕ) 0 27557
hz₆₂ : LT.lt (α := ℕ) 0 64690
hz₆₃ :
  (HMul.hMul (α := ℕ) 2 27557 + 54055) * HPow.hPow (α := ℕ) (β := ℕ) 64690 2 ≤
    HPow.hPow (α := ℕ) (β := ℕ) 128757 2 * 27557
hz₆₄ : LT.lt (α := ℕ) 0 4217
hz₆₅ : LT.lt (α := ℕ) 0 27557
hz₆₆ :
  (HMul.hMul (α := ℕ) 2 4217 + 7792) * HPow.hPow (α := ℕ) (β := ℕ) 27557 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 54055 2 * 4217
hz₆₇ : LT.lt (α := ℕ) 0 8119
hz₆₈ : LT.lt (α := ℕ) 0 4217
hz₆₉ :
  (HMul.hMul (α := ℕ) 2 8119 + 11482) * HPow.hPow (α := ℕ) (β := ℕ) 4217 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 7792 2 * 8119
hb₆ : LT.lt (α := ℕ) 0 1
hd₆ : LT.lt (α := ℕ) 0 8119
h₆ : (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 8119 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 11482 2 * 1
hz₇₀ :
  (HDiv.hDiv (α := ℝ) (↑3399722 : ℝ) (↑1699893 : ℝ)).sqrtTwoAddSeries 2 ≤
    2 - HPow.hPow (β := ℕ) (3.141592 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 10 1)) 2
hz₇₁ : LT.lt (α := ℕ) 0 1108925
hz₇₂ : LT.lt (α := ℕ) 0 1699893
hz₇₃ :
  (HMul.hMul (α := ℕ) 2 1108925 + 2217683) * HPow.hPow (α := ℕ) (β := ℕ) 1699893 2 ≤
    HPow.hPow (α := ℕ) (β := ℕ) 3399722 2 * 1108925
hz₇₄ : LT.lt (α := ℕ) 0 345307
hz₇₅ : LT.lt (α := ℕ) 0 1108925
hz₇₆ :
  (HMul.hMul (α := ℕ) 2 345307 + 690406) * HPow.hPow (α := ℕ) (β := ℕ) 1108925 2 ≤
    HPow.hPow (α := ℕ) (β := ℕ) 2217683 2 * 345307
hz₇₇ : LT.lt (α := ℕ) 0 139887
hz₇₈ : LT.lt (α := ℕ) 0 345307
hz₇₉ :
  (HMul.hMul (α := ℕ) 2 139887 + 279437) * HPow.hPow (α := ℕ) (β := ℕ) 345307 2 ≤
    HPow.hPow (α := ℕ) (β := ℕ) 690406 2 * 139887
hz₈₀ : LT.lt (α := ℕ) 0 64690
hz₈₁ : LT.lt (α := ℕ) 0 139887
hz₈₂ :
  (HMul.hMul (α := ℕ) 2 64690 + 128757) * HPow.hPow (α := ℕ) (β := ℕ) 139887 2 ≤
    HPow.hPow (α := ℕ) (β := ℕ) 279437 2 * 64690
hz₈₃ : LT.lt (α := ℕ) 0 27557
hz₈₄ : LT.lt (α := ℕ) 0 64690
hz₈₅ :
  (HMul.hMul (α := ℕ) 2 27557 + 54055) * HPow.hPow (α := ℕ) (β := ℕ) 64690 2 ≤
    HPow.hPow (α := ℕ) (β := ℕ) 128757 2 * 27557
hz₈₆ : LT.lt (α := ℕ) 0 4217
hz₈₇ : LT.lt (α := ℕ) 0 27557
hz₈₈ :
  (HMul.hMul (α := ℕ) 2 4217 + 7792) * HPow.hPow (α := ℕ) (β := ℕ) 27557 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 54055 2 * 4217
hz₈₉ : LT.lt (α := ℕ) 0 8119
hz₉₀ : LT.lt (α := ℕ) 0 4217
hz₉₁ :
  (HMul.hMul (α := ℕ) 2 8119 + 11482) * HPow.hPow (α := ℕ) (β := ℕ) 4217 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 7792 2 * 8119
hb₇ : LT.lt (α := ℕ) 0 1
hd₇ : LT.lt (α := ℕ) 0 8119
h₇ : (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 8119 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 11482 2 * 1
hz₉₂ :
  (HDiv.hDiv (α := ℝ) (↑6587039 : ℝ) (↑3293535 : ℝ)).sqrtTwoAddSeries 1 ≤
    2 - HPow.hPow (β := ℕ) (3.141592 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 10 1)) 2
hz₉₃ : LT.lt (α := ℕ) 0 1699893
hz₉₄ : LT.lt (α := ℕ) 0 3293535
hz₉₅ :
  (HMul.hMul (α := ℕ) 2 1699893 + 3399722) * HPow.hPow (α := ℕ) (β := ℕ) 3293535 2 ≤
    HPow.hPow (α := ℕ) (β := ℕ) 6587039 2 * 1699893
hz₉₆ : LT.lt (α := ℕ) 0 1108925
hz₉₇ : LT.lt (α := ℕ) 0 1699893
hz₉₈ :
  (HMul.hMul (α := ℕ) 2 1108925 + 2217683) * HPow.hPow (α := ℕ) (β := ℕ) 1699893 2 ≤
    HPow.hPow (α := ℕ) (β := ℕ) 3399722 2 * 1108925
hz₉₉ : LT.lt (α := ℕ) 0 345307
hz₁₀₀ : LT.lt (α := ℕ) 0 1108925
hz₁₀₁ :
  (HMul.hMul (α := ℕ) 2 345307 + 690406) * HPow.hPow (α := ℕ) (β := ℕ) 1108925 2 ≤
    HPow.hPow (α := ℕ) (β := ℕ) 2217683 2 * 345307
hz₁₀₂ : LT.lt (α := ℕ) 0 139887
hz₁₀₃ : LT.lt (α := ℕ) 0 345307
hz₁₀₄ :
  (HMul.hMul (α := ℕ) 2 139887 + 279437) * HPow.hPow (α := ℕ) (β := ℕ) 345307 2 ≤
    HPow.hPow (α := ℕ) (β := ℕ) 690406 2 * 139887
hz₁₀₅ : LT.lt (α := ℕ) 0 64690
hz₁₀₆ : LT.lt (α := ℕ) 0 139887
hz₁₀₇ :
  (HMul.hMul (α := ℕ) 2 64690 + 128757) * HPow.hPow (α := ℕ) (β := ℕ) 139887 2 ≤
    HPow.hPow (α := ℕ) (β := ℕ) 279437 2 * 64690
hz₁₀₈ : LT.lt (α := ℕ) 0 27557
hz₁₀₉ : LT.lt (α := ℕ) 0 64690
hz₁₁₀ :
  (HMul.hMul (α := ℕ) 2 27557 + 54055) * HPow.hPow (α := ℕ) (β := ℕ) 64690 2 ≤
    HPow.hPow (α := ℕ) (β := ℕ) 128757 2 * 27557
hz₁₁₁ : LT.lt (α := ℕ) 0 4217
hz₁₁₂ : LT.lt (α := ℕ) 0 27557
hz₁₁₃ :
  (HMul.hMul (α := ℕ) 2 4217 + 7792) * HPow.hPow (α := ℕ) (β := ℕ) 27557 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 54055 2 * 4217
hz₁₁₄ : LT.lt (α := ℕ) 0 8119
hz₁₁₅ : LT.lt (α := ℕ) 0 4217
hz₁₁₆ :
  (HMul.hMul (α := ℕ) 2 8119 + 11482) * HPow.hPow (α := ℕ) (β := ℕ) 4217 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 7792 2 * 8119
hb₈ : LT.lt (α := ℕ) 0 1
hd₈ : LT.lt (α := ℕ) 0 8119
h₈ : (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 8119 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 11482 2 * 1
hz₁₁₇ :
  (HDiv.hDiv (α := ℝ) (↑40797266 : ℝ) (↑20398657 : ℝ)).sqrtTwoAddSeries 0 ≤
    2 - HPow.hPow (β := ℕ) (3.141592 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 10 1)) 2
hz₁₁₈ : LT.lt (α := ℕ) 0 3293535
⊢ 3.141592 < π
have hz₁₁₉ : LT.lt (α := ℕ) 0 20398657
Tactic: pi_lower_bound [
    11482/8119, 7792/4217, 54055/27557, 2-623/64690, 2-337/139887, 2-208/345307, 2-167/1108925,
    2-64/1699893, 2-31/3293535, 2-48/20398657]