∀ {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 })
  (x : CategoryTheory.SingleObj (↥↑V ⧸ (↑U).subgroupOf ↑V)),
  (CategoryTheory.PreGaloisCategory.quotientDiag✝ V h u).obj x = A