-- Module: Mathlib.CategoryTheory.Galois.Examples
Goal:
G : Type u
inst : Group G
X : FintypeCat
inst_1 : MulAction.{u, u_1} G X.obj
inst_2 : MulAction.IsPretransitive.{u, u_1} G X.obj
h : Nonempty.{u_1 + 1} X.obj
Y : Action FintypeCat G
i : Y ⟶ Action.FintypeCat.ofMulAction G X
hm : Mono i
hni : ∀ (a : IsInitial Y), False
y : Y.V.obj
x' : (Action.V (Action.FintypeCat.ofMulAction G X)).obj
x : X.obj :=
  (@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))
        _ _ _ i.hom :
      (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y.V) →
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (Action.FintypeCat.ofMulAction G X).V)
    y
σ : G
hσ : σ • x = x'
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))
          _ _ _
          (((Action.ρ (Action.FintypeCat.ofMulAction G X) :
                  MonoidHom.{u, u_1} G (End (Action.V (Action.FintypeCat.ofMulAction G X)))) :
                (a : G) → End (Action.FintypeCat.ofMulAction G X).V)
              σ :
            End (Action.V (Action.FintypeCat.ofMulAction G X))) :
        (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (Action.FintypeCat.ofMulAction G X).V) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (Action.FintypeCat.ofMulAction G X).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))
              _ _ _ i.hom :
            (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y.V) →
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (Action.FintypeCat.ofMulAction G X).V)
          y :
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (Action.V (Action.FintypeCat.ofMulAction G 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))
          _ _ _ ((Y.ρ : (a : G) → End Y.V) σ ≫ i.hom : Y.V ⟶ Action.V (Action.FintypeCat.ofMulAction G X)) :
        (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y.V) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (Action.FintypeCat.ofMulAction G X).V)
      y =
    x'

Tactic:
rw [i.comm, FintypeCat.comp_apply]

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