-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.IsFundamentalgroup (goal)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
G : Type u_1
inst_1 : Group G
inst_2 : (X : C) → MulAction.{u_1, w} G (F.obj X).obj
inst_3 : IsNaturalSMul F G
inst_4 : GaloisCategory.{u₁, u₂} C
inst_5 : FiberFunctor F
inst_6 : TopologicalSpace G
inst_7 : IsTopologicalGroup G
inst_8 : CompactSpace G
inst_9 : ∀ (X : C), ContinuousSMul.{u_1, w} G (F.obj X).obj
h : ∀ (X : C) [IsGalois.{u₁, u₂} X], MulAction.IsPretransitive.{u_1, w} G (F.obj X).obj
t : Aut F
gi : (X : PointedGaloisObject F) → G
hgi :
  ∀ (X : PointedGaloisObject F) (x : (F.obj X.obj).obj),
    gi X • x =
      (@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))
            _ _ _ (t.hom.app X.obj : F.obj X.obj ⟶ F.obj X.obj) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X.obj)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X.obj))
        x
cl : (X : PointedGaloisObject F) → Set G :=
  fun (X : PointedGaloisObject F) ↦ gi X • (↑(MulAction.stabilizer G X.pt) : Set G)
c : Set G := ⋂ (i : PointedGaloisObject F), cl i
g : G
hg : g ∈ c
X : C
h_1 : IsGalois.{u₁, u₂} X
x : (F.obj X).obj
⊢ Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
    ((@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))
            _ _ _ (NatTrans.app (Iso.hom ((toAut F G : (a : G) → Aut F) g)) X : F.obj X ⟶ F.obj X) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
        x :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
    ((@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))
            _ _ _ (t.hom.app X) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
        x :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
have h₁ : g • x =
  (@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))
        _ _ _ (t.hom.app X) :
      (a : (F.obj X).obj) → (F.obj X).obj)
    x
Tactic: simp only [toAut_hom_app_apply]