-- Module: Mathlib.CategoryTheory.MorphismProperty.Concrete
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst_1 : (X Y : C) → FunLike.{u_1 + 1, u_2 + 1, u_2 + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{u_2, v, u, u_1} C FC (CC := CC)
f g : Arrow (Type u)
φ : f ⟶ g
h :
  ∀ (x : Functor.obj Arrow.leftFunc f),
    Eq (α := g.right)
      (↑(TypeCat.Fun.toFun
            (hom (FC := TypeCat.Fun)
              (Functor.map Arrow.leftFunc φ ≫
                ↾fun (x : Functor.obj Arrow.leftFunc g) ↦
                  Subtype.mk (p := Set.range (ι := g.left) (⇑(TypeCat.Hom.hom g.hom) : (a : g.left) → g.right))
                    ((hom (FC := TypeCat.Fun) g.hom :
                        (a : (fun (X : Type u) ↦ X) g.left) → (fun (X : Type u) ↦ X) g.right)
                      x)
                    ⋯))
            x) :
        g.right)
      (↑(TypeCat.Fun.toFun
            (hom (FC := TypeCat.Fun)
              ((↾fun (x : Functor.obj Arrow.leftFunc f) ↦
                  Subtype.mk (p := Set.range (ι := f.left) (⇑(TypeCat.Hom.hom f.hom) : (a : f.left) → f.right))
                    ((hom (FC := TypeCat.Fun) f.hom :
                        (a : (fun (X : Type u) ↦ X) f.left) → (fun (X : Type u) ↦ X) f.right)
                      x)
                    ⋯) ≫
                Functor.map
                  {
                    obj := fun (f : Arrow (Type u)) ↦
                      Subtype (α := f.right)
                        (Set.range (ι := f.left) (⇑(TypeCat.Hom.hom f.hom) : (a : f.left) → f.right)),
                    map := fun {X Y : Arrow (Type u)} (φ : X ⟶ Y) ↦
                      ↾fun
                          (y :
                            Subtype (α := X.right)
                              (Set.range (ι := X.left) (⇑(TypeCat.Hom.hom X.hom) : (a : X.left) → X.right))) ↦
                        Subtype.mk (p := Set.range (ι := Y.left) (⇑(TypeCat.Hom.hom Y.hom) : (a : Y.left) → Y.right))
                          ((hom (FC := TypeCat.Fun) (Arrow.Hom.right φ) :
                              (a : (fun (X : Type u) ↦ X) X.right) → (fun (X : Type u) ↦ X) Y.right)
                            (↑y : X.right))
                          ⋯,
                    map_id := functorialSurjectiveInjectiveFactorizationData._proof_2,
                    map_comp := @functorialSurjectiveInjectiveFactorizationData._proof_3 : Arrow (Type u) ⥤ Type u }
                  φ))
            x) :
        g.right)
⊢ Eq (α :=
    Functor.obj Arrow.leftFunc f ⟶
      Functor.obj
        {
          obj := fun (f : Arrow (Type u)) ↦
            Subtype (α := f.right) (Set.range (ι := f.left) (⇑(TypeCat.Hom.hom f.hom) : (a : f.left) → f.right)),
          map := fun {X Y : Arrow (Type u)} (φ : X ⟶ Y) ↦
            ↾fun
                (y :
                  Subtype (α := X.right)
                    (Set.range (ι := X.left) (⇑(TypeCat.Hom.hom X.hom) : (a : X.left) → X.right))) ↦
              Subtype.mk (p := Set.range (ι := Y.left) (⇑(TypeCat.Hom.hom Y.hom) : (a : Y.left) → Y.right))
                ((hom (FC := TypeCat.Fun) (Arrow.Hom.right φ) :
                    (a : (fun (X : Type u) ↦ X) X.right) → (fun (X : Type u) ↦ X) Y.right)
                  (↑y : X.right))
                ⋯,
          map_id := functorialSurjectiveInjectiveFactorizationData._proof_2,
          map_comp := @functorialSurjectiveInjectiveFactorizationData._proof_3 }
        g)
    (Functor.map Arrow.leftFunc φ ≫
      ↾fun (x : Functor.obj Arrow.leftFunc g) ↦
        Subtype.mk (p := Set.range (ι := g.left) (⇑(TypeCat.Hom.hom g.hom) : (a : g.left) → g.right))
          ((hom (FC := TypeCat.Fun) g.hom : (a : (fun (X : Type u) ↦ X) g.left) → (fun (X : Type u) ↦ X) g.right) x) ⋯)
    ((↾fun (x : Functor.obj Arrow.leftFunc f) ↦
        Subtype.mk (p := Set.range (ι := f.left) (⇑(TypeCat.Hom.hom f.hom) : (a : f.left) → f.right))
          ((hom (FC := TypeCat.Fun) f.hom : (a : (fun (X : Type u) ↦ X) f.left) → (fun (X : Type u) ↦ X) f.right) x)
          ⋯) ≫
      Functor.map
        {
          obj := fun (f : Arrow (Type u)) ↦
            Subtype (α := f.right) (Set.range (ι := f.left) (⇑(TypeCat.Hom.hom f.hom) : (a : f.left) → f.right)),
          map := fun {X Y : Arrow (Type u)} (φ : X ⟶ Y) ↦
            ↾fun
                (y :
                  Subtype (α := X.right)
                    (Set.range (ι := X.left) (⇑(TypeCat.Hom.hom X.hom) : (a : X.left) → X.right))) ↦
              Subtype.mk (p := Set.range (ι := Y.left) (⇑(TypeCat.Hom.hom Y.hom) : (a : Y.left) → Y.right))
                ((hom (FC := TypeCat.Fun) (Arrow.Hom.right φ) :
                    (a : (fun (X : Type u) ↦ X) X.right) → (fun (X : Type u) ↦ X) Y.right)
                  (↑y : X.right))
                ⋯,
          map_id := functorialSurjectiveInjectiveFactorizationData._proof_2,
          map_comp := @functorialSurjectiveInjectiveFactorizationData._proof_3 : Arrow (Type u) ⥤ Type u }
        φ)

Tactic:
ext x