perf(CategoryTheory/Iso): remove low priority on comp_isIso (#37986)

Author: JovanGerb

Mathlib/CategoryTheory/Iso.lean

@@ -311,12 +311,8 @@ variable {f : X ⟶ Y} {h : Y ⟶ Z}
 instance inv_isIso [IsIso f] : IsIso (inv f) :=
   (asIso f).isIso_inv
 
-/- The following instance has lower priority for the following reason:
-Suppose we are given `f : X ≅ Y` with `X Y : Type u`.
-Without the lower priority, typeclass inference cannot deduce `IsIso f.hom`
-because `f.hom` is defeq to `(fun x ↦ x) ≫ f.hom`, triggering a loop. -/
 @[to_dual self (reorder := X Z, f h, 8 9)]
-instance (priority := 900) comp_isIso [IsIso f] [IsIso h] : IsIso (f ≫ h) :=
+instance comp_isIso [IsIso f] [IsIso h] : IsIso (f ≫ h) :=
   (asIso f ≪≫ asIso h).isIso_hom
 
 /--