. exists 1  intro n
  simp
  rw [integral_Ioc_eq_integral_Ioo]
  rw [← norm_eq_abs]
  refine lt_of_le_of_lt (@norm_integral_le_of_norm_le _ _ _ _ _ _ _
    (fun x => ε / 2 * DiracSeq n x) ?_ ?_) ?_
  . refine Integrable.integrableOn ?_
    exact Integrable.const_mul DiracSeq.integrable_pnat _
  . simp
    rw [eventually_inf_principal]
    refine ae_of_all _ ?_
    intro x hx
    simp [abs_of_nonneg, DiracSeq.nonneg_nat]
    refine mul_le_mul_of_nonneg_right ?_ (DiracSeq.nonneg_nat _)
    refine le_of_lt ?_
    apply hδε
    simp [abs_lt]
    exact hx
  . simp [integral_mul_left]
    rw [mul_lt_iff_lt_one_right (half_pos hε)]
    rw [← @DiracSeq.integral_pnat n]
    refine Ne.lt_of_le ?_ ?_
    . symm
      rw [← sub_ne_zero]
      rw [← integral_add_compl (by simp : MeasurableSet (Set.Ioo (-δ) δ)) DiracSeq.integrable_pnat]
      rw [@add_sub_cancel']
      simp
      rw [← ne_eq]
      refine DiracSeq.set_integral_ne_zero (by simp) ?_
      suffices : Set.Ici δ ⊆ (Set.Ioo (-δ) δ)ᶜ
      . exact lt_of_lt_of_le (by simp) (measure_mono this)
      rw [Set.subset_def]
      simp
      intro x hx _
      exact hx
    . refine set_integral_le_integral (DiracSeq.integrable_pnat) ?_
      exact Filter.eventually_of_forall DiracSeq.nonneg_nat
case this.left
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
⊢ ∃ N, ∀ (n : ℕ+), N ≤ n → |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2

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)
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)