-- Module: Mathlib.Probability.ProductMeasure
Goal:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
e : ℕ ≃ ι
I : Finset ι
S : Set ((i : ↥I) → X (↑i : ι))
hS : MeasurableSet S
hs : cylinder (α := X) I S ∈ measurableCylinders X
rw :
  Eq (α := ℝ≥0∞)
    (((Measure.pi (α := fun (i : ↥(I.preimage (⇑e : (a : ℕ) → ι) ⋯)) ↦ X ((e : (a : ℕ) → ι) (↑i : ℕ)))
              fun (i : ↥(I.preimage (⇑e : (a : ℕ) → ι) ⋯)) ↦ μ ((e : (a : ℕ) → ι) (↑i : ℕ)) :
            Measure ((i : ↥(I.preimage (⇑e : (a : ℕ) → ι) ⋯)) → X ((e : (a : ℕ) → ι) (↑i : ℕ)))) :
          (a :
              Set
                ((a : ↥(I.preimage (⇑e : (a : ℕ) → ι) ⋯)) →
                  X (↑((e.restrictPreimageFinset I : (a : ↥(I.preimage (⇑e : (a : ℕ) → ι) ⋯)) → ↥I) a) : ι))) →
            ℝ≥0∞)
        ((⇑(Equiv.piCongrLeft.{u_2 + 1, 1, u_1 + 1} (fun (b : ↥I) ↦ X (↑b : ι)) (e.restrictPreimageFinset I) :
                ((a : ↥(I.preimage (⇑e : (a : ℕ) → ι) ⋯)) →
                    X (↑((e.restrictPreimageFinset I : (a : ↥(I.preimage (⇑e : (a : ℕ) → ι) ⋯)) → ↥I) a) : ι)) ≃
                  ((b : ↥I) → X (↑b : ι))) :
            (a :
                (a : ↥(I.preimage (⇑e : (a : ℕ) → ι) ⋯)) →
                  X (↑((e.restrictPreimageFinset I : (a : ↥(I.preimage (⇑e : (a : ℕ) → ι) ⋯)) → ↥I) a) : ι)) →
              (b : ↥I) → X (↑b : ι)) ⁻¹'
          S) :
      ℝ≥0∞)
    (((Measure.pi (α := fun (i : ↥(I.preimage (⇑e : (a : ℕ) → ι) ⋯)) ↦
              X (↑((e.restrictPreimageFinset I : (a : ↥(I.preimage (⇑e : (a : ℕ) → ι) ⋯)) → ↥I) i) : ι))
              fun (i : ↥(I.preimage (⇑e : (a : ℕ) → ι) ⋯)) ↦
              μ (↑((e.restrictPreimageFinset I : (a : ↥(I.preimage (⇑e : (a : ℕ) → ι) ⋯)) → ↥I) i) : ι) :
            Measure
              ((i : ↥(I.preimage (⇑e : (a : ℕ) → ι) ⋯)) →
                X (↑((e.restrictPreimageFinset I : (a : ↥(I.preimage (⇑e : (a : ℕ) → ι) ⋯)) → ↥I) i) : ι))) :
          (a :
              Set
                ((b : ↥(I.preimage (⇑e : (a : ℕ) → ι) ⋯)) →
                  X (↑((e.restrictPreimageFinset I : (a : ↥(I.preimage (⇑e : (a : ℕ) → ι) ⋯)) → ↥I) b) : ι))) →
            ℝ≥0∞)
        ((⇑(Equiv.piCongrLeft.{u_2 + 1, 1, u_1 + 1} (fun (i : ↥I) ↦ X (↑i : ι)) (e.restrictPreimageFinset I) :
                ((a : ↥(I.preimage (⇑e : (a : ℕ) → ι) ⋯)) →
                    X (↑((e.restrictPreimageFinset I : (a : ↥(I.preimage (⇑e : (a : ℕ) → ι) ⋯)) → ↥I) a) : ι)) ≃
                  ((b : ↥I) → X (↑b : ι))) :
            (a :
                (a : ↥(I.preimage (⇑e : (a : ℕ) → ι) ⋯)) →
                  X (↑((e.restrictPreimageFinset I : (a : ↥(I.preimage (⇑e : (a : ℕ) → ι) ⋯)) → ↥I) a) : ι)) →
              (b : ↥I) → X (↑b : ι)) ⁻¹'
          S) :
      ℝ≥0∞)
rw₁ :
  Measurable (α :=
    (b : ↥(I.preimage (⇑e : (a : ℕ) → ι) ⋯)) →
      X (↑((e.restrictPreimageFinset I : (a : ↥(I.preimage (⇑e : (a : ℕ) → ι) ⋯)) → ↥I) b) : ι))
    (β := (i : ↥I) → X (↑i : ι))
    (⇑(piCongrLeft.{0, u_1, u_2} (fun (i : ↥I) ↦ X (↑i : ι)) (e.restrictPreimageFinset I) :
          ((b : ↥(I.preimage (⇑e : (a : ℕ) → ι) ⋯)) →
              X (↑((e.restrictPreimageFinset I : (a : ↥(I.preimage (⇑e : (a : ℕ) → ι) ⋯)) → ↥I) b) : ι)) ≃ᵐ
            ((a : ↥I) → X (↑a : ι))) :
      (a :
          (b : ↥(I.preimage (⇑e : (a : ℕ) → ι) ⋯)) →
            X (↑((e.restrictPreimageFinset I : (a : ↥(I.preimage (⇑e : (a : ℕ) → ι) ⋯)) → ↥I) b) : ι)) →
        (a : ↥I) → X (↑a : ι))
hf :
  Measurable.{u_2, u_2} (α := (n : ℕ) → X ((e : (a : ℕ) → ι) n))
    ((I.preimage (⇑e : (a : ℕ) → ι) ⋯).restrict (π := fun (i : ℕ) ↦ X ((e : (a : ℕ) → ι) i)))
hs₁ :
  MeasurableSet.{u_2} (α :=
    (a : ↥(I.preimage (⇑e : (a : ℕ) → ι) ⋯)) →
      X (↑((e.restrictPreimageFinset I : (a : ↥(I.preimage (⇑e : (a : ℕ) → ι) ⋯)) → ↥I) a) : ι))
    ((⇑(Equiv.piCongrLeft.{u_2 + 1, 1, u_1 + 1} (fun (b : ↥I) ↦ X (↑b : ι)) (e.restrictPreimageFinset I) :
            ((a : ↥(I.preimage (⇑e : (a : ℕ) → ι) ⋯)) →
                X (↑((e.restrictPreimageFinset I : (a : ↥(I.preimage (⇑e : (a : ℕ) → ι) ⋯)) → ↥I) a) : ι)) ≃
              ((b : ↥I) → X (↑b : ι))) :
        (a :
            (a : ↥(I.preimage (⇑e : (a : ℕ) → ι) ⋯)) →
              X (↑((e.restrictPreimageFinset I : (a : ↥(I.preimage (⇑e : (a : ℕ) → ι) ⋯)) → ↥I) a) : ι)) →
          (b : ↥I) → X (↑b : ι)) ⁻¹'
      S)
rw₂ :
  Measurable (α := (b : ℕ) → X ((e : (a : ℕ) → ι) b)) (β := (i : ι) → X i)
    (⇑(piCongrLeft X e) : (a : (b : ℕ) → X ((e : (a : ℕ) → ι) b)) → (a : ι) → X a)
⊢ Eq (α := ℝ≥0∞)
    ((map (α := (b : ℕ) → X ((e : (a : ℕ) → ι) b))
            (⇑(piCongrLeft X e) : (a : (b : ℕ) → X ((e : (a : ℕ) → ι) b)) → (a : ι) → X a)
            (infinitePiNat (X := fun (n : ℕ) ↦ X ((e : (a : ℕ) → ι) n)) fun (n : ℕ) ↦ μ ((e : (a : ℕ) → ι) n)) :
          (a : Set ((a : ι) → X a)) → ℝ≥0∞)
        (cylinder (α := X) I S) :
      ℝ≥0∞)
    ((piContent (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) (cylinder (α := X) I S) : ℝ≥0∞)

Tactic:
rw [map_apply _ hS.cylinder, cylinder, ← Set.preimage_comp, coe_piCongrLeft,
    restrict_comp_piCongrLeft, Set.preimage_comp, ← map_apply,
    infinitePiNat_map_restrict (fun n ↦ μ (e n)), ← cylinder, piContent_cylinder μ hS,
    ← pi_map_piCongrLeft (e.restrictPreimageFinset I), map_apply _ hS, coe_piCongrLeft]

Premises used: MeasureTheory.Measure.pi_map_piCongrLeft, MeasureTheory.piContent_cylinder, MeasureTheory.Measure.map_apply, Set.preimage_comp, MeasureTheory.cylinder, MeasurableEquiv.coe_piCongrLeft, MeasurableSet.cylinder, MeasureTheory.Measure.infinitePiNat_map_restrict, Equiv.restrictPreimageFinset, Finset.restrict_comp_piCongrLeft, DFunLike.coe