∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] {F : CategoryTheory.Functor C FintypeCat}
  [inst_1 : CategoryTheory.GaloisCategory C] [inst_2 : CategoryTheory.PreGaloisCategory.FiberFunctor F]
  (V : OpenSubgroup (CategoryTheory.Aut F)) {U : OpenSubgroup (CategoryTheory.Aut F)} (h : (↑U).Normal) {A : C}
  (u :
    (CategoryTheory.PreGaloisCategory.functorToAction F).obj A ≅
      Action.FintypeCat.ofMulAction (CategoryTheory.Aut F)
        { carrier := CategoryTheory.Aut F ⧸ ↑U, str := CategoryTheory.PreGaloisCategory.fintypeQuotient✝ U }),
  CategoryTheory.PreGaloisCategory.quotientToEndObjectHom✝ V h u =
    (((CategoryTheory.Functor.FullyFaithful.ofFullyFaithful
                      (CategoryTheory.PreGaloisCategory.functorToAction F)).mulEquivEnd
                  A).trans
              u.conj).symm.toMonoidHom.comp
      (Action.FintypeCat.quotientToEndHom ↑V ↑U)