no goals
α : Type u_1
β : Type ?u.10593
γ : Type ?u.10596
δ : Type ?u.10599
ι : Type ?u.10602
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t s : Set α
⊢ ↑↑μ s = ⨅ (t : Set α) (_ : s ⊆ t) (_ : MeasurableSet t), ↑↑μ t
rw [measure_eq_trim, OuterMeasure.trim_eq_iInf]