mathlib

206ecce7 - chore(category_theory/subobject): different proof of le_of_comm (#7229)

chore(category_theory/subobject): different proof of le_of_comm (#7229) This is certainly a shorter proof of `le_of_comm`; whether it is "cleaner" like the comment asked for is perhaps a matter of taste.