awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Real.Pi.Bounds
Goal:
n : ℕ
a : ℝ
h :
  (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries n ≤
    2 - HPow.hPow (β := ℕ) (a / HPow.hPow (α := ℝ) 2 (n + 1)) 2
⊢ a < π

Tactic:
lt_of_le_of_lt ?_ (pi_gt_sqrtTwoAddSeries n)

Premises used: lt_of_le_of_lt, Real.pi_gt_sqrtTwoAddSeries
-- Module: Mathlib.Analysis.Real.Pi.Bounds
Goal:
n : ℕ
a : ℝ
h :
  (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries n ≤
    2 - HPow.hPow (β := ℕ) (a / HPow.hPow (α := ℝ) 2 (n + 1)) 2
refine : a ≤ HPow.hPow (α := ℝ) 2 (n + 1) * √(2 - sqrtTwoAddSeries 0 n)
⊢ a < π

Tactic:
refine lt_of_le_of_lt ?_ (pi_gt_sqrtTwoAddSeries n)

Premises used: lt_of_le_of_lt, Real.pi_gt_sqrtTwoAddSeries
-- Module: Mathlib.Analysis.Real.Pi.Bounds
Goal:
n : ℕ
a : ℝ
h :
  (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries n ≤
    2 - HPow.hPow (β := ℕ) (a / HPow.hPow (α := ℝ) 2 (n + 1)) 2
rw : a ≤ √(2 - sqrtTwoAddSeries 0 n) * HPow.hPow (α := ℝ) 2 (n + 1)
⊢ a ≤ HPow.hPow (α := ℝ) 2 (n + 1) * √(2 - sqrtTwoAddSeries 0 n)

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Analysis.Real.Pi.Bounds
Goal:
n : ℕ
a : ℝ
h :
  (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries n ≤
    2 - HPow.hPow (β := ℕ) (a / HPow.hPow (α := ℝ) 2 (n + 1)) 2
⊢ LT.lt (α := ℝ) 0 2

Tactic:
simp
-- Module: Mathlib.Analysis.Real.Pi.Bounds
Goal:
n : ℕ
a : ℝ
h :
  (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries n ≤
    2 - HPow.hPow (β := ℕ) (a / HPow.hPow (α := ℝ) 2 (n + 1)) 2
refine : HPow.hPow (β := ℕ) (a / HPow.hPow (α := ℝ) 2 (n + 1)) 2 ≤ 2 - sqrtTwoAddSeries 0 n
⊢ a ≤ √(2 - sqrtTwoAddSeries 0 n) * HPow.hPow (α := ℝ) 2 (n + 1)

Tactic:
refine (div_le_iff₀ (pow_pos (by simp) _)).mp (le_sqrt_of_sq_le ?_)

Premises used: div_le_iff₀, pow_pos, Real.le_sqrt_of_sq_le, Iff.mp
-- Module: Mathlib.Analysis.Real.Pi.Bounds
Goal:
n : ℕ
a : ℝ
h :
  (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries n ≤
    2 - HPow.hPow (β := ℕ) (a / HPow.hPow (α := ℝ) 2 (n + 1)) 2
rw : 0 = HDiv.hDiv (α := ℝ) 0 (↑1 : ℝ)
rw₁ rw₂ : Eq (α := ℝ) 0 0
⊢ 0 = HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)

Tactic:
rw [Nat.cast_zero, zero_div]

Premises used: zero_div, Nat.cast_zero
-- Module: Mathlib.Analysis.Real.Pi.Bounds
Goal:
n : ℕ
a : ℝ
h :
  (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries n ≤
    2 - HPow.hPow (β := ℕ) (a / HPow.hPow (α := ℝ) 2 (n + 1)) 2
rwa : sqrtTwoAddSeries 0 n ≤ 2 - HPow.hPow (β := ℕ) (a / HPow.hPow (α := ℝ) 2 (n + 1)) 2
rwa₁ rwa₂ rwa₃ rwa₄ :
  (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries n ≤
    2 - HPow.hPow (β := ℕ) (a / HPow.hPow (α := ℝ) 2 (n + 1)) 2
⊢ HPow.hPow (β := ℕ) (a / HPow.hPow (α := ℝ) 2 (n + 1)) 2 ≤ 2 - sqrtTwoAddSeries 0 n

Tactic:
rwa [le_sub_comm, show (0 : ℝ) = (0 : ℕ) / (1 : ℕ) by rw [Nat.cast_zero, zero_div]]

Premises used: le_sub_comm
-- Module: Mathlib.Analysis.Real.Pi.Bounds
Goal:
c d a b n : ℕ
z : ℝ
hz : (HDiv.hDiv (α := ℝ) (↑c : ℝ) (↑d : ℝ)).sqrtTwoAddSeries n ≤ z
hb : 0 < b
hd : 0 < d
h : (2 * b + a) * HPow.hPow (β := ℕ) d 2 ≤ HPow.hPow (β := ℕ) c 2 * b
⊢ (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)).sqrtTwoAddSeries (n + 1) ≤ z

Tactic:
le_trans ?_ hz

Premises used: le_trans
-- Module: Mathlib.Analysis.Real.Pi.Bounds
Goal:
c d a b n : ℕ
z : ℝ
hz : (HDiv.hDiv (α := ℝ) (↑c : ℝ) (↑d : ℝ)).sqrtTwoAddSeries n ≤ z
hb : 0 < b
hd : 0 < d
h : (2 * b + a) * HPow.hPow (β := ℕ) d 2 ≤ HPow.hPow (β := ℕ) c 2 * b
refine :
  (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)).sqrtTwoAddSeries (n + 1) ≤
    (HDiv.hDiv (α := ℝ) (↑c : ℝ) (↑d : ℝ)).sqrtTwoAddSeries n
⊢ (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)).sqrtTwoAddSeries (n + 1) ≤ z

Tactic:
refine le_trans ?_ hz

Premises used: le_trans
-- Module: Mathlib.Analysis.Real.Pi.Bounds
Goal:
c d a b n : ℕ
z : ℝ
hz : (HDiv.hDiv (α := ℝ) (↑c : ℝ) (↑d : ℝ)).sqrtTwoAddSeries n ≤ z
hb : 0 < b
hd : 0 < d
h : (2 * b + a) * HPow.hPow (β := ℕ) d 2 ≤ HPow.hPow (β := ℕ) c 2 * b
rw :
  (√(2 + HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ))).sqrtTwoAddSeries n ≤
    (HDiv.hDiv (α := ℝ) (↑c : ℝ) (↑d : ℝ)).sqrtTwoAddSeries n
⊢ (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)).sqrtTwoAddSeries (n + 1) ≤
    (HDiv.hDiv (α := ℝ) (↑c : ℝ) (↑d : ℝ)).sqrtTwoAddSeries n

Tactic:
rw [sqrtTwoAddSeries_succ]

Premises used: Real.sqrtTwoAddSeries_succ
-- Module: Mathlib.Analysis.Real.Pi.Bounds
Goal:
c d a b n : ℕ
z : ℝ
hz : (HDiv.hDiv (α := ℝ) (↑c : ℝ) (↑d : ℝ)).sqrtTwoAddSeries n ≤ z
hb : 0 < b
hd : 0 < d
h : (2 * b + a) * HPow.hPow (β := ℕ) d 2 ≤ HPow.hPow (β := ℕ) c 2 * b
h₁ : √(2 + HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) ≤ HDiv.hDiv (α := ℝ) (↑c : ℝ) (↑d : ℝ)
⊢ (√(2 + HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ))).sqrtTwoAddSeries n ≤
    (HDiv.hDiv (α := ℝ) (↑c : ℝ) (↑d : ℝ)).sqrtTwoAddSeries n

Tactic:
apply sqrtTwoAddSeries_monotone_left

Premises used: Real.sqrtTwoAddSeries_monotone_left
-- Module: Mathlib.Analysis.Real.Pi.Bounds
Goal:
c d a b n : ℕ
z : ℝ
hz : (HDiv.hDiv (α := ℝ) (↑c : ℝ) (↑d : ℝ)).sqrtTwoAddSeries n ≤ z
hb : 0 < b
hd : 0 < d
h : (2 * b + a) * HPow.hPow (β := ℕ) d 2 ≤ HPow.hPow (β := ℕ) c 2 * b
⊢ LT.lt (α := ℝ) 0 (↑b : ℝ)

Tactic:
have hb' : 0 < (b : ℝ) := Nat.cast_pos.2 hb
-- Module: Mathlib.Analysis.Real.Pi.Bounds
Goal:
c d a b n : ℕ
z : ℝ
hz : (HDiv.hDiv (α := ℝ) (↑c : ℝ) (↑d : ℝ)).sqrtTwoAddSeries n ≤ z
hb : 0 < b
hd : 0 < d
h : (2 * b + a) * HPow.hPow (β := ℕ) d 2 ≤ HPow.hPow (β := ℕ) c 2 * b
hb' : LT.lt (α := ℝ) 0 (↑b : ℝ)
⊢ LT.lt (α := ℝ) 0 (↑d : ℝ)

Tactic:
have hd' : 0 < (d : ℝ) := Nat.cast_pos.2 hd
-- Module: Mathlib.Analysis.Real.Pi.Bounds
Goal:
c d a b n : ℕ
z : ℝ
hz : (HDiv.hDiv (α := ℝ) (↑c : ℝ) (↑d : ℝ)).sqrtTwoAddSeries n ≤ z
hb : 0 < b
hd : 0 < d
h : (2 * b + a) * HPow.hPow (β := ℕ) d 2 ≤ HPow.hPow (β := ℕ) c 2 * b
hb' : LT.lt (α := ℝ) 0 (↑b : ℝ)
hd' : LT.lt (α := ℝ) 0 (↑d : ℝ)
h₁ :
  (HMul.hMul (α := ℝ) 2 (↑b : ℝ) + (↑a : ℝ)) * HPow.hPow (α := ℝ) (β := ℕ) (↑d : ℝ) 2 ≤
    HPow.hPow (α := ℝ) (β := ℕ) (↑c : ℝ) 2 * (↑b : ℝ)
⊢ √(2 + HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) ≤ HDiv.hDiv (α := ℝ) (↑c : ℝ) (↑d : ℝ)

Tactic:
rw [sqrt_le_left (div_nonneg c.cast_nonneg d.cast_nonneg), div_pow,
    add_div_eq_mul_add_div _ _ (ne_of_gt hb'), div_le_div_iff₀ hb' (pow_pos hd' _)]

Premises used: pow_pos, Nat.cast_nonneg, ne_of_gt, div_le_div_iff₀, Real.sqrt_le_left, div_pow, div_nonneg, add_div_eq_mul_add_div
-- Module: Mathlib.Analysis.Real.Pi.Bounds
Goal:
c d a b n : ℕ
z : ℝ
hz : (HDiv.hDiv (α := ℝ) (↑c : ℝ) (↑d : ℝ)).sqrtTwoAddSeries n ≤ z
hb : 0 < b
hd : 0 < d
h : (2 * b + a) * HPow.hPow (β := ℕ) d 2 ≤ HPow.hPow (β := ℕ) c 2 * b
hb' : LT.lt (α := ℝ) 0 (↑b : ℝ)
hd' : LT.lt (α := ℝ) 0 (↑d : ℝ)
⊢ (HMul.hMul (α := ℝ) 2 (↑b : ℝ) + (↑a : ℝ)) * HPow.hPow (α := ℝ) (β := ℕ) (↑d : ℝ) 2 ≤
    HPow.hPow (α := ℝ) (β := ℕ) (↑c : ℝ) 2 * (↑b : ℝ)

Tactic:
mod_cast h

Premises used: Nat.cast_mul._simp_1, HMul.hMul, congrArg, Nat.cast_add._simp_1, cast, Nat.cast_le._simp_1, LE.le, Nat.cast, HPow.hPow, HAdd.hAdd, congr, congrFun', OfNat.ofNat, Eq.symm, Eq.trans, Nat.cast_pow._simp_1
-- Module: Mathlib.Analysis.Real.Pi.Bounds
Goal:
c d a b n : ℕ
z : ℝ
hz : (HDiv.hDiv (α := ℝ) (↑c : ℝ) (↑d : ℝ)).sqrtTwoAddSeries n ≤ z
hb : 0 < b
hd : 0 < d
h : (2 * b + a) * HPow.hPow (β := ℕ) d 2 ≤ HPow.hPow (β := ℕ) c 2 * b
hb' : LT.lt (α := ℝ) 0 (↑b : ℝ)
hd' : LT.lt (α := ℝ) 0 (↑d : ℝ)
⊢ (HMul.hMul (α := ℝ) 2 (↑b : ℝ) + (↑a : ℝ)) * HPow.hPow (α := ℝ) (β := ℕ) (↑d : ℝ) 2 ≤
    HPow.hPow (α := ℝ) (β := ℕ) (↑c : ℝ) 2 * (↑b : ℝ)

Tactic:
exact mod_cast h
-- Module: Mathlib.Analysis.Real.Pi.Bounds
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
⊢ π < a

Tactic:
lt_of_lt_of_le (pi_lt_sqrtTwoAddSeries n) ?_

Premises used: Real.pi_lt_sqrtTwoAddSeries, lt_of_lt_of_le
-- Module: Mathlib.Analysis.Real.Pi.Bounds
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
refine : HPow.hPow (α := ℝ) 2 (n + 1) * √(2 - sqrtTwoAddSeries 0 n) + 1 / HPow.hPow (α := ℝ) 4 n ≤ a
⊢ π < a

Tactic:
refine lt_of_lt_of_le (pi_lt_sqrtTwoAddSeries n) ?_

Premises used: Real.pi_lt_sqrtTwoAddSeries, lt_of_lt_of_le
-- Module: Mathlib.Analysis.Real.Pi.Bounds
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
rw : 2 - HPow.hPow (β := ℕ) ((a - 1 / HPow.hPow (α := ℝ) 4 n) / HPow.hPow (α := ℝ) 2 (n + 1)) 2 ≤ sqrtTwoAddSeries 0 n
rw₁ : 0 ≤ (a - 1 / HPow.hPow (α := ℝ) 4 n) / HPow.hPow (α := ℝ) 2 (n + 1)
rw₂ : 0 < HPow.hPow (α := ℝ) 2 (n + 1)
⊢ HPow.hPow (α := ℝ) 2 (n + 1) * √(2 - sqrtTwoAddSeries 0 n) + 1 / HPow.hPow (α := ℝ) 4 n ≤ a

Tactic:
rw [← le_sub_iff_add_le, ← le_div_iff₀', sqrt_le_left, sub_le_comm]

Premises used: le_div_iff₀', sub_le_comm, Real.sqrt_le_left, le_sub_iff_add_le
-- Module: Mathlib.Analysis.Real.Pi.Bounds
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
rwa₁ rwa₂ rwa₃ 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
⊢ 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

Premises used: zero_div, Nat.cast_zero
-- Module: Mathlib.Analysis.Real.Pi.Bounds
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
⊢ 0 ≤ (a - 1 / HPow.hPow (α := ℝ) 4 n) / HPow.hPow (α := ℝ) 2 (n + 1)

Tactic:
div_nonneg (sub_nonneg.2 h₂) (pow_nonneg (le_of_lt zero_lt_two) _)

Premises used: Iff.mpr, pow_nonneg, le_of_lt, div_nonneg, sub_nonneg
-- Module: Mathlib.Analysis.Real.Pi.Bounds
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
⊢ 0 ≤ (a - 1 / HPow.hPow (α := ℝ) 4 n) / HPow.hPow (α := ℝ) 2 (n + 1)

Tactic:
exact div_nonneg (sub_nonneg.2 h₂) (pow_nonneg (le_of_lt zero_lt_two) _)

Premises used: Iff.mpr, pow_nonneg, le_of_lt, div_nonneg, sub_nonneg
-- Module: Mathlib.Analysis.Real.Pi.Bounds
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
⊢ 0 < HPow.hPow (α := ℝ) 2 (n + 1)

Tactic:
pow_pos zero_lt_two _

Premises used: pow_pos
-- Module: Mathlib.Analysis.Real.Pi.Bounds
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
⊢ 0 < HPow.hPow (α := ℝ) 2 (n + 1)

Tactic:
exact pow_pos zero_lt_two _

Premises used: pow_pos
-- Module: Mathlib.Analysis.Real.Pi.Bounds
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
apply :
  (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)).sqrtTwoAddSeries n ≤
    (HDiv.hDiv (α := ℝ) (↑c : ℝ) (↑d : ℝ)).sqrtTwoAddSeries (n + 1)
⊢ z ≤ (HDiv.hDiv (α := ℝ) (↑c : ℝ) (↑d : ℝ)).sqrtTwoAddSeries (n + 1)

Tactic:
apply le_trans hz

Premises used: le_trans
-- Module: Mathlib.Analysis.Real.Pi.Bounds
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
rw :
  (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)).sqrtTwoAddSeries n ≤
    (√(2 + HDiv.hDiv (α := ℝ) (↑c : ℝ) (↑d : ℝ))).sqrtTwoAddSeries n
⊢ (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)).sqrtTwoAddSeries n ≤
    (HDiv.hDiv (α := ℝ) (↑c : ℝ) (↑d : ℝ)).sqrtTwoAddSeries (n + 1)

Tactic:
rw [sqrtTwoAddSeries_succ]

Premises used: Real.sqrtTwoAddSeries_succ
-- Module: Mathlib.Analysis.Real.Pi.Bounds
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
h₁ : HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ) ≤ √(2 + HDiv.hDiv (α := ℝ) (↑c : ℝ) (↑d : ℝ))
⊢ (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)).sqrtTwoAddSeries n ≤
    (√(2 + HDiv.hDiv (α := ℝ) (↑c : ℝ) (↑d : ℝ))).sqrtTwoAddSeries n

Tactic:
apply sqrtTwoAddSeries_monotone_left

Premises used: Real.sqrtTwoAddSeries_monotone_left
-- Module: Mathlib.Analysis.Real.Pi.Bounds
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
h₁ : HPow.hPow (β := ℕ) (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) 2 ≤ 2 + HDiv.hDiv (α := ℝ) (↑c : ℝ) (↑d : ℝ)
⊢ HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ) ≤ √(2 + HDiv.hDiv (α := ℝ) (↑c : ℝ) (↑d : ℝ))

Tactic:
apply le_sqrt_of_sq_le

Premises used: Real.le_sqrt_of_sq_le
-- Module: Mathlib.Analysis.Real.Pi.Bounds
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
⊢ LT.lt (α := ℝ) 0 (↑b : ℝ)

Tactic:
have hb' : 0 < (b : ℝ) := Nat.cast_pos.2 hb
-- Module: Mathlib.Analysis.Real.Pi.Bounds
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 : ℝ)
⊢ LT.lt (α := ℝ) 0 (↑d : ℝ)

Tactic:
have hd' : 0 < (d : ℝ) := Nat.cast_pos.2 hd
-- Module: Mathlib.Analysis.Real.Pi.Bounds
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 : ℝ)
h₁ :
  HPow.hPow (α := ℝ) (β := ℕ) (↑a : ℝ) 2 * (↑d : ℝ) ≤
    (HMul.hMul (α := ℝ) 2 (↑d : ℝ) + (↑c : ℝ)) * HPow.hPow (α := ℝ) (β := ℕ) (↑b : ℝ) 2
⊢ HPow.hPow (β := ℕ) (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) 2 ≤ 2 + HDiv.hDiv (α := ℝ) (↑c : ℝ) (↑d : ℝ)

Tactic:
rw [div_pow, add_div_eq_mul_add_div _ _ (ne_of_gt hd'), div_le_div_iff₀ (pow_pos hb' _) hd']

Premises used: pow_pos, ne_of_gt, div_le_div_iff₀, div_pow, add_div_eq_mul_add_div
-- Module: Mathlib.Analysis.Real.Pi.Bounds
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 (α := ℝ) (β := ℕ) (↑a : ℝ) 2 * (↑d : ℝ) ≤
    (HMul.hMul (α := ℝ) 2 (↑d : ℝ) + (↑c : ℝ)) * HPow.hPow (α := ℝ) (β := ℕ) (↑b : ℝ) 2

Tactic:
mod_cast h

Premises used: Nat.cast_mul._simp_1, HMul.hMul, congrArg, Nat.cast_add._simp_1, cast, Nat.cast_le._simp_1, LE.le, Nat.cast, HPow.hPow, HAdd.hAdd, congr, congrFun', OfNat.ofNat, Eq.symm, Eq.trans, Nat.cast_pow._simp_1
-- Module: Mathlib.Analysis.Real.Pi.Bounds
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 (α := ℝ) (β := ℕ) (↑a : ℝ) 2 * (↑d : ℝ) ≤
    (HMul.hMul (α := ℝ) 2 (↑d : ℝ) + (↑c : ℝ)) * HPow.hPow (α := ℝ) (β := ℕ) (↑b : ℝ) 2

Tactic:
exact mod_cast h
-- Module: Mathlib.Analysis.Real.Pi.Bounds
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
hz₁ : HDiv.hDiv (α := ℝ) 23 16 ≤ 2 - HPow.hPow (β := ℕ) (3 / HPow.hPow (α := ℝ) (β := ℕ) 2 2) 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 < π

Tactic:
pi_lower_bound [23 / 16]
-- Module: Mathlib.Analysis.Real.Pi.Bounds
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
h₇ : 2 ≤ HDiv.hDiv (α := ℝ) 4 3 + HPow.hPow (β := ℕ) (HSub.hSub (α := ℝ) 4 4⁻¹ / HPow.hPow (α := ℝ) (β := ℕ) 2 2) 2
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

Tactic:
pi_upper_bound [4 / 3]
-- Module: Mathlib.Analysis.Real.Pi.Bounds
Goal:
⊢ π < HAdd.hAdd (α := ℝ) (↑3 : ℝ) 1

Tactic:
exact_mod_cast pi_lt_four

Premises used: Real.pi_lt_four
-- Module: Mathlib.Analysis.Real.Pi.Bounds
Goal:
⊢ HSub.hSub (α := ℝ) (↑4 : ℝ) 1 < π

Tactic:
exact_mod_cast pi_gt_three

Premises used: Real.pi_gt_three
-- Module: Mathlib.Analysis.Real.Pi.Bounds
Goal:
⊢ (↑3 : ℝ) ≤ π + 1 / 2

Tactic:
grind [pi_gt_three]

Premises used: Real.pi_gt_three
-- Module: Mathlib.Analysis.Real.Pi.Bounds
Goal:
refine : π + 1 / 2 < HAdd.hAdd (α := ℝ) (↑3 : ℝ) 1
⊢ round π = 3

Tactic:
refine round_eq _ |>.trans <| Int.floor_eq_iff.mpr ⟨by grind [pi_gt_three], ?_⟩

Premises used: Iff.mpr, round_eq, Int.floor_eq_iff, And.intro, Eq.trans
-- Module: Mathlib.Analysis.Real.Pi.Bounds
Goal:
grw : 3.15 + 1 / 2 < HAdd.hAdd (α := ℝ) (↑3 : ℝ) 1
⊢ π + 1 / 2 < HAdd.hAdd (α := ℝ) (↑3 : ℝ) 1

Tactic:
grw [pi_lt_d2]

Premises used: Real.pi_lt_d2
-- Module: Mathlib.Analysis.Real.Pi.Bounds
Goal:
⊢ 3.15 + 1 / 2 < HAdd.hAdd (α := ℝ) (↑3 : ℝ) 1

Tactic:
norm_num
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
θ : ℝ
rw : θ * ∫ (x : ℝ) in -1..1, HPow.hPow (β := ℕ) (1 - HPow.hPow (β := ℕ) x 2) 0 * cos (x * θ) = 2 * sin θ
⊢ I 0 θ * θ = 2 * sin θ

Tactic:
rw [mul_comm, I]

Premises used: mul_comm, _private.0.I
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
θ : ℝ
⊢ θ * ∫ (x : ℝ) in -1..1, HPow.hPow (β := ℕ) (1 - HPow.hPow (β := ℕ) x 2) 0 * cos (x * θ) = 2 * sin θ

Tactic:
simp [mul_integral_comp_mul_right, two_mul]

Premises used: two_mul, intervalIntegral.mul_integral_comp_mul_right
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
θ : ℝ
n : ℕ
f : (x : ℝ) → ℝ := fun (x : ℝ) ↦ 1 - HPow.hPow (β := ℕ) x 2
u₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ (n + 1)
u₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ -(2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * x * f x ^ n)
v₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ sin (x * θ)
v₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ) * θ
u₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ x * f x ^ n
u₂' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ n - HMul.hMul (α := ℝ) 2 (↑n : ℝ) * HPow.hPow (β := ℕ) x 2 * f x ^ (n - 1)
v₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ)
v₂' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ -sin (x * θ) * θ
⊢ Continuous f

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
θ : ℝ
n : ℕ
f : (x : ℝ) → ℝ := fun (x : ℝ) ↦ 1 - HPow.hPow (β := ℕ) x 2
u₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ (n + 1)
u₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ -(2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * x * f x ^ n)
v₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ sin (x * θ)
v₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ) * θ
u₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ x * f x ^ n
u₂' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ n - HMul.hMul (α := ℝ) 2 (↑n : ℝ) * HPow.hPow (β := ℕ) x 2 * f x ^ (n - 1)
v₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ)
v₂' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ -sin (x * θ) * θ
⊢ Continuous f

Tactic:
have hfd : Continuous f := by fun_prop
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
θ : ℝ
n : ℕ
f : (x : ℝ) → ℝ := fun (x : ℝ) ↦ 1 - HPow.hPow (β := ℕ) x 2
u₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ (n + 1)
u₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ -(2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * x * f x ^ n)
v₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ sin (x * θ)
v₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ) * θ
u₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ x * f x ^ n
u₂' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ n - HMul.hMul (α := ℝ) 2 (↑n : ℝ) * HPow.hPow (β := ℕ) x 2 * f x ^ (n - 1)
v₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ)
v₂' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ -sin (x * θ) * θ
hfd : Continuous f
⊢ Continuous u₁'

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
θ : ℝ
n : ℕ
f : (x : ℝ) → ℝ := fun (x : ℝ) ↦ 1 - HPow.hPow (β := ℕ) x 2
u₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ (n + 1)
u₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ -(2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * x * f x ^ n)
v₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ sin (x * θ)
v₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ) * θ
u₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ x * f x ^ n
u₂' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ n - HMul.hMul (α := ℝ) 2 (↑n : ℝ) * HPow.hPow (β := ℕ) x 2 * f x ^ (n - 1)
v₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ)
v₂' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ -sin (x * θ) * θ
hfd : Continuous f
⊢ Continuous u₁'

Tactic:
have hu₁d : Continuous u₁' := by fun_prop
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
θ : ℝ
n : ℕ
f : (x : ℝ) → ℝ := fun (x : ℝ) ↦ 1 - HPow.hPow (β := ℕ) x 2
u₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ (n + 1)
u₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ -(2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * x * f x ^ n)
v₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ sin (x * θ)
v₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ) * θ
u₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ x * f x ^ n
u₂' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ n - HMul.hMul (α := ℝ) 2 (↑n : ℝ) * HPow.hPow (β := ℕ) x 2 * f x ^ (n - 1)
v₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ)
v₂' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ -sin (x * θ) * θ
hfd : Continuous f
hu₁d : Continuous u₁'
⊢ Continuous v₁'

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
θ : ℝ
n : ℕ
f : (x : ℝ) → ℝ := fun (x : ℝ) ↦ 1 - HPow.hPow (β := ℕ) x 2
u₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ (n + 1)
u₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ -(2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * x * f x ^ n)
v₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ sin (x * θ)
v₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ) * θ
u₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ x * f x ^ n
u₂' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ n - HMul.hMul (α := ℝ) 2 (↑n : ℝ) * HPow.hPow (β := ℕ) x 2 * f x ^ (n - 1)
v₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ)
v₂' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ -sin (x * θ) * θ
hfd : Continuous f
hu₁d : Continuous u₁'
⊢ Continuous v₁'

Tactic:
have hv₁d : Continuous v₁' := by fun_prop