-- 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)))
x : Aut F ⧸ (↑U : Subgroup (Aut F))
h₁ :
  ∀ (σ : ↥(↑V : Subgroup (Aut F))) (μ : Aut F),
    Eq (α :=
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
        (Action.V (G := Aut F) (ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑V : Subgroup (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 ≫
                      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 ⟦σ⟧))
                        (u.hom ≫ quotientToQuotientOfLE (↑V : Subgroup (Aut F)) (↑U : Subgroup (Aut F)) hUinV)) :
                  Action.V (G := Aut F) (ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑U : Subgroup (Aut F))))) ⟶
                    Action.V (G := Aut F) (ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑V : Subgroup (Aut F)))))) :
              TypeCat.Fun
                (Action.V (G := Aut F) (ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑U : Subgroup (Aut F)))))).obj
                (Action.V (G := Aut F) (ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑V : Subgroup (Aut F)))))).obj) :
            (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)
                (ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑V : Subgroup (Aut F))))).V)
          ⟦μ⟧ :
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
          (Action.V (G := Aut F) (ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑V : Subgroup (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 (quotientToQuotientOfLE (↑V : Subgroup (Aut F)) (↑U : Subgroup (Aut F)) hUinV) :
                  Action.V (G := Aut F) (ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑U : Subgroup (Aut F))))) ⟶
                    Action.V (G := Aut F) (ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑V : Subgroup (Aut F)))))) :
              TypeCat.Fun
                (Action.V (G := Aut F) (ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑U : Subgroup (Aut F)))))).obj
                (Action.V (G := Aut F) (ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑V : Subgroup (Aut F)))))).obj) :
            (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)
                (ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑V : Subgroup (Aut F))))).V)
          ⟦μ⟧ :
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
          (Action.V (G := Aut F) (ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑V : Subgroup (Aut F)))))))
⊢ Eq (α :=
    (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
      (Action.V (G := Aut F) (ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑V : Subgroup (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 ≫
                    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)) :
                Action.V (G := Aut F) (ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑U : Subgroup (Aut F))))) ⟶
                  Action.V (G := Aut F) (ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑V : Subgroup (Aut F)))))) :
            TypeCat.Fun
              (Action.V (G := Aut F) (ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑U : Subgroup (Aut F)))))).obj
              (Action.V (G := Aut F) (ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑V : Subgroup (Aut F)))))).obj) :
          (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)
              (ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑V : Subgroup (Aut F))))).V)
        x :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
        (Action.V (G := Aut F) (ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑V : Subgroup (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 (quotientToQuotientOfLE (↑V : Subgroup (Aut F)) (↑U : Subgroup (Aut F)) hUinV) :
                Action.V (G := Aut F) (ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑U : Subgroup (Aut F))))) ⟶
                  Action.V (G := Aut F) (ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑V : Subgroup (Aut F)))))) :
            TypeCat.Fun
              (Action.V (G := Aut F) (ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑U : Subgroup (Aut F)))))).obj
              (Action.V (G := Aut F) (ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑V : Subgroup (Aut F)))))).obj) :
          (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)
              (ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑V : Subgroup (Aut F))))).V)
        x :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
        (Action.V (G := Aut F) (ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑V : Subgroup (Aut F)))))))

Tactic:
induction m, x using Quotient.inductionOn₂ with | _ σ μ