Module: Mathlib.CategoryTheory.Sums.Products

Goal state before:
pp: case h₁
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✝
x✝ : A
⊢ (((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).1.app
      x✝ =
    (((((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✝).1.app
      x✝

pp: case h₂.h₁
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✝
x✝ : A'
⊢ (((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).2.1.app
      x✝ =
    (((((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✝).2.1.app
      x✝

pp: case h₂
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✝
x✝ : T
⊢ (((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).2.2.app
      x✝ =
    (((((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✝).2.2.app
      x✝

Tactic:
all_goals
        dsimp
        simp only [Category.comp_id, Category.id_comp, NatTrans.naturality]

Goal state after: