conv => rhs; rw [← add_zero 0]
case this.right
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
δ : ℝ
hδ : 0 < δ
hI₂ : ∀ {a : ℝ}, 0 < a → Tendsto (fun n => ∫ (x : ℝ) in Set.Ioi a, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
hI₁ : ∀ {a : ℝ}, 0 < a → Tendsto (fun n => ∫ (x : ℝ) in Set.Iic (-a), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
⊢ Tendsto
    (fun n =>
      (∫ (x : ℝ) in Set.Iic (-δ), (φ x - φ 0) * DiracSeq (↑↑n) x) +
        ∫ (x : ℝ) in Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x)
    atTop (nhds 0)
case this.right
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
δ : ℝ
hδ : 0 < δ
hI₂ : ∀ {a : ℝ}, 0 < a → Tendsto (fun n => ∫ (x : ℝ) in Set.Ioi a, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
hI₁ : ∀ {a : ℝ}, 0 < a → Tendsto (fun n => ∫ (x : ℝ) in Set.Iic (-a), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
⊢ Tendsto
    (fun n =>
      (∫ (x : ℝ) in Set.Iic (-δ), (φ x - φ 0) * DiracSeq (↑↑n) x) +
        ∫ (x : ℝ) in Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x)
    atTop (nhds (0 + 0))