no goals
Ω : Type u_1
m : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
s t✝ : Set Ω
hms : MeasurableSet s
t : Set Ω
⊢ ↑↑(μ[|s]) (s ∩ t) = ↑↑(μ[|s]) t
rw [cond_apply _ hms, ← Set.inter_assoc, Set.inter_self, ← cond_apply _ hms]