-- 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) (𝓝 ε)
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:
refine tendsto_zero_iff_norm_tendsto_zero.mpr <| tendsto_of_le_liminf_of_limsup_le ?_ ?_ h₂ ?_

Result:
case refine_1
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‖
⊢ 0 ≤ liminf (fun x => ‖(↑x - 1) * LSeries f ↑x - ↑x * l‖) (𝓝[>] 1)

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‖
⊢ limsup (fun x => ‖(↑x - 1) * LSeries f ↑x - ↑x * l‖) (𝓝[>] 1) ≤ 0

case refine_3
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‖
⊢ IsBoundedUnder (fun x1 x2 => x1 ≥ x2) (𝓝[>] 1) fun x => ‖(↑x - 1) * LSeries f ↑x - ↑x * 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 ε : ℝ
⊢ ContinuousAt (fun s => (s - 1) * s * C + s * ε) 1

Tactic:
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‖
this : Tendsto (fun s => (↑s - 1) * LSeries f ↑s - ↑s * l) (𝓝[>] 1) (𝓝 0)
⊢ 𝓝 l = 𝓝 (0 + 1 * l)

Tactic:
congr

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

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) ≤ 0 + ε

Tactic:
rw [zero_add]

Result:
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) ≤ ε

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 ε : ℝ
⊢ 𝓝 ε = 𝓝 ((1 - 1) * 1 * C + 1 * ε)

Tactic:
congr

Result:
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
C ε : ℝ
⊢ ε = (1 - 1) * 1 * C + 1 * ε