. have hI₂ {a} (ha : 0 < a) : Tendsto (fun (n : ℕ+) => ∫ x in Set.Ioi a, (φ x - φ 0) * DiracSeq n x) atTop (nhds 0)
  . exact tendsto_integral_Ioi_bump_sub_const_mul ha hφ (φ 0)
  have hI₁ {a} (ha : 0 < a) : Tendsto (fun (n : ℕ+) => ∫ x in Set.Iic (-a), (φ x - φ 0) * DiracSeq n x) atTop (nhds 0)
  . exact tendsto_integral_Iic_bump_sub_const_mul ha hφ (φ 0)
  clear hδε hε ε  simp [integral_union, hδ.le, h_integrable.integrableOn]
  conv => rhs; rw [← add_zero 0]
  exact Tendsto.add (hI₁ hδ) (hI₂ hδ)
case this.right
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
⊢ Tendsto (fun n => ∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
no goals