-- Mathlib/Data/Real/Pi/Leibniz.lean
theorem tendsto_sum_pi_div_four :
    Tendsto (fun k => ∑ i ∈ range k, (-1 : ℝ) ^ i / (2 * i + 1)) atTop (𝓝 (π / 4))

Proof state:
case hf0

⊢ Tendsto (fun i => (2 * ↑i + 1)⁻¹) atTop (𝓝 0)

Tactic:
apply Tendsto.inv_tendsto_atTop

Result:
case hf0.h

⊢ Tendsto (fun i => 2 * ↑i + 1) atTop atTop

Proof state:
case h1
l : ℝ
h : Tendsto (fun n => ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 l)
abel : Tendsto (fun x => ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) (𝓝[<] 1) (𝓝 l)
m : 𝓝[<] 1 ≤ 𝓝 1
⊢ Tendsto (fun x => x ^ 2) (𝓝[<] 1) (𝓝 (1 ^ 2))

Tactic:
exact Tendsto.pow ‹_› _

Result:
no goals

Proof state:
case right
l : ℝ
h : Tendsto (fun n => ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 l)
m : 𝓝[<] 1 ≤ 𝓝 1
q : Tendsto (fun x => x ^ 2) (𝓝[<] 1) (𝓝[<] 1)
abel : Tendsto (fun x => ((fun x => ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) ∘ fun x => x ^ 2) x * x) (𝓝[<] 1) (𝓝 l)
y : ℝ
hy1 : y - 1 < 1 ∧ 1 - y < 1
hy2 : y < 1
ny : ‖y‖ < 1
⊢ ((fun x => ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) ∘ fun x => x ^ 2) y * y = arctan y

Tactic:
rw [← (hasSum_arctan ny).tsum_eq, Function.comp_apply, ← tsum_mul_right]

Result:
case right
l : ℝ
h : Tendsto (fun n => ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 l)
m : 𝓝[<] 1 ≤ 𝓝 1
q : Tendsto (fun x => x ^ 2) (𝓝[<] 1) (𝓝[<] 1)
abel : Tendsto (fun x => ((fun x => ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) ∘ fun x => x ^ 2) x * x) (𝓝[<] 1) (𝓝 l)
y : ℝ
hy1 : y - 1 < 1 ∧ 1 - y < 1
hy2 : y < 1
ny : ‖y‖ < 1
⊢ ∑' (x : ℕ), (-1) ^ x / (2 * ↑x + 1) * (y ^ 2) ^ x * y = ∑' (b : ℕ), (-1) ^ b * y ^ (2 * b + 1) / ↑(2 * b + 1)

Proof state:
x✝² x✝¹ : ℕ
x✝ : x✝² < x✝¹
⊢ (2 * ↑x✝¹ + 1)⁻¹ ≤ (2 * ↑x✝² + 1)⁻¹

Tactic:
gcongr

Result:
no goals

Proof state:
case intro
l : ℝ
h : Tendsto (fun n => ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 l)
m : 𝓝[<] 1 ≤ 𝓝 1
q : Tendsto (fun x => x ^ 2) (𝓝[<] 1) (𝓝[<] 1)
abel :
  Tendsto (fun x => ((fun x => ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) ∘ fun x => x ^ 2) x * x) (𝓝[<] 1)
    (𝓝 (l * 1))
⊢ Tendsto (fun k => ∑ i ∈ range k, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 (π / 4))

Tactic:
rw [mul_one] at abel

Result:
case intro
l : ℝ
h : Tendsto (fun n => ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 l)
m : 𝓝[<] 1 ≤ 𝓝 1
q : Tendsto (fun x => x ^ 2) (𝓝[<] 1) (𝓝[<] 1)
abel : Tendsto (fun x => ((fun x => ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) ∘ fun x => x ^ 2) x * x) (𝓝[<] 1) (𝓝 l)
⊢ Tendsto (fun k => ∑ i ∈ range k, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 (π / 4))

Proof state:
case intro
l : ℝ
h : Tendsto (fun n => ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 l)
m : 𝓝[<] 1 ≤ 𝓝 1
q : Tendsto (fun x => x ^ 2) (𝓝[<] 1) (𝓝[<] 1)
abel : Tendsto arctan (𝓝[<] 1) (𝓝 l)
⊢ Tendsto (fun k => ∑ i ∈ range k, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 (π / 4))

Tactic:
rwa [tendsto_nhds_unique abel ((continuous_arctan.tendsto 1).mono_left m), arctan_one] at h

Result:
no goals

Proof state:
l : ℝ
h : Tendsto (fun n => ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 l)
abel : Tendsto (fun x => ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) (𝓝[<] 1) (𝓝 l)
m : 𝓝[<] 1 ≤ 𝓝 1
x✝¹ : ℝ
x✝ : x✝¹ ∈ Set.Ioo (-1) 1
⊢ x✝¹ ^ 2 ∈ Set.Iio 1

Tactic:
rwa [Set.mem_Iio, sq_lt_one_iff_abs_lt_one, abs_lt, ← Set.mem_Ioo]

Result:
no goals

Proof state:
case right
l : ℝ
h : Tendsto (fun n => ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 l)
m : 𝓝[<] 1 ≤ 𝓝 1
q : Tendsto (fun x => x ^ 2) (𝓝[<] 1) (𝓝[<] 1)
abel : Tendsto (fun x => ((fun x => ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) ∘ fun x => x ^ 2) x * x) (𝓝[<] 1) (𝓝 l)
y : ℝ
hy1 : y - 1 < 1 ∧ 1 - y < 1
hy2 : y ∈ Set.Iio 1
⊢ ((fun x => ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) ∘ fun x => x ^ 2) y * y = arctan y

Tactic:
rw [Set.mem_Iio] at hy2

Result:
case right
l : ℝ
h : Tendsto (fun n => ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 l)
m : 𝓝[<] 1 ≤ 𝓝 1
q : Tendsto (fun x => x ^ 2) (𝓝[<] 1) (𝓝[<] 1)
abel : Tendsto (fun x => ((fun x => ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) ∘ fun x => x ^ 2) x * x) (𝓝[<] 1) (𝓝 l)
y : ℝ
hy1 : y - 1 < 1 ∧ 1 - y < 1
hy2 : y < 1
⊢ ((fun x => ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) ∘ fun x => x ^ 2) y * y = arctan y

Proof state:
case hfa

⊢ Antitone fun i => (2 * ↑i + 1)⁻¹

Tactic:
exact antitone_iff_forall_lt.mpr fun _ _ _ ↦ by gcongr

Result:
no goals

Proof state:
case intro
l : ℝ
h : Tendsto (fun n => ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 l)
m : 𝓝[<] 1 ≤ 𝓝 1
q : Tendsto (fun x => x ^ 2) (𝓝[<] 1) (𝓝[<] 1)
abel : Tendsto (fun x => ((fun x => ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) ∘ fun x => x ^ 2) x * x) (𝓝[<] 1) (𝓝 l)
⊢ Tendsto (fun k => ∑ i ∈ range k, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 (π / 4))

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

Result:
case intro
l : ℝ
h : Tendsto (fun n => ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 l)
m : 𝓝[<] 1 ≤ 𝓝 1
q : Tendsto (fun x => x ^ 2) (𝓝[<] 1) (𝓝[<] 1)
abel : Tendsto arctan (𝓝[<] 1) (𝓝 l)
⊢ Tendsto (fun k => ∑ i ∈ range k, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 (π / 4))

Proof state:
l : ℝ
h : Tendsto (fun n => ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 l)
m : 𝓝[<] 1 ≤ 𝓝 1
q : Tendsto (fun x => x ^ 2) (𝓝[<] 1) (𝓝[<] 1)
abel : Tendsto (fun x => ((fun x => ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) ∘ fun x => x ^ 2) x * x) (𝓝[<] 1) (𝓝 l)
⊢ (fun x => ((fun x => ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) ∘ fun x => x ^ 2) x * x) =ᶠ[𝓝[<] 1] arctan

Tactic:
rw [eventuallyEq_nhdsWithin_iff, Metric.eventually_nhds_iff]

Result:
l : ℝ
h : Tendsto (fun n => ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 l)
m : 𝓝[<] 1 ≤ 𝓝 1
q : Tendsto (fun x => x ^ 2) (𝓝[<] 1) (𝓝[<] 1)
abel : Tendsto (fun x => ((fun x => ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) ∘ fun x => x ^ 2) x * x) (𝓝[<] 1) (𝓝 l)
⊢ ∃ ε > 0,
    ∀ ⦃y : ℝ⦄,
      dist y 1 < ε →
        y ∈ Set.Iio 1 → ((fun x => ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) ∘ fun x => x ^ 2) y * y = arctan y

Proof state:
l : ℝ
h : Tendsto (fun n => ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 l)
abel : Tendsto (fun x => ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) (𝓝[<] 1) (𝓝 l)
m : 𝓝[<] 1 ≤ 𝓝 1
⊢ Tendsto (fun x => x ^ 2) (𝓝[<] 1) (𝓝[<] 1)

Tactic:
apply tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within

Result:
case h1
l : ℝ
h : Tendsto (fun n => ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 l)
abel : Tendsto (fun x => ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) (𝓝[<] 1) (𝓝 l)
m : 𝓝[<] 1 ≤ 𝓝 1
⊢ Tendsto (fun x => x ^ 2) (𝓝[<] 1) (𝓝 1)

case h2
l : ℝ
h : Tendsto (fun n => ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 l)
abel : Tendsto (fun x => ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) (𝓝[<] 1) (𝓝 l)
m : 𝓝[<] 1 ≤ 𝓝 1
⊢ ∀ᶠ (x : ℝ) in 𝓝[<] 1, x ^ 2 ∈ Set.Iio 1

Proof state:
case intro
l : ℝ
h : Tendsto (fun n => ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 l)
abel : Tendsto (fun x => ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) (𝓝[<] 1) (𝓝 l)
⊢ Tendsto (fun k => ∑ i ∈ range k, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 (π / 4))

Tactic:
have m : 𝓝[<] (1 : ℝ) ≤ 𝓝 1 := tendsto_nhdsWithin_of_tendsto_nhds fun _ a ↦ a

Result:
case intro
l : ℝ
h : Tendsto (fun n => ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 l)
abel : Tendsto (fun x => ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) (𝓝[<] 1) (𝓝 l)
m : 𝓝[<] 1 ≤ 𝓝 1
⊢ Tendsto (fun k => ∑ i ∈ range k, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 (π / 4))