-- Mathlib/NumberTheory/LSeries/SumCoeff.lean
theorem LSeries_tendsto_sub_mul_nhds_one_of_tendsto_sum_div_aux₁
  (hlim : Tendsto (fun n : ℕ ↦ (∑ k ∈ Icc 1 n, f k) / n) atTop (𝓝 l)) {ε : ℝ} (hε : 0 < ε) :
    ∀ᶠ t : ℝ in atTop, ‖(∑ k ∈ Icc 1 ⌊t⌋₊, f k) - l * t‖ < ε * t

Proof state:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n => (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
ε : ℝ
hε : 0 < ε
⊢ ∀ᶠ (t : ℝ) in atTop, ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - l * ↑t‖ < ε * t

Tactic:
have h_lim' : Tendsto (fun t : ℝ ↦ (∑ k ∈ Icc 1 ⌊t⌋₊, f k : ℂ) / t) atTop (𝓝 l) := by
  refine (mul_one l ▸ ofReal_one ▸ ((hlim.comp tendsto_nat_floor_atTop).mul <|
    tendsto_ofReal_iff.mpr <| tendsto_nat_floor_div_atTop)).congr' ?_
  filter_upwards [eventually_ge_atTop 1] with t ht
  simp [div_mul_div_cancel₀ (show (⌊t⌋₊ : ℂ) ≠ 0 by simpa)]

Result:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n => (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
ε : ℝ
hε : 0 < ε
h_lim' : Tendsto (fun t => (∑ k ∈ Icc 1 ⌊t⌋₊, f k) / ↑t) atTop (𝓝 l)
⊢ ∀ᶠ (t : ℝ) in atTop, ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - l * ↑t‖ < ε * t

Proof state:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n => (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
ε : ℝ
hε : 0 < ε
⊢ Tendsto (fun t => (∑ k ∈ Icc 1 ⌊t⌋₊, f k) / ↑t) atTop (𝓝 l)

Tactic:
refine (mul_one l ▸ ofReal_one ▸ ((hlim.comp tendsto_nat_floor_atTop).mul <|
  tendsto_ofReal_iff.mpr <| tendsto_nat_floor_div_atTop)).congr' ?_

Result:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n => (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
ε : ℝ
hε : 0 < ε
⊢ (fun x => ((fun n => (∑ k ∈ Icc 1 n, f k) / ↑n) ∘ fun x => ⌊x⌋₊) x * ↑(↑⌊x⌋₊ / x)) =ᶠ[atTop] fun t =>
    (∑ k ∈ Icc 1 ⌊t⌋₊, f k) / ↑t

Proof state:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n => (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
ε : ℝ
hε : 0 < ε
h_lim' : Tendsto (fun t => (∑ k ∈ Icc 1 ⌊t⌋₊, f k) / ↑t) atTop (𝓝 l)
⊢ ∀ᶠ (t : ℝ) in atTop, ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - l * ↑t‖ < ε * t

Tactic:
filter_upwards [eventually_gt_atTop 0, Metric.tendsto_nhds.mp h_lim' ε hε] with t ht₁ ht₂

Result:
case h
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n => (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
ε : ℝ
hε : 0 < ε
h_lim' : Tendsto (fun t => (∑ k ∈ Icc 1 ⌊t⌋₊, f k) / ↑t) atTop (𝓝 l)
t : ℝ
ht₁ : 0 < t
ht₂ : dist ((∑ k ∈ Icc 1 ⌊t⌋₊, f k) / ↑t) l < ε
⊢ ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - l * ↑t‖ < ε * t

Proof state:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n => (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
ε : ℝ
hε : 0 < ε
⊢ (fun x => ((fun n => (∑ k ∈ Icc 1 n, f k) / ↑n) ∘ fun x => ⌊x⌋₊) x * ↑(↑⌊x⌋₊ / x)) =ᶠ[atTop] fun t =>
    (∑ k ∈ Icc 1 ⌊t⌋₊, f k) / ↑t

Tactic:
filter_upwards [eventually_ge_atTop 1] with t ht

Result:
case h
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n => (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
ε : ℝ
hε : 0 < ε
t : ℝ
ht : 1 ≤ t
⊢ ((fun n => (∑ k ∈ Icc 1 n, f k) / ↑n) ∘ fun x => ⌊x⌋₊) t * ↑(↑⌊t⌋₊ / t) = (∑ k ∈ Icc 1 ⌊t⌋₊, f k) / ↑t

Proof state:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n => (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
ε : ℝ
hε : 0 < ε
t : ℝ
ht : 1 ≤ t
⊢ ↑⌊t⌋₊ ≠ 0

Tactic:
simpa

Result:
no goals

Proof state:
case h
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n => (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
ε : ℝ
hε : 0 < ε
h_lim' : Tendsto (fun t => (∑ k ∈ Icc 1 ⌊t⌋₊, f k) / ↑t) atTop (𝓝 l)
t : ℝ
ht₁ : 0 < t
ht₂ : dist ((∑ k ∈ Icc 1 ⌊t⌋₊, f k) / ↑t) l < ε
⊢ ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - l * ↑t‖ < ε * t

Tactic:
rwa [dist_eq_norm, div_sub' (ne_zero_of_re_pos ht₁), norm_div, norm_real,
  Real.norm_of_nonneg ht₁.le, mul_comm, div_lt_iff₀ ht₁] at ht₂

Result:
no goals

Proof state:
case h
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n => (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
ε : ℝ
hε : 0 < ε
t : ℝ
ht : 1 ≤ t
⊢ ((fun n => (∑ k ∈ Icc 1 n, f k) / ↑n) ∘ fun x => ⌊x⌋₊) t * ↑(↑⌊t⌋₊ / t) = (∑ k ∈ Icc 1 ⌊t⌋₊, f k) / ↑t

Tactic:
simp [div_mul_div_cancel₀ (show (⌊t⌋₊ : ℂ) ≠ 0 by simpa)]

Result:
no goals