mathlib

c804ede6 - feat(category_theory/groupoid): simplify groupoid.inv to category_theory.inv (#16624)

feat(category_theory/groupoid): simplify groupoid.inv to category_theory.inv (#16624) Add simp lemma `groupoid.inv_eq_inv` to simplify `groupoid.inv` to `category_theory.inv` (which uses the `is_iso` instance) to gain access to the developed API around `category_theory.inv`. This isn't a defeq though so I can imagine sometimes we may want to `simp [-groupoid.inv_eq_inv]`, but most of the times this simp lemma makes things smoother.