no goals
α : Type u_1
β : Type ?u.283030
γ : Type ?u.283033
δ : Type ?u.283036
ι : Type ?u.283039
R : Type ?u.283042
R' : Type ?u.283045
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
hs : MeasurableSet s
⊢ ↑↑(restrict μ s) t = ↑↑μ (t ∩ s)
rw [Measure.restrict_toOuterMeasure_eq_toOuterMeasure_restrict hs,
  OuterMeasure.restrict_apply s t _]