-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
pi_lower_bound :
  (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries 6 ≤
    2 - HPow.hPow (β := ℕ) (3.1415 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 6 1)) 2
hz :
  (HDiv.hDiv (α := ℝ) (↑1970 : ℝ) (↑1393 : ℝ)).sqrtTwoAddSeries 5 ≤
    2 - HPow.hPow (β := ℕ) (3.1415 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 6 1)) 2
hb : LT.lt (α := ℕ) 0 1
hd : LT.lt (α := ℕ) 0 1393
h : (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 1393 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 1970 2 * 1
hz₁ :
  (HDiv.hDiv (α := ℝ) (↑3010 : ℝ) (↑1629 : ℝ)).sqrtTwoAddSeries 4 ≤
    2 - HPow.hPow (β := ℕ) (3.1415 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 6 1)) 2
hz₂ : LT.lt (α := ℕ) 0 1393
hz₃ : LT.lt (α := ℕ) 0 1629
hz₄ :
  (HMul.hMul (α := ℕ) 2 1393 + 1970) * HPow.hPow (α := ℕ) (β := ℕ) 1629 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 3010 2 * 1393
hb₁ : LT.lt (α := ℕ) 0 1
hd₁ : LT.lt (α := ℕ) 0 1393
h₁ : (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 1393 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 1970 2 * 1
hz₅ :
  (HDiv.hDiv (α := ℝ) (↑11689 : ℝ) (↑5959 : ℝ)).sqrtTwoAddSeries 3 ≤
    2 - HPow.hPow (β := ℕ) (3.1415 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 6 1)) 2
hz₆ : LT.lt (α := ℕ) 0 1629
hz₇ : LT.lt (α := ℕ) 0 5959
hz₈ :
  (HMul.hMul (α := ℕ) 2 1629 + 3010) * HPow.hPow (α := ℕ) (β := ℕ) 5959 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 11689 2 * 1629
hz₉ : LT.lt (α := ℕ) 0 1393
hz₁₀ : LT.lt (α := ℕ) 0 1629
hz₁₁ :
  (HMul.hMul (α := ℕ) 2 1393 + 1970) * HPow.hPow (α := ℕ) (β := ℕ) 1629 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 3010 2 * 1393
hb₂ : LT.lt (α := ℕ) 0 1
hd₂ : LT.lt (α := ℕ) 0 1393
h₂ : (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 1393 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 1970 2 * 1
hz₁₂ :
  (HDiv.hDiv (α := ℝ) (↑10127 : ℝ) (↑5088 : ℝ)).sqrtTwoAddSeries 2 ≤
    2 - HPow.hPow (β := ℕ) (3.1415 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 6 1)) 2
hz₁₃ : LT.lt (α := ℕ) 0 5959
hz₁₄ : LT.lt (α := ℕ) 0 5088
hz₁₅ :
  (HMul.hMul (α := ℕ) 2 5959 + 11689) * HPow.hPow (α := ℕ) (β := ℕ) 5088 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 10127 2 * 5959
hz₁₆ : LT.lt (α := ℕ) 0 1629
hz₁₇ : LT.lt (α := ℕ) 0 5959
hz₁₈ :
  (HMul.hMul (α := ℕ) 2 1629 + 3010) * HPow.hPow (α := ℕ) (β := ℕ) 5959 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 11689 2 * 1629
hz₁₉ : LT.lt (α := ℕ) 0 1393
hz₂₀ : LT.lt (α := ℕ) 0 1629
hz₂₁ :
  (HMul.hMul (α := ℕ) 2 1393 + 1970) * HPow.hPow (α := ℕ) (β := ℕ) 1629 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 3010 2 * 1393
hb₃ : LT.lt (α := ℕ) 0 1
hd₃ : LT.lt (α := ℕ) 0 1393
h₃ : (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 1393 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 1970 2 * 1
hz₂₂ :
  (HDiv.hDiv (α := ℝ) (↑33997 : ℝ) (↑17019 : ℝ)).sqrtTwoAddSeries 1 ≤
    2 - HPow.hPow (β := ℕ) (3.1415 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 6 1)) 2
hz₂₃ : LT.lt (α := ℕ) 0 5088
hz₂₄ : LT.lt (α := ℕ) 0 17019
hz₂₅ :
  (HMul.hMul (α := ℕ) 2 5088 + 10127) * HPow.hPow (α := ℕ) (β := ℕ) 17019 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 33997 2 * 5088
hz₂₆ : LT.lt (α := ℕ) 0 5959
hz₂₇ : LT.lt (α := ℕ) 0 5088
hz₂₈ :
  (HMul.hMul (α := ℕ) 2 5959 + 11689) * HPow.hPow (α := ℕ) (β := ℕ) 5088 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 10127 2 * 5959
hz₂₉ : LT.lt (α := ℕ) 0 1629
hz₃₀ : LT.lt (α := ℕ) 0 5959
hz₃₁ :
  (HMul.hMul (α := ℕ) 2 1629 + 3010) * HPow.hPow (α := ℕ) (β := ℕ) 5959 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 11689 2 * 1629
hz₃₂ : LT.lt (α := ℕ) 0 1393
hz₃₃ : LT.lt (α := ℕ) 0 1629
hz₃₄ :
  (HMul.hMul (α := ℕ) 2 1393 + 1970) * HPow.hPow (α := ℕ) (β := ℕ) 1629 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 3010 2 * 1393
hb₄ : LT.lt (α := ℕ) 0 1
hd₄ : LT.lt (α := ℕ) 0 1393
h₄ : (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 1393 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 1970 2 * 1
hz₃₅ :
  (HDiv.hDiv (α := ℝ) (↑23235 : ℝ) (↑11621 : ℝ)).sqrtTwoAddSeries 0 ≤
    2 - HPow.hPow (β := ℕ) (3.1415 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 6 1)) 2
hz₃₆ : LT.lt (α := ℕ) 0 17019
⊢ 3.1415 < π
have hz₃₇ : LT.lt (α := ℕ) 0 11621
Tactic: pi_lower_bound [
    1970 / 1393, 3010 / 1629, 11689 / 5959, 10127 / 5088, 33997 / 17019, 23235 / 11621]