-- Mathlib/NumberTheory/LSeries/SumCoeff.lean
theorem LSeries_tendsto_sub_mul_nhds_one_of_tendsto_sum_div
    (hlim : Tendsto (fun n : ℕ ↦ (∑ k ∈ Icc 1 n, f k) / n) atTop (𝓝 l))
    (hfS : ∀ s : ℝ, 1 < s → LSeriesSummable f s) :
    Tendsto (fun s : ℝ ↦ (s - 1) * LSeries f s) (𝓝[>] 1) (𝓝 l)

Proof state:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n => (∑ 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:
obtain ⟨C, _, hC₂⟩ :=
  LSeries_tendsto_sub_mul_nhds_one_of_tendsto_sum_div_aux₃ hlim hfS zero_lt_one

Result:
case intro.intro
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n => (∑ 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₂ : (fun s => ‖(↑s - 1) * LSeries f ↑s - ↑s * l‖) ≤ᶠ[𝓝[>] 1] fun s => (s - 1) * s * C + s * 1
⊢ IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (𝓝[>] 1) fun s => ‖(↑s - 1) * LSeries f ↑s - ↑s * l‖

Proof state:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n => (∑ 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 (fun s => ↑s * l) 1

Tactic:
fun_prop

Result:
no goals

Proof state:
case e_x
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n => (∑ 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

Result:
no goals

Proof state:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n => (∑ 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

Result:
no goals

Proof state:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n => (∑ 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 - 1) * LSeries f ↑s) (𝓝[>] 1) (𝓝 (0 + 1 * l))

Tactic:
have h₃ : Tendsto (fun s : ℝ ↦ s * l) (𝓝[>] 1) (𝓝 (1 * l)) :=
  tendsto_nhdsWithin_of_tendsto_nhds (ContinuousAt.tendsto (by fun_prop))

Result:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n => (∑ 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))

Proof state:
case refine_2.intro.intro
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n => (∑ 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₂ : (fun s => ‖(↑s - 1) * LSeries f ↑s - ↑s * l‖) ≤ᶠ[𝓝[>] 1] 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 _)

Result:
no goals

Proof state:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n => (∑ 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 - 1) * LSeries f ↑s) (𝓝[>] 1) (𝓝 l)

Tactic:
rw [show 𝓝 l = 𝓝 (0 + 1 * l) by congr; ring]

Result:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n => (∑ 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 - 1) * LSeries f ↑s) (𝓝[>] 1) (𝓝 (0 + 1 * l))

Proof state:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n => (∑ 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) (𝓝 ((1 - 1) * 1 * C + 1 * ε))

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

Result:
no goals

Proof state:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n => (∑ 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) (𝓝[>] 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

Result:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n => (∑ 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)

Proof state:
case refine_2
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n => (∑ 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 < ε
⊢ 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ε

Result:
case refine_2.intro.intro
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n => (∑ 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₂ : (fun s => ‖(↑s - 1) * LSeries f ↑s - ↑s * l‖) ≤ᶠ[𝓝[>] 1] fun s => (s - 1) * s * C + s * ε
⊢ limsup (fun x => ‖(↑x - 1) * LSeries f ↑x - ↑x * l‖) (𝓝[>] 1) ≤ ε