no goals
α : Type u_2
β : Type ?u.14786
γ : Type ?u.14789
δ : Type ?u.14792
ι✝ : Type ?u.14795
inst✝¹ : MeasurableSpace α
μ✝ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
ι : Sort u_1
inst✝ : Countable ι
μ : ι → Measure α
s : Set α
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ∀ (i : ι), ↑↑(μ i) t = ↑↑(μ i) s
simpa only [← measure_eq_trim] using
  OuterMeasure.exists_measurable_superset_forall_eq_trim (fun i => (μ i).toOuterMeasure) s