-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
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
⊢ 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∞)
have rw : Eq (α := ℝ≥0∞)
  (((Measure.pi (α := fun (i : ↥(I.preimage (⇑e : (a : ℕ) → ι) sorry)) ↦ X ((e : (a : ℕ) → ι) (↑i : ℕ)))
            fun (i : ↥(I.preimage (⇑e : (a : ℕ) → ι) sorry)) ↦ μ ((e : (a : ℕ) → ι) (↑i : ℕ)) :
          Measure ((i : ↥(I.preimage (⇑e : (a : ℕ) → ι) sorry)) → X ((e : (a : ℕ) → ι) (↑i : ℕ)))) :
        (a :
            Set
              ((a : ↥(I.preimage (⇑e : (a : ℕ) → ι) sorry)) →
                X (↑((e.restrictPreimageFinset I : (a : ↥(I.preimage (⇑e : (a : ℕ) → ι) sorry)) → ↥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 : ℕ) → ι) sorry)) →
                  X (↑((e.restrictPreimageFinset I : (a : ↥(I.preimage (⇑e : (a : ℕ) → ι) sorry)) → ↥I) a) : ι)) ≃
                ((b : ↥I) → X (↑b : ι))) :
          (a :
              (a : ↥(I.preimage (⇑e : (a : ℕ) → ι) sorry)) →
                X (↑((e.restrictPreimageFinset I : (a : ↥(I.preimage (⇑e : (a : ℕ) → ι) sorry)) → ↥I) a) : ι)) →
            (b : ↥I) → X (↑b : ι)) ⁻¹'
        S) :
    ℝ≥0∞)
  (((Measure.pi (α := fun (i : ↥(I.preimage (⇑e : (a : ℕ) → ι) sorry)) ↦
            X (↑((e.restrictPreimageFinset I : (a : ↥(I.preimage (⇑e : (a : ℕ) → ι) sorry)) → ↥I) i) : ι))
            fun (i : ↥(I.preimage (⇑e : (a : ℕ) → ι) sorry)) ↦
            μ (↑((e.restrictPreimageFinset I : (a : ↥(I.preimage (⇑e : (a : ℕ) → ι) sorry)) → ↥I) i) : ι) :
          Measure
            ((i : ↥(I.preimage (⇑e : (a : ℕ) → ι) sorry)) →
              X (↑((e.restrictPreimageFinset I : (a : ↥(I.preimage (⇑e : (a : ℕ) → ι) sorry)) → ↥I) i) : ι))) :
        (a :
            Set
              ((b : ↥(I.preimage (⇑e : (a : ℕ) → ι) sorry)) →
                X (↑((e.restrictPreimageFinset I : (a : ↥(I.preimage (⇑e : (a : ℕ) → ι) sorry)) → ↥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 : ℕ) → ι) sorry)) →
                  X (↑((e.restrictPreimageFinset I : (a : ↥(I.preimage (⇑e : (a : ℕ) → ι) sorry)) → ↥I) a) : ι)) ≃
                ((b : ↥I) → X (↑b : ι))) :
          (a :
              (a : ↥(I.preimage (⇑e : (a : ℕ) → ι) sorry)) →
                X (↑((e.restrictPreimageFinset I : (a : ↥(I.preimage (⇑e : (a : ℕ) → ι) sorry)) → ↥I) a) : ι)) →
            (b : ↥I) → X (↑b : ι)) ⁻¹'
        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]