-- Module: Mathlib.NumberTheory.AbelSummation
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
m : ℕ
h_bdd : Asymptotics.IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖f (↑n : ℝ)‖ * ∑ k ∈ Icc 0 n, ‖c k‖) fun (x : ℕ) ↦ 1
hf_int : LocallyIntegrableOn (X := ℝ) (ε := ℝ) (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‖ -
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc (↑m : ℝ) (↑n : ℝ)))
          fun (t : ℝ) ↦ HMul.hMul (α := ℝ) (deriv (fun (t : ℝ) ↦ ‖f t‖) t) (∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖)
g : ℝ → ℝ
hg₁ :
  Asymptotics.IsBigO (E := ℝ) atTop
    (fun (t : ℝ) ↦ HMul.hMul (α := ℝ) (deriv (fun (t : ℝ) ↦ ‖f t‖) t) (∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖)) g
hg₂ : IntegrableAtFilter (mα := MeasureSpace.toMeasurableSpace) g atTop volume
C₁ : ℝ
hC₁ : ∀ (n : ℕ), ‖‖f (↑n : ℝ)‖ * ∑ k ∈ Icc 0 n, ‖c k‖‖ ≤ C₁
C₂ : ℝ :=
  @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi (↑m : ℝ))) fun (t : ℝ) ↦
    ‖HMul.hMul (α := ℝ) (deriv (fun (t : ℝ) ↦ ‖f t‖) t) (∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖)‖
n : ℕ
zero : ∑ i ∈ range 0, ‖f (↑i : ℝ) * c i‖ ≤ max (C₁ + C₂) 1
succ : ∀ (n : ℕ), ∑ i ∈ range (n + 1), ‖f (↑i : ℝ) * c i‖ ≤ max (C₁ + C₂) 1
⊢ ∑ i ∈ range n, ‖f (↑i : ℝ) * c i‖ ≤ max (C₁ + C₂) 1

Tactic:
cases n with
  | zero => simp only [range_zero, norm_mul, sum_empty, le_sup_iff, zero_le_one, or_true]
  | succ n =>
      rw [Nat.range_eq_Icc_zero_sub_one _ n.add_one_ne_zero, add_tsub_cancel_right]
      calc
        _ = ∑ k ∈ Icc 0 n, ‖f k‖ * ‖c k‖ := by simp_rw [norm_mul]
        _ = ‖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‖ := ?_
        _ ≤ C₁ + ∫ t in Set.Ioc ↑m ↑n, ‖deriv (fun t ↦ ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖‖ := ?_
        _ ≤ C₁ + C₂ := ?_
        _ ≤ max (C₁ + C₂) 1 := le_max_left _ _
      · exact hf _
      · refine tsub_le_tsub_right (le_of_eq_of_le (Real.norm_of_nonneg ?_).symm (hC₁ n)) _
        exact mul_nonneg (norm_nonneg _) (sum_nonneg fun _ _ ↦ norm_nonneg _)
      · grw [sub_eq_add_neg, neg_le_abs, abs_integral_le_integral_abs]
        simp
      · unfold C₂
        grw [setIntegral_mono_set ?_ (.of_forall fun _ ↦ norm_nonneg _)
          Set.Ioc_subset_Ioi_self.eventuallyLE]
        rw [← integrableOn_Ici_iff_integrableOn_Ioi, IntegrableOn,
          integrable_norm_iff (by fun_prop)]
        exact (locallyIntegrableOn_mul_sum_Icc _ m.cast_nonneg hf_int).integrableOn_of_isBigO_atTop
          hg₁ hg₂

Premises used: Set.Ioc, mul_nonneg, Nat.cast_nonneg, MeasureTheory.setIntegral_mono_set, sub_eq_add_neg, Nat.add_one_ne_zero, Nat.range_eq_Icc_zero_sub_one, MeasureTheory.IntegrableOn, HasSubset.Subset.eventuallyLE, Filter.Eventually.of_forall, norm_mul, Finset.sum_nonneg, Set.Ioc_subset_Ioi_self, Finset.Icc, MeasureTheory.integrable_norm_iff, Nat.cast, zero_le_one, HAdd.hAdd, Max.max, locallyIntegrableOn_mul_sum_Icc, neg_le_abs, integrableOn_Ici_iff_integrableOn_Ioi, MeasureTheory.abs_integral_le_integral_abs, le_of_eq_of_le, le_sup_iff, tsub_le_tsub_right, Finset.sum_empty, add_tsub_cancel_right, OfNat.ofNat, Eq.symm, or_true, le_max_left, norm_nonneg, MeasureTheory.LocallyIntegrableOn.integrableOn_of_isBigO_atTop, Real.norm_of_nonneg, Finset.range_zero