Commit 2025-12-23 14:13 93d1225f

View on Github →

feat(CategoryTheory/Category/Basic): use to_dual (#33146) This PR tags Category and Epi/Mono with to_dual. This is the first step for using to_dual in category theory.

Estimated changes

Modified Mathlib/CategoryTheory/Category/Basic.lean

added theorem CategoryTheory.Category.assoc'

deleted theorem CategoryTheory.cancel_mono

deleted theorem CategoryTheory.cancel_mono_assoc_iff

deleted theorem CategoryTheory.cancel_mono_id

deleted theorem CategoryTheory.dite_comp

modified theorem CategoryTheory.epi_comp'

modified theorem CategoryTheory.epi_iff_forall_injective

modified theorem CategoryTheory.epi_of_epi

modified theorem CategoryTheory.epi_of_epi_fac

deleted theorem CategoryTheory.eq_of_comp_right_eq'

deleted theorem CategoryTheory.eq_of_comp_right_eq

deleted theorem CategoryTheory.id_of_comp_right_id

deleted theorem CategoryTheory.ite_comp

deleted theorem CategoryTheory.mono_comp'

deleted theorem CategoryTheory.mono_iff_forall_injective

deleted theorem CategoryTheory.mono_of_mono

deleted theorem CategoryTheory.mono_of_mono_fac

deleted theorem CategoryTheory.whisker_eq