feat(CategoryTheory/Limits/IsLimit): use to_dual on IsLimit (leanprover-community#36572)

JovanGerb · JovanGerb · commit f4001a93bf4e · 2026-06-23T12:20:09.000Z
This PR makes a start at translating `IsLimit` using `to_dual`.
diff --git a/Mathlib/Algebra/Category/Grp/LargeColimits.lean b/Mathlib/Algebra/Category/Grp/LargeColimits.lean
@@ -46,7 +46,7 @@ lemma isColimit_iff_bijective_desc [DecidableEq J] :
     apply ofHom_injective
     refine hc.hom_ext (fun j ↦ ?_)
     ext x
-    rw [ConcreteCategory.comp_apply, ConcreteCategory.comp_apply, ← Quot.ι_desc _ c j x]
+    erw [ConcreteCategory.comp_apply, ConcreteCategory.comp_apply, ← Quot.ι_desc _ c j x]
     exact DFunLike.congr_fun eq (Quot.ι F j x)
   · set c' : Cocone F :=
       { pt := AddCommGrpCat.of (ULift (AddCircle (1 : ℚ)))
diff --git a/Mathlib/Algebra/Category/ModuleCat/FilteredColimits.lean b/Mathlib/Algebra/Category/ModuleCat/FilteredColimits.lean
@@ -175,9 +175,10 @@ def colimitDesc (t : Cocone F) : colimit F ⟶ t.pt :=
         obtain ⟨j, x, rfl⟩ := M.mk_surjective F x
         simp [hf] }
 
+set_option backward.defeqAttrib.useBackward true in
 @[reassoc (attr := simp)]
 lemma ι_colimitDesc (t : Cocone F) (j : J) :
-    (colimitCocone F).ι.app j ≫ colimitDesc F t = t.ι.app j :=
+    dsimp% (colimitCocone F).ι.app j ≫ colimitDesc F t = t.ι.app j :=
   (forget₂ _ AddCommGrpCat).map_injective
     ((AddCommGrpCat.FilteredColimits.colimitCoconeIsColimit (F ⋙ forget₂ _ _)).fac _ _)
 
diff --git a/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Colim.lean b/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Colim.lean
@@ -109,7 +109,6 @@ short complex `c₁.pt ⟶ c₂.pt ⟶ c₃.pt`. -/
 @[simps]
 def colim.mapShortComplex : ShortComplex C :=
   ShortComplex.mk f g (hc₁.hom_ext (fun j ↦ by
-    dsimp
     rw [reassoc_of% (hf j), hg j, comp_zero, ← NatTrans.comp_app_assoc, S.zero,
       zero_app, zero_comp]))
 
diff --git a/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Connected.lean b/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Connected.lean
@@ -51,6 +51,7 @@ noncomputable def IsColimit.pullbackOfHasExactColimitsOfShape [HasPullbacks C]
   have := hc.isIso_colimMap_ι
   apply hpull.isIso_snd_of_isIso
 
+set_option backward.isDefEq.respectTransparency false in
 /-- Detecting equality of morphisms factoring through a connected colimit by pulling back along
 the inclusions of the colimit. -/
 theorem IsColimit.pullback_hom_ext [HasPullbacks C] [HasColimitsOfShape J C]
diff --git a/Mathlib/CategoryTheory/Limits/Cones.lean b/Mathlib/CategoryTheory/Limits/Cones.lean
@@ -151,13 +151,11 @@ instance inhabitedCone (F : Discrete PUnit ⥤ C) : Inhabited (Cone F) :=
   }⟩
 
 set_option backward.defeqAttrib.useBackward true in
-@[to_dual (attr := reassoc (attr := simp))]
+@[to_dual (attr := reassoc (attr := simp), elementwise)]
 theorem Cone.w {F : J ⥤ C} (c : Cone F) {j j' : J} (f : j ⟶ j') :
     dsimp% c.π.app j ≫ F.map f = c.π.app j' := by
   simpa using (c.π.naturality f).symm
 
-attribute [elementwise] Cocone.w Cone.w
-
 end
 
 variable {F : J ⥤ C}
diff --git a/Mathlib/CategoryTheory/Limits/IsLimit.lean b/Mathlib/CategoryTheory/Limits/IsLimit.lean
diff --git a/Mathlib/CategoryTheory/Limits/MonoCoprod.lean b/Mathlib/CategoryTheory/Limits/MonoCoprod.lean
@@ -76,6 +76,7 @@ instance {A B : C} [MonoCoprod C] [HasBinaryCoproduct A B] : Mono (coprod.inl :
 instance {A B : C} [MonoCoprod C] [HasBinaryCoproduct A B] : Mono (coprod.inr : B ⟶ A ⨿ B) :=
   binaryCofan_inr _ (colimit.isColimit _)
 
+set_option backward.isDefEq.respectTransparency false in
 theorem mono_inl_iff {A B : C} {c₁ c₂ : BinaryCofan A B} (hc₁ : IsColimit c₁) (hc₂ : IsColimit c₂) :
     Mono c₁.inl ↔ Mono c₂.inl := by
   suffices
diff --git a/Mathlib/CategoryTheory/Limits/MorphismProperty.lean b/Mathlib/CategoryTheory/Limits/MorphismProperty.lean
@@ -121,7 +121,7 @@ lemma CostructuredArrow.isClosedUnderColimitsOfShape {J : Type*} [Category* J]
       isColimitOfPreserves _ d.isColimit
     have heq : Y.hom = hd.desc { pt := X, ι := { app j := (d.diag.obj j).hom } } := by
       refine hd.hom_ext fun j ↦ ?_
-      simp only [Functor.const_obj_obj, IsColimit.fac]
+      simp only [IsColimit.fac]
       simp
     rw [P.costructuredArrowObj_iff, heq, ← hd.coconePointUniqueUpToIso_hom_desc (hc _),
       P.cancel_left_of_respectsIso]
diff --git a/Mathlib/CategoryTheory/Limits/Preserves/Basic.lean b/Mathlib/CategoryTheory/Limits/Preserves/Basic.lean
@@ -778,7 +778,7 @@ lemma isIso_app_coconePt_of_preservesColimit
     (isColimitOfPreserves L hc) (isColimitOfPreserves L' hc) (asIso (whiskerLeft K α))
   convert! (inferInstance : IsIso e.hom)
   apply (isColimitOfPreserves L hc).hom_ext fun j ↦ ?_
-  simp only [Functor.comp_obj, Functor.mapCocone_pt, Functor.const_obj_obj, Functor.mapCocone_ι_app,
+  simp only [Functor.comp_obj, Functor.mapCocone_pt, Functor.mapCocone_ι_app,
     NatTrans.naturality, IsColimit.coconePointsIsoOfNatIso_hom, asIso_hom, e]
   refine (((isColimitOfPreserves L hc).ι_map (L'.mapCocone c) (whiskerLeft K α) j).trans ?_).symm
   simp
diff --git a/Mathlib/CategoryTheory/Limits/Preserves/Bifunctor.lean b/Mathlib/CategoryTheory/Limits/Preserves/Bifunctor.lean
@@ -146,6 +146,7 @@ variable {c₁ : Cocone K₁} (hc₁ : IsColimit c₁)
   {c₃ : Cocone <| uncurry.obj (whiskeringLeft₂ C |>.obj K₁ |>.obj K₂ |>.obj G)}
   (hc₃ : IsColimit c₃)
 
+set_option backward.isDefEq.respectTransparency false in
 /-- Characterize the inverse direction of the isomorphism
 `PreservesColimit₂.isoObjCoconePointsOfIsColimit` w.r.t. the canonical maps to the colimit. -/
 @[reassoc (attr := simp)]
@@ -231,10 +232,9 @@ instance of_preservesColimits_in_each_variable
           apply (P j₁).hom_ext
           intro j₂
           haveI := (P j₁).fac s j₂
+          simp only [Functor.mapCocone_pt, Functor.mapCocone_ι_app, Q₀, s] at this
           simp only [Functor.mapCocone_pt,
-            Functor.const_obj_obj, Functor.mapCocone_ι_app, Q₀, s] at this
-          simp only [Functor.mapCocone_pt,
-            Functor.const_obj_obj, Functor.mapCocone_ι_app, NatTrans.naturality, this, Q₀, s])
+            Functor.mapCocone_ι_app, NatTrans.naturality, this, Q₀, s])
     ⟨IsColimit.ofCoconeUncurry P <| IsColimit.precomposeHomEquiv E₀ _ <|
       IsColimit.ofIsoColimit (isColimitOfPreserves _ hc₁) E₁.symm⟩
 
diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Grothendieck.lean b/Mathlib/CategoryTheory/Limits/Shapes/Grothendieck.lean
@@ -178,7 +178,7 @@ def isColimitCoconeOfFiberwiseCocone {c : Cocone (fiberwiseColimit G)} (hc : IsC
   desc s := hc.desc <| Cocone.mk s.pt <|
     { app := fun X => colimit.desc (Grothendieck.ι F X ⋙ G) (s.whisker _) }
   uniq s m hm := hc.hom_ext <| fun X => by
-    simp only [fiberwiseColimit_obj, Functor.const_obj_obj, IsColimit.fac]
+    simp only [fiberwiseColimit_obj, IsColimit.fac]
     simp only [coconeOfCoconeFiberwiseColimit_pt, Functor.const_obj_obj,
       coconeOfCoconeFiberwiseColimit_ι_app, Category.assoc] at hm
     ext d
diff --git a/Mathlib/CategoryTheory/Limits/Types/Colimits.lean b/Mathlib/CategoryTheory/Limits/Types/Colimits.lean
@@ -227,7 +227,7 @@ theorem jointly_surjective_of_isColimit {F : J ⥤ Type u} {t : Cocone F} (h : I
     (↾fun y ↦ ULift.up (y ≠ x)))
   · refine h.hom_ext fun j ↦ ?_
     ext y
-    simp only [Functor.const_obj_obj, TypeCat.Fun.toFun_apply, comp_apply, hom_ofHom,
+    simp only [TypeCat.Fun.toFun_apply, comp_apply, hom_ofHom,
       TypeCat.Fun.coe_mk, ne_eq, true_iff]
     exact hx j y
   · intro he
diff --git a/Mathlib/CategoryTheory/Monad/Limits.lean b/Mathlib/CategoryTheory/Monad/Limits.lean
@@ -413,11 +413,11 @@ def coconePoint : Coalgebra T where
   A := c.pt
   a := t.desc (newCocone D c)
   counit := t.hom_ext fun j ↦ by
-    simp only [Functor.comp_obj, forget_obj, Functor.id_obj, Functor.const_obj_obj,
+    simp only [Functor.comp_obj, forget_obj, Functor.id_obj,
       IsColimit.fac_assoc, newCocone_ι_app, assoc, NatTrans.naturality, Functor.id_map, comp_id]
     rw [← Category.assoc, (D.obj j).counit, Category.id_comp]
   coassoc := t.hom_ext fun j ↦ by
-    simp only [Functor.comp_obj, forget_obj, Functor.const_obj_obj, IsColimit.fac_assoc,
+    simp only [Functor.comp_obj, forget_obj, IsColimit.fac_assoc,
       newCocone_ι_app, assoc, NatTrans.naturality, Functor.comp_map]
     rw [← Category.assoc, (D.obj j).coassoc, ← Functor.map_comp, t.fac (newCocone D c) j,
       newCocone_ι_app, Functor.map_comp, assoc]
diff --git a/Mathlib/CategoryTheory/MorphismProperty/Limits.lean b/Mathlib/CategoryTheory/MorphismProperty/Limits.lean
@@ -517,6 +517,7 @@ inductive colimitsOfShape : MorphismProperty C
     (h₁ : IsColimit c₁) (h₂ : IsColimit c₂) (f : X₁ ⟶ X₂) (_ : W.functorCategory J f) :
       colimitsOfShape (h₁.desc (Cocone.mk _ (f ≫ c₂.ι)))
 
+set_option backward.isDefEq.respectTransparency false in
 variable {W J} in
 lemma colimitsOfShape.mk' (X₁ X₂ : J ⥤ C) (c₁ : Cocone X₁) (c₂ : Cocone X₂)
     (h₁ : IsColimit c₁) (h₂ : IsColimit c₂) (f : X₁ ⟶ X₂) (hf : W.functorCategory J f)
@@ -599,6 +600,7 @@ class IsStableUnderColimitsOfShape : Prop where
     (h₁ : IsColimit c₁) (h₁ : IsColimit c₂) (f : X₁ ⟶ X₂) (_ : W.functorCategory J f)
     (φ : c₁.pt ⟶ c₂.pt) (hφ : ∀ j, c₁.ι.app j ≫ φ = f.app j ≫ c₂.ι.app j) : W φ
 
+set_option backward.isDefEq.respectTransparency false in
 lemma isStableUnderColimitsOfShape_iff_colimitsOfShape_le :
     W.IsStableUnderColimitsOfShape J ↔ W.colimitsOfShape J ≤ W := by
   constructor
@@ -668,6 +670,7 @@ lemma coproducts_of_small {X Y : C} (f : X ⟶ Y) {J : Type w'}
   rwa [← W.colimitsOfShape_eq_of_equivalence (Discrete.equivalence (equivShrink.{w} J))]
 
 set_option backward.defeqAttrib.useBackward true in
+set_option backward.isDefEq.respectTransparency false in
 lemma le_colimitsOfShape_punit : W ≤ W.colimitsOfShape (Discrete PUnit.{w + 1}) := by
   intro X₁ X₂ f hf
   have h := initialIsInitial (C := Discrete (PUnit.{w + 1}))
diff --git a/Mathlib/CategoryTheory/Presentable/ColimitPresentation.lean b/Mathlib/CategoryTheory/Presentable/ColimitPresentation.lean
@@ -151,7 +151,7 @@ def bind {X : C} (P : ColimitPresentation J X) (Q : ∀ j, ColimitPresentation (
   isColimit.fac := fun c ⟨j, i⟩ ↦ by simp [P.isColimit.fac, (Q j).isColimit.fac]
   isColimit.uniq c m hm := by
     refine P.isColimit.hom_ext fun j ↦ ?_
-    simp only [Functor.const_obj_obj, P.isColimit.fac]
+    simp only [P.isColimit.fac]
     refine (Q j).isColimit.hom_ext fun i ↦ ?_
     simpa [(Q j).isColimit.fac] using hm (.mk _ j i)
 
diff --git a/Mathlib/Condensed/Discrete/Colimit.lean b/Mathlib/Condensed/Discrete/Colimit.lean
@@ -62,6 +62,7 @@ noncomputable def isColimitLocallyConstantPresheaf (hc : IsLimit c) [∀ i, Epi
     dsimp
     rwa [dsimp% c.w, dsimp% c.w]
 
+set_option backward.isDefEq.respectTransparency false in
 @[simp]
 lemma isColimitLocallyConstantPresheaf_desc_apply (hc : IsLimit c) [∀ i, Epi (c.π.app i)]
     (s : Cocone ((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X))
@@ -349,6 +350,7 @@ noncomputable def isColimitLocallyConstantPresheaf (hc : IsLimit c) [∀ i, Epi
     dsimp
     rwa [dsimp% c.w, dsimp% c.w]
 
+set_option backward.isDefEq.respectTransparency false in
 @[simp]
 lemma isColimitLocallyConstantPresheaf_desc_apply (hc : IsLimit c) [∀ i, Epi (c.π.app i)]
     (s : Cocone ((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X))
@@ -366,6 +368,7 @@ noncomputable def isColimitLocallyConstantPresheafDiagram (S : LightProfinite) :
   (Functor.Final.isColimitWhiskerEquiv (opOpEquivalence ℕ).inverse _).symm
     (isColimitLocallyConstantPresheaf _ _ S.asLimit)
 
+set_option backward.isDefEq.respectTransparency false in
 @[simp]
 lemma isColimitLocallyConstantPresheafDiagram_desc_apply (S : LightProfinite)
     (s : Cocone (S.diagram.rightOp ⋙ locallyConstantPresheaf X))
