-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Images
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
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))
⊢ 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

Tactic:
apply injective_of_mono (H.m.app Y)

Premises used: CategoryTheory.injective_of_mono, CategoryTheory.Limits.MonoFactorisation.m, CategoryTheory.NatTrans.app