From 3f801100847524b0306727966a19313d5dc58738 Mon Sep 17 00:00:00 2001
From: Moritz Firsching <moritz.firsching@gmail.com>
Date: Wed, 27 Mar 2024 13:47:10 +0000
Subject: [PATCH] chore(Probability/Kernel/CondCdf): cleanup (#10635)

- [x] depends on: #10298


Co-authored-by: Moritz Firsching <firsching@google.com>
---
 Mathlib/Data/Real/Archimedean.lean      | 26 ++++++++++++++++++++++---
 Mathlib/Probability/Kernel/CondCdf.lean | 19 ------------------
 2 files changed, 23 insertions(+), 22 deletions(-)

diff --git a/Mathlib/Data/Real/Archimedean.lean b/Mathlib/Data/Real/Archimedean.lean
index 49b01160dda9d..3b114dc9a7f72 100644
--- a/Mathlib/Data/Real/Archimedean.lean
+++ b/Mathlib/Data/Real/Archimedean.lean
@@ -3,10 +3,10 @@ Copyright (c) 2018 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Floris van Doorn
 -/
-import Mathlib.Data.Real.Basic
-import Mathlib.Data.Set.Image
-import Mathlib.Algebra.Order.Archimedean
 import Mathlib.Algebra.Bounds
+import Mathlib.Algebra.Order.Archimedean
+import Mathlib.Data.Real.Basic
+import Mathlib.Data.Set.Intervals.Disjoint
 
 #align_import data.real.basic from "leanprover-community/mathlib"@"cb42593171ba005beaaf4549fcfe0dece9ada4c9"
 
@@ -346,4 +346,24 @@ theorem iInf_Ioi_eq_iInf_rat_gt {f : ℝ → ℝ} (x : ℝ) (hf : BddBelow (f ''
       norm_cast
 #align infi_Ioi_eq_infi_rat_gt Real.iInf_Ioi_eq_iInf_rat_gt
 
+theorem not_bddAbove_coe : ¬ (BddAbove <| range (fun (x : ℚ) ↦ (x : ℝ))) := by
+  dsimp only [BddAbove, upperBounds]
+  rw [Set.not_nonempty_iff_eq_empty]
+  ext
+  simpa using exists_rat_gt _
+
+theorem not_bddBelow_coe : ¬ (BddBelow <| range (fun (x : ℚ) ↦ (x : ℝ))) := by
+  dsimp only [BddBelow, lowerBounds]
+  rw [Set.not_nonempty_iff_eq_empty]
+  ext
+  simpa using exists_rat_lt _
+
+theorem iUnion_Iic_rat : ⋃ r : ℚ, Iic (r : ℝ) = univ := by
+  exact iUnion_Iic_of_not_bddAbove_range not_bddAbove_coe
+#align real.Union_Iic_rat Real.iUnion_Iic_rat
+
+theorem iInter_Iic_rat : ⋂ r : ℚ, Iic (r : ℝ) = ∅ := by
+  exact iInter_Iic_eq_empty_iff.mpr not_bddBelow_coe
+#align real.Inter_Iic_rat Real.iInter_Iic_rat
+
 end Real
diff --git a/Mathlib/Probability/Kernel/CondCdf.lean b/Mathlib/Probability/Kernel/CondCdf.lean
index d436ec493f77d..4a25e2c24b9ef 100644
--- a/Mathlib/Probability/Kernel/CondCdf.lean
+++ b/Mathlib/Probability/Kernel/CondCdf.lean
@@ -49,25 +49,6 @@ open MeasureTheory Set Filter TopologicalSpace
 
 open scoped NNReal ENNReal MeasureTheory Topology
 
-section AuxLemmasToBeMoved
-
-variable {α β ι : Type*}
-
-theorem Real.iUnion_Iic_rat : ⋃ r : ℚ, Iic (r : ℝ) = univ := by
-  ext1 x
-  simp only [mem_iUnion, mem_Iic, mem_univ, iff_true_iff]
-  obtain ⟨r, hr⟩ := exists_rat_gt x
-  exact ⟨r, hr.le⟩
-#align real.Union_Iic_rat Real.iUnion_Iic_rat
-
-theorem Real.iInter_Iic_rat : ⋂ r : ℚ, Iic (r : ℝ) = ∅ := by
-  ext1 x
-  simp only [mem_iInter, mem_Iic, mem_empty_iff_false, iff_false_iff, not_forall, not_le]
-  exact exists_rat_lt x
-#align real.Inter_Iic_rat Real.iInter_Iic_rat
-
-end AuxLemmasToBeMoved
-
 namespace MeasureTheory.Measure
 
 variable {α β : Type*} {mα : MeasurableSpace α} (ρ : Measure (α × ℝ))