refactor(*): supremum of refactoring PRs #17405 #17418 #17419 #17420 #17421 #17422 #17423 #17427 #17430 (#17424)

Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

Author: 3 people

counterexamples/linear_order_with_pos_mul_pos_eq_zero.lean

@@ -4,7 +4,7 @@ All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin, Damiano Testa, Kevin Buzzard
 -/
-import algebra.order.monoid.basic
+import algebra.order.monoid.defs
 
 /-!
 An example of a `linear_ordered_comm_monoid_with_zero` in which the product of two positive

src/algebra/associated.lean

@@ -3,7 +3,7 @@ Copyright (c) 2018 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Jens Wagemaker
 -/
-import algebra.divisibility
+import algebra.divisibility.basic
 import algebra.group_power.lemmas
 import algebra.invertible
 import order.atoms

src/algebra/big_operators/basic.lean

@@ -5,7 +5,7 @@ Authors: Johannes Hölzl
 -/
 
 import algebra.group.pi
-import algebra.hom.equiv
+import algebra.hom.equiv.basic
 import algebra.ring.opposite
 import data.finset.fold
 import data.fintype.basic

src/algebra/category/Group/equivalence_Group_AddGroup.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jujian Zhang
 -/
 import algebra.category.Group.basic
+import algebra.hom.equiv.type_tags
 
 /-!
 # Equivalence between `Group` and `AddGroup`

src/algebra/category/Semigroup/basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Julian Kuelshammer
 -/
 import algebra.pempty_instances
-import algebra.hom.equiv
+import algebra.hom.equiv.basic
 import category_theory.concrete_category.bundled_hom
 import category_theory.functor.reflects_isomorphisms
 import category_theory.elementwise