simp [Metric.tendsto_atTop]
case h_tendsto
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
hδ : ∀ (ε : ℝ), 0 < ε → ∃ δ, 0 < δ ∧ ∀ {x : ℝ}, |x| < δ → |φ x - φ 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 : ℝ}, |x| < δ → |φ x - φ 0| < ε
⊢ ∀ (ε : ℝ), 0 < ε → ∃ N, ∀ (n : ℕ+), N ≤ n → |∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x| < ε