no goals
α : Type u_1
β : Type ?u.45104
E : Type u_2
F : Type ?u.45110
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht : MeasurableSet t
⊢ (∫ (x : α) in s, indicator t f x ∂μ) = ∫ (x : α) in s ∩ t, f x ∂μ
rw [integral_indicator ht, Measure.restrict_restrict ht, Set.inter_comm]