chore: Split large file MeasureTheory.MeasurableSpace.Basic (#13937)

Mathlib.lean

@@ -3026,6 +3026,8 @@ import Mathlib.MeasureTheory.MeasurableSpace.Basic
 import Mathlib.MeasureTheory.MeasurableSpace.Card
 import Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
 import Mathlib.MeasureTheory.MeasurableSpace.Defs
+import Mathlib.MeasureTheory.MeasurableSpace.Embedding
+import Mathlib.MeasureTheory.MeasurableSpace.Instances
 import Mathlib.MeasureTheory.MeasurableSpace.Invariants
 import Mathlib.MeasureTheory.Measure.AEDisjoint
 import Mathlib.MeasureTheory.Measure.AEMeasurable

Mathlib/MeasureTheory/MeasurableSpace/CountablyGenerated.lean

@@ -3,7 +3,7 @@ Copyright (c) 2023 Felix Weilacher. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Felix Weilacher, Yury G. Kudryashov, Rémy Degenne
 -/
-import Mathlib.MeasureTheory.MeasurableSpace.Basic
+import Mathlib.MeasureTheory.MeasurableSpace.Embedding
 import Mathlib.Data.Set.MemPartition
 import Mathlib.Order.Filter.CountableSeparatingOn
 

Mathlib/MeasureTheory/MeasurableSpace/Instances.lean

@@ -0,0 +1,65 @@
+/-
+Copyright (c) 2017 Johannes Hölzl. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johannes Hölzl, Mario Carneiro
+-/
+import Mathlib.MeasureTheory.MeasurableSpace.Defs
+import Mathlib.Data.Rat.Init
+
+#align_import measure_theory.measurable_space from "leanprover-community/mathlib"@"001ffdc42920050657fd45bd2b8bfbec8eaaeb29"
+
+/-!
+# Measurable-space typeclass instances
+
+This file provides measurable-space instances for a selection of standard countable types,
+in each case defining the Σ-algebra to be `⊤` (the discrete measurable-space structure).
+-/
+
+instance Empty.instMeasurableSpace : MeasurableSpace Empty := ⊤
+#align empty.measurable_space Empty.instMeasurableSpace
+
+instance PUnit.instMeasurableSpace : MeasurableSpace PUnit := ⊤
+#align punit.measurable_space PUnit.instMeasurableSpace
+
+instance Bool.instMeasurableSpace : MeasurableSpace Bool := ⊤
+#align bool.measurable_space Bool.instMeasurableSpace
+
+instance Prop.instMeasurableSpace : MeasurableSpace Prop := ⊤
+#align Prop.measurable_space Prop.instMeasurableSpace
+
+instance Nat.instMeasurableSpace : MeasurableSpace ℕ := ⊤
+#align nat.measurable_space Nat.instMeasurableSpace
+
+instance Fin.instMeasurableSpace (n : ℕ) : MeasurableSpace (Fin n) := ⊤
+
+instance Int.instMeasurableSpace : MeasurableSpace ℤ := ⊤
+#align int.measurable_space Int.instMeasurableSpace
+
+instance Rat.instMeasurableSpace : MeasurableSpace ℚ := ⊤
+#align rat.measurable_space Rat.instMeasurableSpace
+
+instance Subsingleton.measurableSingletonClass {α} [MeasurableSpace α] [Subsingleton α] :
+    MeasurableSingletonClass α := by
+  refine ⟨fun i => ?_⟩
+  convert MeasurableSet.univ
+  simp [Set.eq_univ_iff_forall, eq_iff_true_of_subsingleton]
+#noalign empty.measurable_singleton_class
+#noalign punit.measurable_singleton_class
+
+instance Bool.instMeasurableSingletonClass : MeasurableSingletonClass Bool := ⟨fun _ => trivial⟩
+#align bool.measurable_singleton_class Bool.instMeasurableSingletonClass
+
+instance Prop.instMeasurableSingletonClass : MeasurableSingletonClass Prop := ⟨fun _ => trivial⟩
+#align Prop.measurable_singleton_class Prop.instMeasurableSingletonClass
+
+instance Nat.instMeasurableSingletonClass : MeasurableSingletonClass ℕ := ⟨fun _ => trivial⟩
+#align nat.measurable_singleton_class Nat.instMeasurableSingletonClass
+
+instance Fin.instMeasurableSingletonClass (n : ℕ) : MeasurableSingletonClass (Fin n) :=
+  ⟨fun _ => trivial⟩
+
+instance Int.instMeasurableSingletonClass : MeasurableSingletonClass ℤ := ⟨fun _ => trivial⟩
+#align int.measurable_singleton_class Int.instMeasurableSingletonClass
+
+instance Rat.instMeasurableSingletonClass : MeasurableSingletonClass ℚ := ⟨fun _ => trivial⟩
+#align rat.measurable_singleton_class Rat.instMeasurableSingletonClass

Mathlib/MeasureTheory/Measure/MeasureSpace.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro
 -/
 import Mathlib.MeasureTheory.Measure.NullMeasurable
-import Mathlib.MeasureTheory.MeasurableSpace.Basic
+import Mathlib.MeasureTheory.MeasurableSpace.Embedding
 import Mathlib.Topology.Algebra.Order.LiminfLimsup
 
 #align_import measure_theory.measure.measure_space from "leanprover-community/mathlib"@"343e80208d29d2d15f8050b929aa50fe4ce71b55"

scripts/style-exceptions.txt

@@ -75,7 +75,6 @@ Mathlib/MeasureTheory/Integral/FundThmCalculus.lean : line 1 : ERR_NUM_LIN : 180
 Mathlib/MeasureTheory/Integral/Lebesgue.lean : line 1 : ERR_NUM_LIN : 2200 file contains 2032 lines, try to split it up
 Mathlib/MeasureTheory/Integral/SetIntegral.lean : line 1 : ERR_NUM_LIN : 1900 file contains 1778 lines, try to split it up
 Mathlib/MeasureTheory/Integral/SetToL1.lean : line 1 : ERR_NUM_LIN : 2000 file contains 1815 lines, try to split it up
-Mathlib/MeasureTheory/MeasurableSpace/Basic.lean : line 1 : ERR_NUM_LIN : 2400 file contains 2267 lines, try to split it up
 Mathlib/MeasureTheory/Measure/MeasureSpace.lean : line 1 : ERR_NUM_LIN : 2400 file contains 2243 lines, try to split it up
 Mathlib/MeasureTheory/Measure/Typeclasses.lean : line 1 : ERR_NUM_LIN : 1800 file contains 1619 lines, try to split it up
 Mathlib/Order/Basic.lean : line 1 : ERR_NUM_LIN : 1700 file contains 1556 lines, try to split it up