no goals
α : Type u_1
β : Type ?u.754301
γ : Type ?u.754304
δ : Type ?u.754307
ι : Type ?u.754310
R : Type ?u.754313
R' : Type ?u.754316
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s : Set α
v : ℕ → Set α
hv : s ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), ↑↑μ (s ∩ v n) ≠ ⊤
t : Set α
ht : MeasurableSet t
⊢ ↑↑(restrict μ (toMeasurable μ s)) t = ↑↑(restrict μ s) t
simp only [restrict_apply ht, inter_comm t, measure_toMeasurable_inter_of_cover ht hv h'v]