no goals
α : Type u_1
β : Type ?u.10941
γ : Type ?u.10944
δ : Type ?u.10947
ι : Type ?u.10950
inst✝ : MeasurableSpace α
μ✝ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
μ : Measure α
s : Set α
⊢ ↑↑μ s = ⨅ (t : { t // s ⊆ t ∧ MeasurableSet t }), ↑↑μ ↑t
simp_rw [iInf_subtype, iInf_and, Subtype.coe_mk, ← measure_eq_iInf]