α : Type u_2
ι : Sort u_1
m : ι → OuterMeasure α
s : Set α
hs : Set.Nonempty s
⊢ (⨅ (t : ℕ → Set α) (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ (μ : OuterMeasure α) (_ : μ ∈ range fun i => m i), ↑μ (t n)) =
    ⨅ (t : ℕ → Set α) (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ (i : ι), ↑(m i) (t n)
α : Type u_2
ι : Sort u_1
m : ι → OuterMeasure α
s : Set α
hs : Set.Nonempty s
⊢ ↑(⨅ (i : ι), m i) s = ⨅ (t : ℕ → Set α) (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ (i : ι), ↑(m i) (t n)
rw [iInf, sInf_apply' hs]
no goals
α : Type u_2
ι : Sort u_1
m : ι → OuterMeasure α
s : Set α
hs : Set.Nonempty s
⊢ (⨅ (t : ℕ → Set α) (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ (μ : OuterMeasure α) (_ : μ ∈ range fun i => m i), ↑μ (t n)) =
    ⨅ (t : ℕ → Set α) (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ (i : ι), ↑(m i) (t n)
simp only [iInf_range]