-- Mathlib/NumberTheory/AbelSummation.lean
theorem tendsto_sum_mul_atTop_nhds_one_sub_integral₀ (hc : c 0 = 0)
    (hf_diff : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ f t)
    (hf_int : LocallyIntegrableOn (deriv f) (Set.Ici 1)) {l : 𝕜}
    (h_lim: Tendsto (fun n : ℕ ↦ f n * ∑ k ∈ Icc 0 n, c k) atTop (𝓝 l))
    {g : ℝ → ℝ} (hg_dom : (fun t ↦ deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k) =O[atTop] g)
    (hg_int : IntegrableAtFilter g atTop) :
    Tendsto (fun n : ℕ ↦ ∑ k ∈ Icc 0 n, f k * c k) atTop
      (𝓝 (l - ∫ t in Set.Ioi 1, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k))

Proof state:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hc : c 0 = 0
hf_diff : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ f t
hf_int : LocallyIntegrableOn (deriv f) (Set.Ici 1) volume
l : 𝕜
h_lim : Tendsto (fun n => f ↑n * ∑ k ∈ Icc 0 n, c k) atTop (𝓝 l)
g : ℝ → ℝ
hg_dom : (fun t => deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k) =O[atTop] g
hg_int : IntegrableAtFilter g atTop volume
h :
  (fun n => ∫ (x : ℝ) in 1 ..↑n, deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k) =ᶠ[atTop] fun n =>
    ∫ (t : ℝ) in Set.Ioc 1 ↑n, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k
⊢ IntegrableOn (fun x => deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k) (Set.Ioi 1) volume

Tactic:
exact integrableOn_Ici_iff_integrableOn_Ioi.mp
  <| (locallyIntegrableOn_mul_sum_Icc c zero_le_one hf_int).integrableOn_of_isBigO_atTop
    hg_dom hg_int

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hc : c 0 = 0
hf_diff : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ f t
hf_int : LocallyIntegrableOn (deriv f) (Set.Ici 1) volume
l : 𝕜
h_lim : Tendsto (fun n => f ↑n * ∑ k ∈ Icc 0 n, c k) atTop (𝓝 l)
g : ℝ → ℝ
hg_dom : (fun t => deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k) =O[atTop] g
hg_int : IntegrableAtFilter g atTop volume
h :
  (fun n => ∫ (x : ℝ) in 1 ..↑n, deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k) =ᶠ[atTop] fun n =>
    ∫ (t : ℝ) in Set.Ioc 1 ↑n, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k
⊢ Tendsto (fun n => ∑ k ∈ Icc 0 n, f ↑k * c k) atTop (𝓝 (l - ∫ (t : ℝ) in Set.Ioi 1, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k))

Tactic:
have h_lim' : Tendsto (fun n : ℕ ↦ ∫ t in Set.Ioc (1 : ℝ) n, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k)
    atTop (𝓝 (∫ t in Set.Ioi 1, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k)) := by
  refine Tendsto.congr' h (intervalIntegral_tendsto_integral_Ioi _ ?_ tendsto_natCast_atTop_atTop)
  exact integrableOn_Ici_iff_integrableOn_Ioi.mp
    <| (locallyIntegrableOn_mul_sum_Icc c zero_le_one hf_int).integrableOn_of_isBigO_atTop
      hg_dom hg_int

Result:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hc : c 0 = 0
hf_diff : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ f t
hf_int : LocallyIntegrableOn (deriv f) (Set.Ici 1) volume
l : 𝕜
h_lim : Tendsto (fun n => f ↑n * ∑ k ∈ Icc 0 n, c k) atTop (𝓝 l)
g : ℝ → ℝ
hg_dom : (fun t => deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k) =O[atTop] g
hg_int : IntegrableAtFilter g atTop volume
h :
  (fun n => ∫ (x : ℝ) in 1 ..↑n, deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k) =ᶠ[atTop] fun n =>
    ∫ (t : ℝ) in Set.Ioc 1 ↑n, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k
h_lim' :
  Tendsto (fun n => ∫ (t : ℝ) in Set.Ioc 1 ↑n, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k) atTop
    (𝓝 (∫ (t : ℝ) in Set.Ioi 1, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k))
⊢ Tendsto (fun n => ∑ k ∈ Icc 0 n, f ↑k * c k) atTop (𝓝 (l - ∫ (t : ℝ) in Set.Ioi 1, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k))

Proof state:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hc : c 0 = 0
hf_diff : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ f t
hf_int : LocallyIntegrableOn (deriv f) (Set.Ici 1) volume
l : 𝕜
h_lim : Tendsto (fun n => f ↑n * ∑ k ∈ Icc 0 n, c k) atTop (𝓝 l)
g : ℝ → ℝ
hg_dom : (fun t => deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k) =O[atTop] g
hg_int : IntegrableAtFilter g atTop volume
h :
  (fun n => ∫ (x : ℝ) in 1 ..↑n, deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k) =ᶠ[atTop] fun n =>
    ∫ (t : ℝ) in Set.Ioc 1 ↑n, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k
⊢ Tendsto (fun n => ∫ (t : ℝ) in Set.Ioc 1 ↑n, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k) atTop
    (𝓝 (∫ (t : ℝ) in Set.Ioi 1, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k))

Tactic:
refine Tendsto.congr' h (intervalIntegral_tendsto_integral_Ioi _ ?_ tendsto_natCast_atTop_atTop)

Result:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hc : c 0 = 0
hf_diff : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ f t
hf_int : LocallyIntegrableOn (deriv f) (Set.Ici 1) volume
l : 𝕜
h_lim : Tendsto (fun n => f ↑n * ∑ k ∈ Icc 0 n, c k) atTop (𝓝 l)
g : ℝ → ℝ
hg_dom : (fun t => deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k) =O[atTop] g
hg_int : IntegrableAtFilter g atTop volume
h :
  (fun n => ∫ (x : ℝ) in 1 ..↑n, deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k) =ᶠ[atTop] fun n =>
    ∫ (t : ℝ) in Set.Ioc 1 ↑n, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k
⊢ IntegrableOn (fun x => deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k) (Set.Ioi 1) volume