∀ {C : Type u_4} [inst : CategoryTheory.Category.{u_3, u_4} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{u_1, u_2} D] {A B : C} (f g : A ⟶ B) (s : B ⟶ A)
  (sl : CategoryTheory.CategoryStruct.comp s f = CategoryTheory.CategoryStruct.id B)
  (sr : CategoryTheory.CategoryStruct.comp s g = CategoryTheory.CategoryStruct.id B) (F : CategoryTheory.Functor C D),
  CategoryTheory.CategoryStruct.comp
      (((CategoryTheory.Limits.reflexivePair f g s sl sr).comp F).map
        CategoryTheory.Limits.WalkingReflexivePair.Hom.reflexion)
      (CategoryTheory.Iso.refl
          (((CategoryTheory.Limits.reflexivePair f g s sl sr).comp F).obj
            CategoryTheory.Limits.WalkingReflexivePair.one)).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Iso.refl
          (((CategoryTheory.Limits.reflexivePair f g s sl sr).comp F).obj
            CategoryTheory.Limits.WalkingReflexivePair.zero)).hom
      ((CategoryTheory.Limits.reflexivePair (F.map f) (F.map g) (F.map s) ⋯ ⋯).map
        CategoryTheory.Limits.WalkingReflexivePair.Hom.reflexion)