Commit 2026-08-02 09:28 e75dd843

View on Github →

chore(CategoryTheory/Limits/HasLimit): use to_dual (#41017) This PR uses to_dual to generate stuff about HasColimit from HasLimit.

Estimated changes

Modified Mathlib/CategoryTheory/Functor/Const.lean

Modified Mathlib/CategoryTheory/Limits/Constructions/FiniteProductsOfBinaryProducts.lean

Modified Mathlib/CategoryTheory/Limits/HasLimits.lean

deleted def CategoryTheory.Limits.HasColimit.isoOfNatIso

deleted theorem CategoryTheory.Limits.HasColimit.mk

deleted theorem CategoryTheory.Limits.HasColimits.hasColimitsOfShape

deleted def CategoryTheory.Limits.colimMap

deleted def CategoryTheory.Limits.colimit.cocone

deleted def CategoryTheory.Limits.colimit.coconeMorphism

deleted theorem CategoryTheory.Limits.colimit.coconeMorphism_hom

deleted theorem CategoryTheory.Limits.colimit.cocone_x

deleted theorem CategoryTheory.Limits.colimit.cocone_ι

deleted theorem CategoryTheory.Limits.colimit.comp_coconePointUniqueUpToIso_hom

deleted theorem CategoryTheory.Limits.colimit.comp_coconePointUniqueUpToIso_inv

deleted def CategoryTheory.Limits.colimit.desc

deleted theorem CategoryTheory.Limits.colimit.desc_cocone

deleted theorem CategoryTheory.Limits.colimit.desc_extend

deleted theorem CategoryTheory.Limits.colimit.existsUnique

deleted theorem CategoryTheory.Limits.colimit.hom_ext

deleted def CategoryTheory.Limits.colimit.isColimit

deleted theorem CategoryTheory.Limits.colimit.isColimit_desc

deleted def CategoryTheory.Limits.colimit.isoColimitCocone

deleted theorem CategoryTheory.Limits.colimit.isoColimitCocone_ι_hom

deleted theorem CategoryTheory.Limits.colimit.isoColimitCocone_ι_inv

deleted theorem CategoryTheory.Limits.colimit.map_desc

deleted theorem CategoryTheory.Limits.colimit.w

deleted def CategoryTheory.Limits.colimit.ι

deleted theorem CategoryTheory.Limits.colimit.ι_coconeMorphism

deleted theorem CategoryTheory.Limits.colimit.ι_desc

deleted def CategoryTheory.Limits.colimit

deleted def CategoryTheory.Limits.getColimitCocone

deleted theorem CategoryTheory.Limits.hasColimit_iff_of_iso

deleted theorem CategoryTheory.Limits.ι_colimMap

Modified Mathlib/CategoryTheory/Limits/IsLimit.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/Reflexive.lean

Modified Mathlib/Tactic/Translate/ToDual.lean