mathlib

489f5225 - feat(category_theory/subobject): API for working with inequalities (#6818)

feat(category_theory/subobject): API for working with inequalities (#6818) This PR adds two types of declarations: * Helper functions for showing that two subobjects are equal by giving a compatible isomorphism, and * functions `of_le`/`of_le_mk`/`of_mk_le`/`of_mk_le_mk` that produce a morphism between the underlying objects from a proof of `X ≤ Y`. These are in essence just thin wrappers around `underlying.map`.