-- Module: Mathlib.CategoryTheory.Galois.EssSurj
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, u₁, u₁, u₁ + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
G : Type u_1
inst_3 : Group G
inst_4 : TopologicalSpace G
inst_5 : IsTopologicalGroup G
inst_6 : CompactSpace G
V U : OpenSubgroup (Aut F)
h : (↑U : Subgroup (Aut F)).Normal
A : C
u : (functorToAction F).obj A ≅ ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑U : Subgroup (Aut F))))
hUinV : U ≤ V
s : Cocone (quotientDiag V h u ⋙ functorToAction F)
g : Aut F
h₁ :
  ∀ (x : Aut F ⧸ (↑V : Subgroup (Aut F))),
    Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) s.pt.V)
      ((@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
              (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
              (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
                (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
              _ _ _
              (CategoryStruct.comp (Y :=
                  (Cocone.pt (F := quotientDiag V h u ⋙ functorToAction F) (coconeQuotientDiag h u hUinV)).V)
                  (((Cocone.pt (F := quotientDiag V h u ⋙ functorToAction F) (coconeQuotientDiag h u hUinV)).ρ :
                      (a : Aut F) → End (coconeQuotientDiag h u hUinV).pt.V)
                    g)
                  (FintypeCat.homMk
                    (Quotient.lift
                      (fun (σ : Aut F) ↦
                        (@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
                              (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
                              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
                              (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
                                (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
                              _ _ _
                              (Action.Hom.hom
                                  (u.inv ≫
                                    s.ι.app
                                      (SingleObj.star
                                        (HasQuotient.Quotient ↥(↑V : Subgroup (Aut F)) (B :=
                                          Subgroup ↥(↑V : Subgroup (Aut F)))
                                          ((↑U : Subgroup (Aut F)).subgroupOf (↑V : Subgroup (Aut F)))))) :
                                Action.V (G := Aut F)
                                    (ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑U : Subgroup (Aut F))))) ⟶
                                  (obj (C :=
                                      SingleObj.{u₁}
                                        (HasQuotient.Quotient ↥(↑V : Subgroup (Aut F)) (B :=
                                          Subgroup ↥(↑V : Subgroup (Aut F)))
                                          ((↑U : Subgroup (Aut F)).subgroupOf (↑V : Subgroup (Aut F)))))
                                      (obj
                                        (const
                                          (SingleObj.{u₁}
                                            (HasQuotient.Quotient ↥(↑V : Subgroup (Aut F)) (B :=
                                              Subgroup ↥(↑V : Subgroup (Aut F)))
                                              ((↑U : Subgroup (Aut F)).subgroupOf (↑V : Subgroup (Aut F))))))
                                        s.pt)
                                      (SingleObj.star
                                        (HasQuotient.Quotient ↥(↑V : Subgroup (Aut F)) (B :=
                                          Subgroup ↥(↑V : Subgroup (Aut F)))
                                          ((↑U : Subgroup (Aut F)).subgroupOf (↑V : Subgroup (Aut F)))))).V) :
                            (a :
                                (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
                                  (ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑U : Subgroup (Aut F))))).V) →
                              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
                                (((const
                                            (SingleObj
                                              (↥(↑V : Subgroup (Aut F)) ⧸
                                                (↑U : Subgroup (Aut F)).subgroupOf (↑V : Subgroup (Aut F))))).obj
                                        s.pt).obj
                                    (SingleObj.star
                                      (↥(↑V : Subgroup (Aut F)) ⧸
                                        (↑U : Subgroup (Aut F)).subgroupOf (↑V : Subgroup (Aut F))))).V)
                          ⟦σ⟧)
                      ⋯)) :
                (Cocone.pt (F := quotientDiag V h u ⋙ functorToAction F) (coconeQuotientDiag h u hUinV)).V ⟶ s.pt.V) :
            (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (coconeQuotientDiag h u hUinV).pt.V) →
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) s.pt.V)
          x :
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) s.pt.V)
      ((@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
              (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
              (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
                (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
              _ _ _
              (CategoryStruct.comp (Y := s.pt.V)
                  (FintypeCat.homMk
                    (Quotient.lift
                      (fun (σ : Aut F) ↦
                        (@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
                              (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
                              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
                              (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
                                (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
                              _ _ _
                              (Action.Hom.hom
                                  (u.inv ≫
                                    s.ι.app
                                      (SingleObj.star
                                        (HasQuotient.Quotient ↥(↑V : Subgroup (Aut F)) (B :=
                                          Subgroup ↥(↑V : Subgroup (Aut F)))
                                          ((↑U : Subgroup (Aut F)).subgroupOf (↑V : Subgroup (Aut F)))))) :
                                Action.V (G := Aut F)
                                    (ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑U : Subgroup (Aut F))))) ⟶
                                  (obj (C :=
                                      SingleObj.{u₁}
                                        (HasQuotient.Quotient ↥(↑V : Subgroup (Aut F)) (B :=
                                          Subgroup ↥(↑V : Subgroup (Aut F)))
                                          ((↑U : Subgroup (Aut F)).subgroupOf (↑V : Subgroup (Aut F)))))
                                      (obj
                                        (const
                                          (SingleObj.{u₁}
                                            (HasQuotient.Quotient ↥(↑V : Subgroup (Aut F)) (B :=
                                              Subgroup ↥(↑V : Subgroup (Aut F)))
                                              ((↑U : Subgroup (Aut F)).subgroupOf (↑V : Subgroup (Aut F))))))
                                        s.pt)
                                      (SingleObj.star
                                        (HasQuotient.Quotient ↥(↑V : Subgroup (Aut F)) (B :=
                                          Subgroup ↥(↑V : Subgroup (Aut F)))
                                          ((↑U : Subgroup (Aut F)).subgroupOf (↑V : Subgroup (Aut F)))))).V) :
                            (a :
                                (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
                                  (ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑U : Subgroup (Aut F))))).V) →
                              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
                                (((const
                                            (SingleObj
                                              (↥(↑V : Subgroup (Aut F)) ⧸
                                                (↑U : Subgroup (Aut F)).subgroupOf (↑V : Subgroup (Aut F))))).obj
                                        s.pt).obj
                                    (SingleObj.star
                                      (↥(↑V : Subgroup (Aut F)) ⧸
                                        (↑U : Subgroup (Aut F)).subgroupOf (↑V : Subgroup (Aut F))))).V)
                          ⟦σ⟧)
                      ⋯))
                  ((s.pt.ρ : (a : Aut F) → End s.pt.V) g) :
                (Cocone.pt (F := quotientDiag V h u ⋙ functorToAction F) (coconeQuotientDiag h u hUinV)).V ⟶ s.pt.V) :
            (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (coconeQuotientDiag h u hUinV).pt.V) →
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) s.pt.V)
          x :
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) s.pt.V)
⊢ Eq.{u₁ + 1} (α := (Cocone.pt (F := quotientDiag V h u ⋙ functorToAction F) (coconeQuotientDiag h u hUinV)).V ⟶ s.pt.V)
    (CategoryStruct.comp (Y :=
      (Cocone.pt (F := quotientDiag V h u ⋙ functorToAction F) (coconeQuotientDiag h u hUinV)).V)
      (((Cocone.pt (F := quotientDiag V h u ⋙ functorToAction F) (coconeQuotientDiag h u hUinV)).ρ :
          (a : Aut F) → End (coconeQuotientDiag h u hUinV).pt.V)
        g)
      (FintypeCat.homMk
        (Quotient.lift
          (fun (σ : Aut F) ↦
            (@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
                  (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
                  (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
                  (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
                    (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
                  _ _ _
                  (Action.Hom.hom
                      (u.inv ≫
                        s.ι.app
                          (SingleObj.star
                            (HasQuotient.Quotient ↥(↑V : Subgroup (Aut F)) (B := Subgroup ↥(↑V : Subgroup (Aut F)))
                              ((↑U : Subgroup (Aut F)).subgroupOf (↑V : Subgroup (Aut F)))))) :
                    Action.V (G := Aut F) (ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑U : Subgroup (Aut F))))) ⟶
                      (obj (C :=
                          SingleObj.{u₁}
                            (HasQuotient.Quotient ↥(↑V : Subgroup (Aut F)) (B := Subgroup ↥(↑V : Subgroup (Aut F)))
                              ((↑U : Subgroup (Aut F)).subgroupOf (↑V : Subgroup (Aut F)))))
                          (obj
                            (const
                              (SingleObj.{u₁}
                                (HasQuotient.Quotient ↥(↑V : Subgroup (Aut F)) (B := Subgroup ↥(↑V : Subgroup (Aut F)))
                                  ((↑U : Subgroup (Aut F)).subgroupOf (↑V : Subgroup (Aut F))))))
                            s.pt)
                          (SingleObj.star
                            (HasQuotient.Quotient ↥(↑V : Subgroup (Aut F)) (B := Subgroup ↥(↑V : Subgroup (Aut F)))
                              ((↑U : Subgroup (Aut F)).subgroupOf (↑V : Subgroup (Aut F)))))).V) :
                (a :
                    (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
                      (ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑U : Subgroup (Aut F))))).V) →
                  (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
                    (((const
                                (SingleObj
                                  (↥(↑V : Subgroup (Aut F)) ⧸
                                    (↑U : Subgroup (Aut F)).subgroupOf (↑V : Subgroup (Aut F))))).obj
                            s.pt).obj
                        (SingleObj.star
                          (↥(↑V : Subgroup (Aut F)) ⧸ (↑U : Subgroup (Aut F)).subgroupOf (↑V : Subgroup (Aut F))))).V)
              ⟦σ⟧)
          ⋯)))
    (CategoryStruct.comp (Y := s.pt.V)
      (FintypeCat.homMk
        (Quotient.lift
          (fun (σ : Aut F) ↦
            (@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
                  (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
                  (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
                  (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
                    (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
                  _ _ _
                  (Action.Hom.hom
                      (u.inv ≫
                        s.ι.app
                          (SingleObj.star
                            (HasQuotient.Quotient ↥(↑V : Subgroup (Aut F)) (B := Subgroup ↥(↑V : Subgroup (Aut F)))
                              ((↑U : Subgroup (Aut F)).subgroupOf (↑V : Subgroup (Aut F)))))) :
                    Action.V (G := Aut F) (ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑U : Subgroup (Aut F))))) ⟶
                      (obj (C :=
                          SingleObj.{u₁}
                            (HasQuotient.Quotient ↥(↑V : Subgroup (Aut F)) (B := Subgroup ↥(↑V : Subgroup (Aut F)))
                              ((↑U : Subgroup (Aut F)).subgroupOf (↑V : Subgroup (Aut F)))))
                          (obj
                            (const
                              (SingleObj.{u₁}
                                (HasQuotient.Quotient ↥(↑V : Subgroup (Aut F)) (B := Subgroup ↥(↑V : Subgroup (Aut F)))
                                  ((↑U : Subgroup (Aut F)).subgroupOf (↑V : Subgroup (Aut F))))))
                            s.pt)
                          (SingleObj.star
                            (HasQuotient.Quotient ↥(↑V : Subgroup (Aut F)) (B := Subgroup ↥(↑V : Subgroup (Aut F)))
                              ((↑U : Subgroup (Aut F)).subgroupOf (↑V : Subgroup (Aut F)))))).V) :
                (a :
                    (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
                      (ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑U : Subgroup (Aut F))))).V) →
                  (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
                    (((const
                                (SingleObj
                                  (↥(↑V : Subgroup (Aut F)) ⧸
                                    (↑U : Subgroup (Aut F)).subgroupOf (↑V : Subgroup (Aut F))))).obj
                            s.pt).obj
                        (SingleObj.star
                          (↥(↑V : Subgroup (Aut F)) ⧸ (↑U : Subgroup (Aut F)).subgroupOf (↑V : Subgroup (Aut F))))).V)
              ⟦σ⟧)
          ⋯))
      ((s.pt.ρ : (a : Aut F) → End s.pt.V) g))

Tactic:
ext (x : Aut F ⧸ V.toSubgroup)

Premises used: CategoryTheory.Aut, OpenSubgroup.toSubgroup