chore(CategoryTheory): fix hasLimitOfIso (#22514)

`hasLimitOfIso` is renamed `hasLimit_of_iso`. A new lemma `hasLimit_iff_of_iso` is added.

Author: joelriou

Mathlib/Algebra/Category/ModuleCat/Sheaf/Colimits.lean

@@ -30,6 +30,6 @@ instance [HasColimitsOfShape K (PresheafOfModules.{v} R.val)] :
   has_colimit F := by
     let e : F ≅ (F ⋙ forget R) ⋙ PresheafOfModules.sheafification (𝟙 R.val) :=
       isoWhiskerLeft F (asIso (PresheafOfModules.sheafificationAdjunction (𝟙 R.val)).counit).symm
-    exact hasColimitOfIso e
+    exact hasColimit_of_iso e
 
 end SheafOfModules

Mathlib/Algebra/Homology/HomologicalComplexBiprod.lean

@@ -27,11 +27,11 @@ instance (i : ι) : HasBinaryBiproduct ((eval C c i).obj K) ((eval C c i).obj L)
 
 instance (i : ι) : HasLimit ((pair K L) ⋙ (eval C c i)) := by
   have e : _ ≅ pair (K.X i) (L.X i) := diagramIsoPair (pair K L ⋙ eval C c i)
-  exact hasLimitOfIso e.symm
+  exact hasLimit_of_iso e.symm
 
 instance (i : ι) : HasColimit ((pair K L) ⋙ (eval C c i)) := by
   have e : _ ≅ pair (K.X i) (L.X i) := diagramIsoPair (pair K L ⋙ eval C c i)
-  exact hasColimitOfIso e
+  exact hasColimit_of_iso e
 
 instance : HasBinaryBiproduct K L := HasBinaryBiproduct.of_hasBinaryProduct _ _
 

Mathlib/Algebra/Homology/ShortComplex/LeftHomology.lean

@@ -1009,7 +1009,7 @@ lemma hasCokernel [S.HasLeftHomology] [HasKernel S.g] :
   let e : parallelPair (kernel.lift S.g S.f S.zero) 0 ≅ parallelPair h.f' 0 :=
     parallelPair.ext (Iso.refl _) (IsLimit.conePointUniqueUpToIso (kernelIsKernel S.g) h.hi)
       (by aesop_cat) (by simp)
-  exact hasColimitOfIso e
+  exact hasColimit_of_iso e
 
 end HasLeftHomology
 

Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean

@@ -1288,7 +1288,7 @@ lemma hasKernel [S.HasRightHomology] [HasCokernel S.f] :
   let e : parallelPair (cokernel.desc S.f S.g S.zero) 0 ≅ parallelPair h.g' 0 :=
     parallelPair.ext (IsColimit.coconePointUniqueUpToIso (colimit.isColimit _) h.hp)
       (Iso.refl _) (coequalizer.hom_ext (by simp)) (by simp)
-  exact hasLimitOfIso e.symm
+  exact hasLimit_of_iso e.symm
 
 end HasRightHomology
 

Mathlib/AlgebraicGeometry/OpenImmersion.lean

@@ -437,9 +437,8 @@ instance forget_map_isOpenImmersion : LocallyRingedSpace.IsOpenImmersion ((forge
 
 instance hasLimit_cospan_forget_of_left :
     HasLimit (cospan f g ⋙ Scheme.forgetToLocallyRingedSpace) := by
-  apply @hasLimitOfIso _ _ _ _ _ _ ?_ (diagramIsoCospan.{u} _).symm
-  change HasLimit (cospan ((forget).map f) ((forget).map g))
-  infer_instance
+  rw [hasLimit_iff_of_iso (diagramIsoCospan _)]
+  exact inferInstanceAs (HasLimit (cospan ((forget).map f) ((forget).map g)))
 
 open CategoryTheory.Limits.WalkingCospan
 
@@ -448,9 +447,8 @@ instance hasLimit_cospan_forget_of_left' :
   show HasLimit (cospan ((forget).map f) ((forget).map g)) from inferInstance
 
 instance hasLimit_cospan_forget_of_right : HasLimit (cospan g f ⋙ forget) := by
-  apply @hasLimitOfIso _ _ _ _ _ _ ?_ (diagramIsoCospan.{u} _).symm
-  change HasLimit (cospan ((forget).map g) ((forget).map f))
-  infer_instance
+  rw [hasLimit_iff_of_iso (diagramIsoCospan _)]
+  exact inferInstanceAs (HasLimit (cospan ((forget).map g) ((forget).map f)))
 
 instance hasLimit_cospan_forget_of_right' :
     HasLimit (cospan ((cospan g f ⋙ forget).map Hom.inl) ((cospan g f ⋙ forget).map Hom.inr)) :=

Mathlib/CategoryTheory/Adjunction/Limits.lean

@@ -146,10 +146,10 @@ theorem hasColimit_comp_equivalence (E : C ⥤ D) [E.IsEquivalence] [HasColimit
       isColimit := isColimitOfPreserves _ (colimit.isColimit K) }
 
 theorem hasColimit_of_comp_equivalence (E : C ⥤ D) [E.IsEquivalence] [HasColimit (K ⋙ E)] :
-    HasColimit K :=
-  @hasColimitOfIso _ _ _ _ (K ⋙ E ⋙ E.inv) K
-    (@hasColimit_comp_equivalence _ _ _ _ _ _ (K ⋙ E) E.inv _ _)
-    ((Functor.rightUnitor _).symm ≪≫ isoWhiskerLeft K E.asEquivalence.unitIso)
+    HasColimit K := by
+  rw [hasColimit_iff_of_iso
+    ((Functor.rightUnitor _).symm ≪≫ isoWhiskerLeft K E.asEquivalence.unitIso)]
+  exact hasColimit_comp_equivalence (K ⋙ E) E.inv
 
 /-- Transport a `HasColimitsOfShape` instance across an equivalence. -/
 theorem hasColimitsOfShape_of_equivalence (E : C ⥤ D) [E.IsEquivalence] [HasColimitsOfShape J D] :
@@ -265,10 +265,10 @@ theorem hasLimit_comp_equivalence (E : D ⥤ C) [E.IsEquivalence] [HasLimit K] :
       isLimit := isLimitOfPreserves _ (limit.isLimit K) }
 
 theorem hasLimit_of_comp_equivalence (E : D ⥤ C) [E.IsEquivalence] [HasLimit (K ⋙ E)] :
-    HasLimit K :=
-  @hasLimitOfIso _ _ _ _ (K ⋙ E ⋙ E.inv) K
-    (@hasLimit_comp_equivalence _ _ _ _ _ _ (K ⋙ E) E.inv _ _)
-    (isoWhiskerLeft K E.asEquivalence.unitIso.symm ≪≫ Functor.rightUnitor _)
+    HasLimit K := by
+  rw [← hasLimit_iff_of_iso
+    (isoWhiskerLeft K E.asEquivalence.unitIso.symm ≪≫ Functor.rightUnitor _)]
+  exact hasLimit_comp_equivalence (K ⋙ E) E.inv
 
 /-- Transport a `HasLimitsOfShape` instance across an equivalence. -/
 theorem hasLimitsOfShape_of_equivalence (E : D ⥤ C) [E.IsEquivalence] [HasLimitsOfShape J C] :

Mathlib/CategoryTheory/Functor/KanExtension/Adjunction.lean

@@ -106,7 +106,7 @@ lemma leftKanExtensionUnit_leftKanExtensionObjIsoColimit_hom (X : C) :
 @[instance]
 theorem hasColimit_map_comp_ι_comp_grotendieckProj {X Y : D} (f : X ⟶ Y) :
     HasColimit ((functor L).map f ⋙ Grothendieck.ι (functor L) Y ⋙ grothendieckProj L ⋙ F) :=
-  hasColimitOfIso (isoWhiskerRight (mapCompιCompGrothendieckProj L f) F)
+  hasColimit_of_iso (isoWhiskerRight (mapCompιCompGrothendieckProj L f) F)
 
 /-- The left Kan extension of `F : C ⥤ H` along a functor `L : C ⥤ D` is isomorphic to the
 fiberwise colimit of the projection functor on the Grothendieck construction of the costructured
@@ -115,8 +115,9 @@ arrow category composed with `F`. -/
 noncomputable def leftKanExtensionIsoFiberwiseColimit [HasLeftKanExtension L F] :
     leftKanExtension L F ≅ fiberwiseColimit (grothendieckProj L ⋙ F) :=
   letI : ∀ X, HasColimit (Grothendieck.ι (functor L) X ⋙ grothendieckProj L ⋙ F) :=
-      fun X => hasColimitOfIso <| Iso.symm <| isoWhiskerRight (eqToIso ((functor L).map_id X)) _ ≪≫
-      Functor.leftUnitor (Grothendieck.ι (functor L) X ⋙ grothendieckProj L ⋙ F)
+      fun X => hasColimit_of_iso <| Iso.symm <|
+        isoWhiskerRight (eqToIso ((functor L).map_id X)) _ ≪≫
+        Functor.leftUnitor (Grothendieck.ι (functor L) X ⋙ grothendieckProj L ⋙ F)
   Iso.symm <| NatIso.ofComponents
     (fun X => HasColimit.isoOfNatIso (isoWhiskerRight (ιCompGrothendieckProj L X) F) ≪≫
       (leftKanExtensionObjIsoColimit L F X).symm)

Mathlib/CategoryTheory/GlueData.lean

@@ -284,7 +284,7 @@ attribute [local instance] hasColimit_multispan_comp
 variable [∀ i j k, PreservesLimit (cospan (D.f i j) (D.f i k)) F]
 
 theorem hasColimit_mapGlueData_diagram : HasMulticoequalizer (D.mapGlueData F).diagram :=
-  hasColimitOfIso (D.diagramIso F).symm
+  hasColimit_of_iso (D.diagramIso F).symm
 
 attribute [local instance] hasColimit_mapGlueData_diagram
 

Mathlib/CategoryTheory/GradedObject.lean

@@ -310,7 +310,7 @@ variable {X Y} in
 lemma hasMap_of_iso (e : X ≅ Y) (p: I → J) [HasMap X p] : HasMap Y p := fun j => by
   have α : Discrete.functor (X.mapObjFun p j) ≅ Discrete.functor (Y.mapObjFun p j) :=
     Discrete.natIso (fun ⟨i, _⟩ => (GradedObject.eval i).mapIso e)
-  exact hasColimitOfIso α.symm
+  exact hasColimit_of_iso α.symm
 
 section
 variable [X.HasMap p] [Y.HasMap p]

Mathlib/CategoryTheory/Limits/Constructions/FiniteProductsOfBinaryProducts.lean

@@ -99,10 +99,10 @@ private theorem hasProduct_fin : ∀ (n : ℕ) (f : Fin n → C), HasProduct f
 
 /-- If `C` has a terminal object and binary products, then it has finite products. -/
 theorem hasFiniteProducts_of_has_binary_and_terminal : HasFiniteProducts C :=
-  ⟨fun n => ⟨fun K =>
-    let this := hasProduct_fin n fun n => K.obj ⟨n⟩
+  ⟨fun n => ⟨fun K => by
     let that : (Discrete.functor fun n => K.obj ⟨n⟩) ≅ K := Discrete.natIso fun ⟨_⟩ => Iso.refl _
-    @hasLimitOfIso _ _ _ _ _ _ this that⟩⟩
+    rw [← hasLimit_iff_of_iso that]
+    apply hasProduct_fin⟩⟩
 
 
 end
@@ -231,10 +231,10 @@ private theorem hasCoproduct_fin : ∀ (n : ℕ) (f : Fin n → C), HasCoproduct
 
 /-- If `C` has an initial object and binary coproducts, then it has finite coproducts. -/
 theorem hasFiniteCoproducts_of_has_binary_and_initial : HasFiniteCoproducts C :=
-  ⟨fun n => ⟨fun K =>
-    letI := hasCoproduct_fin n fun n => K.obj ⟨n⟩
+  ⟨fun n => ⟨fun K => by
     let that : K ≅ Discrete.functor fun n => K.obj ⟨n⟩ := Discrete.natIso fun ⟨_⟩ => Iso.refl _
-    @hasColimitOfIso _ _ _ _ _ _ this that⟩⟩
+    rw [hasColimit_iff_of_iso that]
+    apply hasCoproduct_fin⟩⟩
 
 end