-- 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
⊢ Summable fun n => f ↑n * c n

Tactic:
refine Summable.congr_atTop (summable_mul_of_bigO_atTop_aux (fun n ↦ if n = 0 then 0 else c n) 1
  h_bdd (by rwa [Nat.cast_one]) (fun n ↦ ?_) hg₁ hg₂) ?_

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

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

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
h : ∀ (n : ℕ), ∑ k ∈ Icc 1 n, ‖c k‖ = ∑ k ∈ Icc 0 n, ‖(fun n => if n = 0 then 0 else c n) k‖
⊢ Summable fun n => f ↑n * c n

Tactic:
simp_rw [h] at h_bdd hg₁

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
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
⊢ 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
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
⊢ Summable fun n => f ↑n * c n

Tactic:
have h : ∀ n, ∑ k ∈ Icc 1 n, ‖c k‖ = ∑ k ∈ Icc 0 n, ‖(fun n ↦ if n = 0 then 0 else c n) k‖ := by
  intro n
  rw [Icc_eq_cons_Ioc n.zero_le, sum_cons, ← Nat.Icc_succ_left, Nat.succ_eq_add_one, zero_add]
  simp_rw [if_pos, norm_zero, zero_add]
  exact Finset.sum_congr rfl fun _ h ↦ by rw [if_neg (zero_lt_one.trans_le (mem_Icc.mp h).1).ne']

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
h : ∀ (n : ℕ), ∑ k ∈ Icc 1 n, ‖c k‖ = ∑ k ∈ Icc 0 n, ‖(fun n => if n = 0 then 0 else c n) k‖
⊢ 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
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‖

Tactic:
simp_rw [if_pos, norm_zero, 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‖ = ∑ x ∈ Icc 1 n, ‖if x = 0 then 0 else c x‖

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‖ = ∑ x ∈ Icc 1 n, ‖if x = 0 then 0 else c x‖

Tactic:
exact Finset.sum_congr rfl fun _ h ↦ by 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
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
⊢ LocallyIntegrableOn (deriv fun t => ‖f t‖) (Set.Ici ↑1) volume

Tactic:
rwa [Nat.cast_one]

Result:
no goals