-- 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
this :
  Eq (α :=
    ((functorToAction F).obj A).V ⟶
      (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)
    ((((functorToAction F).obj A).ρ : (a : Aut F) → End ((functorToAction F).obj A).V) g ≫
        Action.Hom.hom
          (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)))))) :
      ((functorToAction F).obj A).V ⟶
        (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)
    (Action.Hom.hom
          (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)))))) ≫
        (s.pt.ρ : (a : Aut F) → End s.pt.V) g :
      ((quotientDiag V h u ⋙ functorToAction F).obj
            (SingleObj.star
              (HasQuotient.Quotient ↥(↑V : Subgroup (Aut F)) (B := Subgroup ↥(↑V : Subgroup (Aut F)))
                ((↑U : Subgroup (Aut F)).subgroupOf (↑V : Subgroup (Aut F)))))).V ⟶
        s.pt.V)
h₁ :
  Eq (α :=
    (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
      (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)
    ((@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))
            _ _ _
            ((u.inv.hom ≫ (((functorToAction F).obj A).ρ : (a : Aut F) → End ((functorToAction F).obj A).V) g) ≫
                Action.Hom.hom
                  (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)
        ⟦σ⟧ :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
        (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)
    (((@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))
              _ _ _
              ((((functorToAction F).obj A).ρ : (a : Aut F) → End ((functorToAction F).obj A).V) g ≫
                  Action.Hom.hom
                    (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)))))) :
                ((functorToAction F).obj A).V ⟶
                  (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) :
            TypeCat.Fun
              ((quotientDiag V h u ⋙ functorToAction F).obj
                    (SingleObj.star
                      (HasQuotient.Quotient ↥(↑V : Subgroup (Aut F)) (B := Subgroup ↥(↑V : Subgroup (Aut F)))
                        ((↑U : Subgroup (Aut F)).subgroupOf (↑V : Subgroup (Aut F)))))).V.obj
              s.pt.V.obj) :
          (a :
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
                ((quotientDiag V h u ⋙ functorToAction F).obj
                    (SingleObj.star
                      (↥(↑V : Subgroup (Aut F)) ⧸ (↑U : Subgroup (Aut F)).subgroupOf (↑V : Subgroup (Aut F))))).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))
                _ _ _ u.inv.hom :
              (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) ((functorToAction F).obj A).V)
            ⟦σ⟧ :
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) ((functorToAction F).obj A).V) :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) s.pt.V)
⊢ Eq (α :=
    (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
      (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)
    ((@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.ρ (ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑U : Subgroup (Aut F))))) :
                      (a : Aut F) → End (ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑U : Subgroup (Aut F))))).V)
                    g ≫
                  u.inv.hom) ≫
                Action.Hom.hom
                  (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)
        ⟦σ⟧ :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
        (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)
    ((@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
                  (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)))))) ≫
                (s.pt.ρ : (a : Aut F) → End s.pt.V) g :
              ((quotientDiag V h u ⋙ functorToAction F).obj
                    (SingleObj.star
                      (HasQuotient.Quotient ↥(↑V : Subgroup (Aut F)) (B := Subgroup ↥(↑V : Subgroup (Aut F)))
                        ((↑U : Subgroup (Aut F)).subgroupOf (↑V : Subgroup (Aut F)))))).V ⟶
                s.pt.V) :
          (a :
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
                ((quotientDiag V h u ⋙ functorToAction F).obj
                    (SingleObj.star
                      (↥(↑V : Subgroup (Aut F)) ⧸ (↑U : Subgroup (Aut F)).subgroupOf (↑V : Subgroup (Aut F))))).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))
                _ _ _ u.inv.hom :
              (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) ((functorToAction F).obj A).V)
            ⟦σ⟧ :
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) ((functorToAction F).obj A).V) :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) s.pt.V)

Tactic:
rw [← this, u.inv.comm g]

Premises used: CategoryTheory.Iso.inv, Action.Hom.comm