chore: remove some superfluous imports (#31616)

qawbecrdtey · qawbecrdtey · commit 7e683ccc91c6 · 2025-11-14T16:11:43.000Z
diff --git a/Mathlib/Algebra/Group/Basic.lean b/Mathlib/Algebra/Group/Basic.lean
@@ -8,7 +8,6 @@ import Mathlib.Algebra.Group.Defs
 import Mathlib.Data.Int.Init
 import Mathlib.Logic.Function.Iterate
 import Mathlib.Tactic.SimpRw
-import Mathlib.Tactic.SplitIfs
 
 /-!
 # Basic lemmas about semigroups, monoids, and groups
diff --git a/Mathlib/Algebra/Group/Center.lean b/Mathlib/Algebra/Group/Center.lean
@@ -3,11 +3,9 @@ Copyright (c) 2021 Eric Wieser. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser, Jireh Loreaux
 -/
-import Mathlib.Algebra.Group.Commute.Units
 import Mathlib.Algebra.Group.Invertible.Basic
-import Mathlib.Logic.Basic
-import Mathlib.Data.Set.Basic
 import Mathlib.Algebra.Notation.Prod
+import Mathlib.Data.Set.Basic
 
 /-!
 # Centers of magmas and semigroups
diff --git a/Mathlib/Algebra/Group/Defs.lean b/Mathlib/Algebra/Group/Defs.lean
@@ -8,7 +8,6 @@ import Mathlib.Algebra.Notation.Defs
 import Mathlib.Algebra.Regular.Defs
 import Mathlib.Data.Int.Notation
 import Mathlib.Data.Nat.BinaryRec
-import Mathlib.Logic.Function.Defs
 import Mathlib.Tactic.MkIffOfInductiveProp
 import Mathlib.Tactic.OfNat
 import Mathlib.Tactic.Basic
diff --git a/Mathlib/Algebra/Group/Finsupp.lean b/Mathlib/Algebra/Group/Finsupp.lean
@@ -7,7 +7,6 @@ import Mathlib.Algebra.Group.Equiv.Defs
 import Mathlib.Algebra.Group.Pi.Lemmas
 import Mathlib.Data.Finset.Max
 import Mathlib.Data.Finsupp.Single
-import Mathlib.Tactic.FastInstance
 
 /-!
 # Additive monoid structure on `ι →₀ M`
diff --git a/Mathlib/Algebra/Group/Nat/Hom.lean b/Mathlib/Algebra/Group/Nat/Hom.lean
@@ -3,8 +3,6 @@ Copyright (c) 2020 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
-import Mathlib.Algebra.Group.Equiv.Defs
-import Mathlib.Algebra.Group.Hom.Basic
 import Mathlib.Algebra.Group.Nat.Defs
 import Mathlib.Algebra.Group.TypeTags.Hom
 import Mathlib.Tactic.Spread
diff --git a/Mathlib/Algebra/GroupWithZero/Defs.lean b/Mathlib/Algebra/GroupWithZero/Defs.lean
@@ -5,7 +5,6 @@ Authors: Johan Commelin
 -/
 import Mathlib.Algebra.Group.Defs
 import Mathlib.Logic.Nontrivial.Defs
-import Mathlib.Tactic.SplitIfs
 import Mathlib.Logic.Basic
 
 /-!
diff --git a/Mathlib/Algebra/Opposites.lean b/Mathlib/Algebra/Opposites.lean
@@ -6,7 +6,6 @@ Authors: Kenny Lau
 import Mathlib.Algebra.Group.Defs
 import Mathlib.Logic.Equiv.Defs
 import Mathlib.Logic.Nontrivial.Basic
-import Mathlib.Logic.IsEmpty
 
 /-!
 # Multiplicative opposite and algebraic operations on it
diff --git a/Mathlib/Algebra/Order/GroupWithZero/Canonical.lean b/Mathlib/Algebra/Order/GroupWithZero/Canonical.lean
@@ -14,6 +14,7 @@ import Mathlib.Algebra.Order.Monoid.Basic
 import Mathlib.Algebra.Order.Monoid.OrderDual
 import Mathlib.Algebra.Order.Monoid.TypeTags
 import Mathlib.Algebra.Group.WithOne.Map
+import Mathlib.Tactic.Tauto
 
 /-!
 # Linearly ordered commutative groups and monoids with a zero element adjoined
diff --git a/Mathlib/Algebra/Order/Quantale.lean b/Mathlib/Algebra/Order/Quantale.lean
@@ -3,7 +3,6 @@ Copyright (c) 2024 Pieter Cuijpers. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Pieter Cuijpers
 -/
-import Mathlib.Algebra.Group.Defs
 import Mathlib.Algebra.Order.Monoid.Unbundled.Basic
 import Mathlib.Order.CompleteLattice.Basic
 import Mathlib.Tactic.Variable
diff --git a/Mathlib/Algebra/PEmptyInstances.lean b/Mathlib/Algebra/PEmptyInstances.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Julian Kuelshammer
 -/
 import Mathlib.Algebra.Group.Defs
-import Mathlib.Tactic.ToAdditive
 
 /-!
 # Instances on pempty
diff --git a/Mathlib/Algebra/Ring/Defs.lean b/Mathlib/Algebra/Ring/Defs.lean
@@ -3,11 +3,9 @@ Copyright (c) 2014 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Yury Kudryashov, Neil Strickland
 -/
-import Mathlib.Algebra.Group.Defs
 import Mathlib.Algebra.GroupWithZero.Defs
 import Mathlib.Data.Int.Cast.Defs
 import Mathlib.Tactic.Spread
-import Mathlib.Util.AssertExists
 import Mathlib.Tactic.StacksAttribute
 
 /-!
diff --git a/Mathlib/Algebra/Ring/Equiv.lean b/Mathlib/Algebra/Ring/Equiv.lean
@@ -6,9 +6,9 @@ Authors: Johannes Hölzl, Callum Sutton, Yury Kudryashov
 import Mathlib.Algebra.Group.Equiv.Opposite
 import Mathlib.Algebra.GroupWithZero.Equiv
 import Mathlib.Algebra.GroupWithZero.InjSurj
+import Mathlib.Algebra.Notation.Prod
 import Mathlib.Algebra.Ring.Hom.Defs
 import Mathlib.Logic.Equiv.Set
-import Mathlib.Algebra.Notation.Prod
 
 /-!
 # (Semi)ring equivs
diff --git a/Mathlib/Control/Basic.lean b/Mathlib/Control/Basic.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl
 -/
 import Mathlib.Control.Combinators
-import Mathlib.Logic.Function.Defs
 import Mathlib.Tactic.CasesM
 import Mathlib.Tactic.Attr.Core
 
diff --git a/Mathlib/Data/Int/Basic.lean b/Mathlib/Data/Int/Basic.lean
@@ -6,6 +6,7 @@ Authors: Jeremy Avigad
 import Mathlib.Data.Int.Init
 import Mathlib.Data.Nat.Basic
 import Mathlib.Logic.Nontrivial.Defs
+import Mathlib.Tactic.Conv
 import Mathlib.Tactic.Convert
 import Mathlib.Tactic.Lift
 import Mathlib.Tactic.OfNat
diff --git a/Mathlib/Data/Nat/Basic.lean b/Mathlib/Data/Nat/Basic.lean
@@ -4,10 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn, Leonardo de Moura, Jeremy Avigad, Mario Carneiro
 -/
 import Mathlib.Data.Nat.Init
-import Mathlib.Data.Set.Defs
+import Mathlib.Logic.Basic
 import Mathlib.Logic.Nontrivial.Defs
 import Mathlib.Order.Defs.LinearOrder
-import Mathlib.Tactic.Contrapose
 import Mathlib.Tactic.GCongr.Core
 import Mathlib.Util.AssertExists
 
diff --git a/Mathlib/Data/Nat/Cast/Defs.lean b/Mathlib/Data/Nat/Cast/Defs.lean
@@ -6,7 +6,6 @@ Authors: Mario Carneiro, Gabriel Ebner
 import Mathlib.Algebra.Group.Defs
 import Mathlib.Data.Nat.Init
 import Mathlib.Tactic.SplitIfs
-import Mathlib.Tactic.OfNat
 
 /-!
 # Cast of natural numbers
diff --git a/Mathlib/Data/Nat/Find.lean b/Mathlib/Data/Nat/Find.lean
@@ -5,6 +5,7 @@ Authors: Leonardo de Moura, Johannes Hölzl, Mario Carneiro
 -/
 
 import Mathlib.Data.Nat.Basic
+import Mathlib.Tactic.Push
 import Batteries.WF
 
 /-!
diff --git a/Mathlib/Data/Nat/Order/Lemmas.lean b/Mathlib/Data/Nat/Order/Lemmas.lean
@@ -5,6 +5,7 @@ Authors: Floris van Doorn, Leonardo de Moura, Jeremy Avigad, Mario Carneiro
 -/
 import Mathlib.Data.Nat.Find
 import Mathlib.Data.Set.Basic
+import Mathlib.Tactic.ByContra
 
 /-!
 # Further lemmas about the natural numbers
diff --git a/Mathlib/Data/Rat/Defs.lean b/Mathlib/Data/Rat/Defs.lean
@@ -4,10 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro
 -/
 import Mathlib.Algebra.Group.Defs
+import Mathlib.Data.Nat.Basic
 import Mathlib.Data.Rat.Init
 import Mathlib.Order.Basic
 import Mathlib.Tactic.Common
-import Mathlib.Data.Nat.Basic
 
 /-!
 # Basics for the Rational Numbers
diff --git a/Mathlib/Data/Set/Basic.lean b/Mathlib/Data/Set/Basic.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Leonardo de Moura
 -/
 import Mathlib.Order.PropInstances
-import Mathlib.Tactic.ByContra
 import Mathlib.Tactic.Lift
 import Mathlib.Tactic.Tauto
 import Mathlib.Util.Delaborators
diff --git a/Mathlib/Order/Monotone/Basic.lean b/Mathlib/Order/Monotone/Basic.lean
@@ -11,6 +11,7 @@ import Mathlib.Order.Max
 import Mathlib.Order.Monotone.Defs
 import Mathlib.Order.RelClasses
 import Mathlib.Tactic.Choose
+import Mathlib.Tactic.Contrapose
 
 /-!
 # Monotonicity
diff --git a/Mathlib/Order/RelIso/Basic.lean b/Mathlib/Order/RelIso/Basic.lean
@@ -3,7 +3,6 @@ Copyright (c) 2017 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
-import Mathlib.Data.FunLike.Basic
 import Mathlib.Logic.Embedding.Basic
 import Mathlib.Order.RelClasses
 
diff --git a/Mathlib/Tactic/Measurability.lean b/Mathlib/Tactic/Measurability.lean
@@ -6,7 +6,6 @@ Authors: Miyahara Kō
 
 import Mathlib.Tactic.Measurability.Init
 import Mathlib.Tactic.FunProp.Decl
-import Mathlib.Algebra.Group.Defs
 
 /-!
 # Measurability
diff --git a/Mathlib/Topology/Algebra/Semigroup.lean b/Mathlib/Topology/Algebra/Semigroup.lean
@@ -3,7 +3,6 @@ Copyright (c) 2021 David Wärn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: David Wärn
 -/
-import Mathlib.Algebra.Group.Defs
 import Mathlib.Topology.Separation.Hausdorff
 
 /-!
diff --git a/Mathlib/Topology/Order/LocalExtr.lean b/Mathlib/Topology/Order/LocalExtr.lean
@@ -3,7 +3,6 @@ Copyright (c) 2019 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
-import Mathlib.Algebra.Group.Defs
 import Mathlib.Order.Filter.Extr
 import Mathlib.Topology.ContinuousOn
 
diff --git a/Mathlib/Topology/UniformSpace/Defs.lean b/Mathlib/Topology/UniformSpace/Defs.lean
@@ -3,10 +3,7 @@ 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, Patrick Massot
 -/
-import Mathlib.Algebra.Group.Defs
 import Mathlib.Data.Rel
-import Mathlib.Order.Filter.Tendsto
-import Mathlib.Tactic.Monotonicity.Basic
 import Mathlib.Topology.Order
 
 /-!
