ι : Type u_2
ι' : Type ?u.2392482
α : ι → Type u_1
inst✝³ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝² : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝¹ : Encodable ι
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (α i)
⊢ ↑↑(map (TProd.elim' (_ : ∀ (x : ι), x ∈ sortedUniv ι)) (Measure.tprod (sortedUniv ι) μ)) (Set.pi univ s) =
    ∏ i : ι, ↑↑(μ i) (s i)
ι : Type u_2
ι' : Type ?u.2392482
α : ι → Type u_1
inst✝³ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝² : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝¹ : Encodable ι
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (α i)
⊢ ↑↑(pi' μ) (Set.pi univ s) = ∏ i : ι, ↑↑(μ i) (s i)
rw [pi']
ι : Type u_2
ι' : Type ?u.2392482
α : ι → Type u_1
inst✝³ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝² : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝¹ : Encodable ι
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (α i)
⊢ ↑↑(map (fun v i => TProd.elim v (_ : i ∈ sortedUniv ι)) (Measure.tprod (sortedUniv ι) μ)) (Set.pi univ s) =
    ∏ i : ι, ↑↑(μ i) (s i)
ι : Type u_2
ι' : Type ?u.2392482
α : ι → Type u_1
inst✝³ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝² : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝¹ : Encodable ι
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (α i)
⊢ ↑↑(map (TProd.elim' (_ : ∀ (x : ι), x ∈ sortedUniv ι)) (Measure.tprod (sortedUniv ι) μ)) (Set.pi univ s) =
    ∏ i : ι, ↑↑(μ i) (s i)
simp only [TProd.elim']
no goals
ι : Type u_2
ι' : Type ?u.2392482
α : ι → Type u_1
inst✝³ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝² : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝¹ : Encodable ι
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (α i)
⊢ ↑↑(map (fun v i => TProd.elim v (_ : i ∈ sortedUniv ι)) (Measure.tprod (sortedUniv ι) μ)) (Set.pi univ s) =
    ∏ i : ι, ↑↑(μ i) (s i)
erw [← MeasurableEquiv.piMeasurableEquivTProd_symm_apply, MeasurableEquiv.map_apply,
  MeasurableEquiv.piMeasurableEquivTProd_symm_apply, elim_preimage_pi, tprod_tprod _ μ, ←
  List.prod_toFinset, sortedUniv_toFinset] <;>
exact sortedUniv_nodup ι