rw [set_integral_pos_iff_support_of_nonneg_ae]
b : ℝ
hb : 0 < b
s : Set ℝ
hs : 0 < ↑↑volume s
⊢ 0 < ∫ (x : ℝ) in s, DiracSeq b x
b : ℝ
hb : 0 < b
s : Set ℝ
hs : 0 < ↑↑volume s
⊢ 0 < ↑↑volume ((Function.support fun x => DiracSeq b x) ∩ s)

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