awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
n : ℕ
a : ℝ
h :
  2 - HPow.hPow (β := ℕ) ((a - 1 / HPow.hPow (α := ℝ) 4 n) / HPow.hPow (α := ℝ) 2 (n + 1)) 2 ≤
    (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries n
h₂ : 1 / HPow.hPow (α := ℝ) 4 n ≤ a
rwa :
  ∀
    (h :
      2 - HPow.hPow (β := ℕ) ((a - 1 / HPow.hPow (α := ℝ) 4 n) / HPow.hPow (α := ℝ) 2 (n + 1)) 2 ≤
        (HDiv.hDiv (α := ℝ) 0 (↑1 : ℝ)).sqrtTwoAddSeries n)
    (h₂ : 1 / HPow.hPow (α := ℝ) 4 n ≤ a),
    2 - HPow.hPow (β := ℕ) ((a - 1 / HPow.hPow (α := ℝ) 4 n) / HPow.hPow (α := ℝ) 2 (n + 1)) 2 ≤ sqrtTwoAddSeries 0 n
⊢ 2 - HPow.hPow (β := ℕ) ((a - 1 / HPow.hPow (α := ℝ) 4 n) / HPow.hPow (α := ℝ) 2 (n + 1)) 2 ≤ sqrtTwoAddSeries 0 n
have rwa₁ : ∀
  (h :
    2 - HPow.hPow (β := ℕ) ((a - 1 / HPow.hPow (α := ℝ) 4 n) / HPow.hPow (α := ℝ) 2 (n + 1)) 2 ≤ sqrtTwoAddSeries 0 n)
  (h₂ : 1 / HPow.hPow (α := ℝ) 4 n ≤ a),
  2 - HPow.hPow (β := ℕ) ((a - 1 / HPow.hPow (α := ℝ) 4 n) / HPow.hPow (α := ℝ) 2 (n + 1)) 2 ≤ sqrtTwoAddSeries 0 n
Tactic: rwa [Nat.cast_zero, zero_div] at h
Cleared hypotheses: h, h₂
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
a b c d n : ℕ
z : ℝ
hz : z ≤ (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)).sqrtTwoAddSeries n
hb : 0 < b
hd : 0 < d
h : HPow.hPow (β := ℕ) a 2 * d ≤ (2 * d + c) * HPow.hPow (β := ℕ) b 2
⊢ z ≤ (HDiv.hDiv (α := ℝ) (↑c : ℝ) (↑d : ℝ)).sqrtTwoAddSeries (n + 1)
have apply : (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)).sqrtTwoAddSeries n ≤
  (HDiv.hDiv (α := ℝ) (↑c : ℝ) (↑d : ℝ)).sqrtTwoAddSeries (n + 1)
Tactic: apply le_trans hz
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
a b c d n : ℕ
z : ℝ
hz : z ≤ (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)).sqrtTwoAddSeries n
hb : 0 < b
hd : 0 < d
h : HPow.hPow (β := ℕ) a 2 * d ≤ (2 * d + c) * HPow.hPow (β := ℕ) b 2
⊢ (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)).sqrtTwoAddSeries n ≤
    (HDiv.hDiv (α := ℝ) (↑c : ℝ) (↑d : ℝ)).sqrtTwoAddSeries (n + 1)
have rw : (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)).sqrtTwoAddSeries n ≤
  (√(2 + HDiv.hDiv (α := ℝ) (↑c : ℝ) (↑d : ℝ))).sqrtTwoAddSeries n
Tactic: rw [sqrtTwoAddSeries_succ]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
a b c d n : ℕ
z : ℝ
hz : z ≤ (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)).sqrtTwoAddSeries n
hb : 0 < b
hd : 0 < d
h : HPow.hPow (β := ℕ) a 2 * d ≤ (2 * d + c) * HPow.hPow (β := ℕ) b 2
⊢ (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)).sqrtTwoAddSeries n ≤
    (√(2 + HDiv.hDiv (α := ℝ) (↑c : ℝ) (↑d : ℝ))).sqrtTwoAddSeries n
have h₁ : HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ) ≤ √(2 + HDiv.hDiv (α := ℝ) (↑c : ℝ) (↑d : ℝ))
Tactic: apply sqrtTwoAddSeries_monotone_left
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
a b c d n : ℕ
z : ℝ
hz : z ≤ (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)).sqrtTwoAddSeries n
hb : 0 < b
hd : 0 < d
h : HPow.hPow (β := ℕ) a 2 * d ≤ (2 * d + c) * HPow.hPow (β := ℕ) b 2
⊢ HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ) ≤ √(2 + HDiv.hDiv (α := ℝ) (↑c : ℝ) (↑d : ℝ))
have h₁ : HPow.hPow (β := ℕ) (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) 2 ≤ 2 + HDiv.hDiv (α := ℝ) (↑c : ℝ) (↑d : ℝ)
Tactic: apply le_sqrt_of_sq_le
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (hypothesis)
Goal:
a b c d n : ℕ
z : ℝ
hz : z ≤ (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)).sqrtTwoAddSeries n
hb : 0 < b
hd : 0 < d
h : HPow.hPow (β := ℕ) a 2 * d ≤ (2 * d + c) * HPow.hPow (β := ℕ) b 2
⊢ HPow.hPow (β := ℕ) (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) 2 ≤ 2 + HDiv.hDiv (α := ℝ) (↑c : ℝ) (↑d : ℝ)
have hb' : LT.lt (α := ℝ) 0 (↑b : ℝ)
Tactic: have hb' : 0 < (b : ℝ) := Nat.cast_pos.2 hb
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (hypothesis)
Goal:
a b c d n : ℕ
z : ℝ
hz : z ≤ (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)).sqrtTwoAddSeries n
hb : 0 < b
hd : 0 < d
h : HPow.hPow (β := ℕ) a 2 * d ≤ (2 * d + c) * HPow.hPow (β := ℕ) b 2
hb' : LT.lt (α := ℝ) 0 (↑b : ℝ)
⊢ HPow.hPow (β := ℕ) (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) 2 ≤ 2 + HDiv.hDiv (α := ℝ) (↑c : ℝ) (↑d : ℝ)
have hd' : LT.lt (α := ℝ) 0 (↑d : ℝ)
Tactic: have hd' : 0 < (d : ℝ) := Nat.cast_pos.2 hd
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
a b c d n : ℕ
z : ℝ
hz : z ≤ (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)).sqrtTwoAddSeries n
hb : 0 < b
hd : 0 < d
h : HPow.hPow (β := ℕ) a 2 * d ≤ (2 * d + c) * HPow.hPow (β := ℕ) b 2
hb' : LT.lt (α := ℝ) 0 (↑b : ℝ)
hd' : LT.lt (α := ℝ) 0 (↑d : ℝ)
⊢ HPow.hPow (β := ℕ) (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) 2 ≤ 2 + HDiv.hDiv (α := ℝ) (↑c : ℝ) (↑d : ℝ)
have h₁ : HPow.hPow (α := ℝ) (β := ℕ) (↑a : ℝ) 2 * (↑d : ℝ) ≤
  (HMul.hMul (α := ℝ) 2 (↑d : ℝ) + (↑c : ℝ)) * HPow.hPow (α := ℝ) (β := ℕ) (↑b : ℝ) 2
Tactic: rw [div_pow, add_div_eq_mul_add_div _ _ (ne_of_gt hd'), div_le_div_iff₀ (pow_pos hb' _) hd']
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
⊢ 3 < π
have pi_lower_bound : (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries 1 ≤
  2 - HPow.hPow (β := ℕ) (3 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 1 1)) 2
Tactic: pi_lower_bound [23 / 16]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
pi_lower_bound :
  (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries 1 ≤
    2 - HPow.hPow (β := ℕ) (3 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 1 1)) 2
⊢ 3 < π
have hz : (HDiv.hDiv (α := ℝ) (↑23 : ℝ) (↑16 : ℝ)).sqrtTwoAddSeries 0 ≤
  2 - HPow.hPow (β := ℕ) (3 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 1 1)) 2
Tactic: pi_lower_bound [23 / 16]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
pi_lower_bound :
  (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries 1 ≤
    2 - HPow.hPow (β := ℕ) (3 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 1 1)) 2
hz :
  (HDiv.hDiv (α := ℝ) (↑23 : ℝ) (↑16 : ℝ)).sqrtTwoAddSeries 0 ≤
    2 - HPow.hPow (β := ℕ) (3 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 1 1)) 2
⊢ 3 < π
have hb : LT.lt (α := ℕ) 0 1
Tactic: pi_lower_bound [23 / 16]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
pi_lower_bound :
  (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries 1 ≤
    2 - HPow.hPow (β := ℕ) (3 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 1 1)) 2
hz :
  (HDiv.hDiv (α := ℝ) (↑23 : ℝ) (↑16 : ℝ)).sqrtTwoAddSeries 0 ≤
    2 - HPow.hPow (β := ℕ) (3 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 1 1)) 2
hb : LT.lt (α := ℕ) 0 1
⊢ 3 < π
have hd : LT.lt (α := ℕ) 0 16
Tactic: pi_lower_bound [23 / 16]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
pi_lower_bound :
  (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries 1 ≤
    2 - HPow.hPow (β := ℕ) (3 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 1 1)) 2
hz :
  (HDiv.hDiv (α := ℝ) (↑23 : ℝ) (↑16 : ℝ)).sqrtTwoAddSeries 0 ≤
    2 - HPow.hPow (β := ℕ) (3 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 1 1)) 2
hb : LT.lt (α := ℕ) 0 1
hd : LT.lt (α := ℕ) 0 16
⊢ 3 < π
have h : (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 16 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 23 2 * 1
Tactic: pi_lower_bound [23 / 16]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
pi_lower_bound :
  (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries 1 ≤
    2 - HPow.hPow (β := ℕ) (3 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 1 1)) 2
hz :
  (HDiv.hDiv (α := ℝ) (↑23 : ℝ) (↑16 : ℝ)).sqrtTwoAddSeries 0 ≤
    2 - HPow.hPow (β := ℕ) (3 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 1 1)) 2
hb : LT.lt (α := ℕ) 0 1
hd : LT.lt (α := ℕ) 0 16
h : (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 16 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 23 2 * 1
⊢ 3 < π
have hz₁ : HDiv.hDiv (α := ℝ) 23 16 ≤ 2 - HPow.hPow (β := ℕ) (3 / HPow.hPow (α := ℝ) (β := ℕ) 2 2) 2
Tactic: pi_lower_bound [23 / 16]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
⊢ π < 4
have h : 2 - HPow.hPow (β := ℕ) ((4 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 1) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 1 1)) 2 ≤
  (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries 1
Tactic: pi_upper_bound [4 / 3]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
h :
  2 - HPow.hPow (β := ℕ) ((4 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 1) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 1 1)) 2 ≤
    (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries 1
⊢ π < 4
have h₂ : 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 1 ≤ 4
Tactic: pi_upper_bound [4 / 3]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
h :
  2 - HPow.hPow (β := ℕ) ((4 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 1) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 1 1)) 2 ≤
    (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries 1
h₂ : 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 1 ≤ 4
⊢ π < 4
have h₁ : 2 - HPow.hPow (β := ℕ) ((4 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 1) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 1 1)) 2 ≤
  (HDiv.hDiv (α := ℝ) (↑4 : ℝ) (↑3 : ℝ)).sqrtTwoAddSeries 0
Tactic: pi_upper_bound [4 / 3]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
h :
  2 - HPow.hPow (β := ℕ) ((4 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 1) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 1 1)) 2 ≤
    (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries 1
h₂ : 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 1 ≤ 4
h₁ :
  2 - HPow.hPow (β := ℕ) ((4 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 1) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 1 1)) 2 ≤
    (HDiv.hDiv (α := ℝ) (↑4 : ℝ) (↑3 : ℝ)).sqrtTwoAddSeries 0
⊢ π < 4
have h₃ : LT.lt (α := ℕ) 0 3
Tactic: pi_upper_bound [4 / 3]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
h :
  2 - HPow.hPow (β := ℕ) ((4 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 1) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 1 1)) 2 ≤
    (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries 1
h₂ : 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 1 ≤ 4
h₁ :
  2 - HPow.hPow (β := ℕ) ((4 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 1) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 1 1)) 2 ≤
    (HDiv.hDiv (α := ℝ) (↑4 : ℝ) (↑3 : ℝ)).sqrtTwoAddSeries 0
h₃ : LT.lt (α := ℕ) 0 3
⊢ π < 4
have h₄ : LT.lt (α := ℕ) 0 1
Tactic: pi_upper_bound [4 / 3]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
h :
  2 - HPow.hPow (β := ℕ) ((4 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 1) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 1 1)) 2 ≤
    (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries 1
h₂ : 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 1 ≤ 4
h₁ :
  2 - HPow.hPow (β := ℕ) ((4 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 1) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 1 1)) 2 ≤
    (HDiv.hDiv (α := ℝ) (↑4 : ℝ) (↑3 : ℝ)).sqrtTwoAddSeries 0
h₃ : LT.lt (α := ℕ) 0 3
h₄ : LT.lt (α := ℕ) 0 1
⊢ π < 4
have h₅ : HPow.hPow (α := ℕ) (β := ℕ) 4 2 * 1 ≤ (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 3 2
Tactic: pi_upper_bound [4 / 3]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
h :
  2 - HPow.hPow (β := ℕ) ((4 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 1) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 1 1)) 2 ≤
    (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries 1
h₂ : 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 1 ≤ 4
h₁ :
  2 - HPow.hPow (β := ℕ) ((4 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 1) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 1 1)) 2 ≤
    (HDiv.hDiv (α := ℝ) (↑4 : ℝ) (↑3 : ℝ)).sqrtTwoAddSeries 0
h₃ : LT.lt (α := ℕ) 0 3
h₄ : LT.lt (α := ℕ) 0 1
h₅ : HPow.hPow (α := ℕ) (β := ℕ) 4 2 * 1 ≤ (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 3 2
h₆ : 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 1 ≤ 4
⊢ π < 4
have h₇ : 2 ≤ HDiv.hDiv (α := ℝ) 4 3 + HPow.hPow (β := ℕ) (HSub.hSub (α := ℝ) 4 4⁻¹ / HPow.hPow (α := ℝ) (β := ℕ) 2 2) 2
Tactic: pi_upper_bound [4 / 3]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
⊢ 3.14 < π
have pi_lower_bound : (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries 4 ≤
  2 - HPow.hPow (β := ℕ) (3.14 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1)) 2
Tactic: pi_lower_bound [338 / 239, 704 / 381, 1940 / 989, 1447 / 727]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
pi_lower_bound :
  (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries 4 ≤
    2 - HPow.hPow (β := ℕ) (3.14 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1)) 2
⊢ 3.14 < π
have hz : (HDiv.hDiv (α := ℝ) (↑338 : ℝ) (↑239 : ℝ)).sqrtTwoAddSeries 3 ≤
  2 - HPow.hPow (β := ℕ) (3.14 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1)) 2
Tactic: pi_lower_bound [338 / 239, 704 / 381, 1940 / 989, 1447 / 727]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
pi_lower_bound :
  (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries 4 ≤
    2 - HPow.hPow (β := ℕ) (3.14 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1)) 2
hz :
  (HDiv.hDiv (α := ℝ) (↑338 : ℝ) (↑239 : ℝ)).sqrtTwoAddSeries 3 ≤
    2 - HPow.hPow (β := ℕ) (3.14 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1)) 2
⊢ 3.14 < π
have hb : LT.lt (α := ℕ) 0 1
Tactic: pi_lower_bound [338 / 239, 704 / 381, 1940 / 989, 1447 / 727]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
pi_lower_bound :
  (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries 4 ≤
    2 - HPow.hPow (β := ℕ) (3.14 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1)) 2
hz :
  (HDiv.hDiv (α := ℝ) (↑338 : ℝ) (↑239 : ℝ)).sqrtTwoAddSeries 3 ≤
    2 - HPow.hPow (β := ℕ) (3.14 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1)) 2
hb : LT.lt (α := ℕ) 0 1
⊢ 3.14 < π
have hd : LT.lt (α := ℕ) 0 239
Tactic: pi_lower_bound [338 / 239, 704 / 381, 1940 / 989, 1447 / 727]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
pi_lower_bound :
  (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries 4 ≤
    2 - HPow.hPow (β := ℕ) (3.14 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1)) 2
hz :
  (HDiv.hDiv (α := ℝ) (↑338 : ℝ) (↑239 : ℝ)).sqrtTwoAddSeries 3 ≤
    2 - HPow.hPow (β := ℕ) (3.14 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1)) 2
hb : LT.lt (α := ℕ) 0 1
hd : LT.lt (α := ℕ) 0 239
⊢ 3.14 < π
have h : (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 239 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 338 2 * 1
Tactic: pi_lower_bound [338 / 239, 704 / 381, 1940 / 989, 1447 / 727]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
pi_lower_bound :
  (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries 4 ≤
    2 - HPow.hPow (β := ℕ) (3.14 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1)) 2
hz :
  (HDiv.hDiv (α := ℝ) (↑338 : ℝ) (↑239 : ℝ)).sqrtTwoAddSeries 3 ≤
    2 - HPow.hPow (β := ℕ) (3.14 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1)) 2
hb : LT.lt (α := ℕ) 0 1
hd : LT.lt (α := ℕ) 0 239
h : (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 239 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 338 2 * 1
⊢ 3.14 < π
have hz₁ : (HDiv.hDiv (α := ℝ) (↑704 : ℝ) (↑381 : ℝ)).sqrtTwoAddSeries 2 ≤
  2 - HPow.hPow (β := ℕ) (3.14 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1)) 2
Tactic: pi_lower_bound [338 / 239, 704 / 381, 1940 / 989, 1447 / 727]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
pi_lower_bound :
  (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries 4 ≤
    2 - HPow.hPow (β := ℕ) (3.14 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1)) 2
hz :
  (HDiv.hDiv (α := ℝ) (↑338 : ℝ) (↑239 : ℝ)).sqrtTwoAddSeries 3 ≤
    2 - HPow.hPow (β := ℕ) (3.14 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1)) 2
hb : LT.lt (α := ℕ) 0 1
hd : LT.lt (α := ℕ) 0 239
h : (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 239 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 338 2 * 1
hz₁ :
  (HDiv.hDiv (α := ℝ) (↑704 : ℝ) (↑381 : ℝ)).sqrtTwoAddSeries 2 ≤
    2 - HPow.hPow (β := ℕ) (3.14 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1)) 2
hz₂ : LT.lt (α := ℕ) 0 239
⊢ 3.14 < π
have hz₃ : LT.lt (α := ℕ) 0 381
Tactic: pi_lower_bound [338 / 239, 704 / 381, 1940 / 989, 1447 / 727]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
pi_lower_bound :
  (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries 4 ≤
    2 - HPow.hPow (β := ℕ) (3.14 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1)) 2
hz :
  (HDiv.hDiv (α := ℝ) (↑338 : ℝ) (↑239 : ℝ)).sqrtTwoAddSeries 3 ≤
    2 - HPow.hPow (β := ℕ) (3.14 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1)) 2
hb : LT.lt (α := ℕ) 0 1
hd : LT.lt (α := ℕ) 0 239
h : (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 239 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 338 2 * 1
hz₁ :
  (HDiv.hDiv (α := ℝ) (↑704 : ℝ) (↑381 : ℝ)).sqrtTwoAddSeries 2 ≤
    2 - HPow.hPow (β := ℕ) (3.14 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1)) 2
hz₂ : LT.lt (α := ℕ) 0 239
hz₃ : LT.lt (α := ℕ) 0 381
⊢ 3.14 < π
have hz₄ : (HMul.hMul (α := ℕ) 2 239 + 338) * HPow.hPow (α := ℕ) (β := ℕ) 381 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 704 2 * 239
Tactic: pi_lower_bound [338 / 239, 704 / 381, 1940 / 989, 1447 / 727]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
pi_lower_bound :
  (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries 4 ≤
    2 - HPow.hPow (β := ℕ) (3.14 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1)) 2
hz :
  (HDiv.hDiv (α := ℝ) (↑338 : ℝ) (↑239 : ℝ)).sqrtTwoAddSeries 3 ≤
    2 - HPow.hPow (β := ℕ) (3.14 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1)) 2
hb : LT.lt (α := ℕ) 0 1
hd : LT.lt (α := ℕ) 0 239
h : (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 239 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 338 2 * 1
hz₁ :
  (HDiv.hDiv (α := ℝ) (↑704 : ℝ) (↑381 : ℝ)).sqrtTwoAddSeries 2 ≤
    2 - HPow.hPow (β := ℕ) (3.14 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1)) 2
hz₂ : LT.lt (α := ℕ) 0 239
hz₃ : LT.lt (α := ℕ) 0 381
hz₄ : (HMul.hMul (α := ℕ) 2 239 + 338) * HPow.hPow (α := ℕ) (β := ℕ) 381 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 704 2 * 239
hb₁ : LT.lt (α := ℕ) 0 1
hd₁ : LT.lt (α := ℕ) 0 239
h₁ : (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 239 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 338 2 * 1
⊢ 3.14 < π
have hz₅ : (HDiv.hDiv (α := ℝ) (↑1940 : ℝ) (↑989 : ℝ)).sqrtTwoAddSeries 1 ≤
  2 - HPow.hPow (β := ℕ) (3.14 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1)) 2
Tactic: pi_lower_bound [338 / 239, 704 / 381, 1940 / 989, 1447 / 727]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
pi_lower_bound :
  (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries 4 ≤
    2 - HPow.hPow (β := ℕ) (3.14 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1)) 2
hz :
  (HDiv.hDiv (α := ℝ) (↑338 : ℝ) (↑239 : ℝ)).sqrtTwoAddSeries 3 ≤
    2 - HPow.hPow (β := ℕ) (3.14 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1)) 2
hb : LT.lt (α := ℕ) 0 1
hd : LT.lt (α := ℕ) 0 239
h : (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 239 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 338 2 * 1
hz₁ :
  (HDiv.hDiv (α := ℝ) (↑704 : ℝ) (↑381 : ℝ)).sqrtTwoAddSeries 2 ≤
    2 - HPow.hPow (β := ℕ) (3.14 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1)) 2
hz₂ : LT.lt (α := ℕ) 0 239
hz₃ : LT.lt (α := ℕ) 0 381
hz₄ : (HMul.hMul (α := ℕ) 2 239 + 338) * HPow.hPow (α := ℕ) (β := ℕ) 381 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 704 2 * 239
hb₁ : LT.lt (α := ℕ) 0 1
hd₁ : LT.lt (α := ℕ) 0 239
h₁ : (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 239 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 338 2 * 1
hz₅ :
  (HDiv.hDiv (α := ℝ) (↑1940 : ℝ) (↑989 : ℝ)).sqrtTwoAddSeries 1 ≤
    2 - HPow.hPow (β := ℕ) (3.14 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1)) 2
hz₆ : LT.lt (α := ℕ) 0 381
⊢ 3.14 < π
have hz₇ : LT.lt (α := ℕ) 0 989
Tactic: pi_lower_bound [338 / 239, 704 / 381, 1940 / 989, 1447 / 727]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
pi_lower_bound :
  (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries 4 ≤
    2 - HPow.hPow (β := ℕ) (3.14 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1)) 2
hz :
  (HDiv.hDiv (α := ℝ) (↑338 : ℝ) (↑239 : ℝ)).sqrtTwoAddSeries 3 ≤
    2 - HPow.hPow (β := ℕ) (3.14 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1)) 2
hb : LT.lt (α := ℕ) 0 1
hd : LT.lt (α := ℕ) 0 239
h : (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 239 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 338 2 * 1
hz₁ :
  (HDiv.hDiv (α := ℝ) (↑704 : ℝ) (↑381 : ℝ)).sqrtTwoAddSeries 2 ≤
    2 - HPow.hPow (β := ℕ) (3.14 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1)) 2
hz₂ : LT.lt (α := ℕ) 0 239
hz₃ : LT.lt (α := ℕ) 0 381
hz₄ : (HMul.hMul (α := ℕ) 2 239 + 338) * HPow.hPow (α := ℕ) (β := ℕ) 381 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 704 2 * 239
hb₁ : LT.lt (α := ℕ) 0 1
hd₁ : LT.lt (α := ℕ) 0 239
h₁ : (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 239 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 338 2 * 1
hz₅ :
  (HDiv.hDiv (α := ℝ) (↑1940 : ℝ) (↑989 : ℝ)).sqrtTwoAddSeries 1 ≤
    2 - HPow.hPow (β := ℕ) (3.14 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1)) 2
hz₆ : LT.lt (α := ℕ) 0 381
hz₇ : LT.lt (α := ℕ) 0 989
⊢ 3.14 < π
have hz₈ : (HMul.hMul (α := ℕ) 2 381 + 704) * HPow.hPow (α := ℕ) (β := ℕ) 989 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 1940 2 * 381
Tactic: pi_lower_bound [338 / 239, 704 / 381, 1940 / 989, 1447 / 727]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
pi_lower_bound :
  (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries 4 ≤
    2 - HPow.hPow (β := ℕ) (3.14 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1)) 2
hz :
  (HDiv.hDiv (α := ℝ) (↑338 : ℝ) (↑239 : ℝ)).sqrtTwoAddSeries 3 ≤
    2 - HPow.hPow (β := ℕ) (3.14 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1)) 2
hb : LT.lt (α := ℕ) 0 1
hd : LT.lt (α := ℕ) 0 239
h : (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 239 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 338 2 * 1
hz₁ :
  (HDiv.hDiv (α := ℝ) (↑704 : ℝ) (↑381 : ℝ)).sqrtTwoAddSeries 2 ≤
    2 - HPow.hPow (β := ℕ) (3.14 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1)) 2
hz₂ : LT.lt (α := ℕ) 0 239
hz₃ : LT.lt (α := ℕ) 0 381
hz₄ : (HMul.hMul (α := ℕ) 2 239 + 338) * HPow.hPow (α := ℕ) (β := ℕ) 381 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 704 2 * 239
hb₁ : LT.lt (α := ℕ) 0 1
hd₁ : LT.lt (α := ℕ) 0 239
h₁ : (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 239 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 338 2 * 1
hz₅ :
  (HDiv.hDiv (α := ℝ) (↑1940 : ℝ) (↑989 : ℝ)).sqrtTwoAddSeries 1 ≤
    2 - HPow.hPow (β := ℕ) (3.14 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1)) 2
hz₆ : LT.lt (α := ℕ) 0 381
hz₇ : LT.lt (α := ℕ) 0 989
hz₈ : (HMul.hMul (α := ℕ) 2 381 + 704) * HPow.hPow (α := ℕ) (β := ℕ) 989 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 1940 2 * 381
hz₉ : LT.lt (α := ℕ) 0 239
hz₁₀ : LT.lt (α := ℕ) 0 381
hz₁₁ : (HMul.hMul (α := ℕ) 2 239 + 338) * HPow.hPow (α := ℕ) (β := ℕ) 381 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 704 2 * 239
hb₂ : LT.lt (α := ℕ) 0 1
hd₂ : LT.lt (α := ℕ) 0 239
h₂ : (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 239 2 ≤ HPow.hPow (α := ℕ) (β := ℕ) 338 2 * 1
⊢ 3.14 < π
have hz₁₂ : (HDiv.hDiv (α := ℝ) (↑1447 : ℝ) (↑727 : ℝ)).sqrtTwoAddSeries 0 ≤
  2 - HPow.hPow (β := ℕ) (3.14 / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 4 1)) 2
Tactic: pi_lower_bound [338 / 239, 704 / 381, 1940 / 989, 1447 / 727]