diff --git a/Archive/Wiedijk100Theorems/BuffonsNeedle.lean b/Archive/Wiedijk100Theorems/BuffonsNeedle.lean
index e27b8be9851f2..eff8809144258 100644
--- a/Archive/Wiedijk100Theorems/BuffonsNeedle.lean
+++ b/Archive/Wiedijk100Theorems/BuffonsNeedle.lean
@@ -4,11 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Enrico Z. Borba
 -/
 
-import Mathlib.Probability.Density
-import Mathlib.Probability.Notation
-import Mathlib.MeasureTheory.Constructions.Prod.Integral
 import Mathlib.Analysis.SpecialFunctions.Integrals
+import Mathlib.MeasureTheory.Integral.Prod
+import Mathlib.Probability.Density
 import Mathlib.Probability.Distributions.Uniform
+import Mathlib.Probability.Notation
 
 /-!
 
diff --git a/Mathlib.lean b/Mathlib.lean
index f176ac0021cf7..b6e8beed2f35a 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -3324,8 +3324,6 @@ import Mathlib.MeasureTheory.Constructions.HaarToSphere
 import Mathlib.MeasureTheory.Constructions.Pi
 import Mathlib.MeasureTheory.Constructions.Polish.Basic
 import Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal
-import Mathlib.MeasureTheory.Constructions.Prod.Basic
-import Mathlib.MeasureTheory.Constructions.Prod.Integral
 import Mathlib.MeasureTheory.Constructions.Projective
 import Mathlib.MeasureTheory.Constructions.SubmoduleQuotient
 import Mathlib.MeasureTheory.Constructions.UnitInterval
@@ -3427,6 +3425,7 @@ import Mathlib.MeasureTheory.Integral.MeanInequalities
 import Mathlib.MeasureTheory.Integral.PeakFunction
 import Mathlib.MeasureTheory.Integral.Periodic
 import Mathlib.MeasureTheory.Integral.Pi
+import Mathlib.MeasureTheory.Integral.Prod
 import Mathlib.MeasureTheory.Integral.RieszMarkovKakutani
 import Mathlib.MeasureTheory.Integral.SetIntegral
 import Mathlib.MeasureTheory.Integral.SetToL1
@@ -3441,6 +3440,7 @@ import Mathlib.MeasureTheory.MeasurableSpace.Instances
 import Mathlib.MeasureTheory.MeasurableSpace.Invariants
 import Mathlib.MeasureTheory.MeasurableSpace.NCard
 import Mathlib.MeasureTheory.MeasurableSpace.PreorderRestrict
+import Mathlib.MeasureTheory.MeasurableSpace.Prod
 import Mathlib.MeasureTheory.Measure.AEDisjoint
 import Mathlib.MeasureTheory.Measure.AEMeasurable
 import Mathlib.MeasureTheory.Measure.AddContent
@@ -3478,6 +3478,7 @@ import Mathlib.MeasureTheory.Measure.NullMeasurable
 import Mathlib.MeasureTheory.Measure.OpenPos
 import Mathlib.MeasureTheory.Measure.Portmanteau
 import Mathlib.MeasureTheory.Measure.ProbabilityMeasure
+import Mathlib.MeasureTheory.Measure.Prod
 import Mathlib.MeasureTheory.Measure.Regular
 import Mathlib.MeasureTheory.Measure.Restrict
 import Mathlib.MeasureTheory.Measure.SeparableMeasure
diff --git a/Mathlib/Analysis/Convolution.lean b/Mathlib/Analysis/Convolution.lean
index 00f566fb58ae2..cd64fca205ba0 100644
--- a/Mathlib/Analysis/Convolution.lean
+++ b/Mathlib/Analysis/Convolution.lean
@@ -5,7 +5,7 @@ Authors: Floris van Doorn
 -/
 import Mathlib.Analysis.Calculus.ContDiff.Basic
 import Mathlib.Analysis.Calculus.ParametricIntegral
-import Mathlib.MeasureTheory.Constructions.Prod.Integral
+import Mathlib.MeasureTheory.Integral.Prod
 import Mathlib.MeasureTheory.Function.LocallyIntegrable
 import Mathlib.MeasureTheory.Group.Integral
 import Mathlib.MeasureTheory.Group.Prod
diff --git a/Mathlib/Analysis/Fourier/FourierTransform.lean b/Mathlib/Analysis/Fourier/FourierTransform.lean
index 8a1b83c8d5e3e..a5d1ddb0067c9 100644
--- a/Mathlib/Analysis/Fourier/FourierTransform.lean
+++ b/Mathlib/Analysis/Fourier/FourierTransform.lean
@@ -3,13 +3,13 @@ Copyright (c) 2023 David Loeffler. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: David Loeffler
 -/
+import Mathlib.Algebra.Group.AddChar
 import Mathlib.Analysis.Complex.Circle
 import Mathlib.MeasureTheory.Group.Integral
+import Mathlib.MeasureTheory.Integral.Prod
 import Mathlib.MeasureTheory.Integral.SetIntegral
-import Mathlib.MeasureTheory.Measure.Haar.OfBasis
-import Mathlib.MeasureTheory.Constructions.Prod.Integral
 import Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
-import Mathlib.Algebra.Group.AddChar
+import Mathlib.MeasureTheory.Measure.Haar.OfBasis
 
 /-!
 # The Fourier transform
diff --git a/Mathlib/MeasureTheory/Constructions/HaarToSphere.lean b/Mathlib/MeasureTheory/Constructions/HaarToSphere.lean
index c236710f3f0fa..8b8f004c2cbd6 100644
--- a/Mathlib/MeasureTheory/Constructions/HaarToSphere.lean
+++ b/Mathlib/MeasureTheory/Constructions/HaarToSphere.lean
@@ -6,7 +6,7 @@ Authors: Yury Kudryashov
 import Mathlib.Algebra.Order.Field.Pointwise
 import Mathlib.Analysis.NormedSpace.SphereNormEquiv
 import Mathlib.Analysis.SpecialFunctions.Integrals
-import Mathlib.MeasureTheory.Constructions.Prod.Integral
+import Mathlib.MeasureTheory.Integral.Prod
 import Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
 
 /-!
diff --git a/Mathlib/MeasureTheory/Constructions/Pi.lean b/Mathlib/MeasureTheory/Constructions/Pi.lean
index 2a10e3da58fe6..222b04a9c5ac8 100644
--- a/Mathlib/MeasureTheory/Constructions/Pi.lean
+++ b/Mathlib/MeasureTheory/Constructions/Pi.lean
@@ -3,8 +3,8 @@ Copyright (c) 2020 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn
 -/
-import Mathlib.MeasureTheory.Constructions.Prod.Basic
 import Mathlib.MeasureTheory.Group.Measure
+import Mathlib.MeasureTheory.Measure.Prod
 import Mathlib.Topology.Constructions
 
 /-!
diff --git a/Mathlib/MeasureTheory/Group/Convolution.lean b/Mathlib/MeasureTheory/Group/Convolution.lean
index 0796630b4e41a..07a0fe4cdab79 100644
--- a/Mathlib/MeasureTheory/Group/Convolution.lean
+++ b/Mathlib/MeasureTheory/Group/Convolution.lean
@@ -3,8 +3,8 @@ Copyright (c) 2023 Josha Dekker. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Josha Dekker
 -/
-import Mathlib.MeasureTheory.Constructions.Prod.Basic
 import Mathlib.MeasureTheory.Measure.MeasureSpace
+import Mathlib.MeasureTheory.Measure.Prod
 
 /-!
 # The multiplicative and additive convolution of measures
diff --git a/Mathlib/MeasureTheory/Group/Measure.lean b/Mathlib/MeasureTheory/Group/Measure.lean
index 49764e92934c6..c4565fc448a20 100644
--- a/Mathlib/MeasureTheory/Group/Measure.lean
+++ b/Mathlib/MeasureTheory/Group/Measure.lean
@@ -3,8 +3,8 @@ Copyright (c) 2020 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn
 -/
-import Mathlib.MeasureTheory.Constructions.Prod.Basic
 import Mathlib.MeasureTheory.Group.Action
+import Mathlib.MeasureTheory.Measure.Prod
 import Mathlib.Topology.ContinuousMap.CocompactMap
 
 /-!
diff --git a/Mathlib/MeasureTheory/Group/Prod.lean b/Mathlib/MeasureTheory/Group/Prod.lean
index 29e7a7bd7f934..8c7b2f7d77ef1 100644
--- a/Mathlib/MeasureTheory/Group/Prod.lean
+++ b/Mathlib/MeasureTheory/Group/Prod.lean
@@ -3,8 +3,8 @@ Copyright (c) 2021 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn
 -/
-import Mathlib.MeasureTheory.Constructions.Prod.Basic
 import Mathlib.MeasureTheory.Group.Measure
+import Mathlib.MeasureTheory.Measure.Prod
 
 /-!
 # Measure theory in the product of groups
diff --git a/Mathlib/MeasureTheory/Integral/DivergenceTheorem.lean b/Mathlib/MeasureTheory/Integral/DivergenceTheorem.lean
index c42a397ec5d54..827108c784d82 100644
--- a/Mathlib/MeasureTheory/Integral/DivergenceTheorem.lean
+++ b/Mathlib/MeasureTheory/Integral/DivergenceTheorem.lean
@@ -6,9 +6,9 @@ Authors: Yury Kudryashov
 import Mathlib.Analysis.BoxIntegral.DivergenceTheorem
 import Mathlib.Analysis.BoxIntegral.Integrability
 import Mathlib.Analysis.Calculus.Deriv.Basic
-import Mathlib.MeasureTheory.Constructions.Prod.Integral
-import Mathlib.MeasureTheory.Integral.IntervalIntegral
 import Mathlib.Analysis.Calculus.FDeriv.Equiv
+import Mathlib.MeasureTheory.Integral.Prod
+import Mathlib.MeasureTheory.Integral.IntervalIntegral
 
 /-!
 # Divergence theorem for Bochner integral
diff --git a/Mathlib/MeasureTheory/Integral/Pi.lean b/Mathlib/MeasureTheory/Integral/Pi.lean
index 3445cc3f930f1..2bf9b9af0c309 100644
--- a/Mathlib/MeasureTheory/Integral/Pi.lean
+++ b/Mathlib/MeasureTheory/Integral/Pi.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Xavier Roblot
 -/
 import Mathlib.MeasureTheory.Constructions.Pi
-import Mathlib.MeasureTheory.Constructions.Prod.Integral
+import Mathlib.MeasureTheory.Integral.Prod
 
 /-!
 # Integration with respect to a finite product of measures
diff --git a/Mathlib/MeasureTheory/Constructions/Prod/Integral.lean b/Mathlib/MeasureTheory/Integral/Prod.lean
similarity index 99%
rename from Mathlib/MeasureTheory/Constructions/Prod/Integral.lean
rename to Mathlib/MeasureTheory/Integral/Prod.lean
index c86c172d3f6b7..f2ec386e8dfd7 100644
--- a/Mathlib/MeasureTheory/Constructions/Prod/Integral.lean
+++ b/Mathlib/MeasureTheory/Integral/Prod.lean
@@ -3,9 +3,9 @@ Copyright (c) 2020 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn
 -/
-import Mathlib.MeasureTheory.Constructions.Prod.Basic
 import Mathlib.MeasureTheory.Integral.DominatedConvergence
 import Mathlib.MeasureTheory.Integral.SetIntegral
+import Mathlib.MeasureTheory.Measure.Prod
 
 /-!
 # Integration with respect to the product measure
diff --git a/Mathlib/MeasureTheory/Integral/TorusIntegral.lean b/Mathlib/MeasureTheory/Integral/TorusIntegral.lean
index 9591233916874..80b6f7583b816 100644
--- a/Mathlib/MeasureTheory/Integral/TorusIntegral.lean
+++ b/Mathlib/MeasureTheory/Integral/TorusIntegral.lean
@@ -3,8 +3,8 @@ Copyright (c) 2022 Cuma Kökmen. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Cuma Kökmen, Yury Kudryashov
 -/
-import Mathlib.MeasureTheory.Constructions.Prod.Integral
 import Mathlib.MeasureTheory.Integral.CircleIntegral
+import Mathlib.MeasureTheory.Integral.Prod
 import Mathlib.Order.Fin.Tuple
 
 /-!
diff --git a/Mathlib/MeasureTheory/MeasurableSpace/Basic.lean b/Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
index fa14f94db23e7..2416e12bc0baf 100644
--- a/Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
+++ b/Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
@@ -1268,6 +1268,13 @@ theorem isCountablySpanning_measurableSet [MeasurableSpace α] :
     IsCountablySpanning { s : Set α | MeasurableSet s } :=
   ⟨fun _ => univ, fun _ => MeasurableSet.univ, iUnion_const _⟩
 
+/-- Rectangles of countably spanning sets are countably spanning. -/
+lemma IsCountablySpanning.prod {C : Set (Set α)} {D : Set (Set β)} (hC : IsCountablySpanning C)
+    (hD : IsCountablySpanning D) : IsCountablySpanning (image2 (· ×ˢ ·) C D) := by
+  rcases hC, hD with ⟨⟨s, h1s, h2s⟩, t, h1t, h2t⟩
+  refine ⟨fun n => s n.unpair.1 ×ˢ t n.unpair.2, fun n => mem_image2_of_mem (h1s _) (h1t _), ?_⟩
+  rw [iUnion_unpair_prod, h2s, h2t, univ_prod_univ]
+
 namespace MeasurableSet
 
 /-!
diff --git a/Mathlib/MeasureTheory/MeasurableSpace/Prod.lean b/Mathlib/MeasureTheory/MeasurableSpace/Prod.lean
new file mode 100644
index 0000000000000..e9f2db14bfc25
--- /dev/null
+++ b/Mathlib/MeasureTheory/MeasurableSpace/Prod.lean
@@ -0,0 +1,136 @@
+/-
+Copyright (c) 2020 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Floris van Doorn
+-/
+import Mathlib.MeasureTheory.MeasurableSpace.Embedding
+import Mathlib.MeasureTheory.PiSystem
+
+/-!
+# The product sigma algebra
+
+This file talks about the measurability of operations on binary functions.
+-/
+
+assert_not_exists MeasureTheory.Measure
+
+noncomputable section
+
+open Set MeasurableSpace
+
+variable {α β γ : Type*} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ]
+
+/-- The product of generated σ-algebras is the one generated by rectangles, if both generating sets
+  are countably spanning. -/
+theorem generateFrom_prod_eq {α β} {C : Set (Set α)} {D : Set (Set β)} (hC : IsCountablySpanning C)
+    (hD : IsCountablySpanning D) :
+    @Prod.instMeasurableSpace _ _ (generateFrom C) (generateFrom D) =
+      generateFrom (image2 (· ×ˢ ·) C D) := by
+  apply le_antisymm
+  · refine sup_le ?_ ?_ <;> rw [comap_generateFrom] <;> apply generateFrom_le <;>
+      rintro _ ⟨s, hs, rfl⟩
+    · rcases hD with ⟨t, h1t, h2t⟩
+      rw [← prod_univ, ← h2t, prod_iUnion]
+      apply MeasurableSet.iUnion
+      intro n
+      apply measurableSet_generateFrom
+      exact ⟨s, hs, t n, h1t n, rfl⟩
+    · rcases hC with ⟨t, h1t, h2t⟩
+      rw [← univ_prod, ← h2t, iUnion_prod_const]
+      apply MeasurableSet.iUnion
+      rintro n
+      apply measurableSet_generateFrom
+      exact mem_image2_of_mem (h1t n) hs
+  · apply generateFrom_le
+    rintro _ ⟨s, hs, t, ht, rfl⟩
+    dsimp only
+    rw [prod_eq]
+    apply (measurable_fst _).inter (measurable_snd _)
+    · exact measurableSet_generateFrom hs
+    · exact measurableSet_generateFrom ht
+
+/-- If `C` and `D` generate the σ-algebras on `α` resp. `β`, then rectangles formed by `C` and `D`
+  generate the σ-algebra on `α × β`. -/
+theorem generateFrom_eq_prod {C : Set (Set α)} {D : Set (Set β)} (hC : generateFrom C = ‹_›)
+    (hD : generateFrom D = ‹_›) (h2C : IsCountablySpanning C) (h2D : IsCountablySpanning D) :
+    generateFrom (image2 (· ×ˢ ·) C D) = Prod.instMeasurableSpace := by
+  rw [← hC, ← hD, generateFrom_prod_eq h2C h2D]
+
+/-- The product σ-algebra is generated from boxes, i.e. `s ×ˢ t` for sets `s : Set α` and
+  `t : Set β`. -/
+lemma generateFrom_prod :
+    generateFrom (image2 (· ×ˢ ·) { s : Set α | MeasurableSet s } { t : Set β | MeasurableSet t }) =
+      Prod.instMeasurableSpace :=
+  generateFrom_eq_prod generateFrom_measurableSet generateFrom_measurableSet
+    isCountablySpanning_measurableSet isCountablySpanning_measurableSet
+
+/-- Rectangles form a π-system. -/
+lemma isPiSystem_prod :
+    IsPiSystem (image2 (· ×ˢ ·) { s : Set α | MeasurableSet s } { t : Set β | MeasurableSet t }) :=
+  isPiSystem_measurableSet.prod isPiSystem_measurableSet
+
+lemma MeasurableEmbedding.prod_mk {α β γ δ : Type*} {mα : MeasurableSpace α}
+    {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} {f : α → β}
+    {g : γ → δ} (hg : MeasurableEmbedding g) (hf : MeasurableEmbedding f) :
+    MeasurableEmbedding fun x : γ × α => (g x.1, f x.2) := by
+  have h_inj : Function.Injective fun x : γ × α => (g x.fst, f x.snd) := by
+    intro x y hxy
+    rw [← @Prod.mk.eta _ _ x, ← @Prod.mk.eta _ _ y]
+    simp only [Prod.mk.inj_iff] at hxy ⊢
+    exact ⟨hg.injective hxy.1, hf.injective hxy.2⟩
+  refine ⟨h_inj, ?_, ?_⟩
+  · exact (hg.measurable.comp measurable_fst).prod_mk (hf.measurable.comp measurable_snd)
+  · -- Induction using the π-system of rectangles
+    refine fun s hs =>
+      @MeasurableSpace.induction_on_inter _
+        (fun s => MeasurableSet ((fun x : γ × α => (g x.fst, f x.snd)) '' s)) _ _
+        generateFrom_prod.symm isPiSystem_prod ?_ ?_ ?_ ?_ _ hs
+    · simp only [Set.image_empty, MeasurableSet.empty]
+    · rintro t ⟨t₁, ht₁, t₂, ht₂, rfl⟩
+      rw [← Set.prod_image_image_eq]
+      exact (hg.measurableSet_image.mpr ht₁).prod (hf.measurableSet_image.mpr ht₂)
+    · intro t _ ht_m
+      rw [← Set.range_diff_image h_inj, ← Set.prod_range_range_eq]
+      exact
+        MeasurableSet.diff (MeasurableSet.prod hg.measurableSet_range hf.measurableSet_range) ht_m
+    · intro g _ _ hg
+      simp_rw [Set.image_iUnion]
+      exact MeasurableSet.iUnion hg
+
+lemma MeasurableEmbedding.prod_mk_left {β γ : Type*} [MeasurableSingletonClass α]
+    {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ}
+    (x : α) {f : γ → β} (hf : MeasurableEmbedding f) :
+    MeasurableEmbedding (fun y ↦ (x, f y)) where
+  injective := by
+    intro y y'
+    simp only [Prod.mk.injEq, true_and]
+    exact fun h ↦ hf.injective h
+  measurable := Measurable.prod_mk measurable_const hf.measurable
+  measurableSet_image' := by
+    intro s hs
+    convert (MeasurableSet.singleton x).prod (hf.measurableSet_image.mpr hs)
+    ext x
+    simp
+
+lemma measurableEmbedding_prod_mk_left [MeasurableSingletonClass α] (x : α) :
+    MeasurableEmbedding (Prod.mk x : β → α × β) :=
+  MeasurableEmbedding.prod_mk_left x MeasurableEmbedding.id
+
+lemma MeasurableEmbedding.prod_mk_right {β γ : Type*} [MeasurableSingletonClass α]
+    {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ}
+    {f : γ → β} (hf : MeasurableEmbedding f) (x : α) :
+    MeasurableEmbedding (fun y ↦ (f y, x)) where
+  injective := by
+    intro y y'
+    simp only [Prod.mk.injEq, and_true]
+    exact fun h ↦ hf.injective h
+  measurable := Measurable.prod_mk hf.measurable measurable_const
+  measurableSet_image' := by
+    intro s hs
+    convert (hf.measurableSet_image.mpr hs).prod (MeasurableSet.singleton x)
+    ext x
+    simp
+
+lemma measurableEmbedding_prod_mk_right [MeasurableSingletonClass α] (x : α) :
+    MeasurableEmbedding (fun y ↦ (y, x) : β → β × α) :=
+  MeasurableEmbedding.prod_mk_right MeasurableEmbedding.id x
diff --git a/Mathlib/MeasureTheory/Measure/FiniteMeasureProd.lean b/Mathlib/MeasureTheory/Measure/FiniteMeasureProd.lean
index 97ffeece7c11c..422da03a98cea 100644
--- a/Mathlib/MeasureTheory/Measure/FiniteMeasureProd.lean
+++ b/Mathlib/MeasureTheory/Measure/FiniteMeasureProd.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kalle Kytölä
 -/
 import Mathlib.MeasureTheory.Measure.ProbabilityMeasure
-import Mathlib.MeasureTheory.Constructions.Prod.Basic
+import Mathlib.MeasureTheory.Measure.Prod
 
 /-!
 # Products of finite measures and probability measures
diff --git a/Mathlib/MeasureTheory/Measure/Haar/Unique.lean b/Mathlib/MeasureTheory/Measure/Haar/Unique.lean
index 0b75436b65433..a9088acc3aeda 100644
--- a/Mathlib/MeasureTheory/Measure/Haar/Unique.lean
+++ b/Mathlib/MeasureTheory/Measure/Haar/Unique.lean
@@ -3,14 +3,14 @@ Copyright (c) 2023 Sébastien Gouëzel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel
 -/
-import Mathlib.MeasureTheory.Constructions.Prod.Integral
 import Mathlib.MeasureTheory.Function.LocallyIntegrable
 import Mathlib.MeasureTheory.Group.Integral
+import Mathlib.MeasureTheory.Integral.Prod
+import Mathlib.MeasureTheory.Integral.SetIntegral
+import Mathlib.MeasureTheory.Measure.EverywherePos
+import Mathlib.MeasureTheory.Measure.Haar.Basic
 import Mathlib.Topology.Metrizable.Urysohn
 import Mathlib.Topology.UrysohnsLemma
-import Mathlib.MeasureTheory.Measure.Haar.Basic
-import Mathlib.MeasureTheory.Measure.EverywherePos
-import Mathlib.MeasureTheory.Integral.SetIntegral
 
 /-!
 # Uniqueness of Haar measure in locally compact groups
diff --git a/Mathlib/MeasureTheory/Constructions/Prod/Basic.lean b/Mathlib/MeasureTheory/Measure/Prod.lean
similarity index 87%
rename from Mathlib/MeasureTheory/Constructions/Prod/Basic.lean
rename to Mathlib/MeasureTheory/Measure/Prod.lean
index 7b687ed495686..76a9fe13f08da 100644
--- a/Mathlib/MeasureTheory/Constructions/Prod/Basic.lean
+++ b/Mathlib/MeasureTheory/Measure/Prod.lean
@@ -3,9 +3,10 @@ Copyright (c) 2020 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn
 -/
-import Mathlib.MeasureTheory.Measure.GiryMonad
 import Mathlib.Dynamics.Ergodic.MeasurePreserving
 import Mathlib.MeasureTheory.Integral.Lebesgue
+import Mathlib.MeasureTheory.MeasurableSpace.Prod
+import Mathlib.MeasureTheory.Measure.GiryMonad
 import Mathlib.MeasureTheory.Measure.OpenPos
 
 /-!
@@ -62,81 +63,11 @@ open Filter hiding prod_eq map
 
 variable {α α' β β' γ E : Type*}
 
-/-- Rectangles formed by π-systems form a π-system. -/
-theorem IsPiSystem.prod {C : Set (Set α)} {D : Set (Set β)} (hC : IsPiSystem C)
-    (hD : IsPiSystem D) : IsPiSystem (image2 (· ×ˢ ·) C D) := by
-  rintro _ ⟨s₁, hs₁, t₁, ht₁, rfl⟩ _ ⟨s₂, hs₂, t₂, ht₂, rfl⟩ hst
-  rw [prod_inter_prod] at hst ⊢; rw [prod_nonempty_iff] at hst
-  exact mem_image2_of_mem (hC _ hs₁ _ hs₂ hst.1) (hD _ ht₁ _ ht₂ hst.2)
-
-/-- Rectangles of countably spanning sets are countably spanning. -/
-theorem IsCountablySpanning.prod {C : Set (Set α)} {D : Set (Set β)} (hC : IsCountablySpanning C)
-    (hD : IsCountablySpanning D) : IsCountablySpanning (image2 (· ×ˢ ·) C D) := by
-  rcases hC, hD with ⟨⟨s, h1s, h2s⟩, t, h1t, h2t⟩
-  refine ⟨fun n => s n.unpair.1 ×ˢ t n.unpair.2, fun n => mem_image2_of_mem (h1s _) (h1t _), ?_⟩
-  rw [iUnion_unpair_prod, h2s, h2t, univ_prod_univ]
-
 variable [MeasurableSpace α] [MeasurableSpace α'] [MeasurableSpace β] [MeasurableSpace β']
 variable [MeasurableSpace γ]
 variable {μ μ' : Measure α} {ν ν' : Measure β} {τ : Measure γ}
 variable [NormedAddCommGroup E]
 
-/-! ### Measurability
-
-Before we define the product measure, we can talk about the measurability of operations on binary
-functions. We show that if `f` is a binary measurable function, then the function that integrates
-along one of the variables (using either the Lebesgue or Bochner integral) is measurable.
--/
-
-/-- The product of generated σ-algebras is the one generated by rectangles, if both generating sets
-  are countably spanning. -/
-theorem generateFrom_prod_eq {α β} {C : Set (Set α)} {D : Set (Set β)} (hC : IsCountablySpanning C)
-    (hD : IsCountablySpanning D) :
-    @Prod.instMeasurableSpace _ _ (generateFrom C) (generateFrom D) =
-      generateFrom (image2 (· ×ˢ ·) C D) := by
-  apply le_antisymm
-  · refine sup_le ?_ ?_ <;> rw [comap_generateFrom] <;> apply generateFrom_le <;>
-      rintro _ ⟨s, hs, rfl⟩
-    · rcases hD with ⟨t, h1t, h2t⟩
-      rw [← prod_univ, ← h2t, prod_iUnion]
-      apply MeasurableSet.iUnion
-      intro n
-      apply measurableSet_generateFrom
-      exact ⟨s, hs, t n, h1t n, rfl⟩
-    · rcases hC with ⟨t, h1t, h2t⟩
-      rw [← univ_prod, ← h2t, iUnion_prod_const]
-      apply MeasurableSet.iUnion
-      rintro n
-      apply measurableSet_generateFrom
-      exact mem_image2_of_mem (h1t n) hs
-  · apply generateFrom_le
-    rintro _ ⟨s, hs, t, ht, rfl⟩
-    dsimp only
-    rw [prod_eq]
-    apply (measurable_fst _).inter (measurable_snd _)
-    · exact measurableSet_generateFrom hs
-    · exact measurableSet_generateFrom ht
-
-/-- If `C` and `D` generate the σ-algebras on `α` resp. `β`, then rectangles formed by `C` and `D`
-  generate the σ-algebra on `α × β`. -/
-theorem generateFrom_eq_prod {C : Set (Set α)} {D : Set (Set β)} (hC : generateFrom C = ‹_›)
-    (hD : generateFrom D = ‹_›) (h2C : IsCountablySpanning C) (h2D : IsCountablySpanning D) :
-    generateFrom (image2 (· ×ˢ ·) C D) = Prod.instMeasurableSpace := by
-  rw [← hC, ← hD, generateFrom_prod_eq h2C h2D]
-
-/-- The product σ-algebra is generated from boxes, i.e. `s ×ˢ t` for sets `s : Set α` and
-  `t : Set β`. -/
-theorem generateFrom_prod :
-    generateFrom (image2 (· ×ˢ ·) { s : Set α | MeasurableSet s } { t : Set β | MeasurableSet t }) =
-      Prod.instMeasurableSpace :=
-  generateFrom_eq_prod generateFrom_measurableSet generateFrom_measurableSet
-    isCountablySpanning_measurableSet isCountablySpanning_measurableSet
-
-/-- Rectangles form a π-system. -/
-theorem isPiSystem_prod :
-    IsPiSystem (image2 (· ×ˢ ·) { s : Set α | MeasurableSet s } { t : Set β | MeasurableSet t }) :=
-  isPiSystem_measurableSet.prod isPiSystem_measurableSet
-
 /-- If `ν` is a finite measure, and `s ⊆ α × β` is measurable, then `x ↦ ν { y | (x, y) ∈ s }` is
   a measurable function. `measurable_measure_prod_mk_left` is strictly more general. -/
 theorem measurable_measure_prod_mk_left_finite [IsFiniteMeasure ν] {s : Set (α × β)}
@@ -185,72 +116,6 @@ theorem Measurable.map_prod_mk_right {μ : Measure α} [SFinite μ] :
   simp_rw [map_apply measurable_prod_mk_right hs]
   exact measurable_measure_prod_mk_right hs
 
-theorem MeasurableEmbedding.prod_mk {α β γ δ : Type*} {mα : MeasurableSpace α}
-    {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} {f : α → β}
-    {g : γ → δ} (hg : MeasurableEmbedding g) (hf : MeasurableEmbedding f) :
-    MeasurableEmbedding fun x : γ × α => (g x.1, f x.2) := by
-  have h_inj : Function.Injective fun x : γ × α => (g x.fst, f x.snd) := by
-    intro x y hxy
-    rw [← @Prod.mk.eta _ _ x, ← @Prod.mk.eta _ _ y]
-    simp only [Prod.mk.inj_iff] at hxy ⊢
-    exact ⟨hg.injective hxy.1, hf.injective hxy.2⟩
-  refine ⟨h_inj, ?_, ?_⟩
-  · exact (hg.measurable.comp measurable_fst).prod_mk (hf.measurable.comp measurable_snd)
-  · -- Induction using the π-system of rectangles
-    refine fun s hs =>
-      @MeasurableSpace.induction_on_inter _
-        (fun s => MeasurableSet ((fun x : γ × α => (g x.fst, f x.snd)) '' s)) _ _
-        generateFrom_prod.symm isPiSystem_prod ?_ ?_ ?_ ?_ _ hs
-    · simp only [Set.image_empty, MeasurableSet.empty]
-    · rintro t ⟨t₁, ht₁, t₂, ht₂, rfl⟩
-      rw [← Set.prod_image_image_eq]
-      exact (hg.measurableSet_image.mpr ht₁).prod (hf.measurableSet_image.mpr ht₂)
-    · intro t _ ht_m
-      rw [← Set.range_diff_image h_inj, ← Set.prod_range_range_eq]
-      exact
-        MeasurableSet.diff (MeasurableSet.prod hg.measurableSet_range hf.measurableSet_range) ht_m
-    · intro g _ _ hg
-      simp_rw [Set.image_iUnion]
-      exact MeasurableSet.iUnion hg
-
-lemma MeasurableEmbedding.prod_mk_left {β γ : Type*} [MeasurableSingletonClass α]
-    {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ}
-    (x : α) {f : γ → β} (hf : MeasurableEmbedding f) :
-    MeasurableEmbedding (fun y ↦ (x, f y)) where
-  injective := by
-    intro y y'
-    simp only [Prod.mk.injEq, true_and]
-    exact fun h ↦ hf.injective h
-  measurable := Measurable.prod_mk measurable_const hf.measurable
-  measurableSet_image' := by
-    intro s hs
-    convert (MeasurableSet.singleton x).prod (hf.measurableSet_image.mpr hs)
-    ext x
-    simp
-
-lemma measurableEmbedding_prod_mk_left [MeasurableSingletonClass α] (x : α) :
-    MeasurableEmbedding (Prod.mk x : β → α × β) :=
-  MeasurableEmbedding.prod_mk_left x MeasurableEmbedding.id
-
-lemma MeasurableEmbedding.prod_mk_right {β γ : Type*} [MeasurableSingletonClass α]
-    {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ}
-    {f : γ → β} (hf : MeasurableEmbedding f) (x : α) :
-    MeasurableEmbedding (fun y ↦ (f y, x)) where
-  injective := by
-    intro y y'
-    simp only [Prod.mk.injEq, and_true]
-    exact fun h ↦ hf.injective h
-  measurable := Measurable.prod_mk hf.measurable measurable_const
-  measurableSet_image' := by
-    intro s hs
-    convert (hf.measurableSet_image.mpr hs).prod (MeasurableSet.singleton x)
-    ext x
-    simp
-
-lemma measurableEmbedding_prod_mk_right [MeasurableSingletonClass α] (x : α) :
-    MeasurableEmbedding (fun y ↦ (y, x) : β → β × α) :=
-  MeasurableEmbedding.prod_mk_right MeasurableEmbedding.id x
-
 /-- The Lebesgue integral is measurable. This shows that the integrand of (the right-hand-side of)
   Tonelli's theorem is measurable. -/
 theorem Measurable.lintegral_prod_right' [SFinite ν] :
diff --git a/Mathlib/MeasureTheory/PiSystem.lean b/Mathlib/MeasureTheory/PiSystem.lean
index fdcbf376f1d77..2f16137420ef0 100644
--- a/Mathlib/MeasureTheory/PiSystem.lean
+++ b/Mathlib/MeasureTheory/PiSystem.lean
@@ -58,10 +58,12 @@ open MeasurableSpace Set
 
 open MeasureTheory
 
+variable {α β : Type*}
+
 /-- A π-system is a collection of subsets of `α` that is closed under binary intersection of
   non-disjoint sets. Usually it is also required that the collection is nonempty, but we don't do
   that here. -/
-def IsPiSystem {α} (C : Set (Set α)) : Prop :=
+def IsPiSystem (C : Set (Set α)) : Prop :=
   ∀ᵉ (s ∈ C) (t ∈ C), (s ∩ t : Set α).Nonempty → s ∩ t ∈ C
 
 namespace MeasurableSpace
@@ -71,12 +73,12 @@ theorem isPiSystem_measurableSet {α : Type*} [MeasurableSpace α] :
 
 end MeasurableSpace
 
-theorem IsPiSystem.singleton {α} (S : Set α) : IsPiSystem ({S} : Set (Set α)) := by
+theorem IsPiSystem.singleton (S : Set α) : IsPiSystem ({S} : Set (Set α)) := by
   intro s h_s t h_t _
   rw [Set.mem_singleton_iff.1 h_s, Set.mem_singleton_iff.1 h_t, Set.inter_self,
     Set.mem_singleton_iff]
 
-theorem IsPiSystem.insert_empty {α} {S : Set (Set α)} (h_pi : IsPiSystem S) :
+theorem IsPiSystem.insert_empty {S : Set (Set α)} (h_pi : IsPiSystem S) :
     IsPiSystem (insert ∅ S) := by
   intro s hs t ht hst
   cases' hs with hs hs
@@ -85,7 +87,7 @@ theorem IsPiSystem.insert_empty {α} {S : Set (Set α)} (h_pi : IsPiSystem S) :
     · simp [ht]
     · exact Set.mem_insert_of_mem _ (h_pi s hs t ht hst)
 
-theorem IsPiSystem.insert_univ {α} {S : Set (Set α)} (h_pi : IsPiSystem S) :
+theorem IsPiSystem.insert_univ {S : Set (Set α)} (h_pi : IsPiSystem S) :
     IsPiSystem (insert Set.univ S) := by
   intro s hs t ht hst
   cases' hs with hs hs
@@ -114,9 +116,16 @@ theorem isPiSystem_iUnion_of_monotone {α ι} [SemilatticeSup ι] (p : ι → Se
     (hp_pi : ∀ n, IsPiSystem (p n)) (hp_mono : Monotone p) : IsPiSystem (⋃ n, p n) :=
   isPiSystem_iUnion_of_directed_le p hp_pi (Monotone.directed_le hp_mono)
 
+/-- Rectangles formed by π-systems form a π-system. -/
+lemma IsPiSystem.prod {C : Set (Set α)} {D : Set (Set β)} (hC : IsPiSystem C) (hD : IsPiSystem D) :
+    IsPiSystem (image2 (· ×ˢ ·) C D) := by
+  rintro _ ⟨s₁, hs₁, t₁, ht₁, rfl⟩ _ ⟨s₂, hs₂, t₂, ht₂, rfl⟩ hst
+  rw [prod_inter_prod] at hst ⊢; rw [prod_nonempty_iff] at hst
+  exact mem_image2_of_mem (hC _ hs₁ _ hs₂ hst.1) (hD _ ht₁ _ ht₂ hst.2)
+
 section Order
 
-variable {α : Type*} {ι ι' : Sort*} [LinearOrder α]
+variable {ι ι' : Sort*} [LinearOrder α]
 
 theorem isPiSystem_image_Iio (s : Set α) : IsPiSystem (Iio '' s) := by
   rintro _ ⟨a, ha, rfl⟩ _ ⟨b, hb, rfl⟩ -
@@ -194,45 +203,45 @@ end Order
 
 /-- Given a collection `S` of subsets of `α`, then `generatePiSystem S` is the smallest
 π-system containing `S`. -/
-inductive generatePiSystem {α} (S : Set (Set α)) : Set (Set α)
+inductive generatePiSystem (S : Set (Set α)) : Set (Set α)
   | base {s : Set α} (h_s : s ∈ S) : generatePiSystem S s
   | inter {s t : Set α} (h_s : generatePiSystem S s) (h_t : generatePiSystem S t)
     (h_nonempty : (s ∩ t).Nonempty) : generatePiSystem S (s ∩ t)
 
-theorem isPiSystem_generatePiSystem {α} (S : Set (Set α)) : IsPiSystem (generatePiSystem S) :=
+theorem isPiSystem_generatePiSystem (S : Set (Set α)) : IsPiSystem (generatePiSystem S) :=
   fun _ h_s _ h_t h_nonempty => generatePiSystem.inter h_s h_t h_nonempty
 
-theorem subset_generatePiSystem_self {α} (S : Set (Set α)) : S ⊆ generatePiSystem S := fun _ =>
+theorem subset_generatePiSystem_self (S : Set (Set α)) : S ⊆ generatePiSystem S := fun _ =>
   generatePiSystem.base
 
-theorem generatePiSystem_subset_self {α} {S : Set (Set α)} (h_S : IsPiSystem S) :
+theorem generatePiSystem_subset_self {S : Set (Set α)} (h_S : IsPiSystem S) :
     generatePiSystem S ⊆ S := fun x h => by
   induction h with
   | base h_s => exact h_s
   | inter _ _ h_nonempty h_s h_u => exact h_S _ h_s _ h_u h_nonempty
 
-theorem generatePiSystem_eq {α} {S : Set (Set α)} (h_pi : IsPiSystem S) : generatePiSystem S = S :=
+theorem generatePiSystem_eq {S : Set (Set α)} (h_pi : IsPiSystem S) : generatePiSystem S = S :=
   Set.Subset.antisymm (generatePiSystem_subset_self h_pi) (subset_generatePiSystem_self S)
 
-theorem generatePiSystem_mono {α} {S T : Set (Set α)} (hST : S ⊆ T) :
+theorem generatePiSystem_mono {S T : Set (Set α)} (hST : S ⊆ T) :
     generatePiSystem S ⊆ generatePiSystem T := fun t ht => by
   induction ht with
   | base h_s => exact generatePiSystem.base (Set.mem_of_subset_of_mem hST h_s)
   | inter _ _ h_nonempty h_s h_u => exact isPiSystem_generatePiSystem T _ h_s _ h_u h_nonempty
 
-theorem generatePiSystem_measurableSet {α} [M : MeasurableSpace α] {S : Set (Set α)}
+theorem generatePiSystem_measurableSet [M : MeasurableSpace α] {S : Set (Set α)}
     (h_meas_S : ∀ s ∈ S, MeasurableSet s) (t : Set α) (h_in_pi : t ∈ generatePiSystem S) :
     MeasurableSet t := by
   induction h_in_pi with
   | base h_s => apply h_meas_S _ h_s
   | inter _ _ _ h_s h_u => apply MeasurableSet.inter h_s h_u
 
-theorem generateFrom_measurableSet_of_generatePiSystem {α} {g : Set (Set α)} (t : Set α)
+theorem generateFrom_measurableSet_of_generatePiSystem {g : Set (Set α)} (t : Set α)
     (ht : t ∈ generatePiSystem g) : MeasurableSet[generateFrom g] t :=
   @generatePiSystem_measurableSet α (generateFrom g) g
     (fun _ h_s_in_g => measurableSet_generateFrom h_s_in_g) t ht
 
-theorem generateFrom_generatePiSystem_eq {α} {g : Set (Set α)} :
+theorem generateFrom_generatePiSystem_eq {g : Set (Set α)} :
     generateFrom (generatePiSystem g) = generateFrom g := by
   apply le_antisymm <;> apply generateFrom_le
   · exact fun t h_t => generateFrom_measurableSet_of_generatePiSystem t h_t
@@ -535,7 +544,7 @@ theorem has_diff {s₁ s₂ : Set α} (h₁ : d.Has s₁) (h₂ : d.Has s₂) (h
 
 instance instLEDynkinSystem : LE (DynkinSystem α) where le m₁ m₂ := m₁.Has ≤ m₂.Has
 
-theorem le_def {α} {a b : DynkinSystem α} : a ≤ b ↔ a.Has ≤ b.Has :=
+theorem le_def {a b : DynkinSystem α} : a ≤ b ↔ a.Has ≤ b.Has :=
   Iff.rfl
 
 instance : PartialOrder (DynkinSystem α) :=