no goals
α : Type u_1
β : Type ?u.283441
γ : Type ?u.283444
δ : Type ?u.283447
ι : Type ?u.283450
R : Type ?u.283453
R' : Type ?u.283456
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
hs : NullMeasurableSet s
⊢ ↑↑(restrict μ s) t = ↑↑μ (t ∩ s)
rw [← restrict_congr_set hs.toMeasurable_ae_eq,
  restrict_apply' (measurableSet_toMeasurable _ _),
  measure_congr ((ae_eq_refl t).inter hs.toMeasurable_ae_eq)]