-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Concrete (goal)
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
⊢ 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 }
        φ)
have 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)
                  sorry))
          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)
                  sorry) ≫
              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))
                        sorry,
                  map_id := functorialSurjectiveInjectiveFactorizationData._proof_2,
                  map_comp := @functorialSurjectiveInjectiveFactorizationData._proof_3 : Arrow (Type u) ⥤ Type u }
                φ))
          x) :
      g.right)
Tactic: ext x