-- Module: Mathlib.CategoryTheory.Action.Concrete
Goal:
G : Type u_1
inst : Group G
H N : Subgroup G
inst_1 : Fintype (G ⧸ N)
inst_2 : Fintype (G ⧸ H)
h : N ≤ H
g : G
x : G ⧸ N
h₁ :
  ∀ (a : G),
    Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (V (ofMulAction G (FintypeCat.of (G ⧸ H)))))
      ((@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))
              _ _ _
              (CategoryStruct.comp (Y := V (ofMulAction G (FintypeCat.of (G ⧸ N))))
                  ((ρ (ofMulAction G (FintypeCat.of (G ⧸ N))) : (a : G) → End (ofMulAction G (FintypeCat.of (G ⧸ N))).V)
                    g)
                  (FintypeCat.homMk (Quotient.lift (fun (x : G) ↦ ⟦x⟧) ⋯)) :
                V (ofMulAction G (FintypeCat.of (G ⧸ N))) ⟶ V (ofMulAction G (FintypeCat.of (G ⧸ H)))) :
            (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 ⧸ H))).V)
          ⟦a⟧ :
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (V (ofMulAction G (FintypeCat.of (G ⧸ H)))))
      ((@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))
              _ _ _
              (CategoryStruct.comp (Y := V (ofMulAction G (FintypeCat.of (G ⧸ H))))
                  (FintypeCat.homMk (Quotient.lift (fun (x : G) ↦ ⟦x⟧) ⋯))
                  ((ρ (ofMulAction G (FintypeCat.of (G ⧸ H))) : (a : G) → End (ofMulAction G (FintypeCat.of (G ⧸ H))).V)
                    g) :
                V (ofMulAction G (FintypeCat.of (G ⧸ N))) ⟶ V (ofMulAction G (FintypeCat.of (G ⧸ H)))) :
            (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 ⧸ H))).V)
          ⟦a⟧ :
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (V (ofMulAction G (FintypeCat.of (G ⧸ H)))))
⊢ Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (V (ofMulAction G (FintypeCat.of (G ⧸ H)))))
    ((@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))
            _ _ _
            (CategoryStruct.comp (Y := V (ofMulAction G (FintypeCat.of (G ⧸ N))))
                ((ρ (ofMulAction G (FintypeCat.of (G ⧸ N))) : (a : G) → End (ofMulAction G (FintypeCat.of (G ⧸ N))).V)
                  g)
                (FintypeCat.homMk (Quotient.lift (fun (x : G) ↦ ⟦x⟧) ⋯)) :
              V (ofMulAction G (FintypeCat.of (G ⧸ N))) ⟶ V (ofMulAction G (FintypeCat.of (G ⧸ H)))) :
          (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 ⧸ H))).V)
        x :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (V (ofMulAction G (FintypeCat.of (G ⧸ H)))))
    ((@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))
            _ _ _
            (CategoryStruct.comp (Y := V (ofMulAction G (FintypeCat.of (G ⧸ H))))
                (FintypeCat.homMk (Quotient.lift (fun (x : G) ↦ ⟦x⟧) ⋯))
                ((ρ (ofMulAction G (FintypeCat.of (G ⧸ H))) : (a : G) → End (ofMulAction G (FintypeCat.of (G ⧸ H))).V)
                  g) :
              V (ofMulAction G (FintypeCat.of (G ⧸ N))) ⟶ V (ofMulAction G (FintypeCat.of (G ⧸ H)))) :
          (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 ⧸ H))).V)
        x :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (V (ofMulAction G (FintypeCat.of (G ⧸ H)))))

Tactic:
induction x using Quotient.inductionOn