awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
h' : ¬Irrational (π / 2)
a : ℤ
b : ℕ
hb : 0 < b
h : π / 2 = HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)
ha : LT.lt (α := ℝ) 0 (↑a : ℝ)
k : ∀ (n : ℕ), 0 < HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ)
j : ∀ᶠ (n : ℕ) in atTop, HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ) * I n (π / 2) < 1
n : ℕ
hn : HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ) * I n (π / 2) < 1
hn' : 0 < HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ) * I n (π / 2)
z : ℤ
hz :
  eval₂ (Int.castRingHom ℝ) (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (sinPoly n) *
      HPow.hPow (α := ℝ) (↑b : ℝ) (2 * n + 1) =
    (↑z : ℝ)
e : I n (π / 2) * (π / 2) ^ (2 * n + 1) = (↑n ! : ℝ) * eval₂ (Int.castRingHom ℝ) (π / 2) (sinPoly n)
this :
  HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ) * I n (π / 2) =
    eval₂ (Int.castRingHom ℝ) (π / 2) (sinPoly n) * HPow.hPow (α := ℝ) (↑b : ℝ) (2 * n + 1)
⊢ LT.lt (α := ℝ) 0 (↑z : ℝ) ∧ LT.lt (α := ℝ) (↑z : ℝ) 1

Tactic:
have : (0 : ℝ) < z ∧ (z : ℝ) < 1 := by simp [← hz, ← h, ← this, hn', hn]
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
h' : ¬Irrational (π / 2)
a : ℤ
b : ℕ
hb : 0 < b
h : π / 2 = HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)
ha : LT.lt (α := ℝ) 0 (↑a : ℝ)
k : ∀ (n : ℕ), 0 < HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ)
j : ∀ᶠ (n : ℕ) in atTop, HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ) * I n (π / 2) < 1
n : ℕ
hn : HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ) * I n (π / 2) < 1
hn' : 0 < HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ) * I n (π / 2)
z : ℤ
hz :
  eval₂ (Int.castRingHom ℝ) (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (sinPoly n) *
      HPow.hPow (α := ℝ) (↑b : ℝ) (2 * n + 1) =
    (↑z : ℝ)
e : I n (π / 2) * (π / 2) ^ (2 * n + 1) = (↑n ! : ℝ) * eval₂ (Int.castRingHom ℝ) (π / 2) (sinPoly n)
this_1 :
  HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ) * I n (π / 2) =
    eval₂ (Int.castRingHom ℝ) (π / 2) (sinPoly n) * HPow.hPow (α := ℝ) (↑b : ℝ) (2 * n + 1)
this : LT.lt (α := ℝ) 0 (↑z : ℝ) ∧ LT.lt (α := ℝ) (↑z : ℝ) 1
⊢ 0 < z ∧ z < 1

Tactic:
norm_cast at this
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
h' : ¬Irrational (π / 2)
a : ℤ
b : ℕ
hb : 0 < b
h : π / 2 = HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)
ha : LT.lt (α := ℝ) 0 (↑a : ℝ)
k : ∀ (n : ℕ), 0 < HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ)
j : ∀ᶠ (n : ℕ) in atTop, HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ) * I n (π / 2) < 1
n : ℕ
hn : HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ) * I n (π / 2) < 1
hn' : 0 < HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ) * I n (π / 2)
z : ℤ
hz :
  eval₂ (Int.castRingHom ℝ) (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (sinPoly n) *
      HPow.hPow (α := ℝ) (↑b : ℝ) (2 * n + 1) =
    (↑z : ℝ)
e : I n (π / 2) * (π / 2) ^ (2 * n + 1) = (↑n ! : ℝ) * eval₂ (Int.castRingHom ℝ) (π / 2) (sinPoly n)
this_1 :
  HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ) * I n (π / 2) =
    eval₂ (Int.castRingHom ℝ) (π / 2) (sinPoly n) * HPow.hPow (α := ℝ) (↑b : ℝ) (2 * n + 1)
this : 0 < z ∧ z < 1
⊢ False

Tactic:
lia
-- Module: Mathlib.Analysis.Real.Pi.Leibniz
Goal:
hfa : Antitone (β := ℝ) fun (i : ℕ) ↦ (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)⁻¹
hf0 : Tendsto (β := ℝ) (fun (i : ℕ) ↦ (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)⁻¹) atTop (𝓝 0)
⊢ ∃ (l : ℝ),
    Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, HPow.hPow (α := ℝ) (-1) i / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)) atTop (𝓝 l)

Tactic:
apply Antitone.tendsto_alternating_series_of_tendsto_zero

Premises used: Antitone.tendsto_alternating_series_of_tendsto_zero
-- Module: Mathlib.Analysis.Real.Pi.Leibniz
Goal:
x x_1 : ℕ
h : x < x_1
hb : 0 < HMul.hMul (α := ℝ) 2 (↑x : ℝ) + 1
hba : LE.le (α := ℝ) 0 2
⊢ (HMul.hMul (α := ℝ) 2 (↑x_1 : ℝ) + 1)⁻¹ ≤ (HMul.hMul (α := ℝ) 2 (↑x : ℝ) + 1)⁻¹

Tactic:
gcongr
-- Module: Mathlib.Analysis.Real.Pi.Leibniz
Goal:
⊢ Antitone (β := ℝ) fun (i : ℕ) ↦ (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)⁻¹

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

Premises used: Iff.mpr, antitone_iff_forall_lt
-- Module: Mathlib.Analysis.Real.Pi.Leibniz
Goal:
hf0 : Tendsto (β := ℝ) (fun (i : ℕ) ↦ HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) atTop atTop
⊢ Tendsto (β := ℝ) (fun (i : ℕ) ↦ (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)⁻¹) atTop (𝓝 0)

Tactic:
apply Tendsto.inv_tendsto_atTop

Premises used: Filter.Tendsto.inv_tendsto_atTop
-- Module: Mathlib.Analysis.Real.Pi.Leibniz
Goal:
hf0 : Tendsto (β := ℝ) (fun (x : ℕ) ↦ HMul.hMul (α := ℝ) 2 (↑x : ℝ)) atTop atTop
⊢ Tendsto (β := ℝ) (fun (i : ℕ) ↦ HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) atTop atTop

Tactic:
apply tendsto_atTop_add_const_right

Premises used: Filter.tendsto_atTop_add_const_right
-- Module: Mathlib.Analysis.Real.Pi.Leibniz
Goal:
⊢ Tendsto (β := ℝ) (fun (x : ℕ) ↦ HMul.hMul (α := ℝ) 2 (↑x : ℝ)) atTop atTop

Tactic:
tendsto_natCast_atTop_atTop.const_mul_atTop zero_lt_two

Premises used: Filter.Tendsto.const_mul_atTop, tendsto_natCast_atTop_atTop, zero_lt_two
-- Module: Mathlib.Analysis.Real.Pi.Leibniz
Goal:
⊢ Tendsto (β := ℝ) (fun (x : ℕ) ↦ HMul.hMul (α := ℝ) 2 (↑x : ℝ)) atTop atTop

Tactic:
exact tendsto_natCast_atTop_atTop.const_mul_atTop zero_lt_two

Premises used: Filter.Tendsto.const_mul_atTop, tendsto_natCast_atTop_atTop
-- Module: Mathlib.Analysis.Real.Pi.Leibniz
Goal:
obtain :
  ∀ (l : ℝ)
    (h :
      Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, HPow.hPow (α := ℝ) (-1) i / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)) atTop
        (𝓝 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))

Tactic:
obtain ⟨l, h⟩ :
      ∃ l, Tendsto (fun n ↦ ∑ i ∈ range n, (-1 : ℝ) ^ i / (2 * i + 1)) atTop (𝓝 l) := by
    apply Antitone.tendsto_alternating_series_of_tendsto_zero
    · exact antitone_iff_forall_lt.mpr fun _ _ _ ↦ by gcongr
    · apply Tendsto.inv_tendsto_atTop; apply tendsto_atTop_add_const_right
      exact tendsto_natCast_atTop_atTop.const_mul_atTop zero_lt_two
-- Module: Mathlib.Analysis.Real.Pi.Leibniz
Goal:
l : ℝ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, HPow.hPow (α := ℝ) (-1) i / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)) atTop (𝓝 l)
⊢ Tendsto (fun (x : ℝ) ↦ ∑' (n : ℕ), HPow.hPow (α := ℝ) (-1) n / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * x ^ n) (𝓝[<] 1)
    (𝓝 l)

Tactic:
have abel := tendsto_tsum_powerSeries_nhdsWithin_lt h
-- Module: Mathlib.Analysis.Real.Pi.Leibniz
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)
⊢ LE.le (α := Filter ℝ) (𝓝[<] 1) (𝓝 1)

Tactic:
have m : 𝓝[<] (1 : ℝ) ≤ 𝓝 1 := tendsto_nhdsWithin_of_tendsto_nhds fun _ a ↦ a
-- Module: Mathlib.Analysis.Real.Pi.Leibniz
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)
h1 : Tendsto (β := ℝ) (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2) (𝓝[<] 1) (𝓝 1)
h2 : ∀ᶠ (x : ℝ) in 𝓝[<] 1, Membership.mem (γ := Set ℝ) (Set.Iio 1) (HPow.hPow (β := ℕ) x 2)
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2) (𝓝[<] 1) (𝓝[<] 1)

Tactic:
apply tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within

Premises used: tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within
-- Module: Mathlib.Analysis.Real.Pi.Leibniz
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)
h1 : Tendsto (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2) (𝓝[<] 1) (𝓝 (HPow.hPow (α := ℝ) (β := ℕ) 1 2))
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2) (𝓝[<] 1) (𝓝 1)

Tactic:
nth_rw 3 [← one_pow 2]

Premises used: one_pow, OfNat.ofNat
-- Module: Mathlib.Analysis.Real.Pi.Leibniz
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 (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2) (𝓝[<] 1) (𝓝 (HPow.hPow (α := ℝ) (β := ℕ) 1 2))

Tactic:
Tendsto.pow ‹_› _

Premises used: Filter.Tendsto.pow
-- Module: Mathlib.Analysis.Real.Pi.Leibniz
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 (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2) (𝓝[<] 1) (𝓝 (HPow.hPow (α := ℝ) (β := ℕ) 1 2))

Tactic:
exact Tendsto.pow ‹_› _

Premises used: Filter.Tendsto.pow
-- Module: Mathlib.Analysis.Real.Pi.Leibniz
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)
h2 :
  ∃ (v : Set ℝ),
    Membership.mem (γ := Filter ℝ) (𝓝[<] 1) v ∧
      ∀ y ∈ v, Membership.mem (γ := Set ℝ) (Set.Iio 1) (HPow.hPow (β := ℕ) y 2)
⊢ ∀ᶠ (x : ℝ) in 𝓝[<] 1, Membership.mem (γ := Set ℝ) (Set.Iio 1) (HPow.hPow (β := ℕ) x 2)

Tactic:
rw [eventually_iff_exists_mem]

Premises used: Filter.eventually_iff_exists_mem
-- Module: Mathlib.Analysis.Real.Pi.Leibniz
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)
h₁ :
  Membership.mem (γ := Filter ℝ) (𝓝[<] 1) (Set.Ioo (-1) 1) ∧
    ∀ (y : ℝ),
      Membership.mem (γ := Set ℝ) (Set.Ioo (-1) 1) y → Membership.mem (γ := Set ℝ) (Set.Iio 1) (HPow.hPow (β := ℕ) y 2)
⊢ ∃ (v : Set ℝ),
    Membership.mem (γ := Filter ℝ) (𝓝[<] 1) v ∧
      ∀ y ∈ v, Membership.mem (γ := Set ℝ) (Set.Iio 1) (HPow.hPow (β := ℕ) y 2)

Tactic:
use Set.Ioo (-1) 1

Premises used: OfNat.ofNat, Set.Ioo, Neg.neg
-- Module: Mathlib.Analysis.Real.Pi.Leibniz
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)
⊢ LT.lt (α := ℝ) (-1) 1

Tactic:
simp
-- Module: Mathlib.Analysis.Real.Pi.Leibniz
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)
x : ℝ
h_1 : Membership.mem (γ := Set ℝ) (Set.Ioo (-1) 1) x
rwa : HPow.hPow (β := ℕ) x 2 < 1
rwa₁ : |x| < 1
rwa₂ : -1 < x ∧ x < 1
rwa₃ rwa₄ rwa₅ rwa₆ : Membership.mem (γ := Set ℝ) (Set.Ioo (-1) 1) x
⊢ Membership.mem (γ := Set ℝ) (Set.Iio 1) (HPow.hPow (β := ℕ) x 2)

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

Premises used: Set.mem_Iio, Set.mem_Ioo, sq_lt_one_iff_abs_lt_one, abs_lt
-- Module: Mathlib.Analysis.Real.Pi.Leibniz
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)
⊢ Membership.mem (γ := Filter ℝ) (𝓝[<] 1) (Set.Ioo (-1) 1) ∧
    ∀ (y : ℝ),
      Membership.mem (γ := Set ℝ) (Set.Ioo (-1) 1) y → Membership.mem (γ := Set ℝ) (Set.Iio 1) (HPow.hPow (β := ℕ) y 2)

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]⟩
-- Module: Mathlib.Analysis.Real.Pi.Leibniz
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 (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]⟩
-- Module: Mathlib.Analysis.Real.Pi.Leibniz
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 (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
-- Module: Mathlib.Analysis.Real.Pi.Leibniz
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 (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

Premises used: mul_one
-- Module: Mathlib.Analysis.Real.Pi.Leibniz
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)
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
⊢ Tendsto arctan (𝓝[<] 1) (𝓝 l)

Tactic:
apply abel.congr'

Premises used: Filter.Tendsto.congr'
-- Module: Mathlib.Analysis.Real.Pi.Leibniz
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)
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
⊢ (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:
rw [eventuallyEq_nhdsWithin_iff, Metric.eventually_nhds_iff]

Premises used: Metric.eventually_nhds_iff, eventuallyEq_nhdsWithin_iff
-- Module: Mathlib.Analysis.Real.Pi.Leibniz
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)
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
⊢ ∃ ε > 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:
use 1, zero_lt_one

Premises used: zero_lt_one
-- Module: Mathlib.Analysis.Real.Pi.Leibniz
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
⊢ y - 1 < 1 ∧ 1 - y < 1

Tactic:
rw [dist_eq, abs_sub_lt_iff] at hy1

Premises used: abs_sub_lt_iff, Real.dist_eq
-- Module: Mathlib.Analysis.Real.Pi.Leibniz
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
hy1₁ : y - 1 < 1 ∧ 1 - y < 1
⊢ Membership.mem (γ := Set ℝ) (Set.Iio 1) y

Tactic:
rw [dist_eq, abs_sub_lt_iff] at hy1

Premises used: abs_sub_lt_iff, Real.dist_eq
-- Module: Mathlib.Analysis.Real.Pi.Leibniz
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
⊢ y < 1

Tactic:
rw [Set.mem_Iio] at hy2

Premises used: Set.mem_Iio
-- Module: Mathlib.Analysis.Real.Pi.Leibniz
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
rw : -1 < y ∧ y < 1
⊢ ‖y‖ < 1

Tactic:
rw [norm_eq_abs, abs_lt]

Premises used: abs_lt, Real.norm_eq_abs
-- Module: Mathlib.Analysis.Real.Pi.Leibniz
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
left : -1 < y
right : y < 1
⊢ -1 < y ∧ y < 1

Tactic:
constructor
-- Module: Mathlib.Analysis.Real.Pi.Leibniz
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
linarith₁ : y ≤ -1 → GT.gt (α := ℝ) 2 0
⊢ -1 < y

Tactic:
linarith
-- Module: Mathlib.Analysis.Real.Pi.Leibniz
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 : 1 ≤ y → y - 1 + (1 - y) = 0
⊢ y < 1

Tactic:
linarith
-- Module: Mathlib.Analysis.Real.Pi.Leibniz
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

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