∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] (r : HomRel C) {D : Type u_4}
  [inst_1 : CategoryTheory.Category.{u_3, u_4} D] (F : CategoryTheory.Functor C D)
  (H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂) {X Y : C} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp
      (((CategoryTheory.Quotient.functor r).comp (CategoryTheory.Quotient.lift r F H)).map f)
      ((fun x =>
            CategoryTheory.Iso.refl
              (((CategoryTheory.Quotient.functor r).comp (CategoryTheory.Quotient.lift r F H)).obj x))
          Y).hom =
    CategoryTheory.CategoryStruct.comp
      ((fun x =>
            CategoryTheory.Iso.refl
              (((CategoryTheory.Quotient.functor r).comp (CategoryTheory.Quotient.lift r F H)).obj x))
          X).hom
      (F.map f)