Module: Mathlib.CategoryTheory.Sums.Associator

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
x : (C ⊕ D) ⊕ E
d : D
⊢ (associator C D E).map
        ((sumIsoExt
                (sumIsoExt
                  (((inl_ C D).associator (inl_ (C ⊕ D) E) (𝟭 ((C ⊕ D) ⊕ E))).symm ≪≫
                    (inl_ C D ⋙ inl_ (C ⊕ D) E).rightUnitor ≪≫
                      (isoWhiskerRight (inlCompInlCompAssociator C D E) (inverseAssociator C D E) ≪≫
                            inlCompInverseAssociator C D E).symm ≪≫
                        (inl_ C D).associator (inl_ (C ⊕ D) E ⋙ associator C D E) (inverseAssociator C D E) ≪≫
                          (inl_ C D).isoWhiskerLeft
                            ((inl_ (C ⊕ D) E).associator (associator C D E) (inverseAssociator C D E)))
                  (((inr_ C D).associator (inl_ (C ⊕ D) E) (𝟭 ((C ⊕ D) ⊕ E))).symm ≪≫
                    (inr_ C D ⋙ inl_ (C ⊕ D) E).rightUnitor ≪≫
                      (isoWhiskerRight (inrCompInlCompAssociator C D E) (inverseAssociator C D E) ≪≫
                            (inl_ D E).associator (inr_ C (D ⊕ E)) (inverseAssociator C D E) ≪≫
                              inlCompInrCompInverseAssociator C D E).symm ≪≫
                        (inr_ C D).associator (inl_ (C ⊕ D) E ⋙ associator C D E) (inverseAssociator C D E) ≪≫
                          (inr_ C D).isoWhiskerLeft
                            ((inl_ (C ⊕ D) E).associator (associator C D E) (inverseAssociator C D E))))
                ((inr_ (C ⊕ D) E).rightUnitor ≪≫
                  (isoWhiskerRight (inrCompAssociator C D E) (inverseAssociator C D E) ≪≫
                        (inr_ D E).associator (inr_ C (D ⊕ E)) (inverseAssociator C D E) ≪≫
                          inrCompInrCompInverseAssociator C D E).symm ≪≫
                    (inr_ (C ⊕ D) E).associator (associator C D E) (inverseAssociator C D E))).hom.app
          (inl (inr d))) ≫
      (sumIsoExt
              (((inl_ C (D ⊕ E)).associator (inverseAssociator C D E) (associator C D E)).symm ≪≫
                isoWhiskerRight (inlCompInverseAssociator C D E) (associator C D E) ≪≫
                  (inl_ C D).associator (inl_ (C ⊕ D) E) (associator C D E) ≪≫
                    inlCompInlCompAssociator C D E ≪≫ (inl_ C (D ⊕ E)).rightUnitor.symm)
              (sumIsoExt
                (((inl_ D E).associator (inr_ C (D ⊕ E)) (inverseAssociator C D E ⋙ associator C D E)).symm ≪≫
                  ((inl_ D E ⋙ inr_ C (D ⊕ E)).associator (inverseAssociator C D E) (associator C D E)).symm ≪≫
                    isoWhiskerRight
                        ((inl_ D E).associator (inr_ C (D ⊕ E)) (inverseAssociator C D E) ≪≫
                          inlCompInrCompInverseAssociator C D E)
                        (associator C D E) ≪≫
                      (inr_ C D).associator (inl_ (C ⊕ D) E) (associator C D E) ≪≫
                        inrCompInlCompAssociator C D E ≪≫
                          (inl_ D E ⋙ inr_ C (D ⊕ E)).rightUnitor.symm ≪≫
                            (inl_ D E).associator (inr_ C (D ⊕ E)) (𝟭 (C ⊕ D ⊕ E)))
                (((inr_ D E).associator (inr_ C (D ⊕ E)) (inverseAssociator C D E ⋙ associator C D E)).symm ≪≫
                  ((inr_ D E ⋙ inr_ C (D ⊕ E)).associator (inverseAssociator C D E) (associator C D E)).symm ≪≫
                    isoWhiskerRight
                        ((inr_ D E).associator (inr_ C (D ⊕ E)) (inverseAssociator C D E) ≪≫
                          inrCompInrCompInverseAssociator C D E)
                        (associator C D E) ≪≫
                      inrCompAssociator C D E ≪≫ (inr_ D E).isoWhiskerLeft (inr_ C (D ⊕ E)).rightUnitor.symm))).hom.app
        ((associator C D E).obj (inl (inr d))) =
    𝟙 ((associator C D E).obj (inl (inr d)))

Tactic:
by

Goal state after: