-- 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₁ :
  Eq (α := s.pt.V.obj)
    ((@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))))) ⟶
                                s.pt.V) :
                          (a : (ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑U : Subgroup (Aut F))))).V.obj) →
                            s.pt.V.obj)
                        ⟦σ⟧)
                    ⋯)) :
              (Cocone.pt (F := quotientDiag V h u ⋙ functorToAction F) (coconeQuotientDiag h u hUinV)).V ⟶ s.pt.V) :
          (a : (coconeQuotientDiag h u hUinV).pt.V.obj) → s.pt.V.obj)
        ⟦σ⟧ :
      s.pt.V.obj)
    ((@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))))) ⟶
                                s.pt.V) :
                          (a : (ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑U : Subgroup (Aut F))))).V.obj) →
                            s.pt.V.obj)
                        ⟦σ⟧)
                    ⋯))
                ((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 : (coconeQuotientDiag h u hUinV).pt.V.obj) → s.pt.V.obj)
        ⟦σ⟧ :
      s.pt.V.obj)
⊢ 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)
        ⟦σ⟧ :
      (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)
        ⟦σ⟧ :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) s.pt.V)

Tactic:
simp only [const_obj_obj]

Premises used: CategoryTheory.Functor.const_obj_obj