no goals
α : Type u_1
β : Type ?u.306428
γ : Type ?u.306431
δ : Type ?u.306434
ι : Type ?u.306437
R : Type ?u.306440
R' : Type ?u.306443
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t✝ : Set α
h : ↑↑μ s ≠ ⊤
t : Set α
ht : MeasurableSet t
⊢ ↑↑(restrict μ (toMeasurable μ s)) t = ↑↑(restrict μ s) t
rw [restrict_apply ht, restrict_apply ht, inter_comm, measure_toMeasurable_inter ht h,
  inter_comm]