no goals
α : Type u_1
β : Type ?u.755823
γ : Type ?u.755826
δ : Type ?u.755829
ι : Type ?u.755832
R : Type ?u.755835
R' : Type ?u.755838
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
inst✝ : SigmaFinite μ
s t : Set α
ht : MeasurableSet t
⊢ ↑↑(restrict μ (toMeasurable μ s)) t = ↑↑(restrict μ s) t
rw [restrict_apply ht, inter_comm t, measure_toMeasurable_inter_of_sigmaFinite ht,
  restrict_apply ht, inter_comm t]