chore(*): removed unneeded imports (#18926)

This is another run of #17568, scrubbing unnecessary imports. Like last time we only remove genuinely unneeded imports, and leave merely transitively redundant imports alone. (I *still* disagree with the objectors to removing transitively redundant imports Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
leanprover-community · May 4, 2023 · f0c8bf9 · f0c8bf9
1 parent 73f9623
commit f0c8bf9
Show file tree

Hide file tree

Showing 68 changed files with 40 additions and 77 deletions.
diff --git a/src/algebra/category/Module/biproducts.lean b/src/algebra/category/Module/biproducts.lean
@@ -5,7 +5,6 @@ Authors: Scott Morrison
 -/
 import algebra.group.pi
 import category_theory.limits.shapes.biproducts
-import algebra.category.Module.limits
 import algebra.category.Module.abelian
 import algebra.homology.short_exact.abelian
 

diff --git a/src/algebra/continued_fractions/computation/approximation_corollaries.lean b/src/algebra/continued_fractions/computation/approximation_corollaries.lean
@@ -6,7 +6,8 @@ Authors: Kevin Kappelmann
 import algebra.continued_fractions.computation.approximations
 import algebra.continued_fractions.convergents_equiv
 import algebra.order.archimedean
-import topology.algebra.order.field
+import algebra.algebra.basic
+import topology.order.basic
 
 /-!
 # Corollaries From Approximation Lemmas (`algebra.continued_fractions.computation.approximations`)

diff --git a/src/algebra/direct_limit.lean b/src/algebra/direct_limit.lean
@@ -6,7 +6,7 @@ Authors: Kenny Lau, Chris Hughes
 import data.finset.order
 import algebra.direct_sum.module
 import ring_theory.free_comm_ring
-import ring_theory.ideal.quotient_operations
+import ring_theory.ideal.quotient
 /-!
 # Direct limit of modules, abelian groups, rings, and fields.
 

diff --git a/src/algebra/order/interval.lean b/src/algebra/order/interval.lean
@@ -15,7 +15,7 @@ import tactic.positivity
 
 This file defines arithmetic operations on intervals and prove their correctness. Note that this is
 full precision operations. The essentials of float operations can be found
-in `data.fp.basic`. We hsve not yet integrated these with the rest of the library.
+in `data.fp.basic`. We have not yet integrated these with the rest of the library.
 -/
 
 open function set

diff --git a/src/algebraic_geometry/Spec.lean b/src/algebraic_geometry/Spec.lean
@@ -5,7 +5,6 @@ Authors: Scott Morrison, Justus Springer
 -/
 import algebraic_geometry.locally_ringed_space
 import algebraic_geometry.structure_sheaf
-import logic.equiv.transfer_instance
 import ring_theory.localization.localization_localization
 import topology.sheaves.sheaf_condition.sites
 import topology.sheaves.functors

diff --git a/src/algebraic_geometry/elliptic_curve/point.lean b/src/algebraic_geometry/elliptic_curve/point.lean
@@ -5,8 +5,6 @@ Authors: David Kurniadi Angdinata
 -/
 
 import algebraic_geometry.elliptic_curve.weierstrass
-import field_theory.galois -- temporary import to enable point notation
-import ring_theory.class_group
 
 /-!
 # The group of nonsingular rational points on a Weierstrass curve over a field

diff --git a/src/algebraic_geometry/locally_ringed_space.lean b/src/algebraic_geometry/locally_ringed_space.lean
@@ -6,7 +6,6 @@ Authors: Johan Commelin
 
 import algebraic_geometry.ringed_space
 import algebraic_geometry.stalks
-import logic.equiv.transfer_instance
 
 /-!
 # The category of locally ringed spaces

diff --git a/src/algebraic_geometry/morphisms/open_immersion.lean b/src/algebraic_geometry/morphisms/open_immersion.lean
@@ -3,8 +3,8 @@ Copyright (c) 2022 Andrew Yang. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andrew Yang
 -/
-import algebraic_geometry.morphisms.ring_hom_properties
 import topology.local_at_target
+import algebraic_geometry.morphisms.basic
 
 /-!
 

diff --git a/src/algebraic_geometry/open_immersion.lean b/src/algebraic_geometry/open_immersion.lean
@@ -12,7 +12,6 @@ import algebraic_geometry.Scheme
 import category_theory.limits.shapes.strict_initial
 import category_theory.limits.shapes.comm_sq
 import algebra.category.Ring.instances
-import topology.local_at_target
 
 /-!
 # Open immersions of structured spaces

diff --git a/src/analysis/bounded_variation.lean b/src/analysis/bounded_variation.lean
@@ -3,7 +3,6 @@ Copyright (c) 2022 Sébastien Gouëzel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel
 -/
-import measure_theory.measure.lebesgue
 import analysis.calculus.monotone
 import data.set.function
 import algebra.group.basic

diff --git a/src/analysis/calculus/bump_function_findim.lean b/src/analysis/calculus/bump_function_findim.lean
@@ -6,6 +6,7 @@ Authors: Sébastien Gouëzel
 import analysis.calculus.series
 import analysis.convolution
 import analysis.inner_product_space.euclidean_dist
+import measure_theory.measure.haar_lebesgue
 import data.set.pointwise.support
 
 /-!

diff --git a/src/analysis/complex/upper_half_plane/topology.lean b/src/analysis/complex/upper_half_plane/topology.lean
@@ -9,7 +9,6 @@ import analysis.convex.normed
 import analysis.convex.complex
 import analysis.complex.re_im_topology
 import topology.homotopy.contractible
-import geometry.manifold.mfderiv
 import geometry.manifold.cont_mdiff_mfderiv
 
 /-!

diff --git a/src/analysis/constant_speed.lean b/src/analysis/constant_speed.lean
@@ -3,8 +3,6 @@ Copyright (c) 2023 Rémi Bottinelli. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Rémi Bottinelli
 -/
-import measure_theory.measure.lebesgue
-import analysis.calculus.monotone
 import data.set.function
 import analysis.bounded_variation
 import tactic.swap_var

diff --git a/src/analysis/convex/between.lean b/src/analysis/convex/between.lean
@@ -6,8 +6,8 @@ Authors: Joseph Myers
 import data.set.intervals.group
 import analysis.convex.segment
 import linear_algebra.affine_space.finite_dimensional
-import linear_algebra.affine_space.midpoint_zero
 import tactic.field_simp
+import algebra.char_p.invertible
 
 /-!
 # Betweenness in affine spaces

diff --git a/src/analysis/convex/cone/proper.lean b/src/analysis/convex/cone/proper.lean
@@ -3,7 +3,7 @@ Copyright (c) 2022 Apurva Nakade All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Apurva Nakade
 -/
-import analysis.inner_product_space.adjoint
+import analysis.convex.cone.basic
 
 /-!
 

diff --git a/src/analysis/convex/intrinsic.lean b/src/analysis/convex/intrinsic.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Paul Reichert, Yaël Dillies
 -/
 import analysis.normed_space.add_torsor_bases
-import analysis.normed_space.linear_isometry
 
 /-!
 # Intrinsic frontier and interior

diff --git a/src/analysis/fourier/fourier_transform.lean b/src/analysis/fourier/fourier_transform.lean
@@ -4,9 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: David Loeffler
 -/
 
-import analysis.special_functions.complex.circle
 import measure_theory.group.integration
-import measure_theory.integral.integral_eq_improper
+import measure_theory.measure.haar_of_basis
 
 /-!
 # The Fourier transform

diff --git a/src/analysis/fourier/riemann_lebesgue_lemma.lean b/src/analysis/fourier/riemann_lebesgue_lemma.lean
@@ -5,9 +5,7 @@ Authors: David Loeffler
 -/
 
 import measure_theory.function.continuous_map_dense
-import measure_theory.integral.integral_eq_improper
 import measure_theory.group.integration
-import topology.continuous_function.zero_at_infty
 import analysis.fourier.fourier_transform
 import analysis.inner_product_space.dual
 import topology.metric_space.emetric_paracompact

diff --git a/src/analysis/inner_product_space/orthogonal.lean b/src/analysis/inner_product_space/orthogonal.lean
@@ -3,13 +3,7 @@ Copyright (c) 2019 Zhouhang Zhou. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Zhouhang Zhou, Sébastien Gouëzel, Frédéric Dupuis
 -/
-import algebra.direct_sum.module
-import analysis.complex.basic
-import analysis.convex.uniform
-import analysis.normed_space.completion
-import analysis.normed_space.bounded_linear_maps
 import linear_algebra.bilinear_form
-
 import analysis.inner_product_space.basic
 
 /-!

diff --git a/src/analysis/normed_space/affine_isometry.lean b/src/analysis/normed_space/affine_isometry.lean
@@ -7,7 +7,7 @@ import analysis.normed_space.linear_isometry
 import analysis.normed.group.add_torsor
 import analysis.normed_space.basic
 import linear_algebra.affine_space.restrict
-import linear_algebra.affine_space.midpoint_zero
+import algebra.char_p.invertible
 
 /-!
 # Affine isometries

diff --git a/src/analysis/normed_space/compact_operator.lean b/src/analysis/normed_space/compact_operator.lean
@@ -3,8 +3,8 @@ Copyright (c) 2022 Anatole Dedecker. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Anatole Dedecker
 -/
-import analysis.normed_space.operator_norm
 import analysis.locally_convex.bounded
+import topology.algebra.module.strong_topology
 
 /-!
 # Compact operators

diff --git a/src/analysis/normed_space/quaternion_exponential.lean b/src/analysis/normed_space/quaternion_exponential.lean
@@ -5,7 +5,6 @@ Authors: Eric Wieser
 -/
 import analysis.quaternion
 import analysis.normed_space.exponential
-import analysis.inner_product_space.pi_L2
 import analysis.special_functions.trigonometric.series
 
 /-!

diff --git a/src/analysis/normed_space/star/spectrum.lean b/src/analysis/normed_space/star/spectrum.lean
@@ -5,7 +5,6 @@ Authors: Jireh Loreaux
 -/
 import analysis.normed_space.star.basic
 import analysis.normed_space.spectrum
-import analysis.normed_space.star.exponential
 import analysis.special_functions.exponential
 import algebra.star.star_alg_hom
 

diff --git a/src/analysis/special_functions/japanese_bracket.lean b/src/analysis/special_functions/japanese_bracket.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Moritz Doll. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Moritz Doll
 -/
+import measure_theory.measure.haar_lebesgue
 import measure_theory.integral.layercake
 
 /-!

diff --git a/src/category_theory/abelian/generator.lean b/src/category_theory/abelian/generator.lean
@@ -7,7 +7,7 @@ import category_theory.abelian.subobject
 import category_theory.limits.essentially_small
 import category_theory.preadditive.injective
 import category_theory.preadditive.generator
-import category_theory.preadditive.yoneda.limits
+import category_theory.abelian.opposite
 
 /-!
 # A complete abelian category with enough injectives and a separator has an injective coseparator

diff --git a/src/category_theory/abelian/injective_resolution.lean b/src/category_theory/abelian/injective_resolution.lean
@@ -5,7 +5,6 @@ Authors: Jujian Zhang, Scott Morrison
 -/
 import algebra.homology.quasi_iso
 import category_theory.preadditive.injective_resolution
-import category_theory.abelian.homology
 import algebra.homology.homotopy_category
 
 /-!

diff --git a/src/category_theory/abelian/projective.lean b/src/category_theory/abelian/projective.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus Himmel, Scott Morrison, Jakob von Raumer
 -/
 import algebra.homology.quasi_iso
-import category_theory.abelian.homology
 import category_theory.preadditive.projective_resolution
 import category_theory.preadditive.yoneda.limits
 import category_theory.preadditive.yoneda.projective

diff --git a/src/category_theory/sites/cover_preserving.lean b/src/category_theory/sites/cover_preserving.lean
@@ -3,9 +3,9 @@ Copyright (c) 2021 Andrew Yang. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andrew Yang
 -/
-import category_theory.sites.limits
 import category_theory.functor.flat
-import category_theory.limits.preserves.filtered
+import category_theory.sites.sheaf
+import tactic.apply_fun
 
 /-!
 # Cover-preserving functors between sites.

diff --git a/src/data/array/lemmas.lean b/src/data/array/lemmas.lean
@@ -3,8 +3,8 @@ Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Mario Carneiro
 -/
-import control.traversable.equiv
-import data.vector.basic
+import data.fin.basic
+import data.list.basic
 
 universes u v w
 

diff --git a/src/data/buffer/basic.lean b/src/data/buffer/basic.lean
@@ -7,6 +7,7 @@ General utility functions for buffers.
 -/
 import data.array.lemmas
 import control.traversable.instances
+import control.traversable.equiv
 
 namespace buffer
 

diff --git a/src/data/hash_map.lean b/src/data/hash_map.lean
@@ -6,6 +6,7 @@ Authors: Leonardo de Moura, Mario Carneiro
 import data.array.lemmas
 import data.list.join
 import data.list.range
+import data.list.nodup
 import data.pnat.defs
 
 /-!

diff --git a/src/field_theory/galois.lean b/src/field_theory/galois.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Thomas Browning, Patrick Lutz
 -/
 
-import field_theory.is_alg_closed.algebraic_closure
 import field_theory.primitive_element
 import field_theory.fixed
 import group_theory.group_action.fixing_subgroup

diff --git a/src/field_theory/minpoly/basic.lean b/src/field_theory/minpoly/basic.lean
@@ -3,7 +3,6 @@ Copyright (c) 2019 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Johan Commelin
 -/
-import data.polynomial.field_division
 import ring_theory.integral_closure
 
 /-!

diff --git a/src/field_theory/minpoly/is_integrally_closed.lean b/src/field_theory/minpoly/is_integrally_closed.lean
@@ -3,7 +3,6 @@ Copyright (c) 2019 Riccardo Brasca. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Riccardo Brasca, Paul Lezeau, Junyan Xu
 -/
-import data.polynomial.field_division
 import ring_theory.adjoin_root
 import field_theory.minpoly.field
 import ring_theory.polynomial.gauss_lemma

diff --git a/src/geometry/euclidean/angle/oriented/basic.lean b/src/geometry/euclidean/angle/oriented/basic.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Myers, Heather Macbeth
 -/
 import analysis.inner_product_space.two_dim
-import analysis.special_functions.complex.circle
 import geometry.euclidean.angle.unoriented.basic
 
 /-!

diff --git a/src/geometry/euclidean/angle/oriented/rotation.lean b/src/geometry/euclidean/angle/oriented/rotation.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Joseph Myers. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Myers, Heather Macbeth
 -/
+import analysis.special_functions.complex.circle
 import geometry.euclidean.angle.oriented.basic
 
 /-!

diff --git a/src/linear_algebra/bilinear_form.lean b/src/linear_algebra/bilinear_form.lean
@@ -6,7 +6,6 @@ Authors: Andreas Swerdlow, Kexing Ying
 
 import linear_algebra.dual
 import linear_algebra.free_module.finite.matrix
-import linear_algebra.matrix.to_lin
 
 /-!
 # Bilinear form

diff --git a/src/linear_algebra/bilinear_form/tensor_product.lean b/src/linear_algebra/bilinear_form/tensor_product.lean
@@ -5,7 +5,6 @@ Authors: Eric Wieser
 -/
 import linear_algebra.bilinear_form
 import linear_algebra.tensor_product
-import linear_algebra.contraction
 
 /-!
 # The bilinear form on a tensor product

diff --git a/src/linear_algebra/eigenspace.lean b/src/linear_algebra/eigenspace.lean
@@ -6,7 +6,6 @@ Authors: Alexander Bentkamp
 
 import algebra.algebra.spectrum
 import order.hom.basic
-import linear_algebra.free_module.finite.basic
 import linear_algebra.general_linear_group
 
 /-!

diff --git a/src/measure_theory/integral/interval_integral.lean b/src/measure_theory/integral/interval_integral.lean
@@ -5,7 +5,7 @@ Authors: Yury G. Kudryashov, Patrick Massot, Sébastien Gouëzel
 -/
 import data.set.intervals.disjoint
 import measure_theory.integral.set_integral
-import measure_theory.measure.haar_lebesgue
+import measure_theory.measure.lebesgue
 
 /-!
 # Integral over an interval

diff --git a/src/measure_theory/integral/periodic.lean b/src/measure_theory/integral/periodic.lean
@@ -3,6 +3,7 @@ Copyright (c) 2021 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov, Alex Kontorovich, Heather Macbeth
 -/
+import measure_theory.measure.haar_lebesgue
 import measure_theory.measure.haar_quotient
 import measure_theory.integral.interval_integral
 import topology.algebra.order.floor

diff --git a/src/measure_theory/measure/complex_lebesgue.lean b/src/measure_theory/measure/complex_lebesgue.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
 import measure_theory.measure.lebesgue
+import measure_theory.measure.haar_of_basis
 
 /-!
 # Lebesgue measure on `ℂ`

diff --git a/src/measure_theory/measure/haar_of_basis.lean b/src/measure_theory/measure/haar_of_basis.lean
@@ -5,7 +5,6 @@ Authors: Sébastien Gouëzel
 -/
 import measure_theory.measure.haar
 import analysis.inner_product_space.pi_L2
-import measure_theory.constructions.pi
 
 /-!
 # Additive Haar measure constructed from a basis

diff --git a/src/measure_theory/measure/probability_measure.lean b/src/measure_theory/measure/probability_measure.lean
@@ -5,7 +5,6 @@ Authors: Kalle Kytölä
 -/
 import measure_theory.measure.finite_measure
 import measure_theory.integral.average
-import probability.conditional_probability
 
 /-!
 # Probability measures

diff --git a/src/measure_theory/tactic.lean b/src/measure_theory/tactic.lean
@@ -7,6 +7,7 @@ import measure_theory.measure.measure_space_def
 import tactic.auto_cases
 import tactic.tidy
 import tactic.with_local_reducibility
+
 /-!
 # Tactics for measure theory