no goals
α : Type u_1
β : Type ?u.988367
γ : Type ?u.988370
δ : Type ?u.988373
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
s : Set α
hsm : MeasurableSet s
hs : ↑↑μ s ≠ 0
hg : Measurable g
hfi : (∫⁻ (x : α) in s, f x ∂μ) ≠ ⊤
h : ∀ᵐ (x : α) ∂μ, x ∈ s → f x < g x
⊢ Measure.restrict μ s ≠ 0
simp [hs]