rw [Metric.tendsto_nhds_nhds] at hδ
case h_tendsto
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
hδ : Tendsto (fun x => |φ x - φ 0|) (nhds 0) (nhds 0)
⊢ Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
case h_tendsto
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
hδ : ∀ ε > 0, ∃ δ > 0, ∀ {x : ℝ}, dist x 0 < δ → dist |φ x - φ 0| 0 < ε
⊢ Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)