no goals
α : Type u_2
β : Type u_1
γ : Type ?u.1365626
δ : Type ?u.1365629
m : MeasurableSpace α
μ ν : Measure α
mβ : MeasurableSpace β
f : α → β
s : Set β
hf : Measurable f
hs : MeasurableSet s
c : ℝ≥0∞
⊢ (∫⁻ (a : α), indicator s (fun x => c) (f a) ∂μ) = c * ↑↑μ (f ⁻¹' s)
erw [lintegral_comp (measurable_const.indicator hs) hf, lintegral_indicator_const hs,
  Measure.map_apply hf hs]