-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Examples (goal)
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'
⊢ (@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'
have 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'
Tactic: rw [i.comm, FintypeCat.comp_apply]