Commit 2026-06-16 12:08 2c3e688d

View on Github →

feat(CategoryTheory/Comma/Basic): use to_dual more (#40355) This PR continues tagging things about Comma with to_dual. This PR also expands the to_dual_name_hint syntax so that you can give multiple name hints with a single command, instead of having to repeat the command. This PR adds CategoryTheory.Comma.map_obj_hom', the dual of CategoryTheory.Comma.map_obj_hom.

Estimated changes

Modified Mathlib/CategoryTheory/Comma/Basic.lean

deleted theorem CategoryTheory.Comma.inv_left_hom_right

deleted theorem CategoryTheory.Comma.inv_right

deleted def CategoryTheory.Comma.mapRight

deleted def CategoryTheory.Comma.mapRightComp

deleted def CategoryTheory.Comma.mapRightEq

deleted def CategoryTheory.Comma.mapRightId

deleted def CategoryTheory.Comma.mapRightIso

deleted def CategoryTheory.Comma.mapSnd

added theorem CategoryTheory.Comma.map_obj_hom'

deleted theorem CategoryTheory.Comma.map_snd

deleted def CategoryTheory.Comma.preRight

deleted def CategoryTheory.Comma.preRightIso

deleted def CategoryTheory.Comma.rightIso

deleted def CategoryTheory.Comma.snd

Modified Mathlib/Order/Interval/Set/Disjoint.lean

Modified Mathlib/Tactic/Translate/ToDual.lean

Modified MathlibTest/Attribute/ToDual.lean