-- 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_2 : ∀ (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_1 : (F.obj A).obj
U : OpenSubgroup (Aut F) := { toSubgroup := MulAction.stabilizer (Aut F) a_1, 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_1))) :=
  fiberIsoQuotientStabilizer A a_1
hUnormal : (↑U : Subgroup (Aut F)).Normal
h1 : ∀ (σ : Aut F) (σinU : σ ∈ U), σ.hom.app A = 𝟙 (F.obj A)
σ : Aut F
σinU : σ ∈ U
X : C
hX : X ∈ I
p : A ⟶ X := f ≫ Pi.π (fun (Z : (↑I : Type u₁)) ↦ (↑Z : C)) (Subtype.mk (p := fun (x : C) ↦ x ∈ I) X hX)
this : IsConnected.{u₁, u₂} X
a : (F.obj A).obj
⊢ Eq (α :=
    (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
      (F.obj (↑(Subtype.mk (p := fun (x : C) ↦ x ∈ I) X hX) : C)))
    ((@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))
            _ _ _
            (σ.hom.app (↑(Subtype.mk (p := fun (x : C) ↦ x ∈ I) X hX) : C) :
              F.obj (↑(Subtype.mk (p := fun (x : C) ↦ x ∈ I) X hX) : C) ⟶
                F.obj (↑(Subtype.mk (p := fun (x : C) ↦ x ∈ I) X hX) : C)) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj (↑⟨X, hX⟩ : C))) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj (↑⟨X, hX⟩ : C)))
        ((@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))
                _ _ _ (F.map p) :
              (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
                (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
            a :
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)) :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
        (F.obj (↑(Subtype.mk (p := fun (x : C) ↦ x ∈ I) X hX) : C)))
    ((@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))
            _ _ _
            (𝟙 (F.obj (↑(Subtype.mk (p := fun (x : C) ↦ x ∈ I) X hX) : C)) :
              F.obj (↑(Subtype.mk (p := fun (x : C) ↦ x ∈ I) X hX) : C) ⟶
                F.obj (↑(Subtype.mk (p := fun (x : C) ↦ x ∈ I) X hX) : C)) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj (↑⟨X, hX⟩ : C))) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj (↑⟨X, hX⟩ : C)))
        ((@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))
                _ _ _ (F.map p) :
              (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
                (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
            a :
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)) :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
        (F.obj (↑(Subtype.mk (p := fun (x : C) ↦ x ∈ I) X hX) : C)))

Tactic:
simp only [FintypeCat.id_apply, NatTrans.naturality_apply, h1 σ σinU]

Premises used: CategoryTheory.NatTrans.naturality_apply, FintypeCat.id_apply