no goals
α : Type u_1
β : Type ?u.289512
γ : Type ?u.289515
δ : Type ?u.289518
ι : Type ?u.289521
R : Type ?u.289524
R' : Type ?u.289527
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
hs : NullMeasurableSet s
u : Set α
hu : MeasurableSet u
⊢ ↑↑(restrict (restrict μ t) s) u = ↑↑(restrict μ (s ∩ t)) u
simp only [Set.inter_assoc, restrict_apply hu,
  restrict_apply₀ (hu.nullMeasurableSet.inter hs)]