-- 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)
σ τ : Aut F
hst : σ ≈ τ
J' : SingleObj.{u₁}
    (HasQuotient.Quotient ↥(↑V : Subgroup (Aut F)) (B := Subgroup ↥(↑V : Subgroup (Aut F)))
      ((↑U : Subgroup (Aut F)).subgroupOf (↑V : Subgroup (Aut F)))) ⥤
  Action FintypeCat (Aut F) :=
  quotientDiag V h u ⋙ functorToAction F
m : End (C :=
  SingleObj.{u₁}
    (HasQuotient.Quotient ↥(↑V : Subgroup (Aut F)) (B := Subgroup ↥(↑V : Subgroup (Aut F)))
      ((↑U : Subgroup (Aut F)).subgroupOf (↑V : Subgroup (Aut F)))))
  (SingleObj.star
    (HasQuotient.Quotient ↥(↑V : Subgroup (Aut F)) (B := Subgroup ↥(↑V : Subgroup (Aut F)))
      ((↑U : Subgroup (Aut F)).subgroupOf (↑V : Subgroup (Aut F))))) :=
  ⟦Subtype.mk (p := fun (x : Aut F) ↦ x ∈ (↑V : Subgroup (Aut F))) (σ⁻¹ * τ) ⋯⟧
h1 :
  J'.map m ≫
      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.ι.app
      (SingleObj.star
        (HasQuotient.Quotient ↥(↑V : Subgroup (Aut F)) (B := Subgroup ↥(↑V : Subgroup (Aut F)))
          ((↑U : Subgroup (Aut F)).subgroupOf (↑V : Subgroup (Aut F)))))
h2 :
  Eq (α :=
    (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
      (J'.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)
    ((@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))
            _ _ _ (J'.map m).hom :
          (a :
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
                (J'.obj
                    (SingleObj.star
                      (↥(↑V : Subgroup (Aut F)) ⧸ (↑U : Subgroup (Aut F)).subgroupOf (↑V : Subgroup (Aut F))))).V) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
              (J'.obj
                  (SingleObj.star
                    (↥(↑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 :
              (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)
        (J'.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)
    ((@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)
⊢ Eq.{u₁ + 1} (α := s.pt.V.obj)
    ((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)
            ⟦σ⟧ :
          (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))
      σ)
    ((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))
                _ _ _
                (u.inv ≫
                    J'.map m ≫
                      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)))))).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)
                  (((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))
      τ)

Tactic:
simp [← h2, J']