∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.GaloisCategory C]
  (F : CategoryTheory.Functor C FintypeCat) {X Y Z : CategoryTheory.PreGaloisCategory.PointedGaloisObject F} (f : X ⟶ Y)
  (g : Y ⟶ Z),
  (match CategoryTheory.CategoryStruct.comp f g with
    | { val := f, comp := comp } => f) =
    CategoryTheory.CategoryStruct.comp
      (match f with
      | { val := f, comp := comp } => f)
      (match g with
      | { val := f, comp := comp } => f)