Module: Mathlib.CategoryTheory.Sums.Products

Goal state before:
pp: A : Type u_1
inst✝³ : Category.{v_1, u_1} A
A' : Type u_2
inst✝² : Category.{v_2, u_2} A'
B : Type u
inst✝¹ : Category.{v, u} B
T : Type u_3
inst✝ : Category.{v_3, u_3} T
⊢ ∀ {X Y : (A ⊕ A') ⊕ T ⥤ B} (f : X ⟶ Y),
    ((sum.associativity A A' T).congrLeft.trans
                ((functorEquiv A (A' ⊕ T) B).trans (Equivalence.refl.prod (functorEquiv A' T B)))).functor.map
          f ≫
        ((((inl_ A (A' ⊕ T)).associator (sum.associativity A A' T).inverse Y).symm ≪≫
                isoWhiskerRight (sum.inlCompInverseAssociator A A' T) Y ≪≫
                  (inl_ A A').associator (inl_ (A ⊕ A') T) Y).prod
            (((inl_ A' T).isoWhiskerLeft ((inr_ A (A' ⊕ T)).associator (sum.associativity A A' T).inverse Y).symm ≪≫
                  ((inl_ A' T).associator (inr_ A (A' ⊕ T) ⋙ (sum.associativity A A' T).inverse) Y).symm ≪≫
                    isoWhiskerRight (sum.inlCompInrCompInverseAssociator A A' T) Y ≪≫
                      (inr_ A A').associator (inl_ (A ⊕ A') T) Y).prod
              ((inr_ A' T).isoWhiskerLeft ((inr_ A (A' ⊕ T)).associator (sum.associativity A A' T).inverse Y).symm ≪≫
                ((inr_ A' T).associator (inr_ A (A' ⊕ T) ⋙ (sum.associativity A A' T).inverse) Y).symm ≪≫
                  isoWhiskerRight (sum.inrCompInrCompInverseAssociator A A' T) Y))).hom =
      ((((inl_ A (A' ⊕ T)).associator (sum.associativity A A' T).inverse X).symm ≪≫
                isoWhiskerRight (sum.inlCompInverseAssociator A A' T) X ≪≫
                  (inl_ A A').associator (inl_ (A ⊕ A') T) X).prod
            (((inl_ A' T).isoWhiskerLeft ((inr_ A (A' ⊕ T)).associator (sum.associativity A A' T).inverse X).symm ≪≫
                  ((inl_ A' T).associator (inr_ A (A' ⊕ T) ⋙ (sum.associativity A A' T).inverse) X).symm ≪≫
                    isoWhiskerRight (sum.inlCompInrCompInverseAssociator A A' T) X ≪≫
                      (inr_ A A').associator (inl_ (A ⊕ A') T) X).prod
              ((inr_ A' T).isoWhiskerLeft ((inr_ A (A' ⊕ T)).associator (sum.associativity A A' T).inverse X).symm ≪≫
                ((inr_ A' T).associator (inr_ A (A' ⊕ T) ⋙ (sum.associativity A A' T).inverse) X).symm ≪≫
                  isoWhiskerRight (sum.inrCompInrCompInverseAssociator A A' T) X))).hom ≫
        (((functorEquiv (A ⊕ A') T B).trans ((functorEquiv A A' B).prod Equivalence.refl)).trans
                (prod.associativity (A ⥤ B) (A' ⥤ B) (T ⥤ B))).functor.map
          f

Tactic:
intros

Goal state after:
A : Type u_1
inst✝³ : Category.{v_1, u_1} A
A' : Type u_2
inst✝² : Category.{v_2, u_2} A'
B : Type u
inst✝¹ : Category.{v, u} B
T : Type u_3
inst✝ : Category.{v_3, u_3} T
X✝ Y✝ : (A ⊕ A') ⊕ T ⥤ B
f✝ : X✝ ⟶ Y✝
⊢ ((sum.associativity A A' T).congrLeft.trans
              ((functorEquiv A (A' ⊕ T) B).trans (Equivalence.refl.prod (functorEquiv A' T B)))).functor.map
        f✝ ≫
      ((((inl_ A (A' ⊕ T)).associator (sum.associativity A A' T).inverse Y✝).symm ≪≫
              isoWhiskerRight (sum.inlCompInverseAssociator A A' T) Y✝ ≪≫
                (inl_ A A').associator (inl_ (A ⊕ A') T) Y✝).prod
          (((inl_ A' T).isoWhiskerLeft ((inr_ A (A' ⊕ T)).associator (sum.associativity A A' T).inverse Y✝).symm ≪≫
                ((inl_ A' T).associator (inr_ A (A' ⊕ T) ⋙ (sum.associativity A A' T).inverse) Y✝).symm ≪≫
                  isoWhiskerRight (sum.inlCompInrCompInverseAssociator A A' T) Y✝ ≪≫
                    (inr_ A A').associator (inl_ (A ⊕ A') T) Y✝).prod
            ((inr_ A' T).isoWhiskerLeft ((inr_ A (A' ⊕ T)).associator (sum.associativity A A' T).inverse Y✝).symm ≪≫
              ((inr_ A' T).associator (inr_ A (A' ⊕ T) ⋙ (sum.associativity A A' T).inverse) Y✝).symm ≪≫
                isoWhiskerRight (sum.inrCompInrCompInverseAssociator A A' T) Y✝))).hom =
    ((((inl_ A (A' ⊕ T)).associator (sum.associativity A A' T).inverse X✝).symm ≪≫
              isoWhiskerRight (sum.inlCompInverseAssociator A A' T) X✝ ≪≫
                (inl_ A A').associator (inl_ (A ⊕ A') T) X✝).prod
          (((inl_ A' T).isoWhiskerLeft ((inr_ A (A' ⊕ T)).associator (sum.associativity A A' T).inverse X✝).symm ≪≫
                ((inl_ A' T).associator (inr_ A (A' ⊕ T) ⋙ (sum.associativity A A' T).inverse) X✝).symm ≪≫
                  isoWhiskerRight (sum.inlCompInrCompInverseAssociator A A' T) X✝ ≪≫
                    (inr_ A A').associator (inl_ (A ⊕ A') T) X✝).prod
            ((inr_ A' T).isoWhiskerLeft ((inr_ A (A' ⊕ T)).associator (sum.associativity A A' T).inverse X✝).symm ≪≫
              ((inr_ A' T).associator (inr_ A (A' ⊕ T) ⋙ (sum.associativity A A' T).inverse) X✝).symm ≪≫
                isoWhiskerRight (sum.inrCompInrCompInverseAssociator A A' T) X✝))).hom ≫
      (((functorEquiv (A ⊕ A') T B).trans ((functorEquiv A A' B).prod Equivalence.refl)).trans
              (prod.associativity (A ⥤ B) (A' ⥤ B) (T ⥤ B))).functor.map
        f✝