Commit 2026-10-24 14:19 2141ed60

View on Github →

chore(CategoryTheory/Limits/Preserves/Basic): use to_dual (#44647) This PR uses to_dual for declarations about preserving limits and colimits.

Estimated changes

Modified Mathlib/CategoryTheory/Functor/ReflectsIso/Basic.lean

Modified Mathlib/CategoryTheory/Limits/Preserves/Basic.lean

deleted theorem CategoryTheory.Limits.PreservesColimit.mk'

deleted def CategoryTheory.Limits.isColimitOfPreserves

deleted def CategoryTheory.Limits.isColimitOfReflects

deleted theorem CategoryTheory.Limits.preservesColimit_iff_isColimit_mapCocone

deleted theorem CategoryTheory.Limits.preservesColimit_iff_of_iso_diagram

deleted theorem CategoryTheory.Limits.preservesColimit_iff_of_natIso

deleted theorem CategoryTheory.Limits.preservesColimit_of_iso_diagram

deleted theorem CategoryTheory.Limits.preservesColimit_of_natIso

deleted theorem CategoryTheory.Limits.preservesColimit_of_preserves_colimit_cocone

deleted theorem CategoryTheory.Limits.preservesColimit_of_reflects_of_preserves

deleted theorem CategoryTheory.Limits.preservesColimitsOfShape_iff_of_natIso

deleted theorem CategoryTheory.Limits.preservesColimitsOfShape_of_equiv

deleted theorem CategoryTheory.Limits.preservesColimitsOfShape_of_natIso

deleted theorem CategoryTheory.Limits.preservesColimitsOfShape_of_reflects_of_preserves

deleted theorem CategoryTheory.Limits.preservesColimitsOfSize_iff_of_natIso

deleted theorem CategoryTheory.Limits.preservesColimitsOfSize_of_univLE

deleted theorem CategoryTheory.Limits.preservesColimitsOfSize_shrink

deleted theorem CategoryTheory.Limits.preservesColimits_of_natIso

deleted theorem CategoryTheory.Limits.preservesColimits_of_reflects_of_preserves

deleted theorem CategoryTheory.Limits.preservesSmallestColimits_of_preservesColimits

deleted theorem CategoryTheory.Limits.reflectsColimit_of_iso_diagram

deleted theorem CategoryTheory.Limits.reflectsColimit_of_natIso

deleted theorem CategoryTheory.Limits.reflectsColimit_of_reflectsIsomorphisms

deleted theorem CategoryTheory.Limits.reflectsColimitsOfShape_of_equiv

deleted theorem CategoryTheory.Limits.reflectsColimitsOfShape_of_natIso

deleted theorem CategoryTheory.Limits.reflectsColimitsOfShape_of_reflectsIsomorphisms

deleted theorem CategoryTheory.Limits.reflectsColimitsOfSize_of_univLE

deleted theorem CategoryTheory.Limits.reflectsColimitsOfSize_shrink

deleted theorem CategoryTheory.Limits.reflectsColimits_of_natIso

deleted theorem CategoryTheory.Limits.reflectsColimits_of_reflectsIsomorphisms

deleted theorem CategoryTheory.Limits.reflectsSmallestColimits_of_reflectsColimits

Modified Mathlib/CategoryTheory/NatTrans.lean