chore(category_theory/*): reduce imports (#13305)

An unnecessary import of `tactic.monotonicity` earlier in the hierarchy was pulling in quite a lot. A few compensatory imports are needed later.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/algebra/category/Semigroup/basic.lean

@@ -4,6 +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 category_theory.concrete_category.bundled_hom
 import category_theory.functor.reflects_isomorphisms
 

src/category_theory/essential_image.lean

@@ -5,6 +5,7 @@ Authors: Bhavik Mehta
 -/
 import category_theory.natural_isomorphism
 import category_theory.full_subcategory
+import data.set.basic
 
 /-!
 # Essential image of a functor

src/category_theory/functor/basic.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Tim Baumann, Stephen Morgan, Scott Morrison
 -/
 import tactic.reassoc_axiom
-import tactic.monotonicity
 import category_theory.category.basic
 
 /-!
@@ -13,7 +12,7 @@ import category_theory.category.basic
 Defines a functor between categories, extending a `prefunctor` between quivers.
 
 Introduces notation `C ⥤ D` for the type of all functors from `C` to `D`.
-(Unfortunately the `⇒` arrow (`\functor`) is taken by core, 
+(Unfortunately the `⇒` arrow (`\functor`) is taken by core,
 but in mathlib4 we should switch to this.)
 -/