∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.GaloisCategory C]
  (F : CategoryTheory.Functor C FintypeCat) (x x_1 : (CategoryTheory.PreGaloisCategory.PointedGaloisObject F)ᵒᵖ)
  (x_2 : x ⟶ x_1),
  CategoryTheory.CategoryStruct.comp
      (((CategoryTheory.PreGaloisCategory.PointedGaloisObject.incl F).op.comp CategoryTheory.coyoneda).map x_2)
      (match x_1 with
      | Opposite.op { obj := A, pt := a, isGalois := isGalois } =>
        { app := fun X f => (CategoryTheory.ConcreteCategory.hom (F.map f)) a, naturality := ⋯ }) =
    CategoryTheory.CategoryStruct.comp
      (match x with
      | Opposite.op { obj := A, pt := a, isGalois := isGalois } =>
        { app := fun X f => (CategoryTheory.ConcreteCategory.hom (F.map f)) a, naturality := ⋯ })
      (((CategoryTheory.Functor.const (CategoryTheory.PreGaloisCategory.PointedGaloisObject F)ᵒᵖ).obj
            (F.comp FintypeCat.incl)).map
        x_2)