TODO

Rename setLIntegral_congr to setLIntegral_congr_set

theorem MeasureTheory.lintegral_eq_zero_of_ae_zero {α : Type u_1} [MeasurableSpace α] {μ : Measure α} {s : Set α} {f : α → ENNReal} (hs : μ sᶜ = 0) (hf : ∀ x ∈ s, f x = 0) (hmes : MeasurableSet s) : ∫⁻ (x : α), f x ∂μ = 0

theorem MeasureTheory.lintegral_eq_setLIntegral {α : Type u_1} [MeasurableSpace α] {μ : Measure α} {s : Set α} (hs : μ sᶜ = 0) (f : α → ENNReal) : ∫⁻ (x : α), f x ∂μ = ∫⁻ (x : α) in s, f x ∂μ