Reduce imports

nguyenvukhang · nguyenvukhang · commit 28cd77e85a68 · 2025-11-21T11:54:15.000+08:00
diff --git a/Rudin/Lemmas/Globals.lean b/Rudin/Lemmas/Globals.lean
@@ -1,3 +1,5 @@
+import Mathlib.Algebra.BigOperators.Fin
+
 import Rudin.Defs.Globals
 import Rudin.Partition.Interval
 import Rudin.Partition.OrderBot
diff --git a/Rudin/Numbered/Basic.lean b/Rudin/Numbered/Basic.lean
@@ -1,3 +1,6 @@
+import Mathlib.Analysis.Normed.Order.Lattice
+import Mathlib.Analysis.Normed.Ring.Basic
+
 import Rudin.Partition.SpecialPartitions
 import Rudin.Results.Basic
 import Rudin.Results.IsTag
diff --git a/Rudin/Partition/Core/Index.lean b/Rudin/Partition/Core/Index.lean
@@ -1,4 +1,3 @@
-import Rudin.Defs.Partition
 import Rudin.Partition.Core.Endpoints
 import Rudin.Partition.Core.Monotone
 
diff --git a/Rudin/Partition/Core/Length.lean b/Rudin/Partition/Core/Length.lean
@@ -1,5 +1,3 @@
-import Mathlib.Data.Finset.Card
-
 import Rudin.Defs.Partition
 
 namespace Rudin
diff --git a/Rudin/Partition/Core/Monotone.lean b/Rudin/Partition/Core/Monotone.lean
@@ -1,4 +1,4 @@
-import Rudin.Partition.Core.Length
+import Rudin.Defs.Partition
 
 namespace Rudin
 
diff --git a/Rudin/Partition/Cover.lean b/Rudin/Partition/Cover.lean
@@ -1,6 +1,7 @@
 import Mathlib.Data.Set.Lattice
 import Mathlib.Order.Interval.Set.LinearOrder
 
+import Rudin.Partition.Core
 import Rudin.Partition.Endpoints
 
 namespace Rudin
diff --git a/Rudin/Partition/Endpoints.lean b/Rudin/Partition/Endpoints.lean
@@ -1,4 +1,4 @@
-import Rudin.Partition.Core
+import Rudin.Partition.Core.Index
 import Rudin.Partition.Monotone
 
 namespace Rudin
diff --git a/Rudin/Partition/Extend.lean b/Rudin/Partition/Extend.lean
@@ -1,8 +1,3 @@
-import Mathlib.Data.Set.Lattice
-import Mathlib.Order.Interval.Set.LinearOrder
-
-import Rudin.Partition.Endpoints
-import Rudin.Partition.Prelude
 import Rudin.Partition.OrderBot
 import Rudin.Partition.Insert
 
diff --git a/Rudin/Partition/Globals.lean b/Rudin/Partition/Globals.lean
@@ -1,3 +1,6 @@
+import Mathlib.Algebra.BigOperators.Intervals
+import Mathlib.Algebra.Order.BigOperators.Group.Finset
+
 import Rudin.Alpha.Basic
 import Rudin.Partition.Extend
 import Rudin.Partition.Union
diff --git a/Rudin/Partition/Insert.lean b/Rudin/Partition/Insert.lean
@@ -1,9 +1,6 @@
-import Mathlib.Data.Set.Lattice
-import Mathlib.Order.Interval.Set.LinearOrder
-
-import Rudin.Partition.Endpoints
 import Rudin.Partition.Prelude
-import Rudin.Partition.OrderBot
+import Rudin.Partition.Core.Length
+import Rudin.Partition.Endpoints
 
 namespace Rudin
 
diff --git a/Rudin/Partition/Interval.lean b/Rudin/Partition/Interval.lean
@@ -1,4 +1,5 @@
 import Rudin.Partition.Endpoints
+import Rudin.Partition.Core
 import Rudin.Prelude
 
 open Set
diff --git a/Rudin/Partition/OrderBot.lean b/Rudin/Partition/OrderBot.lean
@@ -1,5 +1,5 @@
 import Rudin.Partition.Endpoints
-import Mathlib.Tactic
+import Rudin.Partition.Core
 
 namespace Rudin
 
diff --git a/Rudin/Prelude/BddOn.lean b/Rudin/Prelude/BddOn.lean
@@ -1,8 +1,6 @@
 /-
 This file introduces BddOn, which is BddAbove ∧ BddBelow
 -/
-import Mathlib.Data.Real.Basic
-import Mathlib.Order.ConditionallyCompleteLattice.Defs
 import Mathlib.Data.Real.Archimedean
 
 universe u v
@@ -218,7 +216,7 @@ theorem BddOn.sInf_le_sSup (s : BddOn f A) : sInf (f '' A) ≤ sSup (f '' A)
 
 end RealValuedFunctions
 --------------------------------------------------------------------------------
-section ConditionallyCompleteLattice_lemmas
+section ConditionallyCompleteLattice
 
 variable [ConditionallyCompleteLattice R] {x : β}
 
@@ -250,7 +248,7 @@ theorem BddOn.csInf_le_csSup (s : BddOn f A) (hA : A.Nonempty) : sInf (f '' A) 
   := by --
   exact _root_.csInf_le_csSup s.below' s.above' (hA.image f) -- ∎
 
-end ConditionallyCompleteLattice_lemmas
+end ConditionallyCompleteLattice
 --------------------------------------------------------------------------------
 class Bdd [LE R] (f : β → R) : Prop where
   univ' : BddOn f Set.univ
diff --git a/Rudin/Prelude/Finset.lean b/Rudin/Prelude/Finset.lean
@@ -1,9 +1,6 @@
 import Mathlib.Data.Fintype.BigOperators
-import Mathlib.Algebra.BigOperators.Group.Finset.Basic
-import Mathlib.Algebra.BigOperators.Intervals
 import Mathlib.Data.Real.Basic
 import Mathlib.Order.Interval.Finset.Nat
-import Mathlib.Algebra.BigOperators.Group.Finset.Basic
 
 theorem Finset.sum_fin {f : ℕ → ℝ} {n : ℕ} : ∑ i : Fin n, f i = ∑ i < n, f i
   := by --
diff --git a/fmt/src/error.rs b/fmt/src/error.rs
@@ -7,7 +7,7 @@ use std::path::PathBuf;
 pub enum LineError {
     #[error("If the line contains \"{}\", then it must start with \"{}\".", .0, .0)]
     StartsWith(String),
-    #[error("Leave a space between `Mathlib` imports and `Dino` imports.")]
+    #[error("Leave a space between `Mathlib` imports and `Rudin` imports.")]
     LeaveSpace,
 }
 
diff --git a/fmt/src/fmt.rs b/fmt/src/fmt.rs
@@ -42,7 +42,7 @@ pub fn space_between_import_libraries(path: &Path, text: &str) -> Result<()> {
             continue;
         }
         let Some(pidx) = last_mathlib else { continue };
-        let bad = line.starts_with("Dino") && pidx + 1 == line_idx;
+        let bad = line.starts_with("Rudin") && pidx + 1 == line_idx;
         if bad {
             return Err(Error::Content {
                 filepath: path.to_path_buf(),

Original file line number	Diff line number	Diff line change
`@@ -1,3 +1,5 @@`
	`1`	`+import Mathlib.Algebra.BigOperators.Fin`
	`2`	`+`
`1`	`3`	`import Rudin.Defs.Globals`
`2`	`4`	`import Rudin.Partition.Interval`
`3`	`5`	`import Rudin.Partition.OrderBot`
Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,3 @@`
`1`		`-import Rudin.Defs.Partition`
`2`	`1`	`import Rudin.Partition.Core.Endpoints`
`3`	`2`	`import Rudin.Partition.Core.Monotone`
`4`	`3`
Original file line number	Diff line number	Diff line change
`@@ -1,5 +1,3 @@`
`1`		`-import Mathlib.Data.Finset.Card`
`2`		`-`
`3`	`1`	`import Rudin.Defs.Partition`
`4`	`2`
`5`	`3`	`namespace Rudin`
Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-import Rudin.Partition.Core.Length`
	`1`	`+import Rudin.Defs.Partition`
`2`	`2`
`3`	`3`	`namespace Rudin`
`4`	`4`
Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-import Rudin.Partition.Core`
	`1`	`+import Rudin.Partition.Core.Index`
`2`	`2`	`import Rudin.Partition.Monotone`
`3`	`3`
`4`	`4`	`namespace Rudin`