∀ (C : Type u_1) [inst : CategoryTheory.Groupoid C] {X Y Z : Cᵒᵖ} (f : X ⟶ Y) (g : Y ⟶ Z),
  CategoryTheory.Groupoid.inv (CategoryTheory.CategoryStruct.comp f g).unop =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Groupoid.inv f.unop) (CategoryTheory.Groupoid.inv g.unop)