rw [eventually_inf_principal]
case this.left.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 : ℕ+
⊢ ∀ᶠ (x : ℝ) in Measure.ae volume ⊓ 𝓟 (Set.Ioo (-δ) δ), |φ x - φ 0| * |DiracSeq (↑↑n) x| ≤ ε / 2 * DiracSeq (↑↑n) x
case this.left.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 : ℕ+
⊢ ∀ᵐ (x : ℝ), x ∈ Set.Ioo (-δ) δ → |φ x - φ 0| * |DiracSeq (↑↑n) x| ≤ ε / 2 * DiracSeq (↑↑n) x