no goals
α : Type u_1
β : Type ?u.284395
γ : Type ?u.284398
δ : Type ?u.284401
ι : Type ?u.284404
R : Type ?u.284407
R' : Type ?u.284410
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
h : s ⊆ t
⊢ ↑↑μ (toMeasurable (restrict μ t) s ∩ t) = ↑↑(restrict μ t) s
rw [← restrict_apply (measurableSet_toMeasurable _ _), measure_toMeasurable]