no goals
α : Type u_1
β : Type ?u.159074
γ : Type ?u.159077
δ : Type ?u.159080
ι : Type ?u.159083
R : Type ?u.159086
R' : Type ?u.159089
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝ : MeasurableSpace α
⊢ ↑⊤ = ⊤
rw [← OuterMeasure.toMeasure_top, toMeasure_toOuterMeasure, OuterMeasure.trim_top]