-- Module: Mathlib.CategoryTheory.Galois.Examples
Goal:
G : Type u
inst : Group G
X Y : Action FintypeCat G
f : X ⟶ Y
g : G
y : (FintypeCat.imageComplement f.hom).obj
x : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) X.V
h :
  Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y.V)
    ((@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.hom :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) X.V) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y.V)
        x :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y.V)
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (InducedCategory.Hom.hom (F := ObjectProperty.FullSubcategory.obj) ((Y.ρ : (a : G) → End Y.V) g)) :
          (a : (fun (X : Type u_1) ↦ X) Y.V.obj) → (fun (X : Type u_1) ↦ X) Y.V.obj)
        (↑y : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y.V) :
      (fun (X : Type u_1) ↦ X) Y.V.obj)
rw :
  Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y.V)
    ((@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))
            _ _ _ ((Y.ρ : (a : G) → End Y.V) g⁻¹ : End Y.V) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y.V) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y.V)
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (InducedCategory.Hom.hom (F := ObjectProperty.FullSubcategory.obj) ((Y.ρ : (a : G) → End Y.V) g)) :
              (a : (fun (X : Type u_1) ↦ X) Y.V.obj) → (fun (X : Type u_1) ↦ X) Y.V.obj)
            (↑y : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y.V) :
          (fun (X : Type u_1) ↦ X) Y.V.obj) :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y.V)
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            ((HMul.hMul (α := End Y.V) (β := End Y.V) ((Y.ρ : (a : G) → End Y.V) g⁻¹ : End Y.V)
                  ((Y.ρ : (a : G) → End Y.V) g : End Y.V)).hom
              (F := ObjectProperty.FullSubcategory.obj)) :
          (a : (fun (X : Type u_1) ↦ X) Y.V.obj) → (fun (X : Type u_1) ↦ X) Y.V.obj)
        (↑y : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y.V) :
      (fun (X : Type u_1) ↦ X) Y.V.obj)
⊢ Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y.V)
    ((@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))
            _ _ _ ((X.ρ : (a : G) → End X.V) g⁻¹ ≫ f.hom : X.V ⟶ Y.V) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) X.V) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y.V)
        x :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y.V)
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            ((HMul.hMul (α := End Y.V) (β := End Y.V) ((Y.ρ : (a : G) → End Y.V) g⁻¹ : End Y.V)
                  ((Y.ρ : (a : G) → End Y.V) g : End Y.V)).hom
              (F := ObjectProperty.FullSubcategory.obj)) :
          (a : (fun (X : Type u_1) ↦ X) Y.V.obj) → (fun (X : Type u_1) ↦ X) Y.V.obj)
        (↑y : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y.V) :
      (fun (X : Type u_1) ↦ X) Y.V.obj)

Tactic:
rw [f.comm, FintypeCat.comp_apply, h]

Premises used: FintypeCat.comp_apply, Action.Hom.comm