∀ {C : Type u_9} [inst : CategoryTheory.Category.{u_7, u_9} C] {D : Type u_10}
  [inst_1 : CategoryTheory.Category.{u_8, u_10} D] {T : Type u_12} [inst_2 : CategoryTheory.Category.{u_11, u_12} T]
  {L : CategoryTheory.Functor C T} {R : CategoryTheory.Functor D T} {C' : Type u_3}
  [inst_3 : CategoryTheory.Category.{u_1, u_3} C'] {D' : Type u_4} [inst_4 : CategoryTheory.Category.{u_2, u_4} D']
  {T' : Type u_6} [inst_5 : CategoryTheory.Category.{u_5, u_6} 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 : CategoryTheory.StructuredArrow X (CategoryTheory.Comma.map α β)),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Functor.id (CategoryTheory.StructuredArrow X (CategoryTheory.Comma.map α β))).obj x).hom
      ((CategoryTheory.Comma.map α β).map
        (CategoryTheory.Iso.refl
            ((CategoryTheory.Functor.id (CategoryTheory.StructuredArrow X (CategoryTheory.Comma.map α β))).obj
                x).right).hom) =
    (((CategoryTheory.StructuredArrow.commaMapEquivalenceFunctor α β X).comp
            (CategoryTheory.StructuredArrow.commaMapEquivalenceInverse α β X)).obj
        x).hom