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✝

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