. refine Filter.eventually_of_forall ?_
  simp
  exact DiracSeq.nonneg hb.le
case hf
b : ℝ
hb : 0 < b
s : Set ℝ
hs : 0 < ↑↑volume s
⊢ 0 ≤ᵐ[Measure.restrict volume s] fun x => DiracSeq b x

case hfi
b : ℝ
hb : 0 < b
s : Set ℝ
hs : 0 < ↑↑volume s
⊢ IntegrableOn (fun x => DiracSeq b x) s
case hfi
b : ℝ
hb : 0 < b
s : Set ℝ
hs : 0 < ↑↑volume s
⊢ IntegrableOn (fun x => DiracSeq b x) s