-- 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 : Arrow (Type u)
x₁ x₂ :
  (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)
h :
  Eq (α := (fun (X : Type u) ↦ X) (Functor.obj Arrow.rightFunc f))
    ((hom (FC := TypeCat.Fun)
            ({
                  app := fun (x : Arrow (Type u)) ↦
                    ↾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 :
                              Arrow (Type u) ⥤ Type u }
                            x) ↦
                      (↑y : x.right),
                  naturality := functorialSurjectiveInjectiveFactorizationData._proof_5 :
                  NatTrans (C := Arrow (Type u))
                    {
                      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 }
                    Arrow.rightFunc }.app
              f) :
          (a :
              (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)) →
            (fun (X : Type u) ↦ X) (Arrow.rightFunc.obj f))
        x₁ :
      (fun (X : Type u) ↦ X) (Functor.obj Arrow.rightFunc f))
    ((hom (FC := TypeCat.Fun)
            ({
                  app := fun (x : Arrow (Type u)) ↦
                    ↾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 :
                              Arrow (Type u) ⥤ Type u }
                            x) ↦
                      (↑y : x.right),
                  naturality := functorialSurjectiveInjectiveFactorizationData._proof_5 :
                  NatTrans (C := Arrow (Type u))
                    {
                      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 }
                    Arrow.rightFunc }.app
              f) :
          (a :
              (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)) →
            (fun (X : Type u) ↦ X) (Arrow.rightFunc.obj f))
        x₂ :
      (fun (X : Type u) ↦ X) (Functor.obj Arrow.rightFunc f))
⊢ x₁ = x₂
have rw : (↑x₁ : f.right) = (↑x₂ : f.right)
Tactic: rw [Subtype.ext_iff]