-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Concrete (goal)
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
inst_1 : Fintype (G ⧸ N)
inst_2 : N.Normal
n : G
hn : n ∈ N
x : G ⧸ N
⊢ Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (V (ofMulAction G (FintypeCat.of (G ⧸ N)))))
    ((@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.hom
                (((toEndHom N : G →* End (C := Action FintypeCat G) (ofMulAction G (FintypeCat.of (G ⧸ N)))) :
                    (a : G) → End (ofMulAction G (FintypeCat.of (G ⧸ N))))
                  n) :
              V (ofMulAction G (FintypeCat.of (G ⧸ N))) ⟶ V (ofMulAction G (FintypeCat.of (G ⧸ N)))) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (ofMulAction G (FintypeCat.of (G ⧸ N))).V) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (ofMulAction G (FintypeCat.of (G ⧸ N))).V)
        x :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (V (ofMulAction G (FintypeCat.of (G ⧸ N)))))
    ((@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.hom (𝟙 (ofMulAction G (FintypeCat.of (G ⧸ N)))) :
              V (ofMulAction G (FintypeCat.of (G ⧸ N))) ⟶ V (ofMulAction G (FintypeCat.of (G ⧸ N)))) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (ofMulAction G (FintypeCat.of (G ⧸ N))).V) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (ofMulAction G (FintypeCat.of (G ⧸ N))).V)
        x :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (V (ofMulAction G (FintypeCat.of (G ⧸ N)))))
have h : ∀ (a : G),
  Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (V (ofMulAction G (FintypeCat.of (G ⧸ N)))))
    ((@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.hom
                (((toEndHom N : G →* End (C := Action FintypeCat G) (ofMulAction G (FintypeCat.of (G ⧸ N)))) :
                    (a : G) → End (ofMulAction G (FintypeCat.of (G ⧸ N))))
                  n) :
              V (ofMulAction G (FintypeCat.of (G ⧸ N))) ⟶ V (ofMulAction G (FintypeCat.of (G ⧸ N)))) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (ofMulAction G (FintypeCat.of (G ⧸ N))).V) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (ofMulAction G (FintypeCat.of (G ⧸ N))).V)
        ⟦a⟧ :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (V (ofMulAction G (FintypeCat.of (G ⧸ N)))))
    ((@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.hom (𝟙 (ofMulAction G (FintypeCat.of (G ⧸ N)))) :
              V (ofMulAction G (FintypeCat.of (G ⧸ N))) ⟶ V (ofMulAction G (FintypeCat.of (G ⧸ N)))) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (ofMulAction G (FintypeCat.of (G ⧸ N))).V) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (ofMulAction G (FintypeCat.of (G ⧸ N))).V)
        ⟦a⟧ :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (V (ofMulAction G (FintypeCat.of (G ⧸ N)))))
Tactic: induction x using Quotient.inductionOn
Cleared hypotheses: x