α : Type u_2
ι : Type u_1
I : Set ι
hI : Set.Nonempty I
m : ι → OuterMeasure α
s : Set α
this : Nonempty ↑I
⊢ ↑(⨅ (i : ι) (_ : i ∈ I), m i) s =
    ⨅ (t : ℕ → Set α) (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ (i : ι) (_ : i ∈ I), ↑(m i) (t n)
α : Type u_2
ι : Type u_1
I : Set ι
hI : Set.Nonempty I
m : ι → OuterMeasure α
s : Set α
⊢ ↑(⨅ (i : ι) (_ : i ∈ I), m i) s =
    ⨅ (t : ℕ → Set α) (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ (i : ι) (_ : i ∈ I), ↑(m i) (t n)
haveI := hI.to_subtype
no goals
α : Type u_2
ι : Type u_1
I : Set ι
hI : Set.Nonempty I
m : ι → OuterMeasure α
s : Set α
this : Nonempty ↑I
⊢ ↑(⨅ (i : ι) (_ : i ∈ I), m i) s =
    ⨅ (t : ℕ → Set α) (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ (i : ι) (_ : i ∈ I), ↑(m i) (t n)
simp only [← iInf_subtype'', iInf_apply]