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

Proof state:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hf_diff : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x => ‖f x‖) t
hf_int : LocallyIntegrableOn (deriv fun t => ‖f t‖) (Set.Ici 1) volume
g : ℝ → ℝ
hg₂ : IntegrableAtFilter g atTop volume
h : ∀ (n : ℕ), ∑ k ∈ Icc 1 n, ‖c k‖ = ∑ k ∈ Icc 0 n, ‖(fun n => if n = 0 then 0 else c n) k‖
h_bdd : (fun n => ‖f ↑n‖ * ∑ x ∈ Icc 0 n, ‖if x = 0 then 0 else c x‖) =O[atTop] fun x => 1
hg₁ : (fun t => deriv (fun t => ‖f t‖) t * ∑ x ∈ Icc 0 ⌊t⌋₊, ‖if x = 0 then 0 else c x‖) =O[atTop] g
n : ℕ
⊢ ‖(fun n => if n = 0 then 0 else c n) 0‖ = 0

Tactic:
simp only [reduceIte, norm_zero]

Result:
no goals

Proof state:
case refine_1
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hf_diff : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x => ‖f x‖) t
hf_int : LocallyIntegrableOn (deriv fun t => ‖f t‖) (Set.Ici 1) volume
g : ℝ → ℝ
hg₂ : IntegrableAtFilter g atTop volume
h : ∀ (n : ℕ), ∑ k ∈ Icc 1 n, ‖c k‖ = ∑ k ∈ Icc 0 n, ‖(fun n => if n = 0 then 0 else c n) k‖
h_bdd : (fun n => ‖f ↑n‖ * ∑ x ∈ Icc 0 n, ‖if x = 0 then 0 else c x‖) =O[atTop] fun x => 1
hg₁ : (fun t => deriv (fun t => ‖f t‖) t * ∑ x ∈ Icc 0 ⌊t⌋₊, ‖if x = 0 then 0 else c x‖) =O[atTop] g
n : ℕ
⊢ ∑ k ∈ Icc 0 n, ‖f ↑k‖ * ‖(fun n => if n = 0 then 0 else c n) k‖ =
    ‖f ↑n‖ * ∑ k ∈ Icc 0 n, ‖(fun n => if n = 0 then 0 else c n) k‖ -
      ∫ (t : ℝ) in Set.Ioc ↑1 ↑n, deriv (fun t => ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖(fun n => if n = 0 then 0 else c n) k‖

Tactic:
exact_mod_cast sum_mul_eq_sub_integral_mul₀' _ (by simp only [reduceIte, norm_zero]) n
  (fun _ ht ↦ hf_diff _ ht.1)
  (hf_int.integrableOn_compact_subset Set.Icc_subset_Ici_self isCompact_Icc)

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hf_diff : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x => ‖f x‖) t
hf_int : LocallyIntegrableOn (deriv fun t => ‖f t‖) (Set.Ici 1) volume
h_bdd : (fun n => ‖f ↑n‖ * ∑ k ∈ Icc 1 n, ‖c k‖) =O[atTop] fun x => 1
g : ℝ → ℝ
hg₁ : (fun t => deriv (fun t => ‖f t‖) t * ∑ k ∈ Icc 1 ⌊t⌋₊, ‖c k‖) =O[atTop] g
hg₂ : IntegrableAtFilter g atTop volume
n : ℕ
⊢ ∑ k ∈ Icc 1 n, ‖c k‖ = ∑ k ∈ Icc 0 n, ‖(fun n => if n = 0 then 0 else c n) k‖

Tactic:
rw [Icc_eq_cons_Ioc n.zero_le, sum_cons, ← Nat.Icc_succ_left, Nat.succ_eq_add_one, zero_add]

Result:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hf_diff : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x => ‖f x‖) t
hf_int : LocallyIntegrableOn (deriv fun t => ‖f t‖) (Set.Ici 1) volume
h_bdd : (fun n => ‖f ↑n‖ * ∑ k ∈ Icc 1 n, ‖c k‖) =O[atTop] fun x => 1
g : ℝ → ℝ
hg₁ : (fun t => deriv (fun t => ‖f t‖) t * ∑ k ∈ Icc 1 ⌊t⌋₊, ‖c k‖) =O[atTop] g
hg₂ : IntegrableAtFilter g atTop volume
n : ℕ
⊢ ∑ k ∈ Icc 1 n, ‖c k‖ =
    ‖(fun n => if n = 0 then 0 else c n) 0‖ + ∑ x ∈ Icc 1 n, ‖(fun n => if n = 0 then 0 else c n) x‖

Proof state:
case h
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hf_diff : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x => ‖f x‖) t
hf_int : LocallyIntegrableOn (deriv fun t => ‖f t‖) (Set.Ici 1) volume
g : ℝ → ℝ
hg₂ : IntegrableAtFilter g atTop volume
h : ∀ (n : ℕ), ∑ k ∈ Icc 1 n, ‖c k‖ = ∑ k ∈ Icc 0 n, ‖(fun n => if n = 0 then 0 else c n) k‖
h_bdd : (fun n => ‖f ↑n‖ * ∑ x ∈ Icc 0 n, ‖if x = 0 then 0 else c x‖) =O[atTop] fun x => 1
hg₁ : (fun t => deriv (fun t => ‖f t‖) t * ∑ x ∈ Icc 0 ⌊t⌋₊, ‖if x = 0 then 0 else c x‖) =O[atTop] g
k : ℕ
hk : k ≠ 0
⊢ (f ↑k * if k = 0 then 0 else c k) = f ↑k * c k

Tactic:
simp_rw [if_neg hk]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hf_diff : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x => ‖f x‖) t
hf_int : LocallyIntegrableOn (deriv fun t => ‖f t‖) (Set.Ici 1) volume
h_bdd : (fun n => ‖f ↑n‖ * ∑ k ∈ Icc 1 n, ‖c k‖) =O[atTop] fun x => 1
g : ℝ → ℝ
hg₁ : (fun t => deriv (fun t => ‖f t‖) t * ∑ k ∈ Icc 1 ⌊t⌋₊, ‖c k‖) =O[atTop] g
hg₂ : IntegrableAtFilter g atTop volume
n x✝ : ℕ
h : x✝ ∈ Icc 1 n
⊢ ‖c x✝‖ = ‖if x✝ = 0 then 0 else c x✝‖

Tactic:
rw [if_neg (zero_lt_one.trans_le (mem_Icc.mp h).1).ne']

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hf_diff : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x => ‖f x‖) t
hf_int : LocallyIntegrableOn (deriv fun t => ‖f t‖) (Set.Ici 1) volume
h_bdd : (fun n => ‖f ↑n‖ * ∑ k ∈ Icc 1 n, ‖c k‖) =O[atTop] fun x => 1
g : ℝ → ℝ
hg₁ : (fun t => deriv (fun t => ‖f t‖) t * ∑ k ∈ Icc 1 ⌊t⌋₊, ‖c k‖) =O[atTop] g
hg₂ : IntegrableAtFilter g atTop volume
⊢ ∀ (n : ℕ), ∑ k ∈ Icc 1 n, ‖c k‖ = ∑ k ∈ Icc 0 n, ‖(fun n => if n = 0 then 0 else c n) k‖

Tactic:
intro n

Result:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hf_diff : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x => ‖f x‖) t
hf_int : LocallyIntegrableOn (deriv fun t => ‖f t‖) (Set.Ici 1) volume
h_bdd : (fun n => ‖f ↑n‖ * ∑ k ∈ Icc 1 n, ‖c k‖) =O[atTop] fun x => 1
g : ℝ → ℝ
hg₁ : (fun t => deriv (fun t => ‖f t‖) t * ∑ k ∈ Icc 1 ⌊t⌋₊, ‖c k‖) =O[atTop] g
hg₂ : IntegrableAtFilter g atTop volume
n : ℕ
⊢ ∑ k ∈ Icc 1 n, ‖c k‖ = ∑ k ∈ Icc 0 n, ‖(fun n => if n = 0 then 0 else c n) k‖

Proof state:
case refine_2
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hf_diff : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x => ‖f x‖) t
hf_int : LocallyIntegrableOn (deriv fun t => ‖f t‖) (Set.Ici 1) volume
g : ℝ → ℝ
hg₂ : IntegrableAtFilter g atTop volume
h : ∀ (n : ℕ), ∑ k ∈ Icc 1 n, ‖c k‖ = ∑ k ∈ Icc 0 n, ‖(fun n => if n = 0 then 0 else c n) k‖
h_bdd : (fun n => ‖f ↑n‖ * ∑ x ∈ Icc 0 n, ‖if x = 0 then 0 else c x‖) =O[atTop] fun x => 1
hg₁ : (fun t => deriv (fun t => ‖f t‖) t * ∑ x ∈ Icc 0 ⌊t⌋₊, ‖if x = 0 then 0 else c x‖) =O[atTop] g
⊢ (fun n => f ↑n * (fun n => if n = 0 then 0 else c n) n) =ᶠ[atTop] fun n => f ↑n * c n

Tactic:
filter_upwards [eventually_ne_atTop 0] with k hk

Result:
case h
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hf_diff : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x => ‖f x‖) t
hf_int : LocallyIntegrableOn (deriv fun t => ‖f t‖) (Set.Ici 1) volume
g : ℝ → ℝ
hg₂ : IntegrableAtFilter g atTop volume
h : ∀ (n : ℕ), ∑ k ∈ Icc 1 n, ‖c k‖ = ∑ k ∈ Icc 0 n, ‖(fun n => if n = 0 then 0 else c n) k‖
h_bdd : (fun n => ‖f ↑n‖ * ∑ x ∈ Icc 0 n, ‖if x = 0 then 0 else c x‖) =O[atTop] fun x => 1
hg₁ : (fun t => deriv (fun t => ‖f t‖) t * ∑ x ∈ Icc 0 ⌊t⌋₊, ‖if x = 0 then 0 else c x‖) =O[atTop] g
k : ℕ
hk : k ≠ 0
⊢ (f ↑k * if k = 0 then 0 else c k) = f ↑k * c k