-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- `map₂` along equivalences of categories is an equivalence of categories.  -/
CategoryTheory.StructuredArrow.map₂Iso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {A : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} A] →
            {B : Type u₄} →
              [inst_3 : CategoryTheory.Category.{v₄, u₄} B] →
                {L : D} →
                  {R : CategoryTheory.Functor C D} →
                    {L' : B} →
                      {R' : CategoryTheory.Functor A B} →
                        {F : C ≌ A} →
                          {G : D ≌ B} →
                            (α : L' ⟶ G.functor.obj L) →
                              (α' : L ⟶ G.inverse.obj L') →
                                (β : R.comp G.functor ⟶ F.functor.comp R') →
                                  (β' : R'.comp G.inverse ⟶ F.inverse.comp R) →
                                    CategoryTheory.CategoryStruct.comp α (G.functor.map α') = G.counitIso.inv.app L' →
                                      CategoryTheory.CategoryStruct.comp α' (G.inverse.map α) = G.unitIso.hom.app L →
                                        CategoryTheory.CategoryStruct.comp R.rightUnitor.hom
                                              (CategoryTheory.CategoryStruct.comp R.leftUnitor.inv
                                                (CategoryTheory.CategoryStruct.comp
                                                  (CategoryTheory.Functor.whiskerRight F.unitIso.hom R)
                                                  (F.functor.associator F.inverse R).hom)) =
                                            CategoryTheory.CategoryStruct.comp (R.whiskerLeft G.unitIso.hom)
                                              (CategoryTheory.CategoryStruct.comp (R.associator G.functor G.inverse).inv
                                                (CategoryTheory.CategoryStruct.comp
                                                  (CategoryTheory.Functor.whiskerRight β G.inverse)
                                                  (CategoryTheory.CategoryStruct.comp
                                                    (F.functor.associator R' G.inverse).hom
                                                    (F.functor.whiskerLeft β')))) →
                                          CategoryTheory.CategoryStruct.comp
                                                (CategoryTheory.Functor.whiskerRight β' G.functor)
                                                (CategoryTheory.CategoryStruct.comp
                                                  (F.inverse.associator R G.functor).hom
                                                  (CategoryTheory.CategoryStruct.comp (F.inverse.whiskerLeft β)
                                                    (CategoryTheory.CategoryStruct.comp
                                                      (F.inverse.associator F.functor R').inv
                                                      (CategoryTheory.Functor.whiskerRight F.counitIso.hom R')))) =
                                              CategoryTheory.CategoryStruct.comp (R'.associator G.inverse G.functor).hom
                                                (CategoryTheory.CategoryStruct.comp (R'.whiskerLeft G.counitIso.hom)
                                                  (CategoryTheory.CategoryStruct.comp R'.rightUnitor.hom
                                                    R'.leftUnitor.inv)) →
                                            (CategoryTheory.StructuredArrow L R ≌ CategoryTheory.StructuredArrow L' R')