-- Module: Mathlib.CategoryTheory.Action.Concrete
Goal:
G : Type u_1
inst : Group G
H N : Subgroup G
inst_1 : Fintype (G ⧸ N)
inst_2 : N.Normal
σ τ : G
h :
  ∀ (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 { hom := FintypeCat.homMk (Quotient.lift (fun (σ_1 : G) ↦ ⟦σ_1 * (σ * τ)⁻¹⟧) ⋯), comm := ⋯ } :
                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))
              _ _ _
              (HMul.hMul (α := End (C := Action FintypeCat G) (ofMulAction G (FintypeCat.of (G ⧸ N))))
                  { hom := FintypeCat.homMk (Quotient.lift (fun (σ_1 : G) ↦ ⟦σ_1 * σ⁻¹⟧) ⋯), comm := ⋯ :
                    Hom (ofMulAction G (FintypeCat.of (G ⧸ N))) (ofMulAction G (FintypeCat.of (G ⧸ N))) }
                  { hom := FintypeCat.homMk (Quotient.lift (fun (σ : G) ↦ ⟦σ * τ⁻¹⟧) ⋯), comm := ⋯ :
                    Hom (ofMulAction G (FintypeCat.of (G ⧸ N))) (ofMulAction G (FintypeCat.of (G ⧸ N))) }).hom :
            (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)))))
⊢ Hom.hom { hom := FintypeCat.homMk (Quotient.lift (fun (σ_1 : G) ↦ ⟦σ_1 * (σ * τ)⁻¹⟧) ⋯), comm := ⋯ } =
    (HMul.hMul (α := End (C := Action FintypeCat G) (ofMulAction G (FintypeCat.of (G ⧸ N))))
        { hom := FintypeCat.homMk (Quotient.lift (fun (σ_1 : G) ↦ ⟦σ_1 * σ⁻¹⟧) ⋯), comm := ⋯ :
          Hom (ofMulAction G (FintypeCat.of (G ⧸ N))) (ofMulAction G (FintypeCat.of (G ⧸ N))) }
        { hom := FintypeCat.homMk (Quotient.lift (fun (σ : G) ↦ ⟦σ * τ⁻¹⟧) ⋯), comm := ⋯ :
          Hom (ofMulAction G (FintypeCat.of (G ⧸ N))) (ofMulAction G (FintypeCat.of (G ⧸ N))) }).hom

Tactic:
ext (x : G ⧸ N)