chore: shake some imports (#10341)

leanprover-community · Feb 7, 2024 · c458927 · c458927
1 parent e4d4665
commit c458927
Show file tree

Hide file tree

Showing 9 changed files with 7 additions and 5 deletions.
diff --git a/Mathlib/Analysis/Calculus/SmoothSeries.lean b/Mathlib/Analysis/Calculus/SmoothSeries.lean
@@ -5,8 +5,6 @@ Authors: Sébastien Gouëzel
 -/
 import Mathlib.Analysis.Calculus.ContDiff.Basic
 import Mathlib.Analysis.Calculus.UniformLimitsDeriv
-import Mathlib.Data.Nat.Cast.WithTop
-import Mathlib.RingTheory.Ideal.LocalRing
 import Mathlib.Topology.Algebra.InfiniteSum.Module
 import Mathlib.Analysis.NormedSpace.FunctionSeries
 
@@ -244,7 +242,7 @@ theorem contDiff_tsum (hf : ∀ i, ContDiff 𝕜 N (f i)) (hv : ∀ k : ℕ, (k
       exact h'f _ _ _ hm
   · intro m hm
     have h'm : ((m + 1 : ℕ) : ℕ∞) ≤ N := by
-      simpa only [ENat.coe_add, Nat.cast_withBot, ENat.coe_one] using ENat.add_one_le_of_lt hm
+      simpa only [ENat.coe_add, ENat.coe_one] using ENat.add_one_le_of_lt hm
     rw [iteratedFDeriv_tsum hf hv h'f hm.le]
     have A :
       ∀ n x, HasFDerivAt (iteratedFDeriv 𝕜 m (f n)) (fderiv 𝕜 (iteratedFDeriv 𝕜 m (f n)) x) x :=

diff --git a/Mathlib/Analysis/NormedSpace/Banach.lean b/Mathlib/Analysis/NormedSpace/Banach.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel
 -/
 import Mathlib.Topology.MetricSpace.Baire
+import Mathlib.Analysis.Normed.Group.AddTorsor
 import Mathlib.Analysis.NormedSpace.OperatorNorm
 import Mathlib.Analysis.NormedSpace.AffineIsometry
 

diff --git a/Mathlib/Analysis/NormedSpace/ContinuousAffineMap.lean b/Mathlib/Analysis/NormedSpace/ContinuousAffineMap.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Oliver Nash
 -/
 import Mathlib.Topology.Algebra.ContinuousAffineMap
+import Mathlib.Analysis.Normed.Group.AddTorsor
 import Mathlib.Analysis.NormedSpace.AffineIsometry
 import Mathlib.Analysis.NormedSpace.OperatorNorm
 

diff --git a/Mathlib/Analysis/NormedSpace/FiniteDimension.lean b/Mathlib/Analysis/NormedSpace/FiniteDimension.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel
 -/
 import Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
+import Mathlib.Analysis.Normed.Group.AddTorsor
 import Mathlib.Analysis.NormedSpace.AddTorsor
 import Mathlib.Analysis.NormedSpace.AffineIsometry
 import Mathlib.Analysis.NormedSpace.OperatorNorm

diff --git a/Mathlib/Analysis/Seminorm.lean b/Mathlib/Analysis/Seminorm.lean
@@ -6,7 +6,6 @@ Authors: Jean Lo, Yaël Dillies, Moritz Doll
 import Mathlib.Data.Real.Pointwise
 import Mathlib.Analysis.Convex.Function
 import Mathlib.Analysis.LocallyConvex.Basic
-import Mathlib.Analysis.Normed.Group.AddTorsor
 import Mathlib.Data.Real.Sqrt
 
 #align_import analysis.seminorm from "leanprover-community/mathlib"@"09079525fd01b3dda35e96adaa08d2f943e1648c"

diff --git a/Mathlib/Geometry/Euclidean/Angle/Unoriented/Affine.lean b/Mathlib/Geometry/Euclidean/Angle/Unoriented/Affine.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Myers, Manuel Candales
 -/
 import Mathlib.Analysis.Convex.Between
+import Mathlib.Analysis.Normed.Group.AddTorsor
 import Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
 import Mathlib.Analysis.NormedSpace.AffineIsometry
 

diff --git a/Mathlib/Geometry/Euclidean/Inversion/Basic.lean b/Mathlib/Geometry/Euclidean/Inversion/Basic.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Yury G. Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury G. Kudryashov
 -/
+import Mathlib.Analysis.Normed.Group.AddTorsor
 import Mathlib.Analysis.InnerProductSpace.Basic
 
 #align_import geometry.euclidean.inversion from "leanprover-community/mathlib"@"46b633fd842bef9469441c0209906f6dddd2b4f5"

diff --git a/Mathlib/Geometry/Euclidean/PerpBisector.lean b/Mathlib/Geometry/Euclidean/PerpBisector.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov, Joseph Myers
 -/
 import Mathlib.Analysis.InnerProductSpace.Orthogonal
+import Mathlib.Analysis.Normed.Group.AddTorsor
 
 #align_import geometry.euclidean.basic from "leanprover-community/mathlib"@"2de9c37fa71dde2f1c6feff19876dd6a7b1519f0"
 

diff --git a/Mathlib/MeasureTheory/Integral/BoundedContinuousFunction.lean b/Mathlib/MeasureTheory/Integral/BoundedContinuousFunction.lean
@@ -3,7 +3,6 @@ Copyright (c) 2023 Kalle Kytölä. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kalle Kytölä
 -/
-import Mathlib.Analysis.InnerProductSpace.Basic
 import Mathlib.MeasureTheory.Integral.Bochner
 
 /-!