From 7f41cf3e83e6504ef6a51c98a584bfeddb7e8e6d Mon Sep 17 00:00:00 2001
From: Matthew Ballard <matt@mrb.email>
Date: Thu, 16 Feb 2023 21:56:57 -0500
Subject: [PATCH] fix errors; lint; shorten filename

---
 Mathlib.lean                                  |  2 +-
 ...ectsIsomorphisms.lean => ReflectsIso.lean} | 21 ++++++++++---------
 2 files changed, 12 insertions(+), 11 deletions(-)
 rename Mathlib/CategoryTheory/Functor/{ReflectsIsomorphisms.lean => ReflectsIso.lean} (84%)

diff --git a/Mathlib.lean b/Mathlib.lean
index 1c583a7b5c193..59319f46b5e60 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -246,7 +246,7 @@ import Mathlib.CategoryTheory.Functor.FullyFaithful
 import Mathlib.CategoryTheory.Functor.Functorial
 import Mathlib.CategoryTheory.Functor.Hom
 import Mathlib.CategoryTheory.Functor.InvIsos
-import Mathlib.CategoryTheory.Functor.ReflectsIsomorphisms
+import Mathlib.CategoryTheory.Functor.ReflectsIso
 import Mathlib.CategoryTheory.Groupoid
 import Mathlib.CategoryTheory.Iso
 import Mathlib.CategoryTheory.LiftingProperties.Adjunction
diff --git a/Mathlib/CategoryTheory/Functor/ReflectsIsomorphisms.lean b/Mathlib/CategoryTheory/Functor/ReflectsIso.lean
similarity index 84%
rename from Mathlib/CategoryTheory/Functor/ReflectsIsomorphisms.lean
rename to Mathlib/CategoryTheory/Functor/ReflectsIso.lean
index 8197884ac4029..34192a02d8c1d 100644
--- a/Mathlib/CategoryTheory/Functor/ReflectsIsomorphisms.lean
+++ b/Mathlib/CategoryTheory/Functor/ReflectsIso.lean
@@ -17,7 +17,7 @@ import Mathlib.CategoryTheory.Functor.FullyFaithful
 
 A functor `F` reflects isomorphisms if whenever `F.map f` is an isomorphism, `f` was too.
 
-It is formalized as a `Prop` valued typeclass `reflects_isomorphisms F`.
+It is formalized as a `Prop` valued typeclass `ReflectsIsomorphisms F`.
 
 Any fully faithful functor reflects isomorphisms.
 -/
@@ -42,6 +42,7 @@ morphism `f : A ⟶ B`, if `F.map f` is an isomorphism then `f` is as well.
 Note that we do not assume or require that `F` is faithful.
 -/
 class ReflectsIsomorphisms (F : C ⥤ D) : Prop where
+  /-- For any `f`, if `F.map f` is an iso, then so was `f`-/
   reflects : ∀ {A B : C} (f : A ⟶ B) [IsIso (F.map f)], IsIso f
 #align category_theory.reflects_isomorphisms CategoryTheory.ReflectsIsomorphisms
 
@@ -53,25 +54,25 @@ theorem isIso_of_reflects_iso {A B : C} (f : A ⟶ B) (F : C ⥤ D) [IsIso (F.ma
 
 instance (priority := 100) of_full_and_faithful (F : C ⥤ D) [Full F] [Faithful F] :
     ReflectsIsomorphisms F
-    where reflects X Y f i :=
+    where reflects f i :=
     ⟨⟨F.preimage (inv (F.map f)), ⟨F.map_injective (by simp), F.map_injective (by simp)⟩⟩⟩
 #align category_theory.of_full_and_faithful CategoryTheory.of_full_and_faithful
 
 instance (F : C ⥤ D) (G : D ⥤ E) [ReflectsIsomorphisms F] [ReflectsIsomorphisms G] :
     ReflectsIsomorphisms (F ⋙ G) :=
-  ⟨fun _ _ f (hf : IsIso (G.map _)) => by
+  ⟨fun f (hf : IsIso (G.map _)) => by
     skip
-    haveI := is_iso_of_reflects_iso (F.map f) G
-    exact is_iso_of_reflects_iso f F⟩
+    haveI := isIso_of_reflects_iso (F.map f) G
+    exact isIso_of_reflects_iso f F⟩
 
 instance (priority := 100) reflectsIsomorphisms_of_reflectsMonomorphisms_of_reflectsEpimorphisms
     [Balanced C] (F : C ⥤ D) [ReflectsMonomorphisms F] [ReflectsEpimorphisms F] :
-    ReflectsIsomorphisms F
-    where reflects A B f hf := by
+    ReflectsIsomorphisms F where 
+  reflects f hf := by
     skip
-    haveI : epi f := epi_of_epi_map F inferInstance
-    haveI : mono f := mono_of_mono_map F inferInstance
-    exact is_iso_of_mono_of_epi f
+    haveI : Epi f := epi_of_epi_map F inferInstance
+    haveI : Mono f := mono_of_mono_map F inferInstance
+    exact isIso_of_mono_of_epi f
 #align category_theory.reflects_isomorphisms_of_reflects_monomorphisms_of_reflects_epimorphisms CategoryTheory.reflectsIsomorphisms_of_reflectsMonomorphisms_of_reflectsEpimorphisms
 
 end ReflectsIso