-- 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 : Arrow (Type u)
x : f.left
⊢ ∃ (a : (fun (X : Type u) ↦ X) (Functor.obj Arrow.leftFunc f)),
    Eq (α :=
      (fun (X : Type u) ↦ X)
        (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 }
          f))
      ((hom (FC := TypeCat.Fun)
              (NatTrans.app
                {
                  app := fun (f : Arrow (Type u)) ↦
                    ↾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)
                        ⋯,
                  naturality := ⋯ :
                  NatTrans (C := Arrow (Type u)) Arrow.leftFunc
                    {
                      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) :
            (a : (fun (X : Type u) ↦ X) (Arrow.leftFunc.obj f)) →
              (fun (X : Type u) ↦ X)
                ({
                      obj := fun (f : Arrow (Type u)) ↦
                        Subtype (Set.range (⇑(TypeCat.Hom.hom f.hom) : (a : f.left) → f.right)),
                      map := fun {X Y : Arrow (Type u)} (φ : X ⟶ Y) ↦
                        ↾fun (y : Subtype (Set.range (⇑(TypeCat.Hom.hom X.hom) : (a : X.left) → X.right))) ↦
                          ⟨(hom (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 }.obj
                  f))
          a :
        (fun (X : Type u) ↦ X)
          (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 }
            f))
      (Subtype.mk (p := Set.range (ι := f.left) (⇑(TypeCat.Hom.hom f.hom) : (a : f.left) → f.right))
          ((TypeCat.Hom.hom f.hom : (a : f.left) → f.right) x) ⋯ :
        Subtype (α := f.right) (Set.range (ι := f.left) (⇑(TypeCat.Hom.hom f.hom) : (a : f.left) → f.right)))

Tactic:
⟨x, rfl⟩

Premises used: Exists.intro, rfl