awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Leibniz (hypothesis)
Goal:
l : ℝ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, HPow.hPow (α := ℝ) (-1) i / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)) atTop (𝓝 l)
abel :
  Tendsto (fun (x : ℝ) ↦ ∑' (n : ℕ), HPow.hPow (α := ℝ) (-1) n / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * x ^ n) (𝓝[<] 1)
    (𝓝 l)
m : LE.le (α := Filter ℝ) (𝓝[<] 1) (𝓝 1)
⊢ Tendsto (fun (k : ℕ) ↦ ∑ i ∈ range k, HPow.hPow (α := ℝ) (-1) i / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)) atTop
    (𝓝 (π / 4))
have q : Tendsto (β := ℝ) (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2) (𝓝[<] 1) (𝓝[<] 1)
Tactic: have q : Tendsto (fun x : ℝ ↦ x ^ 2) (𝓝[<] 1) (𝓝[<] 1) := by
    apply tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within
    · nth_rw 3 [← one_pow 2]
      exact Tendsto.pow ‹_› _
    · rw [eventually_iff_exists_mem]
      use Set.Ioo (-1) 1
      exact ⟨Ioo_mem_nhdsLT <| by simp,
        fun _ _ ↦ by rwa [Set.mem_Iio, sq_lt_one_iff_abs_lt_one, abs_lt, ← Set.mem_Ioo]⟩
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Leibniz (hypothesis)
Goal:
l : ℝ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, HPow.hPow (α := ℝ) (-1) i / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)) atTop (𝓝 l)
abel :
  Tendsto (fun (x : ℝ) ↦ ∑' (n : ℕ), HPow.hPow (α := ℝ) (-1) n / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * x ^ n) (𝓝[<] 1)
    (𝓝 l)
m : LE.le (α := Filter ℝ) (𝓝[<] 1) (𝓝 1)
q : Tendsto (β := ℝ) (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2) (𝓝[<] 1) (𝓝[<] 1)
⊢ Tendsto (fun (k : ℕ) ↦ ∑ i ∈ range k, HPow.hPow (α := ℝ) (-1) i / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)) atTop
    (𝓝 (π / 4))
have abel₁ : Tendsto
  (fun (x : ℝ) ↦
    ((fun (x : ℝ) ↦ ∑' (n : ℕ), HPow.hPow (α := ℝ) (-1) n / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * x ^ n) ∘ fun (x : ℝ) ↦
          HPow.hPow (β := ℕ) x 2)
        x *
      x)
  (𝓝[<] 1) (𝓝 (l * 1))
Tactic: replace abel := (abel.comp q).mul m
Cleared hypotheses: abel
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Leibniz (hypothesis)
Goal:
l : ℝ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, HPow.hPow (α := ℝ) (-1) i / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)) atTop (𝓝 l)
m : LE.le (α := Filter ℝ) (𝓝[<] 1) (𝓝 1)
q : Tendsto (β := ℝ) (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2) (𝓝[<] 1) (𝓝[<] 1)
abel :
  Tendsto
    (fun (x : ℝ) ↦
      ((fun (x : ℝ) ↦ ∑' (n : ℕ), HPow.hPow (α := ℝ) (-1) n / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * x ^ n) ∘
            fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2)
          x *
        x)
    (𝓝[<] 1) (𝓝 (l * 1))
⊢ Tendsto (fun (k : ℕ) ↦ ∑ i ∈ range k, HPow.hPow (α := ℝ) (-1) i / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)) atTop
    (𝓝 (π / 4))
have abel₁ : Tendsto
  (fun (x : ℝ) ↦
    ((fun (x : ℝ) ↦ ∑' (n : ℕ), HPow.hPow (α := ℝ) (-1) n / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * x ^ n) ∘ fun (x : ℝ) ↦
          HPow.hPow (β := ℕ) x 2)
        x *
      x)
  (𝓝[<] 1) (𝓝 l)
Tactic: rw [mul_one] at abel
Cleared hypotheses: abel
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Leibniz (goal)
Goal:
l : ℝ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, HPow.hPow (α := ℝ) (-1) i / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)) atTop (𝓝 l)
m : LE.le (α := Filter ℝ) (𝓝[<] 1) (𝓝 1)
q : Tendsto (β := ℝ) (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2) (𝓝[<] 1) (𝓝[<] 1)
abel :
  Tendsto
    (fun (x : ℝ) ↦
      ((fun (x : ℝ) ↦ ∑' (n : ℕ), HPow.hPow (α := ℝ) (-1) n / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * x ^ n) ∘
            fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2)
          x *
        x)
    (𝓝[<] 1) (𝓝 l)
⊢ Tendsto arctan (𝓝[<] 1) (𝓝 l)
have apply : (fun (x : ℝ) ↦
    ((fun (x : ℝ) ↦ ∑' (n : ℕ), HPow.hPow (α := ℝ) (-1) n / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * x ^ n) ∘ fun (x : ℝ) ↦
          HPow.hPow (β := ℕ) x 2)
        x *
      x) =ᶠ[𝓝[<] 1]
  arctan
Tactic: apply abel.congr'
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Leibniz (goal)
Goal:
l : ℝ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, HPow.hPow (α := ℝ) (-1) i / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)) atTop (𝓝 l)
m : LE.le (α := Filter ℝ) (𝓝[<] 1) (𝓝 1)
q : Tendsto (β := ℝ) (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2) (𝓝[<] 1) (𝓝[<] 1)
abel :
  Tendsto
    (fun (x : ℝ) ↦
      ((fun (x : ℝ) ↦ ∑' (n : ℕ), HPow.hPow (α := ℝ) (-1) n / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * x ^ n) ∘
            fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2)
          x *
        x)
    (𝓝[<] 1) (𝓝 l)
⊢ (fun (x : ℝ) ↦
      ((fun (x : ℝ) ↦ ∑' (n : ℕ), HPow.hPow (α := ℝ) (-1) n / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * x ^ n) ∘
            fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2)
          x *
        x) =ᶠ[𝓝[<] 1]
    arctan
have rw : ∃ ε > 0,
  ∀ ⦃y : ℝ⦄,
    dist y 1 < ε →
      Membership.mem (γ := Set ℝ) (Set.Iio 1) y →
        ((fun (x : ℝ) ↦ ∑' (n : ℕ), HPow.hPow (α := ℝ) (-1) n / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * x ^ n) ∘
                fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2)
              y *
            y =
          arctan y
Tactic: rw [eventuallyEq_nhdsWithin_iff, Metric.eventually_nhds_iff]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Leibniz (goal)
Goal:
l : ℝ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, HPow.hPow (α := ℝ) (-1) i / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)) atTop (𝓝 l)
m : LE.le (α := Filter ℝ) (𝓝[<] 1) (𝓝 1)
q : Tendsto (β := ℝ) (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2) (𝓝[<] 1) (𝓝[<] 1)
abel :
  Tendsto
    (fun (x : ℝ) ↦
      ((fun (x : ℝ) ↦ ∑' (n : ℕ), HPow.hPow (α := ℝ) (-1) n / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * x ^ n) ∘
            fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2)
          x *
        x)
    (𝓝[<] 1) (𝓝 l)
⊢ ∃ ε > 0,
    ∀ ⦃y : ℝ⦄,
      dist y 1 < ε →
        Membership.mem (γ := Set ℝ) (Set.Iio 1) y →
          ((fun (x : ℝ) ↦ ∑' (n : ℕ), HPow.hPow (α := ℝ) (-1) n / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * x ^ n) ∘
                  fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2)
                y *
              y =
            arctan y
have right : ∀ ⦃y : ℝ⦄,
  dist y 1 < 1 →
    Membership.mem (γ := Set ℝ) (Set.Iio 1) y →
      ((fun (x : ℝ) ↦ ∑' (n : ℕ), HPow.hPow (α := ℝ) (-1) n / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * x ^ n) ∘
              fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2)
            y *
          y =
        arctan y
Tactic: use 1, zero_lt_one
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Leibniz (hypothesis)
Goal:
l : ℝ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, HPow.hPow (α := ℝ) (-1) i / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)) atTop (𝓝 l)
m : LE.le (α := Filter ℝ) (𝓝[<] 1) (𝓝 1)
q : Tendsto (β := ℝ) (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2) (𝓝[<] 1) (𝓝[<] 1)
abel :
  Tendsto
    (fun (x : ℝ) ↦
      ((fun (x : ℝ) ↦ ∑' (n : ℕ), HPow.hPow (α := ℝ) (-1) n / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * x ^ n) ∘
            fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2)
          x *
        x)
    (𝓝[<] 1) (𝓝 l)
y : ℝ
hy1 : dist y 1 < 1
hy2 : Membership.mem (γ := Set ℝ) (Set.Iio 1) y
⊢ ((fun (x : ℝ) ↦ ∑' (n : ℕ), HPow.hPow (α := ℝ) (-1) n / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * x ^ n) ∘ fun (x : ℝ) ↦
          HPow.hPow (β := ℕ) x 2)
        y *
      y =
    arctan y
have hy1₁ : y - 1 < 1 ∧ 1 - y < 1
Tactic: rw [dist_eq, abs_sub_lt_iff] at hy1
Cleared hypotheses: hy1, hy2
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Leibniz (hypothesis)
Goal:
l : ℝ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, HPow.hPow (α := ℝ) (-1) i / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)) atTop (𝓝 l)
m : LE.le (α := Filter ℝ) (𝓝[<] 1) (𝓝 1)
q : Tendsto (β := ℝ) (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2) (𝓝[<] 1) (𝓝[<] 1)
abel :
  Tendsto
    (fun (x : ℝ) ↦
      ((fun (x : ℝ) ↦ ∑' (n : ℕ), HPow.hPow (α := ℝ) (-1) n / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * x ^ n) ∘
            fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2)
          x *
        x)
    (𝓝[<] 1) (𝓝 l)
y : ℝ
hy1 : y - 1 < 1 ∧ 1 - y < 1
hy2 : Membership.mem (γ := Set ℝ) (Set.Iio 1) y
⊢ ((fun (x : ℝ) ↦ ∑' (n : ℕ), HPow.hPow (α := ℝ) (-1) n / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * x ^ n) ∘ fun (x : ℝ) ↦
          HPow.hPow (β := ℕ) x 2)
        y *
      y =
    arctan y
have hy2₁ : y < 1
Tactic: rw [Set.mem_Iio] at hy2
Cleared hypotheses: hy2
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Leibniz (goal)
Goal:
l : ℝ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, HPow.hPow (α := ℝ) (-1) i / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)) atTop (𝓝 l)
m : LE.le (α := Filter ℝ) (𝓝[<] 1) (𝓝 1)
q : Tendsto (β := ℝ) (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2) (𝓝[<] 1) (𝓝[<] 1)
abel :
  Tendsto
    (fun (x : ℝ) ↦
      ((fun (x : ℝ) ↦ ∑' (n : ℕ), HPow.hPow (α := ℝ) (-1) n / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * x ^ n) ∘
            fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2)
          x *
        x)
    (𝓝[<] 1) (𝓝 l)
y : ℝ
hy1 : y - 1 < 1 ∧ 1 - y < 1
hy2 : y < 1
⊢ ‖y‖ < 1
have rw : -1 < y ∧ y < 1
Tactic: rw [norm_eq_abs, abs_lt]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Leibniz (goal)
Goal:
l : ℝ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, HPow.hPow (α := ℝ) (-1) i / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)) atTop (𝓝 l)
m : LE.le (α := Filter ℝ) (𝓝[<] 1) (𝓝 1)
q : Tendsto (β := ℝ) (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2) (𝓝[<] 1) (𝓝[<] 1)
abel :
  Tendsto
    (fun (x : ℝ) ↦
      ((fun (x : ℝ) ↦ ∑' (n : ℕ), HPow.hPow (α := ℝ) (-1) n / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * x ^ n) ∘
            fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2)
          x *
        x)
    (𝓝[<] 1) (𝓝 l)
y : ℝ
hy1 : y - 1 < 1 ∧ 1 - y < 1
hy2 : y < 1
⊢ -1 < y ∧ y < 1
have left : -1 < y
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Leibniz (goal)
Goal:
l : ℝ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, HPow.hPow (α := ℝ) (-1) i / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)) atTop (𝓝 l)
m : LE.le (α := Filter ℝ) (𝓝[<] 1) (𝓝 1)
q : Tendsto (β := ℝ) (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2) (𝓝[<] 1) (𝓝[<] 1)
abel :
  Tendsto
    (fun (x : ℝ) ↦
      ((fun (x : ℝ) ↦ ∑' (n : ℕ), HPow.hPow (α := ℝ) (-1) n / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * x ^ n) ∘
            fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2)
          x *
        x)
    (𝓝[<] 1) (𝓝 l)
y : ℝ
hy1 : y - 1 < 1 ∧ 1 - y < 1
hy2 : y < 1
⊢ -1 < y
have linarith : y ≤ -1 → 2 * (1 - y - 1) + (y - 1) + (y - -1) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Leibniz (goal)
Goal:
l : ℝ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, HPow.hPow (α := ℝ) (-1) i / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)) atTop (𝓝 l)
m : LE.le (α := Filter ℝ) (𝓝[<] 1) (𝓝 1)
q : Tendsto (β := ℝ) (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2) (𝓝[<] 1) (𝓝[<] 1)
abel :
  Tendsto
    (fun (x : ℝ) ↦
      ((fun (x : ℝ) ↦ ∑' (n : ℕ), HPow.hPow (α := ℝ) (-1) n / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * x ^ n) ∘
            fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2)
          x *
        x)
    (𝓝[<] 1) (𝓝 l)
y : ℝ
hy1 : y - 1 < 1 ∧ 1 - y < 1
hy2 : y < 1
linarith : y ≤ -1 → 2 * (1 - y - 1) + (y - 1) + (y - -1) = 0
⊢ -1 < y
have linarith₁ : y ≤ -1 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Leibniz (goal)
Goal:
l : ℝ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, HPow.hPow (α := ℝ) (-1) i / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)) atTop (𝓝 l)
m : LE.le (α := Filter ℝ) (𝓝[<] 1) (𝓝 1)
q : Tendsto (β := ℝ) (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2) (𝓝[<] 1) (𝓝[<] 1)
abel :
  Tendsto
    (fun (x : ℝ) ↦
      ((fun (x : ℝ) ↦ ∑' (n : ℕ), HPow.hPow (α := ℝ) (-1) n / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * x ^ n) ∘
            fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2)
          x *
        x)
    (𝓝[<] 1) (𝓝 l)
y : ℝ
hy1 : y - 1 < 1 ∧ 1 - y < 1
hy2 : y < 1
⊢ y < 1
have linarith : 1 ≤ y → y - 1 + (1 - y) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Leibniz (hypothesis)
Goal:
l : ℝ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, HPow.hPow (α := ℝ) (-1) i / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)) atTop (𝓝 l)
m : LE.le (α := Filter ℝ) (𝓝[<] 1) (𝓝 1)
q : Tendsto (β := ℝ) (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2) (𝓝[<] 1) (𝓝[<] 1)
abel :
  Tendsto
    (fun (x : ℝ) ↦
      ((fun (x : ℝ) ↦ ∑' (n : ℕ), HPow.hPow (α := ℝ) (-1) n / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * x ^ n) ∘
            fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2)
          x *
        x)
    (𝓝[<] 1) (𝓝 l)
y : ℝ
hy1 : y - 1 < 1 ∧ 1 - y < 1
hy2 : y < 1
⊢ ((fun (x : ℝ) ↦ ∑' (n : ℕ), HPow.hPow (α := ℝ) (-1) n / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * x ^ n) ∘ fun (x : ℝ) ↦
          HPow.hPow (β := ℕ) x 2)
        y *
      y =
    arctan y
have ny : ‖y‖ < 1
Tactic: have ny : ‖y‖ < 1 := by rw [norm_eq_abs, abs_lt]; constructor <;> linarith
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Leibniz (goal)
Goal:
l : ℝ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, HPow.hPow (α := ℝ) (-1) i / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)) atTop (𝓝 l)
m : LE.le (α := Filter ℝ) (𝓝[<] 1) (𝓝 1)
q : Tendsto (β := ℝ) (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2) (𝓝[<] 1) (𝓝[<] 1)
abel :
  Tendsto
    (fun (x : ℝ) ↦
      ((fun (x : ℝ) ↦ ∑' (n : ℕ), HPow.hPow (α := ℝ) (-1) n / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * x ^ n) ∘
            fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2)
          x *
        x)
    (𝓝[<] 1) (𝓝 l)
y : ℝ
hy1 : y - 1 < 1 ∧ 1 - y < 1
hy2 : y < 1
ny : ‖y‖ < 1
⊢ ((fun (x : ℝ) ↦ ∑' (n : ℕ), HPow.hPow (α := ℝ) (-1) n / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * x ^ n) ∘ fun (x : ℝ) ↦
          HPow.hPow (β := ℕ) x 2)
        y *
      y =
    arctan y
have right : Eq (α := ℝ)
  (∑' (x : ℕ), HPow.hPow (α := ℝ) (-1) x / (HMul.hMul (α := ℝ) 2 (↑x : ℝ) + 1) * HPow.hPow (β := ℕ) y 2 ^ x * y)
  (∑' (b : ℕ), HPow.hPow (α := ℝ) (-1) b * y ^ (2 * b + 1) / (↑(2 * b + 1) : ℝ))
Tactic: rw [← (hasSum_arctan ny).tsum_eq, Function.comp_apply, ← tsum_mul_right]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Leibniz (goal)
Goal:
l : ℝ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, HPow.hPow (α := ℝ) (-1) i / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)) atTop (𝓝 l)
m : LE.le (α := Filter ℝ) (𝓝[<] 1) (𝓝 1)
q : Tendsto (β := ℝ) (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2) (𝓝[<] 1) (𝓝[<] 1)
abel :
  Tendsto
    (fun (x : ℝ) ↦
      ((fun (x : ℝ) ↦ ∑' (n : ℕ), HPow.hPow (α := ℝ) (-1) n / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * x ^ n) ∘
            fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2)
          x *
        x)
    (𝓝[<] 1) (𝓝 l)
y : ℝ
hy1 : y - 1 < 1 ∧ 1 - y < 1
hy2 : y < 1
ny : ‖y‖ < 1
⊢ Eq (α := ℝ)
    (∑' (x : ℕ), HPow.hPow (α := ℝ) (-1) x / (HMul.hMul (α := ℝ) 2 (↑x : ℝ) + 1) * HPow.hPow (β := ℕ) y 2 ^ x * y)
    (∑' (b : ℕ), HPow.hPow (α := ℝ) (-1) b * y ^ (2 * b + 1) / (↑(2 * b + 1) : ℝ))
have right : Eq (α := ℝ) (∑' (x : ℕ), HPow.hPow (α := ℝ) (-1) x * y ^ (2 * x + 1) / (HMul.hMul (α := ℝ) 2 (↑x : ℝ) + 1))
  (∑' (b : ℕ), HPow.hPow (α := ℝ) (-1) b * y ^ (2 * b + 1) / (↑(2 * b + 1) : ℝ))
Tactic: simp_rw [mul_assoc, ← pow_mul, ← pow_succ, div_mul_eq_mul_div]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Leibniz (goal)
Goal:
l : ℝ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, HPow.hPow (α := ℝ) (-1) i / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)) atTop (𝓝 l)
m : LE.le (α := Filter ℝ) (𝓝[<] 1) (𝓝 1)
q : Tendsto (β := ℝ) (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2) (𝓝[<] 1) (𝓝[<] 1)
abel :
  Tendsto
    (fun (x : ℝ) ↦
      ((fun (x : ℝ) ↦ ∑' (n : ℕ), HPow.hPow (α := ℝ) (-1) n / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * x ^ n) ∘
            fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2)
          x *
        x)
    (𝓝[<] 1) (𝓝 l)
y : ℝ
hy1 : y - 1 < 1 ∧ 1 - y < 1
hy2 : y < 1
ny : ‖y‖ < 1
⊢ Eq (α := ℝ) (∑' (x : ℕ), HPow.hPow (α := ℝ) (-1) x * y ^ (2 * x + 1) / (HMul.hMul (α := ℝ) 2 (↑x : ℝ) + 1))
    (∑' (b : ℕ), HPow.hPow (α := ℝ) (-1) b * y ^ (2 * b + 1) / (↑(2 * b + 1) : ℝ))
have right : Eq (α := ℝ) (∑' (x : ℕ), (↑(Int.negSucc 0 ^ x) : ℝ) * y ^ (2 * x + 1) / (↑(2 * x + 1) : ℝ))
  (∑' (b : ℕ), (↑(Int.negSucc 0 ^ b) : ℝ) * y ^ (2 * b + 1) / (↑(2 * b + 1) : ℝ))
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Leibniz (hypothesis)
Goal:
l : ℝ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, HPow.hPow (α := ℝ) (-1) i / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)) atTop (𝓝 l)
m : LE.le (α := Filter ℝ) (𝓝[<] 1) (𝓝 1)
q : Tendsto (β := ℝ) (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2) (𝓝[<] 1) (𝓝[<] 1)
abel :
  Tendsto
    (fun (x : ℝ) ↦
      ((fun (x : ℝ) ↦ ∑' (n : ℕ), HPow.hPow (α := ℝ) (-1) n / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * x ^ n) ∘
            fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2)
          x *
        x)
    (𝓝[<] 1) (𝓝 l)
⊢ Tendsto (fun (k : ℕ) ↦ ∑ i ∈ range k, HPow.hPow (α := ℝ) (-1) i / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)) atTop
    (𝓝 (π / 4))
have abel₁ : Tendsto arctan (𝓝[<] 1) (𝓝 l)
Tactic: replace abel : Tendsto arctan (𝓝[<] 1) (𝓝 l) := by
    apply abel.congr'
    rw [eventuallyEq_nhdsWithin_iff, Metric.eventually_nhds_iff]
    use 1, zero_lt_one
    intro y hy1 hy2
    rw [dist_eq, abs_sub_lt_iff] at hy1
    rw [Set.mem_Iio] at hy2
    have ny : ‖y‖ < 1 := by rw [norm_eq_abs, abs_lt]; constructor <;> linarith
    rw [← (hasSum_arctan ny).tsum_eq, Function.comp_apply, ← tsum_mul_right]
    simp_rw [mul_assoc, ← pow_mul, ← pow_succ, div_mul_eq_mul_div]
    norm_cast
Cleared hypotheses: abel
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Leibniz (goal)
Goal:
l : ℝ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, HPow.hPow (α := ℝ) (-1) i / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)) atTop (𝓝 l)
m : LE.le (α := Filter ℝ) (𝓝[<] 1) (𝓝 1)
q : Tendsto (β := ℝ) (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2) (𝓝[<] 1) (𝓝[<] 1)
abel : Tendsto arctan (𝓝[<] 1) (𝓝 l)
⊢ Tendsto (fun (k : ℕ) ↦ ∑ i ∈ range k, HPow.hPow (α := ℝ) (-1) i / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)) atTop
    (𝓝 (π / 4))
have rwa : ∀
  (h :
    Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, HPow.hPow (α := ℝ) (-1) i / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)) atTop
      (𝓝 (arctan 1)))
  (m : LE.le (α := Filter ℝ) (𝓝[<] 1) (𝓝 1))
  (q : Tendsto (β := ℝ) (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2) (𝓝[<] 1) (𝓝[<] 1))
  (abel : Tendsto arctan (𝓝[<] 1) (𝓝 l)),
  Tendsto (fun (k : ℕ) ↦ ∑ i ∈ range k, HPow.hPow (α := ℝ) (-1) i / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)) atTop
    (𝓝 (π / 4))
Tactic: rwa [tendsto_nhds_unique abel ((continuous_arctan.tendsto 1).mono_left m), arctan_one] at h
Cleared hypotheses: h, m, q, abel
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Leibniz (goal)
Goal:
l : ℝ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, HPow.hPow (α := ℝ) (-1) i / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)) atTop (𝓝 l)
m : LE.le (α := Filter ℝ) (𝓝[<] 1) (𝓝 1)
q : Tendsto (β := ℝ) (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2) (𝓝[<] 1) (𝓝[<] 1)
abel : Tendsto arctan (𝓝[<] 1) (𝓝 l)
rwa :
  ∀
    (h :
      Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, HPow.hPow (α := ℝ) (-1) i / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)) atTop
        (𝓝 (arctan 1)))
    (m : LE.le (α := Filter ℝ) (𝓝[<] 1) (𝓝 1))
    (q : Tendsto (β := ℝ) (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2) (𝓝[<] 1) (𝓝[<] 1))
    (abel : Tendsto arctan (𝓝[<] 1) (𝓝 l)),
    Tendsto (fun (k : ℕ) ↦ ∑ i ∈ range k, HPow.hPow (α := ℝ) (-1) i / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)) atTop
      (𝓝 (π / 4))
⊢ Tendsto (fun (k : ℕ) ↦ ∑ i ∈ range k, HPow.hPow (α := ℝ) (-1) i / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)) atTop
    (𝓝 (π / 4))
have rwa₁ : ∀
  (h :
    Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, HPow.hPow (α := ℝ) (-1) i / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)) atTop
      (𝓝 (π / 4)))
  (m : LE.le (α := Filter ℝ) (𝓝[<] 1) (𝓝 1))
  (q : Tendsto (β := ℝ) (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2) (𝓝[<] 1) (𝓝[<] 1))
  (abel : Tendsto arctan (𝓝[<] 1) (𝓝 l)),
  Tendsto (fun (k : ℕ) ↦ ∑ i ∈ range k, HPow.hPow (α := ℝ) (-1) i / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)) atTop
    (𝓝 (π / 4))
Tactic: rwa [tendsto_nhds_unique abel ((continuous_arctan.tendsto 1).mono_left m), arctan_one] at h
Cleared hypotheses: h, m, q, abel
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Wallis (goal)
Goal:
k : ℕ
hk : 0 < W k
⊢ 0 < W (k + 1)
have succ : 0 <
  W k *
    ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) *
      ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 3)))
Tactic: rw [W_succ]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Wallis (goal)
Goal:
k : ℕ
hk : 0 < W k
⊢ 0 <
    W k *
      ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) *
        ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 3)))
have succ : 0 < HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2
Tactic: refine mul_pos hk (mul_pos (div_pos ?_ ?_) (div_pos ?_ ?_))
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Wallis (goal)
Goal:
k : ℕ
hk : 0 < W k
succ : 0 < HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2
⊢ 0 <
    W k *
      ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) *
        ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 3)))
have succ₁ : 0 < HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1
Tactic: refine mul_pos hk (mul_pos (div_pos ?_ ?_) (div_pos ?_ ?_))
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Wallis (goal)
Goal:
k : ℕ
hk : 0 < W k
succ : 0 < HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2
succ₁ : 0 < HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1
succ₂ : 0 < HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2
⊢ 0 <
    W k *
      ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) *
        ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 3)))
have succ₃ : 0 < HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 3
Tactic: refine mul_pos hk (mul_pos (div_pos ?_ ?_) (div_pos ?_ ?_))
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Wallis (goal)
Goal:
k : ℕ
⊢ 0 < W k
have zero : 0 < W 0
Tactic: induction k with
  | zero => unfold W; simp
  | succ k hk =>
    rw [W_succ]
    refine mul_pos hk (mul_pos (div_pos ?_ ?_) (div_pos ?_ ?_)) <;> positivity
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Wallis (goal)
Goal:
k : ℕ
zero : 0 < W 0
⊢ 0 < W k
have succ : ∀ (k : ℕ) (hk : 0 < W k), 0 < W (k + 1)
Tactic: induction k with
  | zero => unfold W; simp
  | succ k hk =>
    rw [W_succ]
    refine mul_pos hk (mul_pos (div_pos ?_ ?_) (div_pos ?_ ?_)) <;> positivity
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Wallis (goal)
Goal:
n : ℕ
IH :
  ∏ i ∈ range n,
      (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) *
        ((HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 3)) =
    HPow.hPow (α := ℝ) 2 (4 * n) * HPow.hPow (α := ℝ) (β := ℕ) (↑n ! : ℝ) 4 /
      (HPow.hPow (α := ℝ) (β := ℕ) (↑(2 * n)! : ℝ) 2 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1))
⊢ ∏ i ∈ range (n + 1),
      (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) *
        ((HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 3)) =
    HPow.hPow (α := ℝ) 2 (4 * (n + 1)) * HPow.hPow (α := ℝ) (β := ℕ) (↑(n + 1)! : ℝ) 4 /
      (HPow.hPow (α := ℝ) (β := ℕ) (↑(2 * (n + 1))! : ℝ) 2 * (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1))
have succ : HPow.hPow (α := ℝ) 2 (4 * n) * HPow.hPow (α := ℝ) (β := ℕ) (↑n ! : ℝ) 4 *
      ((HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2)) /
    (HPow.hPow (α := ℝ) (β := ℕ) (↑(2 * n)! : ℝ) 2 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) *
      ((HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 3))) =
  HPow.hPow (α := ℝ) 2 (4 * (n + 1)) * HPow.hPow (α := ℝ) (β := ℕ) (↑(n + 1)! : ℝ) 4 /
    (HPow.hPow (α := ℝ) (β := ℕ) (↑(2 * (n + 1))! : ℝ) 2 * (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1))
Tactic: rw [prod_range_succ, IH, _root_.div_mul_div_comm, _root_.div_mul_div_comm]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Wallis (goal)
Goal:
n : ℕ
IH :
  ∏ i ∈ range n,
      (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) *
        ((HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 3)) =
    HPow.hPow (α := ℝ) 2 (4 * n) * HPow.hPow (α := ℝ) (β := ℕ) (↑n ! : ℝ) 4 /
      (HPow.hPow (α := ℝ) (β := ℕ) (↑(2 * n)! : ℝ) 2 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1))
⊢ HPow.hPow (α := ℝ) 2 (4 * n) * HPow.hPow (α := ℝ) (β := ℕ) (↑n ! : ℝ) 4 *
        ((HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2)) /
      (HPow.hPow (α := ℝ) (β := ℕ) (↑(2 * n)! : ℝ) 2 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) *
        ((HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 3))) =
    HPow.hPow (α := ℝ) 2 (4 * (n + 1)) * HPow.hPow (α := ℝ) (β := ℕ) (↑(n + 1)! : ℝ) 4 /
      (HPow.hPow (α := ℝ) (β := ℕ) (↑(2 * (n + 1))! : ℝ) 2 * (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1))
have succ : HPow.hPow (α := ℝ) (β := ℕ) (↑(2 * n)! : ℝ) 2 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) *
    ((HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 3)) ≠
  0
Tactic: refine (div_eq_div_iff ?_ ?_).mpr ?_