feat: Over.map of an iso is an equivalence (#27139)

From Toric

Author: YaelDillies

Mathlib/CategoryTheory/Comma/Over/Basic.lean

@@ -172,14 +172,17 @@ theorem map_obj_hom : ((map f).obj U).hom = U.hom ≫ f :=
 @[simp]
 theorem map_map_left : ((map f).map g).left = g.left :=
   rfl
-end
 
 /-- If `f` is an isomorphism, `map f` is an equivalence of categories. -/
-def mapIso {Y : T} (f : X ≅ Y) : Over X ≌ Over Y :=
+def mapIso (f : X ≅ Y) : Over X ≌ Over Y :=
   Comma.mapRightIso _ <| Discrete.natIso fun _ ↦ f
 
-@[simp] lemma mapIso_functor {Y : T} (f : X ≅ Y) : (mapIso f).functor = map f.hom := rfl
-@[simp] lemma mapIso_inverse {Y : T} (f : X ≅ Y) : (mapIso f).inverse = map f.inv := rfl
+@[simp] lemma mapIso_functor (f : X ≅ Y) : (mapIso f).functor = map f.hom := rfl
+@[simp] lemma mapIso_inverse (f : X ≅ Y) : (mapIso f).inverse = map f.inv := rfl
+
+instance [IsIso f] : (Over.map f).IsEquivalence := (Over.mapIso <| asIso f).isEquivalence_functor
+
+end
 
 section coherences
 /-!
@@ -586,14 +589,17 @@ theorem map_obj_hom : ((map f).obj U).hom = f ≫ U.hom :=
 @[simp]
 theorem map_map_right : ((map f).map g).right = g.right :=
   rfl
-end
 
 /-- If `f` is an isomorphism, `map f` is an equivalence of categories. -/
-def mapIso {Y : T} (f : X ≅ Y) : Under Y ≌ Under X :=
+def mapIso (f : X ≅ Y) : Under Y ≌ Under X :=
   Comma.mapLeftIso _ <| Discrete.natIso fun _ ↦ f.symm
 
-@[simp] lemma mapIso_functor {Y : T} (f : X ≅ Y) : (mapIso f).functor = map f.hom := rfl
-@[simp] lemma mapIso_inverse {Y : T} (f : X ≅ Y) : (mapIso f).inverse = map f.inv := rfl
+@[simp] lemma mapIso_functor (f : X ≅ Y) : (mapIso f).functor = map f.hom := rfl
+@[simp] lemma mapIso_inverse (f : X ≅ Y) : (mapIso f).inverse = map f.inv := rfl
+
+instance [IsIso f] : (Under.map f).IsEquivalence := (Under.mapIso <| asIso f).isEquivalence_functor
+
+end
 
 section coherences
 /-!