. 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.refine_3
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ∫ (x : ℝ) in Set.Ioo (-δ) δ, ε / 2 * DiracSeq (↑↑n) x < ε / 2
no goals