Commit 2022-09-30 13:10 c804ede6

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.