refine Filter.eventually_of_forall ?_
case hf
b : ℝ
hb : 0 < b
s : Set ℝ
hs : 0 < ↑↑volume s
⊢ 0 ≤ᵐ[Measure.restrict volume s] fun x => DiracSeq b x
case hf
b : ℝ
hb : 0 < b
s : Set ℝ
hs : 0 < ↑↑volume s
⊢ ∀ (x : ℝ), 0 x ≤ (fun x => DiracSeq b x) x