-- 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
m :
  HasQuotient.Quotient ↥V (B := Subgroup ↥(↑V : Subgroup (Aut F)))
    ((↑U : Subgroup (Aut F)).subgroupOf (↑V : Subgroup (Aut F)))
simp :
  Eq (α :=
    (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))))) ⟶
      ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑V : Subgroup (Aut F)))))
    (CategoryStruct.comp (Y :=
        (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))))))
        ((functorToAction F).map ((quotientDiag V h u).map m))
        (u.hom ≫ quotientToQuotientOfLE (↑V : Subgroup (Aut F)) (↑U : Subgroup (Aut F)) hUinV) :
      (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))))) ⟶
        ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑V : Subgroup (Aut F)))))
    (u.hom ≫ quotientToQuotientOfLE (↑V : Subgroup (Aut F)) (↑U : Subgroup (Aut F)) hUinV :
      (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))))) ⟶
        ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑V : Subgroup (Aut F)))))
⊢ Eq (α :=
    (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))))) ⟶
      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))))))
          (ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑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))))))
    (CategoryStruct.comp (Y :=
        (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))))))
        ((quotientDiag V h u ⋙ functorToAction F).map m)
        (u.hom ≫ quotientToQuotientOfLE (↑V : Subgroup (Aut F)) (↑U : Subgroup (Aut F)) hUinV) :
      (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))))) ⟶
        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))))))
            (ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑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))))))
    (CategoryStruct.comp (Y :=
        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))))))
            (ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑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))))))
        (u.hom ≫ quotientToQuotientOfLE (↑V : Subgroup (Aut F)) (↑U : Subgroup (Aut F)) hUinV :
          (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))))) ⟶
            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))))))
                (ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑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))))))
        (map
            (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))))))
              (ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑V : Subgroup (Aut F))))))
            m :
          Quiver.Hom (V := Action FintypeCat (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))))))
                (ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑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))))))
            (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))))))
                (ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑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))))))) :
      (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))))) ⟶
        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))))))
            (ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑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))))))

Tactic:
simp only [const_obj_obj, Functor.comp_map, const_obj_map, Category.comp_id]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Functor.const_obj_obj, CategoryTheory.Functor.const_obj_map, CategoryTheory.Functor.comp_map