diff --git a/Mathlib.lean b/Mathlib.lean
index 1b810c4cb1e16..b7380aae2e4b5 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -239,6 +239,7 @@ import Mathlib.CategoryTheory.Functor.Category
 import Mathlib.CategoryTheory.Functor.Const
 import Mathlib.CategoryTheory.Functor.Currying
 import Mathlib.CategoryTheory.Functor.Default
+import Mathlib.CategoryTheory.Functor.EpiMono
 import Mathlib.CategoryTheory.Functor.FullyFaithful
 import Mathlib.CategoryTheory.Functor.Functorial
 import Mathlib.CategoryTheory.Functor.Hom
diff --git a/Mathlib/CategoryTheory/Functor/EpiMono.lean b/Mathlib/CategoryTheory/Functor/EpiMono.lean
index 066061e6fefb5..aca32ce70636e 100644
--- a/Mathlib/CategoryTheory/Functor/EpiMono.lean
+++ b/Mathlib/CategoryTheory/Functor/EpiMono.lean
@@ -8,9 +8,9 @@ Authors: Markus Himmel
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
-import Mathbin.CategoryTheory.EpiMono
-import Mathbin.CategoryTheory.Limits.Shapes.StrongEpi
-import Mathbin.CategoryTheory.LiftingProperties.Adjunction
+import Mathlib.CategoryTheory.EpiMono
+import Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
+import Mathlib.CategoryTheory.LiftingProperties.Adjunction
 
 /-!
 # Preservation and reflection of monomorphisms and epimorphisms
@@ -239,8 +239,7 @@ def splitEpiEquiv [Full F] [Faithful F] : SplitEpi f ≃ SplitEpi (F.map f)
 #align category_theory.functor.split_epi_equiv CategoryTheory.Functor.splitEpiEquiv
 
 @[simp]
-theorem isSplitEpi_iff [Full F] [Faithful F] : IsSplitEpi (F.map f) ↔ IsSplitEpi f :=
-  by
+theorem isSplitEpi_iff [Full F] [Faithful F] : IsSplitEpi (F.map f) ↔ IsSplitEpi f := by
   constructor
   · intro h
     exact is_split_epi.mk' ((split_epi_equiv F f).invFun h.exists_split_epi.some)
@@ -262,8 +261,7 @@ def splitMonoEquiv [Full F] [Faithful F] : SplitMono f ≃ SplitMono (F.map f)
 #align category_theory.functor.split_mono_equiv CategoryTheory.Functor.splitMonoEquiv
 
 @[simp]
-theorem isSplitMono_iff [Full F] [Faithful F] : IsSplitMono (F.map f) ↔ IsSplitMono f :=
-  by
+theorem isSplitMono_iff [Full F] [Faithful F] : IsSplitMono (F.map f) ↔ IsSplitMono f := by
   constructor
   · intro h
     exact is_split_mono.mk' ((split_mono_equiv F f).invFun h.exists_split_mono.some)