-- Mathlib/NumberTheory/AbelSummation.lean
theorem summable_mul_of_bigO_atTop_aux (m : ℕ)
    (h_bdd : (fun n : ℕ ↦ ‖f n‖ * ∑ k ∈ Icc 0 n, ‖c k‖) =O[atTop] fun _ ↦ (1 : ℝ))
    (hf_int : LocallyIntegrableOn (deriv (fun t ↦ ‖f t‖)) (Set.Ici (m : ℝ)))
    (hf : ∀ n : ℕ, ∑ k ∈ Icc 0 n, ‖f k‖ * ‖c k‖ =
      ‖f n‖ * ∑ k ∈ Icc 0 n, ‖c k‖ -
        ∫ (t : ℝ) in Set.Ioc ↑m ↑n, deriv (fun t ↦ ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖)
    {g : ℝ → ℝ}
    (hg₁ : (fun t ↦ deriv (fun t ↦ ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖) =O[atTop] g)
    (hg₂ : IntegrableAtFilter g atTop) :
    Summable (fun n : ℕ ↦ f n * c n)

Proof state:
case intro.zero
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
m : ℕ
h_bdd : (fun n => ‖f ↑n‖ * ∑ k ∈ Icc 0 n, ‖c k‖) =O[atTop] fun x => 1
hf_int : LocallyIntegrableOn (deriv fun t => ‖f t‖) (Set.Ici ↑m) volume
hf :
  ∀ (n : ℕ),
    ∑ k ∈ Icc 0 n, ‖f ↑k‖ * ‖c k‖ =
      ‖f ↑n‖ * ∑ k ∈ Icc 0 n, ‖c k‖ - ∫ (t : ℝ) in Set.Ioc ↑m ↑n, deriv (fun t => ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖
g : ℝ → ℝ
hg₁ : (fun t => deriv (fun t => ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖) =O[atTop] g
hg₂ : IntegrableAtFilter g atTop volume
C₁ : ℝ
hC₁ : ∀ (n : ℕ), ‖‖f ↑n‖ * ∑ k ∈ Icc 0 n, ‖c k‖‖ ≤ C₁
C₂ : ℝ := ∫ (t : ℝ) in Set.Ioi ↑m, ‖deriv (fun t => ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖‖
⊢ ∑ i ∈ range 0, ‖f ↑i * c i‖ ≤ (C₁ + C₂) ⊔ 1

Tactic:
simp only [range_zero, norm_mul, sum_empty, le_sup_iff, zero_le_one, or_true]

Result:
no goals

Proof state:
case intro.succ.calc_2
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
m : ℕ
h_bdd : (fun n => ‖f ↑n‖ * ∑ k ∈ Icc 0 n, ‖c k‖) =O[atTop] fun x => 1
hf_int : LocallyIntegrableOn (deriv fun t => ‖f t‖) (Set.Ici ↑m) volume
hf :
  ∀ (n : ℕ),
    ∑ k ∈ Icc 0 n, ‖f ↑k‖ * ‖c k‖ =
      ‖f ↑n‖ * ∑ k ∈ Icc 0 n, ‖c k‖ - ∫ (t : ℝ) in Set.Ioc ↑m ↑n, deriv (fun t => ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖
g : ℝ → ℝ
hg₁ : (fun t => deriv (fun t => ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖) =O[atTop] g
hg₂ : IntegrableAtFilter g atTop volume
C₁ : ℝ
hC₁ : ∀ (n : ℕ), ‖‖f ↑n‖ * ∑ k ∈ Icc 0 n, ‖c k‖‖ ≤ C₁
C₂ : ℝ := ∫ (t : ℝ) in Set.Ioi ↑m, ‖deriv (fun t => ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖‖
n : ℕ
h_mes : Measurable fun t => deriv (fun t => ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖
⊢ ‖f ↑n‖ * ∑ k ∈ Icc 0 n, ‖c k‖ - ∫ (t : ℝ) in Set.Ioc ↑m ↑n, deriv (fun t => ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖ ≤
    C₁ - ∫ (t : ℝ) in Set.Ioc ↑m ↑n, deriv (fun t => ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖

Tactic:
refine tsub_le_tsub_right (le_of_eq_of_le (Real.norm_of_nonneg ?_).symm (hC₁ n)) _

Result:
case intro.succ.calc_2
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
m : ℕ
h_bdd : (fun n => ‖f ↑n‖ * ∑ k ∈ Icc 0 n, ‖c k‖) =O[atTop] fun x => 1
hf_int : LocallyIntegrableOn (deriv fun t => ‖f t‖) (Set.Ici ↑m) volume
hf :
  ∀ (n : ℕ),
    ∑ k ∈ Icc 0 n, ‖f ↑k‖ * ‖c k‖ =
      ‖f ↑n‖ * ∑ k ∈ Icc 0 n, ‖c k‖ - ∫ (t : ℝ) in Set.Ioc ↑m ↑n, deriv (fun t => ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖
g : ℝ → ℝ
hg₁ : (fun t => deriv (fun t => ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖) =O[atTop] g
hg₂ : IntegrableAtFilter g atTop volume
C₁ : ℝ
hC₁ : ∀ (n : ℕ), ‖‖f ↑n‖ * ∑ k ∈ Icc 0 n, ‖c k‖‖ ≤ C₁
C₂ : ℝ := ∫ (t : ℝ) in Set.Ioi ↑m, ‖deriv (fun t => ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖‖
n : ℕ
h_mes : Measurable fun t => deriv (fun t => ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖
⊢ 0 ≤ ‖f ↑n‖ * ∑ k ∈ Icc 0 n, ‖c k‖

Proof state:
case intro
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
m : ℕ
h_bdd : (fun n => ‖f ↑n‖ * ∑ k ∈ Icc 0 n, ‖c k‖) =O[atTop] fun x => 1
hf_int : LocallyIntegrableOn (deriv fun t => ‖f t‖) (Set.Ici ↑m) volume
hf :
  ∀ (n : ℕ),
    ∑ k ∈ Icc 0 n, ‖f ↑k‖ * ‖c k‖ =
      ‖f ↑n‖ * ∑ k ∈ Icc 0 n, ‖c k‖ - ∫ (t : ℝ) in Set.Ioc ↑m ↑n, deriv (fun t => ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖
g : ℝ → ℝ
hg₁ : (fun t => deriv (fun t => ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖) =O[atTop] g
hg₂ : IntegrableAtFilter g atTop volume
C₁ : ℝ
hC₁ : ∀ (n : ℕ), ‖‖f ↑n‖ * ∑ k ∈ Icc 0 n, ‖c k‖‖ ≤ C₁
C₂ : ℝ := ∫ (t : ℝ) in Set.Ioi ↑m, ‖deriv (fun t => ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖‖
⊢ Summable fun n => f ↑n * c n

Tactic:
refine summable_of_sum_range_norm_le (c := max (C₁ + C₂) 1) fun n ↦ ?_

Result:
case intro
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
m : ℕ
h_bdd : (fun n => ‖f ↑n‖ * ∑ k ∈ Icc 0 n, ‖c k‖) =O[atTop] fun x => 1
hf_int : LocallyIntegrableOn (deriv fun t => ‖f t‖) (Set.Ici ↑m) volume
hf :
  ∀ (n : ℕ),
    ∑ k ∈ Icc 0 n, ‖f ↑k‖ * ‖c k‖ =
      ‖f ↑n‖ * ∑ k ∈ Icc 0 n, ‖c k‖ - ∫ (t : ℝ) in Set.Ioc ↑m ↑n, deriv (fun t => ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖
g : ℝ → ℝ
hg₁ : (fun t => deriv (fun t => ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖) =O[atTop] g
hg₂ : IntegrableAtFilter g atTop volume
C₁ : ℝ
hC₁ : ∀ (n : ℕ), ‖‖f ↑n‖ * ∑ k ∈ Icc 0 n, ‖c k‖‖ ≤ C₁
C₂ : ℝ := ∫ (t : ℝ) in Set.Ioi ↑m, ‖deriv (fun t => ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖‖
n : ℕ
⊢ ∑ i ∈ range n, ‖f ↑i * c i‖ ≤ (C₁ + C₂) ⊔ 1

Proof state:
case intro.succ
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
m : ℕ
h_bdd : (fun n => ‖f ↑n‖ * ∑ k ∈ Icc 0 n, ‖c k‖) =O[atTop] fun x => 1
hf_int : LocallyIntegrableOn (deriv fun t => ‖f t‖) (Set.Ici ↑m) volume
hf :
  ∀ (n : ℕ),
    ∑ k ∈ Icc 0 n, ‖f ↑k‖ * ‖c k‖ =
      ‖f ↑n‖ * ∑ k ∈ Icc 0 n, ‖c k‖ - ∫ (t : ℝ) in Set.Ioc ↑m ↑n, deriv (fun t => ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖
g : ℝ → ℝ
hg₁ : (fun t => deriv (fun t => ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖) =O[atTop] g
hg₂ : IntegrableAtFilter g atTop volume
C₁ : ℝ
hC₁ : ∀ (n : ℕ), ‖‖f ↑n‖ * ∑ k ∈ Icc 0 n, ‖c k‖‖ ≤ C₁
C₂ : ℝ := ∫ (t : ℝ) in Set.Ioi ↑m, ‖deriv (fun t => ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖‖
n : ℕ
h_mes : Measurable fun t => deriv (fun t => ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖
⊢ ∑ i ∈ range (n + 1), ‖f ↑i * c i‖ ≤ (C₁ + C₂) ⊔ 1

Tactic:
rw [Nat.range_eq_Icc_zero_sub_one _ n.add_one_ne_zero, add_tsub_cancel_right]

Result:
case intro.succ
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
m : ℕ
h_bdd : (fun n => ‖f ↑n‖ * ∑ k ∈ Icc 0 n, ‖c k‖) =O[atTop] fun x => 1
hf_int : LocallyIntegrableOn (deriv fun t => ‖f t‖) (Set.Ici ↑m) volume
hf :
  ∀ (n : ℕ),
    ∑ k ∈ Icc 0 n, ‖f ↑k‖ * ‖c k‖ =
      ‖f ↑n‖ * ∑ k ∈ Icc 0 n, ‖c k‖ - ∫ (t : ℝ) in Set.Ioc ↑m ↑n, deriv (fun t => ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖
g : ℝ → ℝ
hg₁ : (fun t => deriv (fun t => ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖) =O[atTop] g
hg₂ : IntegrableAtFilter g atTop volume
C₁ : ℝ
hC₁ : ∀ (n : ℕ), ‖‖f ↑n‖ * ∑ k ∈ Icc 0 n, ‖c k‖‖ ≤ C₁
C₂ : ℝ := ∫ (t : ℝ) in Set.Ioi ↑m, ‖deriv (fun t => ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖‖
n : ℕ
h_mes : Measurable fun t => deriv (fun t => ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖
⊢ ∑ i ∈ Icc 0 n, ‖f ↑i * c i‖ ≤ (C₁ + C₂) ⊔ 1