-- 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)
X Y : Arrow (Type u)
f : X ⟶ Y
⊢ Eq (α :=
    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 }
        X ⟶
      Functor.obj Arrow.rightFunc Y)
    (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 }
        f ≫
      ↾fun
          (y :
            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 }
              Y) ↦
        (↑y : Y.right))
    ((↾fun
          (y :
            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 }
              X) ↦
        (↑y : X.right)) ≫
      Functor.map Arrow.rightFunc f)

Tactic:
rfl