no goals
α : Type u_1
β : Type ?u.14385
γ : Type ?u.14388
δ : Type ?u.14391
ι : Type ?u.14394
inst✝ : MeasurableSpace α
μ✝ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
μ : Measure α
s : Set α
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ↑↑μ t = ↑↑μ s
simpa only [← measure_eq_trim] using μ.toOuterMeasure.exists_measurable_superset_eq_trim s