From b772cd7ab2a09530e2e1b80ec58481497ef2645d Mon Sep 17 00:00:00 2001
From: Alvan Caleb Arulandu <calebarulandu@gmail.com>
Date: Thu, 10 Oct 2024 11:32:51 -0400
Subject: [PATCH] move to rclike section

---
 .../MeasureTheory/Integral/IntegrableOn.lean  | 48 ++++++++++---------
 1 file changed, 25 insertions(+), 23 deletions(-)

diff --git a/Mathlib/MeasureTheory/Integral/IntegrableOn.lean b/Mathlib/MeasureTheory/Integral/IntegrableOn.lean
index d48186e7ac4e6..2def8a063c89f 100644
--- a/Mathlib/MeasureTheory/Integral/IntegrableOn.lean
+++ b/Mathlib/MeasureTheory/Integral/IntegrableOn.lean
@@ -338,6 +338,31 @@ theorem IntegrableOn.setLIntegral_lt_top {f : α → ℝ} {s : Set α} (hf : Int
 @[deprecated (since := "2024-06-29")]
 alias IntegrableOn.set_lintegral_lt_top := IntegrableOn.setLIntegral_lt_top
 
+section RCLike
+
+variable {𝕜 : Type*} [RCLike 𝕜]
+
+theorem IntegrableOn.iff_ofReal {f : α → ℝ} :
+    IntegrableOn f s μ ↔ IntegrableOn (fun x ↦ (f x : ℂ)) s μ :=
+  MeasureTheory.Integrable.iff_ofReal
+
+theorem IntegrableOn.ofReal {f : α → ℝ} (hf : IntegrableOn f s μ) :
+    IntegrableOn (fun x => (f x : 𝕜)) s μ := by
+  rw [IntegrableOn, ← memℒp_one_iff_integrable] at hf ⊢
+  exact hf.ofReal
+
+theorem IntegrableOn.re_im_iff {f : α → 𝕜} :
+    IntegrableOn (fun x => RCLike.re (f x)) s μ ∧ IntegrableOn (fun x => RCLike.im (f x)) s μ ↔
+    IntegrableOn f s μ := Integrable.re_im_iff (f := f)
+
+theorem IntegrableOn.re {f : α → 𝕜} (hf : IntegrableOn f s μ) :
+    IntegrableOn (fun x => RCLike.re (f x)) s μ := (IntegrableOn.re_im_iff.2 hf).left
+
+theorem IntegrableOn.im {f : α → 𝕜} (hf : IntegrableOn f s μ) :
+    IntegrableOn (fun x => RCLike.im (f x)) s μ := (IntegrableOn.re_im_iff.2 hf).right
+
+end RCLike
+
 /-- We say that a function `f` is *integrable at filter* `l` if it is integrable on some
 set `s ∈ l`. Equivalently, it is eventually integrable on `s` in `l.smallSets`. -/
 def IntegrableAtFilter (f : α → E) (l : Filter α) (μ : Measure α := by volume_tac) :=
@@ -695,26 +720,3 @@ theorem integrableOn_Iic_iff_integrableOn_Iio :
   integrableOn_Iic_iff_integrableOn_Iio' (by rw [measure_singleton]; exact ENNReal.zero_ne_top)
 
 end PartialOrder
-
-namespace MeasureTheory
-variable {X : Type*} [MeasurableSpace X] {𝕜 : Type*} [RCLike 𝕜] {μ : Measure X} {s : Set X}
-theorem IntegrableOn.iff_ofReal {f : X → ℝ} :
-    IntegrableOn f s μ ↔ IntegrableOn (fun x ↦ (f x : ℂ)) s μ :=
-  MeasureTheory.Integrable.iff_ofReal
-
-theorem IntegrableOn.ofReal {f : X → ℝ} (hf : IntegrableOn f s μ) :
-    IntegrableOn (fun x => (f x : 𝕜)) s μ := by
-  rw [IntegrableOn, ← memℒp_one_iff_integrable] at hf ⊢
-  exact hf.ofReal
-
-theorem IntegrableOn.re_im_iff {f : X → 𝕜} :
-    IntegrableOn (fun x => RCLike.re (f x)) s μ ∧ IntegrableOn (fun x => RCLike.im (f x)) s μ ↔
-    IntegrableOn f s μ := Integrable.re_im_iff (f := f)
-
-theorem IntegrableOn.re {f : X → 𝕜} (hf : IntegrableOn f s μ) :
-    IntegrableOn (fun x => RCLike.re (f x)) s μ := (IntegrableOn.re_im_iff.2 hf).left
-
-theorem IntegrableOn.im {f : X → 𝕜} (hf : IntegrableOn f s μ) :
-    IntegrableOn (fun x => RCLike.im (f x)) s μ := (IntegrableOn.re_im_iff.2 hf).right
-
-end MeasureTheory