no goals
α : Type u_1
β : Type ?u.1769295
γ : Type ?u.1769298
δ : Type ?u.1769301
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
⊢ withDensity μ (indicator s 1) = Measure.restrict μ s
rw [withDensity_indicator hs, withDensity_one]