no goals
α : Type u_1
β : Type ?u.952259
γ : Type ?u.952262
δ : Type ?u.952265
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hs : NullMeasurableSet s
⊢ (∫⁻ (a : α), indicator s f a ∂μ) = ∫⁻ (a : α) in s, f a ∂μ
rw [← lintegral_congr_ae (indicator_ae_eq_of_ae_eq_set hs.toMeasurable_ae_eq),
  lintegral_indicator _ (measurableSet_toMeasurable _ _),
  Measure.restrict_congr_set hs.toMeasurable_ae_eq]