case h
α : Type u_1
β : Type ?u.1768900
γ : Type ?u.1768903
δ : Type ?u.1768906
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
t : Set α
ht : MeasurableSet t
⊢ ↑↑(withDensity μ (indicator s f)) t = ↑↑(withDensity (Measure.restrict μ s) f) t
α : Type u_1
β : Type ?u.1768900
γ : Type ?u.1768903
δ : Type ?u.1768906
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
⊢ withDensity μ (indicator s f) = withDensity (Measure.restrict μ s) f
ext1 t ht
no goals
case h
α : Type u_1
β : Type ?u.1768900
γ : Type ?u.1768903
δ : Type ?u.1768906
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
t : Set α
ht : MeasurableSet t
⊢ ↑↑(withDensity μ (indicator s f)) t = ↑↑(withDensity (Measure.restrict μ s) f) t
rw [withDensity_apply _ ht, lintegral_indicator _ hs, restrict_comm hs, ←
  withDensity_apply _ ht]