-- 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)
ν : Measure ((i : ι) → X i)
hν :
  ∀ (s : Finset ι) (t : (i : ι) → Set (X i)),
    (∀ (i : ι), MeasurableSet (t i)) →
      Eq (α := ℝ≥0∞) ((ν : (a : Set ((i : ι) → X i)) → ℝ≥0∞) ((↑s : Set ι).pi (α := X) t) : ℝ≥0∞)
        (∏ i ∈ s, (μ i : (a : Set (X i)) → ℝ≥0∞) (t i) : ℝ≥0∞)
s : Finset ι
t : (i : ↥s) → Set (X (↑i : ι))
ht : ∀ (i : ↥s), MeasurableSet (t i)
rw :
  Eq (α := ℝ≥0∞)
    ((ν : (a : Set ((i : ι) → X i)) → ℝ≥0∞)
        (s.restrict (π := X) ⁻¹' Set.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) Set.univ t) :
      ℝ≥0∞)
    (∏ i : ↥s, ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (t i) : ℝ≥0∞)
hf : Measurable (α := (i : ι) → X i) (s.restrict (π := X))
hs : MeasurableSet (Set.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) Set.univ t)
rw₁ :
  Eq (α := ℝ≥0∞)
    ((ν : (a : Set ((i : ι) → X i)) → ℝ≥0∞)
        ((↑s : Set ι).pi (α := X) fun (i : ι) ↦
          if h : i ∈ s then t (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i h) else Set.univ) :
      ℝ≥0∞)
    (∏ i : ↥s, ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (t i) : ℝ≥0∞)
hf₁ : Measurable (α := (i : ι) → X i) (s.restrict (π := X))
hs₁ : MeasurableSet (Set.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) Set.univ t)
rw₂ :
  Eq (α := ℝ≥0∞)
    (∏ i ∈ s,
      (μ i : (a : Set (X i)) → ℝ≥0∞) (if h : i ∈ s then t (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i h) else Set.univ))
    (∏ i : ↥s, ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (t i))
a :
  ∀ (i : ι),
    MeasurableSet.{u_2} (α := X i) (if h : i ∈ s then t (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i h) else Set.univ)
hf₂ : Measurable (α := (i : ι) → X i) (s.restrict (π := X))
hs₂ : MeasurableSet (Set.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) Set.univ t)
rw₃ :
  Eq (α := ℝ≥0∞)
    (∏ x ∈ s.attach,
      ((μ (↑x : ι) : Measure (X (↑x : ι))) : (a : Set (X (↑x : ι))) → ℝ≥0∞)
        (if h : (↑x : ι) ∈ s then t (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) (↑x : ι) h) else Set.univ))
    (∏ i : ↥s, ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (t i))
a₁ :
  ∀ (i : ι),
    MeasurableSet.{u_2} (α := X i) (if h : i ∈ s then t (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i h) else Set.univ)
hf₃ : Measurable (α := (i : ι) → X i) (s.restrict (π := X))
hs₃ : MeasurableSet (Set.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) Set.univ t)
rw₄ :
  Eq (α := ℝ≥0∞)
    (∏ x ∈ s.attach,
      ((μ (↑x : ι) : Measure (X (↑x : ι))) : (a : Set (X (↑x : ι))) → ℝ≥0∞)
        (if h : (↑x : ι) ∈ s then t (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) (↑x : ι) h) else Set.univ))
    (∏ i ∈ s.attach, ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (t i))
a₂ :
  ∀ (i : ι),
    MeasurableSet.{u_2} (α := X i) (if h : i ∈ s then t (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i h) else Set.univ)
hf₄ : Measurable (α := (i : ι) → X i) (s.restrict (π := X))
hs₄ : MeasurableSet (Set.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) Set.univ t)
rw₅ :
  Eq (α := ℝ≥0∞)
    (∏ x ∈ s.attach,
      ((μ (↑x : ι) : Measure (X (↑x : ι))) : (a : Set (X (↑x : ι))) → ℝ≥0∞)
        (if h : (↑x : ι) ∈ s then t (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) (↑x : ι) h) else Set.univ))
    (∏ i ∈ s.attach, ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (t i))
a₃ :
  ∀ (i : ι),
    MeasurableSet.{u_2} (α := X i) (if h : i ∈ s then t (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i h) else Set.univ)
hf₅ : Measurable (α := (i : ι) → X i) (s.restrict (π := X))
hs₅ : MeasurableSet (Set.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) Set.univ t)
rw₆ :
  Eq (α := ℝ≥0∞)
    (∏ x ∈ s.attach,
      ((μ (↑x : ι) : Measure (X (↑x : ι))) : (a : Set (X (↑x : ι))) → ℝ≥0∞)
        (if h : (↑x : ι) ∈ s then t (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) (↑x : ι) h) else Set.univ))
    (∏ i ∈ s.attach, ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (t i))
a₄ :
  ∀ (i : ι),
    MeasurableSet.{u_2} (α := X i) (if h : i ∈ s then t (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i h) else Set.univ)
hf₆ : Measurable (α := (i : ι) → X i) (s.restrict (π := X))
hs₆ : MeasurableSet (Set.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) Set.univ t)
a₅ :
  ∀ (i : ι),
    MeasurableSet.{u_2} (α := X i) (if h : i ∈ s then t (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i h) else Set.univ)
hf₇ : Measurable (α := (i : ι) → X i) (s.restrict (π := X))
hs₇ : MeasurableSet (Set.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) Set.univ t)
a₆ :
  ∀ (i : ι),
    MeasurableSet.{u_2} (α := X i) (if h : i ∈ s then t (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i h) else Set.univ)
hs₈ hs₉ : MeasurableSet (Set.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) Set.univ t)
⊢ Eq (α := ℝ≥0∞)
    ((map (s.restrict (π := X)) ν : (a : Set ((i : ↥s) → X (↑i : ι))) → ℝ≥0∞)
        (Set.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) Set.univ t) :
      ℝ≥0∞)
    (∏ i : ↥s, ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (t i) : ℝ≥0∞)

Tactic:
classical
  rw [Measure.map_apply, restrict_preimage_univ, hν, ← prod_attach, univ_eq_attach]
  · congr with i
    rw [dif_pos i.2]
  any_goals fun_prop
  · rintro i
    split_ifs with hi
    · exact ht ⟨i, hi⟩
    · exact .univ
  · exact .univ_pi ht

Premises used: MeasureTheory.Measure.map_apply, Finset.restrict_preimage_univ, Finset.univ_eq_attach, Finset.prod_attach