-- Module: Mathlib.CategoryTheory.Sums.Associator
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
x : (C ⊕ D) ⊕ E
e : E
⊢ Functor.map (associator C D E)
        (NatTrans.app
          (Iso.hom
            (sumIsoExt
              (sumIsoExt
                (Iso.symm (Functor.associator (inl_ C D) (inl_ (C ⊕ D) E) (𝟭 ((C ⊕ D) ⊕ E))) ≪≫
                  rightUnitor (inl_ C D ⋙ inl_ (C ⊕ D) E) ≪≫
                    Iso.symm
                        (isoWhiskerRight (inlCompInlCompAssociator C D E) (inverseAssociator C D E) ≪≫
                          inlCompInverseAssociator C D E) ≪≫
                      Functor.associator (inl_ C D) (inl_ (C ⊕ D) E ⋙ associator C D E) (inverseAssociator C D E) ≪≫
                        isoWhiskerLeft (inl_ C D)
                          (Functor.associator (inl_ (C ⊕ D) E) (associator C D E) (inverseAssociator C D E)))
                (Iso.symm (Functor.associator (inr_ C D) (inl_ (C ⊕ D) E) (𝟭 ((C ⊕ D) ⊕ E))) ≪≫
                  rightUnitor (inr_ C D ⋙ inl_ (C ⊕ D) E) ≪≫
                    Iso.symm
                        (isoWhiskerRight (inrCompInlCompAssociator C D E) (inverseAssociator C D E) ≪≫
                          Functor.associator (inl_ D E) (inr_ C (D ⊕ E)) (inverseAssociator C D E) ≪≫
                            inlCompInrCompInverseAssociator C D E) ≪≫
                      Functor.associator (inr_ C D) (inl_ (C ⊕ D) E ⋙ associator C D E) (inverseAssociator C D E) ≪≫
                        isoWhiskerLeft (inr_ C D)
                          (Functor.associator (inl_ (C ⊕ D) E) (associator C D E) (inverseAssociator C D E))))
              (rightUnitor (inr_ (C ⊕ D) E) ≪≫
                Iso.symm
                    (isoWhiskerRight (inrCompAssociator C D E) (inverseAssociator C D E) ≪≫
                      Functor.associator (inr_ D E) (inr_ C (D ⊕ E)) (inverseAssociator C D E) ≪≫
                        inrCompInrCompInverseAssociator C D E) ≪≫
                  Functor.associator (inr_ (C ⊕ D) E) (associator C D E) (inverseAssociator C D E))))
          (inr e)) ≫
      NatTrans.app
        (Iso.hom
          (sumIsoExt
            (Iso.symm (Functor.associator (inl_ C (D ⊕ E)) (inverseAssociator C D E) (associator C D E)) ≪≫
              isoWhiskerRight (inlCompInverseAssociator C D E) (associator C D E) ≪≫
                Functor.associator (inl_ C D) (inl_ (C ⊕ D) E) (associator C D E) ≪≫
                  inlCompInlCompAssociator C D E ≪≫ Iso.symm (rightUnitor (inl_ C (D ⊕ E))))
            (sumIsoExt
              (Iso.symm (Functor.associator (inl_ D E) (inr_ C (D ⊕ E)) (inverseAssociator C D E ⋙ associator C D E)) ≪≫
                Iso.symm
                    (Functor.associator (inl_ D E ⋙ inr_ C (D ⊕ E)) (inverseAssociator C D E) (associator C D E)) ≪≫
                  isoWhiskerRight
                      (Functor.associator (inl_ D E) (inr_ C (D ⊕ E)) (inverseAssociator C D E) ≪≫
                        inlCompInrCompInverseAssociator C D E)
                      (associator C D E) ≪≫
                    Functor.associator (inr_ C D) (inl_ (C ⊕ D) E) (associator C D E) ≪≫
                      inrCompInlCompAssociator C D E ≪≫
                        Iso.symm (rightUnitor (inl_ D E ⋙ inr_ C (D ⊕ E))) ≪≫
                          Functor.associator (inl_ D E) (inr_ C (D ⊕ E)) (𝟭 (C ⊕ D ⊕ E)))
              (Iso.symm (Functor.associator (inr_ D E) (inr_ C (D ⊕ E)) (inverseAssociator C D E ⋙ associator C D E)) ≪≫
                Iso.symm
                    (Functor.associator (inr_ D E ⋙ inr_ C (D ⊕ E)) (inverseAssociator C D E) (associator C D E)) ≪≫
                  isoWhiskerRight
                      (Functor.associator (inr_ D E) (inr_ C (D ⊕ E)) (inverseAssociator C D E) ≪≫
                        inrCompInrCompInverseAssociator C D E)
                      (associator C D E) ≪≫
                    inrCompAssociator C D E ≪≫ isoWhiskerLeft (inr_ D E) (Iso.symm (rightUnitor (inr_ C (D ⊕ E))))))))
        (obj (associator C D E) (inr e)) =
    𝟙 (obj (associator C D E) (inr e))

Tactic:
simp [inrCompAssociator, inrCompInrCompInverseAssociator]

Premises used: CategoryTheory.sum.inrCompInrCompInverseAssociator, CategoryTheory.sum.inrCompAssociator