From 0c023c1a56fe0723b2f74bc52a2157b8fa6a05fb Mon Sep 17 00:00:00 2001
From: Moritz Firsching <firsching@google.com>
Date: Fri, 26 Jan 2024 11:01:02 -0800
Subject: [PATCH] chore(Probability/Kernel/CondCdf): mv prod_iInter

---
 Mathlib/Data/Set/Lattice.lean           | 7 +++++++
 Mathlib/Probability/Kernel/CondCdf.lean | 9 +--------
 2 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/Mathlib/Data/Set/Lattice.lean b/Mathlib/Data/Set/Lattice.lean
index aefaa1c698564..13eda132f416c 100644
--- a/Mathlib/Data/Set/Lattice.lean
+++ b/Mathlib/Data/Set/Lattice.lean
@@ -1989,6 +1989,13 @@ theorem prod_sInter {T : Set (Set β)} (hT : T.Nonempty) (s : Set α) :
   simp_rw [singleton_prod, mem_image, iInter_exists, biInter_and', iInter_iInter_eq_right]
 #align set.prod_sInter Set.prod_sInter
 
+theorem prod_iInter {s : Set α} {t : ι → Set β} [hι : Nonempty ι] :
+    (s ×ˢ ⋂ i, t i) = ⋂ i, s ×ˢ t i := by
+  ext x
+  simp only [mem_prod, mem_iInter]
+  exact ⟨fun h i => ⟨h.1, h.2 i⟩, fun h => ⟨(h hι.some).1, fun i => (h i).2⟩⟩
+#align prod_Inter Set.prod_iInter
+
 end Prod
 
 section Image2
diff --git a/Mathlib/Probability/Kernel/CondCdf.lean b/Mathlib/Probability/Kernel/CondCdf.lean
index 2d223aba3e6ac..49eaad73a699e 100644
--- a/Mathlib/Probability/Kernel/CondCdf.lean
+++ b/Mathlib/Probability/Kernel/CondCdf.lean
@@ -3,6 +3,7 @@ Copyright (c) 2023 Rémy Degenne. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Rémy Degenne
 -/
+import Mathlib.Data.Set.Lattice
 import Mathlib.MeasureTheory.Measure.Stieltjes
 import Mathlib.MeasureTheory.Decomposition.RadonNikodym
 import Mathlib.MeasureTheory.Constructions.Prod.Basic
@@ -66,14 +67,6 @@ theorem sequence_le (a : α) : f (hf.sequence f (Encodable.encode a + 1)) ≤ f
 
 end Directed
 
--- todo: move to data/set/lattice next to prod_sUnion or prod_sInter
-theorem prod_iInter {s : Set α} {t : ι → Set β} [hι : Nonempty ι] :
-    (s ×ˢ ⋂ i, t i) = ⋂ i, s ×ˢ t i := by
-  ext x
-  simp only [mem_prod, mem_iInter]
-  exact ⟨fun h i => ⟨h.1, h.2 i⟩, fun h => ⟨(h hι.some).1, fun i => (h i).2⟩⟩
-#align prod_Inter prod_iInter
-
 theorem Real.iUnion_Iic_rat : ⋃ r : ℚ, Iic (r : ℝ) = univ := by
   ext1 x
   simp only [mem_iUnion, mem_Iic, mem_univ, iff_true_iff]