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

case this.left.refine_3.refine_2
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ∫ (a : ℝ) in Set.Ioo (-δ) δ, DiracSeq (↑↑n) a ≤ ∫ (x : ℝ), DiracSeq (↑↑n) x
case this.left.refine_3.refine_2
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ∫ (a : ℝ) in Set.Ioo (-δ) δ, DiracSeq (↑↑n) a ≤ ∫ (x : ℝ), DiracSeq (↑↑n) x