∀ {G : Type u_3} [inst : Group G] {C : Type u_2} [inst_1 : CategoryTheory.Category.{u_1, u_2} C] (f : C → G) {X Y Z : C}
  (f_1 : X ⟶ Y) (g : Y ⟶ Z), f Z * (f X)⁻¹ = CategoryTheory.CategoryStruct.comp (f Y * (f X)⁻¹) (f Z * (f Y)⁻¹)