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✝ : 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:
dsimp

Goal state after:
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
⊢ f✝.app (Sum.inr x✝) ≫
      𝟙 (Y✝.obj (Sum.inr x✝)) ≫
        𝟙 (Y✝.obj (Sum.inr x✝)) ≫ Y✝.map ((sum.inrCompInrCompInverseAssociator A A' T).hom.app x✝) =
    (𝟙 (X✝.obj (Sum.inr x✝)) ≫
        𝟙 (X✝.obj (Sum.inr x✝)) ≫ X✝.map ((sum.inrCompInrCompInverseAssociator A A' T).hom.app x✝)) ≫
      f✝.app (Sum.inr x✝)