[Merged by Bors] - feat(category_theory/groupoid): simplify groupoid.inv to category_theory.inv

[alreadydone]

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.

---

Allows to solve the following lemmas needed for #16611 by simp:

@[simp] lemma groupoid.inv_id  [G : groupoid.{v} C] (X : C) :
  G.inv (𝟙 X) = 𝟙 X := by simp

@[simp] lemma groupoid.inv_of_comp  [G : groupoid.{v} C]
  {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : G.inv (f ≫ g) = (G.inv g) ≫ (G.inv f) := by simp

@[simp] lemma groupoid.inv_inv  [G : groupoid.{v} C] (X Y : C) (f : X ⟶ Y) :
  G.inv (G.inv f) = f := by simp

@[simp]
lemma groupoid.functor_map_inv  [G : groupoid.{v} C] {D : Type u₂} [H : groupoid.{v₂} D]
  (φ : C ⥤ D) {c d : C} (f : c ⟶ d) :
  φ.map (G.inv f) = H.inv (φ.map f) := by simp

[kmill]

@rwbarton, @semorrison, or @dwarn: This seems like a reasonable simp normal form to me, but I'd like to run this design decision by at least one of you.

[jcommelin]

I suggest that we try this out. If it causes trouble, we remove it from the simp set.

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests