∀ (f : CategoryTheory.Arrow (Type u_1))
  (x₁ x₂ :
    (fun X => X)
      ({ obj := fun f => Subtype (Set.range f.hom), map := fun {X Y} φ y => ⟨φ.right ↑y, ⋯⟩,
            map_id := CategoryTheory.functorialSurjectiveInjectiveFactorizationData._proof_2,
            map_comp := @CategoryTheory.functorialSurjectiveInjectiveFactorizationData._proof_3 }.obj
        f)),
  (CategoryTheory.ConcreteCategory.hom
          ({ app := fun x y => ↑y,
                naturality := CategoryTheory.functorialSurjectiveInjectiveFactorizationData._proof_5 }.app
            f))
        x₁ =
      (CategoryTheory.ConcreteCategory.hom
          ({ app := fun x y => ↑y,
                naturality := CategoryTheory.functorialSurjectiveInjectiveFactorizationData._proof_5 }.app
            f))
        x₂ →
    x₁ = x₂