-- 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
V : OpenSubgroup (Aut F)
I : Set C
hf : Fintype (↑I : Type u₁)
hc : ∀ X ∈ I, IsConnected.{u₁, u₂} X
hi : ∀ (σ : Aut F), (∀ (X : (↑I : Type u₁)), σ.hom.app (↑X : C) = 𝟙 (F.obj (↑X : C))) → σ ∈ (↑V : Set (Aut F))
this_1 : ∀ (X : (↑I : Type u₁)), IsConnected.{u₁, u₂} (↑X : C)
this : ∀ (X : (↑I : Type u₁)), Nonempty.{u₁ + 1} (F.obj (↑X : C)).obj
hn : Nonempty.{u₁ + 1} (F.obj (piObj.{u₁, u₂, u₁} fun (X : (↑I : Type u₁)) ↦ (↑X : C))).obj
A : C
f : A ⟶ piObj.{u₁, u₂, u₁} fun (X : (↑I : Type u₁)) ↦ (↑X : C)
hgal : IsGalois.{u₁, u₂} A
a : (F.obj A).obj
U : OpenSubgroup (Aut F) := { toSubgroup := MulAction.stabilizer (Aut F) a, isOpen' := ⋯ }
u : (functorToAction F).obj A ≅
  Action.FintypeCat.ofMulAction (Aut F)
    (FintypeCat.of (HasQuotient.Quotient (Aut F) (B := Subgroup (Aut F)) (MulAction.stabilizer (Aut F) a))) :=
  fiberIsoQuotientStabilizer A a
hUnormal : (↑U : Subgroup (Aut F)).Normal
σ : Aut F
σinU : σ ∈ U
x :
  (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
    (Action.V (G := Aut F)
      (Action.FintypeCat.ofMulAction (Aut F)
        (FintypeCat.of (HasQuotient.Quotient (Aut F) (B := Subgroup (Aut F)) (MulAction.stabilizer (Aut F) a)))))
h :
  ∀ (τ : Aut F),
    Eq (α :=
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
        (Action.V (G := Aut F)
          (Action.FintypeCat.ofMulAction (Aut F)
            (FintypeCat.of (HasQuotient.Quotient (Aut F) (B := Subgroup (Aut F)) (MulAction.stabilizer (Aut F) a))))))
      ((@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.ρ
                      (Action.FintypeCat.ofMulAction (Aut F)
                        (FintypeCat.of
                          (HasQuotient.Quotient (Aut F) (B := Subgroup (Aut F)) (MulAction.stabilizer (Aut F) a)))) :
                    (a_1 : Aut F) →
                      End
                        (Action.FintypeCat.ofMulAction (Aut F)
                            (FintypeCat.of (Aut F ⧸ MulAction.stabilizer (Aut F) a))).V)
                  σ :
                End
                  (Action.V (G := Aut F)
                    (Action.FintypeCat.ofMulAction (Aut F)
                      (FintypeCat.of
                        (HasQuotient.Quotient (Aut F) (B := Subgroup (Aut F)) (MulAction.stabilizer (Aut F) a)))))) :
            (a_1 :
                (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
                  (Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ MulAction.stabilizer (Aut F) a))).V) →
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
                (Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ MulAction.stabilizer (Aut F) a))).V)
          ⟦τ⟧ :
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
          (Action.V (G := Aut F)
            (Action.FintypeCat.ofMulAction (Aut F)
              (FintypeCat.of (HasQuotient.Quotient (Aut F) (B := Subgroup (Aut F)) (MulAction.stabilizer (Aut F) a))))))
      ((@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.V (G := Aut F)
                    (Action.FintypeCat.ofMulAction (Aut F)
                      (FintypeCat.of
                        (HasQuotient.Quotient (Aut F) (B := Subgroup (Aut F)) (MulAction.stabilizer (Aut F) a))))) :
                Action.V (G := Aut F)
                    (Action.FintypeCat.ofMulAction (Aut F)
                      (FintypeCat.of
                        (HasQuotient.Quotient (Aut F) (B := Subgroup (Aut F)) (MulAction.stabilizer (Aut F) a)))) ⟶
                  Action.V (G := Aut F)
                    (Action.FintypeCat.ofMulAction (Aut F)
                      (FintypeCat.of
                        (HasQuotient.Quotient (Aut F) (B := Subgroup (Aut F)) (MulAction.stabilizer (Aut F) a))))) :
            (a_1 :
                (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
                  (Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ MulAction.stabilizer (Aut F) a))).V) →
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
                (Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ MulAction.stabilizer (Aut F) a))).V)
          ⟦τ⟧ :
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
          (Action.V (G := Aut F)
            (Action.FintypeCat.ofMulAction (Aut F)
              (FintypeCat.of (HasQuotient.Quotient (Aut F) (B := Subgroup (Aut F)) (MulAction.stabilizer (Aut F) a))))))
⊢ Eq (α :=
    (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
      (Action.V (G := Aut F)
        (Action.FintypeCat.ofMulAction (Aut F)
          (FintypeCat.of (HasQuotient.Quotient (Aut F) (B := Subgroup (Aut F)) (MulAction.stabilizer (Aut F) a))))))
    ((@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.ρ
                    (Action.FintypeCat.ofMulAction (Aut F)
                      (FintypeCat.of
                        (HasQuotient.Quotient (Aut F) (B := Subgroup (Aut F)) (MulAction.stabilizer (Aut F) a)))) :
                  (a_1 : Aut F) →
                    End
                      (Action.FintypeCat.ofMulAction (Aut F)
                          (FintypeCat.of (Aut F ⧸ MulAction.stabilizer (Aut F) a))).V)
                σ :
              End
                (Action.V (G := Aut F)
                  (Action.FintypeCat.ofMulAction (Aut F)
                    (FintypeCat.of
                      (HasQuotient.Quotient (Aut F) (B := Subgroup (Aut F)) (MulAction.stabilizer (Aut F) a)))))) :
          (a_1 :
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
                (Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ MulAction.stabilizer (Aut F) a))).V) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
              (Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ MulAction.stabilizer (Aut F) a))).V)
        x :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
        (Action.V (G := Aut F)
          (Action.FintypeCat.ofMulAction (Aut F)
            (FintypeCat.of (HasQuotient.Quotient (Aut F) (B := Subgroup (Aut F)) (MulAction.stabilizer (Aut F) a))))))
    ((@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.V (G := Aut F)
                  (Action.FintypeCat.ofMulAction (Aut F)
                    (FintypeCat.of
                      (HasQuotient.Quotient (Aut F) (B := Subgroup (Aut F)) (MulAction.stabilizer (Aut F) a))))) :
              Action.V (G := Aut F)
                  (Action.FintypeCat.ofMulAction (Aut F)
                    (FintypeCat.of
                      (HasQuotient.Quotient (Aut F) (B := Subgroup (Aut F)) (MulAction.stabilizer (Aut F) a)))) ⟶
                Action.V (G := Aut F)
                  (Action.FintypeCat.ofMulAction (Aut F)
                    (FintypeCat.of
                      (HasQuotient.Quotient (Aut F) (B := Subgroup (Aut F)) (MulAction.stabilizer (Aut F) a))))) :
          (a_1 :
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
                (Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ MulAction.stabilizer (Aut F) a))).V) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
              (Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ MulAction.stabilizer (Aut F) a))).V)
        x :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
        (Action.V (G := Aut F)
          (Action.FintypeCat.ofMulAction (Aut F)
            (FintypeCat.of (HasQuotient.Quotient (Aut F) (B := Subgroup (Aut F)) (MulAction.stabilizer (Aut F) a))))))

Tactic:
induction x using Quotient.inductionOn with | _ τ