feat: Add lemmas about finite products of measures (#13311)

Add the following lemmas about finite product of measures and measurable equivalences:

- `piCongrLeft_apply_apply`
- `pi_map_piCongrLeft`
- `pi_map_piOptionEquivProd`

Author: LorenzoLuccioli

Mathlib/MeasureTheory/Constructions/Pi.lean

@@ -508,6 +508,44 @@ theorem ae_eq_set_pi {I : Set ι} {s t : ∀ i, Set (α i)} (h : ∀ i ∈ I, s
   (ae_le_set_pi fun i hi => (h i hi).le).antisymm (ae_le_set_pi fun i hi => (h i hi).symm.le)
 #align measure_theory.measure.ae_eq_set_pi MeasureTheory.Measure.ae_eq_set_pi
 
+lemma pi_map_piCongrLeft [hι' : Fintype ι'] (e : ι ≃ ι') {β : ι' → Type*}
+    [∀ i, MeasurableSpace (β i)] (μ : (i : ι') → Measure (β i)) [∀ i, SigmaFinite (μ i)] :
+    (Measure.pi fun i ↦ μ (e i)).map (MeasurableEquiv.piCongrLeft (fun i ↦ β i) e)
+      = Measure.pi μ := by
+  let e_meas : ((b : ι) → β (e b)) ≃ᵐ ((a : ι') → β a) :=
+    MeasurableEquiv.piCongrLeft (fun i ↦ β i) e
+  refine Measure.pi_eq (fun s _ ↦ ?_) |>.symm
+  rw [e_meas.measurableEmbedding.map_apply]
+  let s' : (i : ι) → Set (β (e i)) := fun i ↦ s (e i)
+  have : e_meas ⁻¹' pi univ s = pi univ s' := by
+    ext x
+    simp only [mem_preimage, Set.mem_pi, mem_univ, forall_true_left, s']
+    refine (e.forall_congr ?_).symm
+    intro i
+    rw [MeasurableEquiv.piCongrLeft_apply_apply e x i]
+  rw [this, pi_pi, Finset.prod_equiv e.symm]
+  · simp only [Finset.mem_univ, implies_true]
+  intro i _
+  simp only [s']
+  congr
+  all_goals rw [e.apply_symm_apply]
+
+lemma pi_map_piOptionEquivProd {β : Option ι → Type*} [∀ i, MeasurableSpace (β i)]
+    (μ : (i : Option ι) → Measure (β i)) [∀ (i : Option ι), SigmaFinite (μ i)] :
+    ((Measure.pi fun i ↦ μ (some i)).prod (μ none)).map
+      (MeasurableEquiv.piOptionEquivProd β).symm = Measure.pi μ := by
+  refine pi_eq (fun s _ ↦ ?_) |>.symm
+  let e_meas : ((i : ι) → β (some i)) × β none ≃ᵐ ((i : Option ι) → β i) :=
+    MeasurableEquiv.piOptionEquivProd β |>.symm
+  have me := MeasurableEquiv.measurableEmbedding e_meas
+  have : e_meas ⁻¹' pi univ s = (pi univ (fun i ↦ s (some i))) ×ˢ (s none) := by
+    ext x
+    simp only [mem_preimage, Set.mem_pi, mem_univ, forall_true_left, mem_prod]
+    refine ⟨by tauto, fun _ i ↦ ?_⟩
+    rcases i <;> tauto
+  simp only [me.map_apply, univ_option, le_eq_subset, Finset.prod_insertNone, this, prod_prod,
+    pi_pi, mul_comm]
+
 section Intervals
 
 variable [∀ i, PartialOrder (α i)] [∀ i, NoAtoms (μ i)]

Mathlib/MeasureTheory/MeasurableSpace/Basic.lean

@@ -1763,6 +1763,11 @@ def piCongrLeft (f : δ ≃ δ') : (∀ b, π (f b)) ≃ᵐ ∀ a, π a where
 theorem coe_piCongrLeft (f : δ ≃ δ') :
     ⇑(MeasurableEquiv.piCongrLeft π f) = f.piCongrLeft π := by rfl
 
+lemma piCongrLeft_apply_apply {ι ι' : Type*} (e : ι ≃ ι') {β : ι' → Type*}
+    [∀ i', MeasurableSpace (β i')] (x : (i : ι) → β (e i)) (i : ι) :
+    piCongrLeft (fun i' ↦ β i') e x (e i) = x i := by
+  rw [piCongrLeft, coe_mk, Equiv.piCongrLeft_apply_apply]
+
 /-- Pi-types are measurably equivalent to iterated products. -/
 @[simps! (config := .asFn)]
 def piMeasurableEquivTProd [DecidableEq δ'] {l : List δ'} (hnd : l.Nodup) (h : ∀ i, i ∈ l) :