-- Module: Mathlib.Probability.ProductMeasure
Goal:
ι : Type u_3
κ : ι → Type u_4
X : (i : ι) → κ i → Type u_5
mX : (i : ι) → (j : κ i) → MeasurableSpace (X i j)
μ : (i : ι) → (j : κ i) → Measure (X i j)
hμ : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (μ i j)
s : Finset ((i : ι) × κ i)
t : (i : (i : ι) × κ i) → Set (X (i.fst (β := fun (i : ι) ↦ κ i)) (i.snd (β := fun (i : ι) ↦ κ i)))
ht : ∀ (i : (i : ι) × κ i), MeasurableSet (t i)
hν :
  Eq (α := ℝ≥0∞)
    ((infinitePi (X := fun (i : ι) ↦ (i_1 : κ i) → X i i_1) fun (i : ι) ↦ infinitePi (X := X i) fun (j : κ i) ↦ μ i j :
          (a : Set ((i : ι) → (j : κ i) → X i j)) → ℝ≥0∞)
        (Set.preimage (β := (i : (i : ι) × κ i) → X (i.fst (β := fun (i : ι) ↦ κ i)) (i.snd (β := fun (i : ι) ↦ κ i)))
          (⇑(MeasurableEquiv.symm (piCurry (κ := κ) X)) :
            (a : (i : ι) → (j : κ i) → X i j) → (p : (i : ι) × κ i) → X p.fst p.snd)
          ((↑s : Set ((i : ι) × κ i)).pi (α := fun (i : (i : ι) × κ i) ↦
            X (i.fst (β := fun (i : ι) ↦ κ i)) (i.snd (β := fun (i : ι) ↦ κ i))) fun (x : (i : ι) × κ i) ↦ t x)) :
      ℝ≥0∞)
    (∏ i ∈ s,
        (μ (i.fst (β := fun (i : ι) ↦ κ i)) (i.snd (β := fun (i : ι) ↦ κ i)) : (a : Set (X i.fst i.snd)) → ℝ≥0∞) (t i) :
      ℝ≥0∞)
hν₁ :
  Eq (α := ℝ≥0∞)
    ((infinitePi (X := fun (i : ι) ↦ (i_1 : κ i) → X i i_1) fun (i : ι) ↦ infinitePi (X := X i) fun (j : κ i) ↦ μ i j :
          (a : Set ((i : ι) → (j : κ i) → X i j)) → ℝ≥0∞)
        (Set.preimage (β := (i : (i : ι) × κ i) → X (i.fst (β := fun (i : ι) ↦ κ i)) (i.snd (β := fun (i : ι) ↦ κ i)))
          (⇑(MeasurableEquiv.symm (piCurry (κ := κ) X)) :
            (a : (i : ι) → (j : κ i) → X i j) → (p : (i : ι) × κ i) → X p.fst p.snd)
          ((↑((image (Sigma.fst (β := fun (a : ι) ↦ κ a)) s).sigma (α := fun (a : ι) ↦ κ a) fun (a : ι) ↦
                    s.preimage (Sigma.mk (β := fun (a : ι) ↦ κ a) a) ⋯) :
                Set ((i : ι) × κ i)).pi
            (α := fun (i : (i : ι) × κ i) ↦ X (i.fst (β := fun (i : ι) ↦ κ i)) (i.snd (β := fun (i : ι) ↦ κ i)))
            fun (x : (i : ι) × κ i) ↦ t x)) :
      ℝ≥0∞)
    (∏
        i ∈
          (image (Sigma.fst (β := fun (a : ι) ↦ κ a)) s).sigma (α := fun (a : ι) ↦ κ a) fun (a : ι) ↦
            s.preimage (Sigma.mk (β := fun (a : ι) ↦ κ a) a) ⋯,
        (μ (i.fst (β := fun (i : ι) ↦ κ i)) (i.snd (β := fun (i : ι) ↦ κ i)) : (a : Set (X i.fst i.snd)) → ℝ≥0∞) (t i) :
      ℝ≥0∞)
hν₂ :
  Eq (α := ℝ≥0∞)
    ((infinitePi (X := fun (i : ι) ↦ (i_1 : κ i) → X i i_1) fun (i : ι) ↦ infinitePi (X := X i) fun (j : κ i) ↦ μ i j :
          (a : Set ((i : ι) → (j : κ i) → X i j)) → ℝ≥0∞)
        (Sigma.uncurry (β := κ) (γ := X) ⁻¹'
          (↑((image (Sigma.fst (β := fun (a : ι) ↦ κ a)) s).sigma (α := fun (a : ι) ↦ κ a) fun (a : ι) ↦
                    s.preimage (Sigma.mk (β := fun (a : ι) ↦ κ a) a) ⋯) :
                Set ((i : ι) × κ i)).pi
            (α := fun (i : (i : ι) × κ i) ↦ X (i.fst (β := fun (i : ι) ↦ κ i)) (i.snd (β := fun (i : ι) ↦ κ i)))
            fun (x : (i : ι) × κ i) ↦ t x) :
      ℝ≥0∞)
    (∏
        i ∈
          (image (Sigma.fst (β := fun (a : ι) ↦ κ a)) s).sigma (α := fun (a : ι) ↦ κ a) fun (a : ι) ↦
            s.preimage (Sigma.mk (β := fun (a : ι) ↦ κ a) a) ⋯,
        (μ (i.fst (β := fun (i : ι) ↦ κ i)) (i.snd (β := fun (i : ι) ↦ κ i)) : (a : Set (X i.fst i.snd)) → ℝ≥0∞) (t i) :
      ℝ≥0∞)
hν₃ :
  Eq (α := ℝ≥0∞)
    ((infinitePi (X := fun (i : ι) ↦ (i_1 : κ i) → X i i_1) fun (i : ι) ↦ infinitePi (X := X i) fun (j : κ i) ↦ μ i j :
          (a : Set ((i : ι) → (j : κ i) → X i j)) → ℝ≥0∞)
        (Sigma.uncurry (β := κ) (γ := X) ⁻¹'
          Set.pi (α := fun (i : (i : ι) × κ i) ↦ X (i.fst (β := fun (i : ι) ↦ κ i)) (i.snd (β := fun (i : ι) ↦ κ i)))
            ((↑(image (Sigma.fst (β := fun (a : ι) ↦ κ a)) s) : Set ι).sigma (α := fun (a : ι) ↦ κ a) fun (i : ι) ↦
              (↑(s.preimage (Sigma.mk (β := fun (a : ι) ↦ κ a) i) ⋯) : Set (κ i)))
            fun (x : (i : ι) × κ i) ↦ t x) :
      ℝ≥0∞)
    (∏
        i ∈
          (image (Sigma.fst (β := fun (a : ι) ↦ κ a)) s).sigma (α := fun (a : ι) ↦ κ a) fun (a : ι) ↦
            s.preimage (Sigma.mk (β := fun (a : ι) ↦ κ a) a) ⋯,
        (μ (i.fst (β := fun (i : ι) ↦ κ i)) (i.snd (β := fun (i : ι) ↦ κ i)) : (a : Set (X i.fst i.snd)) → ℝ≥0∞) (t i) :
      ℝ≥0∞)
hν₄ :
  Eq (α := ℝ≥0∞)
    ((infinitePi (X := fun (i : ι) ↦ (i_1 : κ i) → X i i_1) fun (i : ι) ↦ infinitePi (X := X i) fun (j : κ i) ↦ μ i j :
          (a : Set ((i : ι) → (j : κ i) → X i j)) → ℝ≥0∞)
        ((↑(image (Sigma.fst (β := fun (a : ι) ↦ κ a)) s) : Set ι).pi (α := fun (i : ι) ↦
          (i_1 : κ i) →
            X ((Sigma.mk (β := fun (i : ι) ↦ κ i) i i_1).fst (β := fun (i : ι) ↦ κ i))
              ((Sigma.mk (β := fun (i : ι) ↦ κ i) i i_1).snd (β := fun (i : ι) ↦ κ i)))
          fun (i : ι) ↦
          (↑(s.preimage (Sigma.mk (β := fun (a : ι) ↦ κ a) i) ⋯) : Set (κ i)).pi (α := fun (j : κ i) ↦
            X ((Sigma.mk (β := fun (i : ι) ↦ κ i) i j).fst (β := fun (i : ι) ↦ κ i))
              ((Sigma.mk (β := fun (i : ι) ↦ κ i) i j).snd (β := fun (i : ι) ↦ κ i)))
            fun (j : κ i) ↦ t (Sigma.mk (β := fun (i : ι) ↦ κ i) i j)) :
      ℝ≥0∞)
    (∏
        i ∈
          (image (Sigma.fst (β := fun (a : ι) ↦ κ a)) s).sigma (α := fun (a : ι) ↦ κ a) fun (a : ι) ↦
            s.preimage (Sigma.mk (β := fun (a : ι) ↦ κ a) a) ⋯,
        (μ (i.fst (β := fun (i : ι) ↦ κ i)) (i.snd (β := fun (i : ι) ↦ κ i)) : (a : Set (X i.fst i.snd)) → ℝ≥0∞) (t i) :
      ℝ≥0∞)
hν₅ :
  Eq (α := ℝ≥0∞)
    (∏ i ∈ image (Sigma.fst (β := fun (a : ι) ↦ κ a)) s,
      (infinitePi (X := X i) fun (j : κ i) ↦ μ i j : (a : Set ((i_1 : κ i) → X i i_1)) → ℝ≥0∞)
        ((↑(s.preimage (Sigma.mk (β := fun (a : ι) ↦ κ a) i) ⋯) : Set (κ i)).pi (α := fun (j : κ i) ↦
          X ((Sigma.mk (β := fun (i : ι) ↦ κ i) i j).fst (β := fun (i : ι) ↦ κ i))
            ((Sigma.mk (β := fun (i : ι) ↦ κ i) i j).snd (β := fun (i : ι) ↦ κ i)))
          fun (j : κ i) ↦ t (Sigma.mk (β := fun (i : ι) ↦ κ i) i j)))
    (∏
      i ∈
        (image (Sigma.fst (β := fun (a : ι) ↦ κ a)) s).sigma (α := fun (a : ι) ↦ κ a) fun (a : ι) ↦
          s.preimage (Sigma.mk (β := fun (a : ι) ↦ κ a) a) ⋯,
      (μ (i.fst (β := fun (i : ι) ↦ κ i)) (i.snd (β := fun (i : ι) ↦ κ i)) : (a : Set (X i.fst i.snd)) → ℝ≥0∞) (t i))
hν₆ :
  ∀ i ∈ image (Sigma.fst (β := fun (a : ι) ↦ κ a)) s,
    MeasurableSet (α := (i_1 : κ i) → X i i_1)
      ((↑(s.preimage (Sigma.mk (β := fun (a : ι) ↦ κ a) i) ⋯) : Set (κ i)).pi (α := fun (j : κ i) ↦
        X ((Sigma.mk (β := fun (i : ι) ↦ κ i) i j).fst (β := fun (i : ι) ↦ κ i))
          ((Sigma.mk (β := fun (i : ι) ↦ κ i) i j).snd (β := fun (i : ι) ↦ κ i)))
        fun (j : κ i) ↦ t (Sigma.mk (β := fun (i : ι) ↦ κ i) i j))
hν₇ :
  Eq (α := ℝ≥0∞)
    (∏ i ∈ image (Sigma.fst (β := fun (a : ι) ↦ κ a)) s,
      (infinitePi (X := X i) fun (j : κ i) ↦ μ i j : (a : Set ((i_1 : κ i) → X i i_1)) → ℝ≥0∞)
        ((↑(s.preimage (Sigma.mk (β := fun (a : ι) ↦ κ a) i) ⋯) : Set (κ i)).pi (α := fun (j : κ i) ↦
          X ((Sigma.mk (β := fun (i : ι) ↦ κ i) i j).fst (β := fun (i : ι) ↦ κ i))
            ((Sigma.mk (β := fun (i : ι) ↦ κ i) i j).snd (β := fun (i : ι) ↦ κ i)))
          fun (j : κ i) ↦ t (Sigma.mk (β := fun (i : ι) ↦ κ i) i j)))
    (∏ a ∈ image (Sigma.fst (β := fun (a : ι) ↦ κ a)) s,
      ∏ s ∈ s.preimage (Sigma.mk (β := fun (a : ι) ↦ κ a) a) ⋯,
        (μ ((Sigma.mk (β := fun (a : ι) ↦ κ a) a s).fst (β := fun (i : ι) ↦ κ i))
              ((Sigma.mk (β := fun (a : ι) ↦ κ a) a s).snd (β := fun (i : ι) ↦ κ i)) :
            (a : Set (X ⟨a, s⟩.fst ⟨a, s⟩.snd)) → ℝ≥0∞)
          (t (Sigma.mk (β := fun (a : ι) ↦ κ a) a s)))
hν₈ :
  ∀ i ∈ image (Sigma.fst (β := fun (a : ι) ↦ κ a)) s,
    MeasurableSet (α := (i_1 : κ i) → X i i_1)
      ((↑(s.preimage (Sigma.mk (β := fun (a : ι) ↦ κ a) i) ⋯) : Set (κ i)).pi (α := fun (j : κ i) ↦
        X ((Sigma.mk (β := fun (i : ι) ↦ κ i) i j).fst (β := fun (i : ι) ↦ κ i))
          ((Sigma.mk (β := fun (i : ι) ↦ κ i) i j).snd (β := fun (i : ι) ↦ κ i)))
        fun (j : κ i) ↦ t (Sigma.mk (β := fun (i : ι) ↦ κ i) i j))
hν₉ :
  Eq (α := ℝ≥0∞)
    (∏ i ∈ image (Sigma.fst (β := fun (a : ι) ↦ κ a)) s,
      (infinitePi (X := X i) fun (j : κ i) ↦ μ i j : (a : Set ((i_1 : κ i) → X i i_1)) → ℝ≥0∞)
        ((↑(s.preimage (Sigma.mk (β := fun (a : ι) ↦ κ a) i) ⋯) : Set (κ i)).pi (α := fun (j : κ i) ↦
          X ((Sigma.mk (β := fun (i : ι) ↦ κ i) i j).fst (β := fun (i : ι) ↦ κ i))
            ((Sigma.mk (β := fun (i : ι) ↦ κ i) i j).snd (β := fun (i : ι) ↦ κ i)))
          fun (j : κ i) ↦ t (Sigma.mk (β := fun (i : ι) ↦ κ i) i j)))
    (∏ a ∈ image (Sigma.fst (β := fun (a : ι) ↦ κ a)) s,
      ∏ s ∈ s.preimage (Sigma.mk (β := fun (a : ι) ↦ κ a) a) ⋯,
        (μ ((Sigma.mk (β := fun (a : ι) ↦ κ a) a s).fst (β := fun (i : ι) ↦ κ i))
              ((Sigma.mk (β := fun (a : ι) ↦ κ a) a s).snd (β := fun (i : ι) ↦ κ i)) :
            (a : Set (X ⟨a, s⟩.fst ⟨a, s⟩.snd)) → ℝ≥0∞)
          (t (Sigma.mk (β := fun (a : ι) ↦ κ a) a s)))
hν₁₀ :
  ∀ i ∈ image (Sigma.fst (β := fun (a : ι) ↦ κ a)) s,
    MeasurableSet (α := (i_1 : κ i) → X i i_1)
      ((↑(s.preimage (Sigma.mk (β := fun (a : ι) ↦ κ a) i) ⋯) : Set (κ i)).pi (α := fun (j : κ i) ↦
        X ((Sigma.mk (β := fun (i : ι) ↦ κ i) i j).fst (β := fun (i : ι) ↦ κ i))
          ((Sigma.mk (β := fun (i : ι) ↦ κ i) i j).snd (β := fun (i : ι) ↦ κ i)))
        fun (j : κ i) ↦ t (Sigma.mk (β := fun (i : ι) ↦ κ i) i j))
hν₁₁ :
  Eq (α := ℝ≥0∞)
    (∏ i ∈ image (Sigma.fst (β := fun (a : ι) ↦ κ a)) s,
      (infinitePi (X := X i) fun (j : κ i) ↦ μ i j : (a : Set ((i_1 : κ i) → X i i_1)) → ℝ≥0∞)
        ((↑(s.preimage (Sigma.mk (β := fun (a : ι) ↦ κ a) i) ⋯) : Set (κ i)).pi (α := fun (j : κ i) ↦
          X ((Sigma.mk (β := fun (i : ι) ↦ κ i) i j).fst (β := fun (i : ι) ↦ κ i))
            ((Sigma.mk (β := fun (i : ι) ↦ κ i) i j).snd (β := fun (i : ι) ↦ κ i)))
          fun (j : κ i) ↦ t (Sigma.mk (β := fun (i : ι) ↦ κ i) i j)))
    (∏ a ∈ image (Sigma.fst (β := fun (a : ι) ↦ κ a)) s,
      ∏ s ∈ s.preimage (Sigma.mk (β := fun (a : ι) ↦ κ a) a) ⋯,
        (μ ((Sigma.mk (β := fun (a : ι) ↦ κ a) a s).fst (β := fun (i : ι) ↦ κ i))
              ((Sigma.mk (β := fun (a : ι) ↦ κ a) a s).snd (β := fun (i : ι) ↦ κ i)) :
            (a : Set (X ⟨a, s⟩.fst ⟨a, s⟩.snd)) → ℝ≥0∞)
          (t (Sigma.mk (β := fun (a : ι) ↦ κ a) a s)))
hν₁₂ hν₁₃ :
  ∀ i ∈ image (Sigma.fst (β := fun (a : ι) ↦ κ a)) s,
    MeasurableSet (α := (i_1 : κ i) → X i i_1)
      ((↑(s.preimage (Sigma.mk (β := fun (a : ι) ↦ κ a) i) ⋯) : Set (κ i)).pi (α := fun (j : κ i) ↦
        X ((Sigma.mk (β := fun (i : ι) ↦ κ i) i j).fst (β := fun (i : ι) ↦ κ i))
          ((Sigma.mk (β := fun (i : ι) ↦ κ i) i j).snd (β := fun (i : ι) ↦ κ i)))
        fun (j : κ i) ↦ t (Sigma.mk (β := fun (i : ι) ↦ κ i) i j))
⊢ Eq (α := ℝ≥0∞)
    ((map (α := (i : ι) → (j : κ i) → X i j)
            (⇑(MeasurableEquiv.symm (piCurry (κ := κ) X)) :
              (a : (i : ι) → (j : κ i) → X i j) → (p : (i : ι) × κ i) → X p.fst p.snd)
            (infinitePi (X := fun (i : ι) ↦ (i_1 : κ i) → X i i_1) fun (i : ι) ↦
              infinitePi (X := X i) fun (j : κ i) ↦ μ i j) :
          (a : Set ((i : (i : ι) × κ i) → X i.fst i.snd)) → ℝ≥0∞)
        ((↑s : Set ((i : ι) × κ i)).pi (α := fun (i : (i : ι) × κ i) ↦
          X (i.fst (β := fun (i : ι) ↦ κ i)) (i.snd (β := fun (i : ι) ↦ κ i))) t) :
      ℝ≥0∞)
    (∏ i ∈ s,
        (μ (i.fst (β := fun (i : ι) ↦ κ i)) (i.snd (β := fun (i : ι) ↦ κ i)) : (a : Set (X i.fst i.snd)) → ℝ≥0∞) (t i) :
      ℝ≥0∞)

Tactic:
classical
  rw [map_apply (by fun_prop) (.pi (countable_toSet _) fun _ _ ↦ ht _),
    ← Finset.sigma_image_fst_preimage_mk s, coe_piCurry_symm, Finset.coe_sigma,
    Set.uncurry_preimage_sigma_pi, infinitePi_pi, Finset.prod_sigma]
  · exact Finset.prod_congr rfl (fun _ _ ↦ infinitePi_pi _ fun _ _ ↦ ht _)
  · simp only [mem_image, Sigma.exists, exists_and_right, exists_eq_right, forall_exists_index]
    exact fun i j hij ↦ MeasurableSet.pi (countable_toSet _) fun k hk ↦ by simp_all

Premises used: Finset.mem_image, MeasureTheory.Measure.map_apply, Sigma.exists, MeasureTheory.Measure.infinitePi_pi, forall_exists_index, exists_eq_right, Finset.prod_congr, Finset.prod_sigma, exists_and_right, Finset.countable_toSet, Set.uncurry_preimage_sigma_pi, MeasurableEquiv.coe_piCurry_symm, rfl, Finset.coe_sigma, MeasurableSet.pi