-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Images (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F G : Functor.{v_1, u, u_1, u + 1} C (Type u)
f : F ⟶ G
H : MonoFactorisation f
X Y : C
g : X ⟶ Y
x : (monoFactorisation f).I.obj X
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((monoFactorisation f).I.map g ≫
          ↾fun (x : (monoFactorisation f).I.obj Y) ↦
            match (motive := (monoFactorisation f).I.obj Y → H.I.obj Y) x with
            | ⟨x, hx⟩ =>
              (ConcreteCategory.hom (FC := TypeCat.Fun) (H.e.app Y) :
                  (a : (fun (X : Type u) ↦ X) (F.obj Y)) → (fun (X : Type u) ↦ X) (H.I.obj Y))
                (Exists.choose (p := fun (y : F.obj Y) ↦
                  (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app Y) :
                        (a : (fun (X : Type u) ↦ X) (F.obj Y)) → (fun (X : Type u) ↦ X) (G.obj Y))
                      y =
                    x)
                  hx)))
      x =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((↾fun (x : (monoFactorisation f).I.obj X) ↦
            match (motive := (monoFactorisation f).I.obj X → H.I.obj X) x with
            | ⟨x, hx⟩ =>
              (ConcreteCategory.hom (FC := TypeCat.Fun) (H.e.app X) :
                  (a : (fun (X : Type u) ↦ X) (F.obj X)) → (fun (X : Type u) ↦ X) (H.I.obj X))
                (Exists.choose (p := fun (y : F.obj X) ↦
                  (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X) :
                        (a : (fun (X : Type u) ↦ X) (F.obj X)) → (fun (X : Type u) ↦ X) (G.obj X))
                      y =
                    x)
                  hx)) ≫
          H.I.map g))
      x
have h : Eq (α := (fun (X : Type u) ↦ X) (G.obj Y))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (H.m.app Y) :
        (a : (fun (X : Type u) ↦ X) (H.I.obj Y)) → (fun (X : Type u) ↦ X) (G.obj Y))
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          ((monoFactorisation f).I.map g ≫
            ↾fun (x : (monoFactorisation f).I.obj Y) ↦
              match (motive := (monoFactorisation f).I.obj Y → H.I.obj Y) x with
              | ⟨x, hx⟩ =>
                (ConcreteCategory.hom (FC := TypeCat.Fun) (H.e.app Y) :
                    (a : (fun (X : Type u) ↦ X) (F.obj Y)) → (fun (X : Type u) ↦ X) (H.I.obj Y))
                  (Exists.choose (p := fun (y : F.obj Y) ↦
                    (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app Y) :
                          (a : (fun (X : Type u) ↦ X) (F.obj Y)) → (fun (X : Type u) ↦ X) (G.obj Y))
                        y =
                      x)
                    hx)))
        x) :
    (fun (X : Type u) ↦ X) (G.obj Y))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (H.m.app Y) :
        (a : (fun (X : Type u) ↦ X) (H.I.obj Y)) → (fun (X : Type u) ↦ X) (G.obj Y))
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          ((↾fun (x : (monoFactorisation f).I.obj X) ↦
              match (motive := (monoFactorisation f).I.obj X → H.I.obj X) x with
              | ⟨x, hx⟩ =>
                (ConcreteCategory.hom (FC := TypeCat.Fun) (H.e.app X) :
                    (a : (fun (X : Type u) ↦ X) (F.obj X)) → (fun (X : Type u) ↦ X) (H.I.obj X))
                  (Exists.choose (p := fun (y : F.obj X) ↦
                    (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X) :
                          (a : (fun (X : Type u) ↦ X) (F.obj X)) → (fun (X : Type u) ↦ X) (G.obj X))
                        y =
                      x)
                    hx)) ≫
            H.I.map g))
        x) :
    (fun (X : Type u) ↦ X) (G.obj Y))
Tactic: apply injective_of_mono (H.m.app Y)