∀ (C : Type u_4) [inst : CategoryTheory.Category.{u_1, u_4} C] (D : Type u_5)
  [inst_1 : CategoryTheory.Category.{u_2, u_5} D] (E : Type u_6) [inst_2 : CategoryTheory.Category.{u_3, u_6} E]
  (d : D),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.sum.associator C D E).map
        ((CategoryTheory.Functor.sumIsoExt
                (CategoryTheory.Functor.sumIsoExt
                  (((CategoryTheory.Sum.inl_ C D).associator (CategoryTheory.Sum.inl_ (C ⊕ D) E)
                        (CategoryTheory.Functor.id ((C ⊕ D) ⊕ E))).symm ≪≫
                    ((CategoryTheory.Sum.inl_ C D).comp (CategoryTheory.Sum.inl_ (C ⊕ D) E)).rightUnitor ≪≫
                      (CategoryTheory.Functor.isoWhiskerRight (CategoryTheory.sum.inlCompInlCompAssociator C D E)
                              (CategoryTheory.sum.inverseAssociator C D E) ≪≫
                            CategoryTheory.sum.inlCompInverseAssociator C D E).symm ≪≫
                        (CategoryTheory.Sum.inl_ C D).associator
                            ((CategoryTheory.Sum.inl_ (C ⊕ D) E).comp (CategoryTheory.sum.associator C D E))
                            (CategoryTheory.sum.inverseAssociator C D E) ≪≫
                          (CategoryTheory.Sum.inl_ C D).isoWhiskerLeft
                            ((CategoryTheory.Sum.inl_ (C ⊕ D) E).associator (CategoryTheory.sum.associator C D E)
                              (CategoryTheory.sum.inverseAssociator C D E)))
                  (((CategoryTheory.Sum.inr_ C D).associator (CategoryTheory.Sum.inl_ (C ⊕ D) E)
                        (CategoryTheory.Functor.id ((C ⊕ D) ⊕ E))).symm ≪≫
                    ((CategoryTheory.Sum.inr_ C D).comp (CategoryTheory.Sum.inl_ (C ⊕ D) E)).rightUnitor ≪≫
                      (CategoryTheory.Functor.isoWhiskerRight (CategoryTheory.sum.inrCompInlCompAssociator C D E)
                              (CategoryTheory.sum.inverseAssociator C D E) ≪≫
                            (CategoryTheory.Sum.inl_ D E).associator (CategoryTheory.Sum.inr_ C (D ⊕ E))
                                (CategoryTheory.sum.inverseAssociator C D E) ≪≫
                              CategoryTheory.sum.inlCompInrCompInverseAssociator C D E).symm ≪≫
                        (CategoryTheory.Sum.inr_ C D).associator
                            ((CategoryTheory.Sum.inl_ (C ⊕ D) E).comp (CategoryTheory.sum.associator C D E))
                            (CategoryTheory.sum.inverseAssociator C D E) ≪≫
                          (CategoryTheory.Sum.inr_ C D).isoWhiskerLeft
                            ((CategoryTheory.Sum.inl_ (C ⊕ D) E).associator (CategoryTheory.sum.associator C D E)
                              (CategoryTheory.sum.inverseAssociator C D E))))
                ((CategoryTheory.Sum.inr_ (C ⊕ D) E).rightUnitor ≪≫
                  (CategoryTheory.Functor.isoWhiskerRight (CategoryTheory.sum.inrCompAssociator C D E)
                          (CategoryTheory.sum.inverseAssociator C D E) ≪≫
                        (CategoryTheory.Sum.inr_ D E).associator (CategoryTheory.Sum.inr_ C (D ⊕ E))
                            (CategoryTheory.sum.inverseAssociator C D E) ≪≫
                          CategoryTheory.sum.inrCompInrCompInverseAssociator C D E).symm ≪≫
                    (CategoryTheory.Sum.inr_ (C ⊕ D) E).associator (CategoryTheory.sum.associator C D E)
                      (CategoryTheory.sum.inverseAssociator C D E))).hom.app
          (Sum.inl (Sum.inr d))))
      ((CategoryTheory.Functor.sumIsoExt
              (((CategoryTheory.Sum.inl_ C (D ⊕ E)).associator (CategoryTheory.sum.inverseAssociator C D E)
                    (CategoryTheory.sum.associator C D E)).symm ≪≫
                CategoryTheory.Functor.isoWhiskerRight (CategoryTheory.sum.inlCompInverseAssociator C D E)
                    (CategoryTheory.sum.associator C D E) ≪≫
                  (CategoryTheory.Sum.inl_ C D).associator (CategoryTheory.Sum.inl_ (C ⊕ D) E)
                      (CategoryTheory.sum.associator C D E) ≪≫
                    CategoryTheory.sum.inlCompInlCompAssociator C D E ≪≫
                      (CategoryTheory.Sum.inl_ C (D ⊕ E)).rightUnitor.symm)
              (CategoryTheory.Functor.sumIsoExt
                (((CategoryTheory.Sum.inl_ D E).associator (CategoryTheory.Sum.inr_ C (D ⊕ E))
                      ((CategoryTheory.sum.inverseAssociator C D E).comp (CategoryTheory.sum.associator C D E))).symm ≪≫
                  (((CategoryTheory.Sum.inl_ D E).comp (CategoryTheory.Sum.inr_ C (D ⊕ E))).associator
                        (CategoryTheory.sum.inverseAssociator C D E) (CategoryTheory.sum.associator C D E)).symm ≪≫
                    CategoryTheory.Functor.isoWhiskerRight
                        ((CategoryTheory.Sum.inl_ D E).associator (CategoryTheory.Sum.inr_ C (D ⊕ E))
                            (CategoryTheory.sum.inverseAssociator C D E) ≪≫
                          CategoryTheory.sum.inlCompInrCompInverseAssociator C D E)
                        (CategoryTheory.sum.associator C D E) ≪≫
                      (CategoryTheory.Sum.inr_ C D).associator (CategoryTheory.Sum.inl_ (C ⊕ D) E)
                          (CategoryTheory.sum.associator C D E) ≪≫
                        CategoryTheory.sum.inrCompInlCompAssociator C D E ≪≫
                          ((CategoryTheory.Sum.inl_ D E).comp (CategoryTheory.Sum.inr_ C (D ⊕ E))).rightUnitor.symm ≪≫
                            (CategoryTheory.Sum.inl_ D E).associator (CategoryTheory.Sum.inr_ C (D ⊕ E))
                              (CategoryTheory.Functor.id (C ⊕ D ⊕ E)))
                (((CategoryTheory.Sum.inr_ D E).associator (CategoryTheory.Sum.inr_ C (D ⊕ E))
                      ((CategoryTheory.sum.inverseAssociator C D E).comp (CategoryTheory.sum.associator C D E))).symm ≪≫
                  (((CategoryTheory.Sum.inr_ D E).comp (CategoryTheory.Sum.inr_ C (D ⊕ E))).associator
                        (CategoryTheory.sum.inverseAssociator C D E) (CategoryTheory.sum.associator C D E)).symm ≪≫
                    CategoryTheory.Functor.isoWhiskerRight
                        ((CategoryTheory.Sum.inr_ D E).associator (CategoryTheory.Sum.inr_ C (D ⊕ E))
                            (CategoryTheory.sum.inverseAssociator C D E) ≪≫
                          CategoryTheory.sum.inrCompInrCompInverseAssociator C D E)
                        (CategoryTheory.sum.associator C D E) ≪≫
                      CategoryTheory.sum.inrCompAssociator C D E ≪≫
                        (CategoryTheory.Sum.inr_ D E).isoWhiskerLeft
                          (CategoryTheory.Sum.inr_ C (D ⊕ E)).rightUnitor.symm))).hom.app
        ((CategoryTheory.sum.associator C D E).obj (Sum.inl (Sum.inr d)))) =
    CategoryTheory.CategoryStruct.id ((CategoryTheory.sum.associator C D E).obj (Sum.inl (Sum.inr d)))