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.





leanprover-community/mathlib,leanprover-community/mathlib