-- 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 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

Tactic:
rw [eventually_iff_exists_mem]

Result:
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
⊢ ∃ v ∈ 𝓝[<] 1, ∀ y ∈ v, y ^ 2 ∈ Set.Iio 1

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)
⊢ ∃ ε > 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

Tactic:
use 1, zero_lt_one

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 : ℝ⦄,
    dist y 1 < 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)
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
⊢ ‖y‖ < 1

Tactic:
rw [norm_eq_abs, abs_lt]

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)
y : ℝ
hy1 : y - 1 < 1 ∧ 1 - y < 1
hy2 : y < 1
⊢ -1 < y ∧ y < 1

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)
⊢ Tendsto arctan (𝓝[<] 1) (𝓝 l)

Tactic:
apply abel.congr'

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)
⊢ (fun x => ((fun x => ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) ∘ fun x => x ^ 2) x * x) =ᶠ[𝓝[<] 1] arctan

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 : dist y 1 < 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 [dist_eq, abs_sub_lt_iff] at hy1

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 ∈ Set.Iio 1
⊢ ((fun x => ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) ∘ fun x => x ^ 2) y * y = arctan y

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
⊢ ((fun x => ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) ∘ fun x => x ^ 2) y * y = arctan y

Tactic:
have ny : ‖y‖ < 1 := by rw [norm_eq_abs, abs_lt]; constructor <;> linarith

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
⊢ ((fun x => ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) ∘ fun x => x ^ 2) y * y = arctan y

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)

Tactic:
nth_rw 3 [← one_pow 2]

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 ^ 2))

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)
m : 𝓝[<] 1 ≤ 𝓝 1
q : Tendsto (fun x => x ^ 2) (𝓝[<] 1) (𝓝[<] 1)
⊢ Tendsto (fun k => ∑ i ∈ range k, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 (π / 4))

Tactic:
replace abel := (abel.comp q).mul m

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 * 1))
⊢ 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)
abel : Tendsto (fun x => ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) (𝓝[<] 1) (𝓝 l)
m : 𝓝[<] 1 ≤ 𝓝 1
⊢ -1 < 1

Tactic:
simp

Result:
no goals

Proof state:
case hf0.h

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

Tactic:
apply tendsto_atTop_add_const_right

Result:
case hf0.h.hf

⊢ Tendsto (fun x => 2 * ↑x) atTop atTop

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

Tactic:
have abel := tendsto_tsum_powerSeries_nhdsWithin_lt h

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)
⊢ Tendsto (fun k => ∑ i ∈ range k, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 (π / 4))

Proof state:
case h
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
⊢ Set.Ioo (-1) 1 ∈ 𝓝[<] 1 ∧ ∀ y ∈ Set.Ioo (-1) 1, y ^ 2 ∈ Set.Iio 1

Tactic:
exact ⟨Ioo_mem_nhdsLT <| by simp,
  fun _ _ ↦ by rwa [Set.mem_Iio, sq_lt_one_iff_abs_lt_one, abs_lt, ← Set.mem_Ioo]⟩

Result:
no goals