no goals
α : Type u_1
β : Type ?u.291082
γ : Type ?u.291085
δ : Type ?u.291088
ι : Type ?u.291091
R : Type ?u.291094
R' : Type ?u.291097
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
hs : MeasurableSet s
⊢ restrict (restrict μ t) s = restrict (restrict μ s) t
rw [restrict_restrict hs, restrict_restrict' hs, inter_comm]