no goals
α : Type u_1
m : Set (OuterMeasure α)
s : Set α
h : Set.Nonempty m
⊢ ↑(sInf m) s = ⨅ (t : ℕ → Set α) (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ (μ : OuterMeasure α) (_ : μ ∈ m), ↑μ (t n)
simp_rw [sInf_eq_boundedBy_sInfGen, boundedBy_apply, iSup_sInfGen_nonempty h]