awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f (↑s : ℂ)
ε : ℝ
hε : ε > 0
T : ℝ
hT₁ : 1 ≤ T
hT : ∀ (y : ℝ), T ≤ y → ‖∑ k ∈ Icc 1 ⌊y⌋₊, f k - l * (↑y : ℂ)‖ < ε * y
S : ℝ → ℂ := fun (t : ℝ) ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k
C : ℝ :=
  @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 T)) fun (t : ℝ) ↦
    ‖S t - l * (↑t : ℂ)‖ * t ^ HSub.hSub (α := ℝ) (-1) 1
hC : 0 ≤ C
s : ℝ
hs : 1 < s
hs' : 0 ≤ (s - 1) * s
h₀ : LocallyIntegrableOn (ε := ℂ) (fun (t : ℝ) ↦ S t - l * (↑t : ℂ)) (Set.Ici 1) volume
h₁ :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1))
    (Set.Ici 1) volume
h₂ :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (t : ℝ) ↦ ‖S t - l * (↑t : ℂ)‖ * t ^ HSub.hSub (α := ℝ) (-1) 1) (Set.Ioc 1 T) volume
h₃ :
  (((↑s : ℂ) - 1) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 1)) fun (t : ℝ) ↦
        (↑t : ℂ) ^ (-(↑s : ℂ))) =
    1
Cs : ℝ :=
  @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 T)) fun (t : ℝ) ↦
    ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1)
h₄ : Cs ≤ C
⊢ ((s - 1) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi T)) fun (t : ℝ) ↦
        ‖S t - l * (↑t : ℂ)‖ * t ^ (-s - 1)) ≤
    ε

Tactic:
exact LSeries_tendsto_sub_mul_nhds_one_of_tendsto_sum_div_aux₂ h₀ hε hs hT₁
        fun t ht ↦ (hT t ht.le).le

Premises used: LT.lt.le, _private.0.LSeries_tendsto_sub_mul_nhds_one_of_tendsto_sum_div_aux₂, GE.ge.le
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f (↑s : ℂ)
C ε : ℝ
e_x : ε = HSub.hSub (α := ℝ) 1 1 * 1 * C + 1 * ε
⊢ 𝓝 ε = 𝓝 (HSub.hSub (α := ℝ) 1 1 * 1 * C + 1 * ε)

Tactic:
congr
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f (↑s : ℂ)
C ε : ℝ
⊢ ε = HSub.hSub (α := ℝ) 1 1 * 1 * C + 1 * ε

Tactic:
ring
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f (↑s : ℂ)
C ε : ℝ
rw : Tendsto (fun (s : ℝ) ↦ (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 (HSub.hSub (α := ℝ) 1 1 * 1 * C + 1 * ε))
⊢ Tendsto (fun (s : ℝ) ↦ (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ε)

Tactic:
rw [show 𝓝 ε = 𝓝 ((1 - 1) * 1 * C + 1 * ε) by congr; ring]
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f (↑s : ℂ)
C ε : ℝ
⊢ ContinuousAt (Y := ℝ) (fun (s : ℝ) ↦ (s - 1) * s * C + s * ε) 1

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f (↑s : ℂ)
C ε : ℝ
⊢ Tendsto (fun (s : ℝ) ↦ (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 (HSub.hSub (α := ℝ) 1 1 * 1 * C + 1 * ε))

Tactic:
exact tendsto_nhdsWithin_of_tendsto_nhds (ContinuousAt.tendsto (by fun_prop))

Premises used: tendsto_nhdsWithin_of_tendsto_nhds, ContinuousAt.tendsto
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f (↑s : ℂ)
⊢ ∀ {C ε : ℝ}, Tendsto (fun (s : ℝ) ↦ (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ε)

Tactic:
have h₁ {C ε : ℝ} : Tendsto (fun s ↦ (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ε) := by
    rw [show 𝓝 ε = 𝓝 ((1 - 1) * 1 * C + 1 * ε) by congr; ring]
    exact tendsto_nhdsWithin_of_tendsto_nhds (ContinuousAt.tendsto (by fun_prop))
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f (↑s : ℂ)
h₁ : ∀ {C ε : ℝ}, Tendsto (fun (s : ℝ) ↦ (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ε)
obtain :
  ∀ C ≥ 0,
    ∀
      (hC₂ :
        EventuallyLE (β := ℝ) (𝓝[>] 1) (fun (s : ℝ) ↦ ‖((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l‖)
          fun (s : ℝ) ↦ (s - 1) * s * C + s * 1),
      IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝[>] 1) fun (s : ℝ) ↦
        ‖((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l‖
⊢ IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝[>] 1) fun (s : ℝ) ↦ ‖((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l‖

Tactic:
obtain ⟨C, _, hC₂⟩ :=
      LSeries_tendsto_sub_mul_nhds_one_of_tendsto_sum_div_aux₃ hlim hfS zero_lt_one

Premises used: zero_lt_one, _private.0.LSeries_tendsto_sub_mul_nhds_one_of_tendsto_sum_div_aux₃
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f (↑s : ℂ)
h₁ : ∀ {C ε : ℝ}, Tendsto (fun (s : ℝ) ↦ (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ε)
C : ℝ
left : C ≥ 0
hC₂ :
  EventuallyLE (β := ℝ) (𝓝[>] 1) (fun (s : ℝ) ↦ ‖((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l‖) fun (s : ℝ) ↦
    (s - 1) * s * C + s * 1
⊢ IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝[>] 1) fun (s : ℝ) ↦ ‖((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l‖

Tactic:
h₁.isBoundedUnder_le.mono_le hC₂

Premises used: Filter.Tendsto.isBoundedUnder_le, Filter.IsBoundedUnder.mono_le
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f (↑s : ℂ)
h₁ : ∀ {C ε : ℝ}, Tendsto (fun (s : ℝ) ↦ (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ε)
C : ℝ
left : C ≥ 0
hC₂ :
  EventuallyLE (β := ℝ) (𝓝[>] 1) (fun (s : ℝ) ↦ ‖((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l‖) fun (s : ℝ) ↦
    (s - 1) * s * C + s * 1
⊢ IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝[>] 1) fun (s : ℝ) ↦ ‖((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l‖

Tactic:
exact h₁.isBoundedUnder_le.mono_le hC₂

Premises used: Filter.Tendsto.isBoundedUnder_le, Filter.IsBoundedUnder.mono_le
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f (↑s : ℂ)
h₁ : ∀ {C ε : ℝ}, Tendsto (fun (s : ℝ) ↦ (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ε)
⊢ IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝[>] 1) fun (s : ℝ) ↦ ‖((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l‖

Tactic:
have h₂ : IsBoundedUnder
      (fun x1 x2 ↦ x1 ≤ x2) (𝓝[>] 1) fun s : ℝ ↦ ‖(s - 1) * LSeries f s - s * l‖ := by
    obtain ⟨C, _, hC₂⟩ :=
      LSeries_tendsto_sub_mul_nhds_one_of_tendsto_sum_div_aux₃ hlim hfS zero_lt_one
    exact h₁.isBoundedUnder_le.mono_le hC₂
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f (↑s : ℂ)
h₁ : ∀ {C ε : ℝ}, Tendsto (fun (s : ℝ) ↦ (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ε)
h₂ :
  IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝[>] 1) fun (s : ℝ) ↦ ‖((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l‖
this : Tendsto (β := ℂ) (fun (s : ℝ) ↦ ((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l) (𝓝[>] 1) (𝓝 0)
e_x : l = 0 + 1 * l
⊢ 𝓝 l = 𝓝 (0 + 1 * l)

Tactic:
congr
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f (↑s : ℂ)
h₁ : ∀ {C ε : ℝ}, Tendsto (fun (s : ℝ) ↦ (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ε)
h₂ :
  IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝[>] 1) fun (s : ℝ) ↦ ‖((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l‖
this : Tendsto (β := ℂ) (fun (s : ℝ) ↦ ((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l) (𝓝[>] 1) (𝓝 0)
⊢ l = 0 + 1 * l

Tactic:
ring
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f (↑s : ℂ)
h₁ : ∀ {C ε : ℝ}, Tendsto (fun (s : ℝ) ↦ (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ε)
h₂ :
  IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝[>] 1) fun (s : ℝ) ↦ ‖((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l‖
this : Tendsto (β := ℂ) (fun (s : ℝ) ↦ ((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l) (𝓝[>] 1) (𝓝 0)
rw : Tendsto (fun (s : ℝ) ↦ ((↑s : ℂ) - 1) * LSeries f (↑s : ℂ)) (𝓝[>] 1) (𝓝 (0 + 1 * l))
⊢ Tendsto (fun (s : ℝ) ↦ ((↑s : ℂ) - 1) * LSeries f (↑s : ℂ)) (𝓝[>] 1) (𝓝 l)

Tactic:
rw [show 𝓝 l = 𝓝 (0 + 1 * l) by congr; ring]
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f (↑s : ℂ)
h₁ : ∀ {C ε : ℝ}, Tendsto (fun (s : ℝ) ↦ (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ε)
h₂ :
  IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝[>] 1) fun (s : ℝ) ↦ ‖((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l‖
this : Tendsto (β := ℂ) (fun (s : ℝ) ↦ ((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l) (𝓝[>] 1) (𝓝 0)
⊢ ContinuousAt (Y := ℂ) (fun (s : ℝ) ↦ (↑s : ℂ) * l) 1

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f (↑s : ℂ)
h₁ : ∀ {C ε : ℝ}, Tendsto (fun (s : ℝ) ↦ (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ε)
h₂ :
  IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝[>] 1) fun (s : ℝ) ↦ ‖((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l‖
this : Tendsto (β := ℂ) (fun (s : ℝ) ↦ ((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l) (𝓝[>] 1) (𝓝 0)
⊢ Tendsto (fun (s : ℝ) ↦ (↑s : ℂ) * l) (𝓝[>] 1) (𝓝 (1 * l))

Tactic:
have h₃ : Tendsto (fun s : ℝ ↦ s * l) (𝓝[>] 1) (𝓝 (1 * l)) :=
      tendsto_nhdsWithin_of_tendsto_nhds (ContinuousAt.tendsto (by fun_prop))
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f (↑s : ℂ)
h₁ : ∀ {C ε : ℝ}, Tendsto (fun (s : ℝ) ↦ (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ε)
h₂ :
  IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝[>] 1) fun (s : ℝ) ↦ ‖((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l‖
this : Tendsto (β := ℂ) (fun (s : ℝ) ↦ ((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l) (𝓝[>] 1) (𝓝 0)
h₃ : Tendsto (fun (s : ℝ) ↦ (↑s : ℂ) * l) (𝓝[>] 1) (𝓝 (1 * l))
x : ℝ
⊢ ((↑x : ℂ) - 1) * LSeries f (↑x : ℂ) - (↑x : ℂ) * l + (↑x : ℂ) * l = ((↑x : ℂ) - 1) * LSeries f (↑x : ℂ)

Tactic:
ring
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f (↑s : ℂ)
h₁ : ∀ {C ε : ℝ}, Tendsto (fun (s : ℝ) ↦ (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ε)
h₂ :
  IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝[>] 1) fun (s : ℝ) ↦ ‖((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l‖
this : Tendsto (β := ℂ) (fun (s : ℝ) ↦ ((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l) (𝓝[>] 1) (𝓝 0)
h₃ : Tendsto (fun (s : ℝ) ↦ (↑s : ℂ) * l) (𝓝[>] 1) (𝓝 (1 * l))
⊢ Tendsto (fun (s : ℝ) ↦ ((↑s : ℂ) - 1) * LSeries f (↑s : ℂ)) (𝓝[>] 1) (𝓝 (0 + 1 * l))

Tactic:
exact (this.add h₃).congr fun _ ↦ by ring

Premises used: Filter.Tendsto.add, Filter.Tendsto.congr
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f (↑s : ℂ)
h₁ : ∀ {C ε : ℝ}, Tendsto (fun (s : ℝ) ↦ (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ε)
h₂ :
  IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝[>] 1) fun (s : ℝ) ↦ ‖((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l‖
suffices : Tendsto (β := ℂ) (fun (s : ℝ) ↦ ((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l) (𝓝[>] 1) (𝓝 0)
⊢ Tendsto (fun (s : ℝ) ↦ ((↑s : ℂ) - 1) * LSeries f (↑s : ℂ)) (𝓝[>] 1) (𝓝 l)

Tactic:
suffices Tendsto (fun s : ℝ ↦ (s - 1) * LSeries f s - s * l) (𝓝[>] 1) (𝓝 0) by
    rw [show 𝓝 l = 𝓝 (0 + 1 * l) by congr; ring]
    have h₃ : Tendsto (fun s : ℝ ↦ s * l) (𝓝[>] 1) (𝓝 (1 * l)) :=
      tendsto_nhdsWithin_of_tendsto_nhds (ContinuousAt.tendsto (by fun_prop))
    exact (this.add h₃).congr fun _ ↦ by ring
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f (↑s : ℂ)
h₁ : ∀ {C ε : ℝ}, Tendsto (fun (s : ℝ) ↦ (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ε)
h₂ :
  IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝[>] 1) fun (s : ℝ) ↦ ‖((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l‖
⊢ Tendsto (β := ℂ) (fun (s : ℝ) ↦ ((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l) (𝓝[>] 1) (𝓝 0)

Tactic:
tendsto_zero_iff_norm_tendsto_zero.mpr <| tendsto_of_le_liminf_of_limsup_le ?_ ?_ h₂ ?_

Premises used: Iff.mpr, tendsto_zero_iff_norm_tendsto_zero, tendsto_of_le_liminf_of_limsup_le
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f (↑s : ℂ)
h₁ : ∀ {C ε : ℝ}, Tendsto (fun (s : ℝ) ↦ (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ε)
h₂ :
  IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝[>] 1) fun (s : ℝ) ↦ ‖((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l‖
refine_1 : LE.le (α := ℝ) 0 (liminf (fun (x : ℝ) ↦ ‖((↑x : ℂ) - 1) * LSeries f (↑x : ℂ) - (↑x : ℂ) * l‖) (𝓝[>] 1))
refine_2 : LE.le (α := ℝ) (limsup (fun (x : ℝ) ↦ ‖((↑x : ℂ) - 1) * LSeries f (↑x : ℂ) - (↑x : ℂ) * l‖) (𝓝[>] 1)) 0
refine_3 :
  IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) (𝓝[>] 1) fun (x : ℝ) ↦ ‖((↑x : ℂ) - 1) * LSeries f (↑x : ℂ) - (↑x : ℂ) * l‖
⊢ Tendsto (β := ℂ) (fun (s : ℝ) ↦ ((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l) (𝓝[>] 1) (𝓝 0)

Tactic:
refine tendsto_zero_iff_norm_tendsto_zero.mpr <| tendsto_of_le_liminf_of_limsup_le ?_ ?_ h₂ ?_

Premises used: Iff.mpr, tendsto_zero_iff_norm_tendsto_zero, tendsto_of_le_liminf_of_limsup_le
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f (↑s : ℂ)
h₁ : ∀ {C ε : ℝ}, Tendsto (fun (s : ℝ) ↦ (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ε)
h₂ :
  IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝[>] 1) fun (s : ℝ) ↦ ‖((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l‖
⊢ LE.le (α := ℝ) 0 (liminf (fun (x : ℝ) ↦ ‖((↑x : ℂ) - 1) * LSeries f (↑x : ℂ) - (↑x : ℂ) * l‖) (𝓝[>] 1))

Tactic:
le_liminf_of_le h₂.isCoboundedUnder_ge (univ_mem' (fun _ ↦ norm_nonneg _))

Premises used: HMul.hMul, HSub.hSub, Complex.ofReal, LSeries, Filter.IsBoundedUnder.isCoboundedUnder_ge, OfNat.ofNat, norm_nonneg, Filter.univ_mem', Filter.le_liminf_of_le
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f (↑s : ℂ)
h₁ : ∀ {C ε : ℝ}, Tendsto (fun (s : ℝ) ↦ (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ε)
h₂ :
  IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝[>] 1) fun (s : ℝ) ↦ ‖((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l‖
⊢ LE.le (α := ℝ) 0 (liminf (fun (x : ℝ) ↦ ‖((↑x : ℂ) - 1) * LSeries f (↑x : ℂ) - (↑x : ℂ) * l‖) (𝓝[>] 1))

Tactic:
exact le_liminf_of_le h₂.isCoboundedUnder_ge (univ_mem' (fun _ ↦ norm_nonneg _))

Premises used: HMul.hMul, HSub.hSub, Complex.ofReal, LSeries, Filter.IsBoundedUnder.isCoboundedUnder_ge, OfNat.ofNat, norm_nonneg, Filter.univ_mem', Filter.le_liminf_of_le
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f (↑s : ℂ)
h₁ : ∀ {C ε : ℝ}, Tendsto (fun (s : ℝ) ↦ (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ε)
h₂ :
  IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝[>] 1) fun (s : ℝ) ↦ ‖((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l‖
⊢ LE.le (α := ℝ) (limsup (fun (x : ℝ) ↦ ‖((↑x : ℂ) - 1) * LSeries f (↑x : ℂ) - (↑x : ℂ) * l‖) (𝓝[>] 1)) 0

Tactic:
le_of_forall_pos_le_add fun ε hε ↦ ?_

Premises used: le_of_forall_pos_le_add
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f (↑s : ℂ)
h₁ : ∀ {C ε : ℝ}, Tendsto (fun (s : ℝ) ↦ (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ε)
h₂ :
  IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝[>] 1) fun (s : ℝ) ↦ ‖((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l‖
refine_2 :
  ∀ (ε : ℝ) (hε : 0 < ε), limsup (fun (x : ℝ) ↦ ‖((↑x : ℂ) - 1) * LSeries f (↑x : ℂ) - (↑x : ℂ) * l‖) (𝓝[>] 1) ≤ 0 + ε
⊢ LE.le (α := ℝ) (limsup (fun (x : ℝ) ↦ ‖((↑x : ℂ) - 1) * LSeries f (↑x : ℂ) - (↑x : ℂ) * l‖) (𝓝[>] 1)) 0

Tactic:
refine le_of_forall_pos_le_add fun ε hε ↦ ?_

Premises used: le_of_forall_pos_le_add
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f (↑s : ℂ)
h₁ : ∀ {C ε : ℝ}, Tendsto (fun (s : ℝ) ↦ (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ε)
h₂ :
  IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝[>] 1) fun (s : ℝ) ↦ ‖((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l‖
ε : ℝ
hε : 0 < ε
refine_2 : limsup (fun (x : ℝ) ↦ ‖((↑x : ℂ) - 1) * LSeries f (↑x : ℂ) - (↑x : ℂ) * l‖) (𝓝[>] 1) ≤ ε
⊢ limsup (fun (x : ℝ) ↦ ‖((↑x : ℂ) - 1) * LSeries f (↑x : ℂ) - (↑x : ℂ) * l‖) (𝓝[>] 1) ≤ 0 + ε

Tactic:
rw [zero_add]

Premises used: zero_add
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f (↑s : ℂ)
h₁ : ∀ {C ε : ℝ}, Tendsto (fun (s : ℝ) ↦ (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ε)
h₂ :
  IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝[>] 1) fun (s : ℝ) ↦ ‖((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l‖
ε : ℝ
hε : 0 < ε
refine_2 :
  ∀ (C : ℝ) (hC₁ : C ≥ 0)
    (hC₂ :
      EventuallyLE (β := ℝ) (𝓝[>] 1) (fun (s : ℝ) ↦ ‖((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l‖) fun (s : ℝ) ↦
        (s - 1) * s * C + s * ε),
    limsup (fun (x : ℝ) ↦ ‖((↑x : ℂ) - 1) * LSeries f (↑x : ℂ) - (↑x : ℂ) * l‖) (𝓝[>] 1) ≤ ε
⊢ limsup (fun (x : ℝ) ↦ ‖((↑x : ℂ) - 1) * LSeries f (↑x : ℂ) - (↑x : ℂ) * l‖) (𝓝[>] 1) ≤ ε

Tactic:
obtain ⟨C, hC₁, hC₂⟩ := LSeries_tendsto_sub_mul_nhds_one_of_tendsto_sum_div_aux₃ hlim hfS hε

Premises used: _private.0.LSeries_tendsto_sub_mul_nhds_one_of_tendsto_sum_div_aux₃
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f (↑s : ℂ)
h₁ : ∀ {C ε : ℝ}, Tendsto (fun (s : ℝ) ↦ (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ε)
h₂ :
  IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝[>] 1) fun (s : ℝ) ↦ ‖((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l‖
ε : ℝ
hε : 0 < ε
C : ℝ
hC₁ : C ≥ 0
hC₂ :
  EventuallyLE (β := ℝ) (𝓝[>] 1) (fun (s : ℝ) ↦ ‖((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l‖) fun (s : ℝ) ↦
    (s - 1) * s * C + s * ε
⊢ limsup (fun (x : ℝ) ↦ ‖((↑x : ℂ) - 1) * LSeries f (↑x : ℂ) - (↑x : ℂ) * l‖) (𝓝[>] 1) ≤ ε

Tactic:
le_of_le_of_eq (limsup_le_limsup hC₂ ?_ h₁.isBoundedUnder_le) h₁.limsup_eq

Premises used: Filter.Tendsto.limsup_eq, Filter.Tendsto.isBoundedUnder_le, le_of_le_of_eq, Filter.limsup_le_limsup
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f (↑s : ℂ)
h₁ : ∀ {C ε : ℝ}, Tendsto (fun (s : ℝ) ↦ (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ε)
h₂ :
  IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝[>] 1) fun (s : ℝ) ↦ ‖((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l‖
ε : ℝ
hε : 0 < ε
C : ℝ
hC₁ : C ≥ 0
hC₂ :
  EventuallyLE (β := ℝ) (𝓝[>] 1) (fun (s : ℝ) ↦ ‖((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l‖) fun (s : ℝ) ↦
    (s - 1) * s * C + s * ε
refine_2 :
  IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝[>] 1) fun (x : ℝ) ↦
    ‖((↑x : ℂ) - 1) * LSeries f (↑x : ℂ) - (↑x : ℂ) * l‖
⊢ limsup (fun (x : ℝ) ↦ ‖((↑x : ℂ) - 1) * LSeries f (↑x : ℂ) - (↑x : ℂ) * l‖) (𝓝[>] 1) ≤ ε

Tactic:
refine le_of_le_of_eq (limsup_le_limsup hC₂ ?_ h₁.isBoundedUnder_le) h₁.limsup_eq

Premises used: Filter.Tendsto.limsup_eq, Filter.Tendsto.isBoundedUnder_le, le_of_le_of_eq, Filter.limsup_le_limsup
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f (↑s : ℂ)
h₁ : ∀ {C ε : ℝ}, Tendsto (fun (s : ℝ) ↦ (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ε)
h₂ :
  IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝[>] 1) fun (s : ℝ) ↦ ‖((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l‖
ε : ℝ
hε : 0 < ε
C : ℝ
hC₁ : C ≥ 0
hC₂ :
  EventuallyLE (β := ℝ) (𝓝[>] 1) (fun (s : ℝ) ↦ ‖((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l‖) fun (s : ℝ) ↦
    (s - 1) * s * C + s * ε
⊢ IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝[>] 1) fun (x : ℝ) ↦
    ‖((↑x : ℂ) - 1) * LSeries f (↑x : ℂ) - (↑x : ℂ) * l‖

Tactic:
isCoboundedUnder_le_of_eventually_le _ (univ_mem' fun _ ↦ norm_nonneg _)

Premises used: HMul.hMul, HSub.hSub, Complex.ofReal, LSeries, Filter.isCoboundedUnder_le_of_eventually_le, OfNat.ofNat, norm_nonneg, Filter.univ_mem'
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f (↑s : ℂ)
h₁ : ∀ {C ε : ℝ}, Tendsto (fun (s : ℝ) ↦ (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ε)
h₂ :
  IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝[>] 1) fun (s : ℝ) ↦ ‖((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l‖
ε : ℝ
hε : 0 < ε
C : ℝ
hC₁ : C ≥ 0
hC₂ :
  EventuallyLE (β := ℝ) (𝓝[>] 1) (fun (s : ℝ) ↦ ‖((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l‖) fun (s : ℝ) ↦
    (s - 1) * s * C + s * ε
⊢ IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝[>] 1) fun (x : ℝ) ↦
    ‖((↑x : ℂ) - 1) * LSeries f (↑x : ℂ) - (↑x : ℂ) * l‖

Tactic:
exact isCoboundedUnder_le_of_eventually_le _ (univ_mem' fun _ ↦ norm_nonneg _)

Premises used: Filter.isCoboundedUnder_le_of_eventually_le, Filter.univ_mem'
-- Module: Mathlib.NumberTheory.LSeries.SumCoeff
Goal:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) (∑ k ∈ Icc 1 n, f k) (↑n : ℂ)) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f (↑s : ℂ)
h₁ : ∀ {C ε : ℝ}, Tendsto (fun (s : ℝ) ↦ (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ε)
h₂ :
  IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝[>] 1) fun (s : ℝ) ↦ ‖((↑s : ℂ) - 1) * LSeries f (↑s : ℂ) - (↑s : ℂ) * l‖
⊢ IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) (𝓝[>] 1) fun (x : ℝ) ↦ ‖((↑x : ℂ) - 1) * LSeries f (↑x : ℂ) - (↑x : ℂ) * l‖

Tactic:
isBoundedUnder_of_eventually_ge (univ_mem' fun _ ↦ norm_nonneg _)

Premises used: HMul.hMul, HSub.hSub, Complex.ofReal, LSeries, Filter.isBoundedUnder_of_eventually_ge, OfNat.ofNat, norm_nonneg, Filter.univ_mem'