∀ {C : Type u_4} [inst : CategoryTheory.Category.{u_1, u_4} C] {D : Type u_6}
  [inst_1 : CategoryTheory.Category.{u_2, u_6} D] {T : Type u_8} [inst_2 : CategoryTheory.Category.{u_3, u_8} T]
  {L : CategoryTheory.Functor C T} {R : CategoryTheory.Functor D T} {C' : Type u_10}
  [inst_3 : CategoryTheory.Category.{u_5, u_10} C'] {D' : Type u_11} [inst_4 : CategoryTheory.Category.{u_7, u_11} D']
  {T' : Type u_12} [inst_5 : CategoryTheory.Category.{u_9, u_12} T'] {L' : CategoryTheory.Functor C' T'}
  {R' : CategoryTheory.Functor D' T'} {F₁ : CategoryTheory.Functor C C'} {F₂ : CategoryTheory.Functor D D'}
  {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R')
  [inst_6 : CategoryTheory.IsIso β] (X : CategoryTheory.Comma L' R')
  {X_1 Y :
    CategoryTheory.Comma (CategoryTheory.StructuredArrow.map₂ (CategoryTheory.CategoryStruct.id (L'.obj X.left)) α)
      (CategoryTheory.StructuredArrow.map₂ X.hom (CategoryTheory.inv β))}
  (f : X_1 ⟶ Y),
  CategoryTheory.CategoryStruct.comp
      (((CategoryTheory.StructuredArrow.commaMapEquivalenceInverse α β X).comp
            (CategoryTheory.StructuredArrow.commaMapEquivalenceFunctor α β X)).map
        f)
      ((fun x =>
            CategoryTheory.Comma.isoMk
              (CategoryTheory.Iso.refl
                (((CategoryTheory.StructuredArrow.commaMapEquivalenceInverse α β X).comp
                        (CategoryTheory.StructuredArrow.commaMapEquivalenceFunctor α β X)).obj
                    x).left)
              (CategoryTheory.Iso.refl
                (((CategoryTheory.StructuredArrow.commaMapEquivalenceInverse α β X).comp
                        (CategoryTheory.StructuredArrow.commaMapEquivalenceFunctor α β X)).obj
                    x).right)
              ⋯)
          Y).hom =
    CategoryTheory.CategoryStruct.comp
      ((fun x =>
            CategoryTheory.Comma.isoMk
              (CategoryTheory.Iso.refl
                (((CategoryTheory.StructuredArrow.commaMapEquivalenceInverse α β X).comp
                        (CategoryTheory.StructuredArrow.commaMapEquivalenceFunctor α β X)).obj
                    x).left)
              (CategoryTheory.Iso.refl
                (((CategoryTheory.StructuredArrow.commaMapEquivalenceInverse α β X).comp
                        (CategoryTheory.StructuredArrow.commaMapEquivalenceFunctor α β X)).obj
                    x).right)
              ⋯)
          X_1).hom
      ((CategoryTheory.Functor.id
            (CategoryTheory.Comma
              (CategoryTheory.StructuredArrow.map₂ (CategoryTheory.CategoryStruct.id (L'.obj X.left)) α)
              (CategoryTheory.StructuredArrow.map₂ X.hom (CategoryTheory.inv β)))).map
        f)