-- Lean 4 proof step from Mathlib.CategoryTheory.Sums.Products (goal)
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
A' : Type u_2
inst_1 : Category.{v_2, u_2} A'
B : Type u
inst_2 : Category.{v, u} B
T : Type u_3
inst_3 : Category.{v_3, u_3} T
X Y : (A ⊕ A') ⊕ T ⥤ B
f : X ⟶ Y
x : A'
⊢ Eq (α :=
    (obj
                (Equivalence.functor
                  (Equivalence.trans (Equivalence.congrLeft (sum.associativity A A' T))
                    (Equivalence.trans (functorEquiv A (A' ⊕ T) B)
                      (Equivalence.prod Equivalence.refl (functorEquiv A' T B)))))
                X).2.1.obj
        x ⟶
      (obj
                (Equivalence.functor
                  (Equivalence.trans
                    (Equivalence.trans (functorEquiv (A ⊕ A') T B)
                      (Equivalence.prod (functorEquiv A A' B) Equivalence.refl))
                    (prod.associativity (Functor.{v_1, v, u_1, u} A B) (Functor.{v_2, v, u_2, u} A' B)
                      (Functor.{v_3, v, u_3, u} T B))))
                Y).2.1.obj
        x)
    (NatTrans.app
      (map
              (Equivalence.functor
                (Equivalence.trans (Equivalence.congrLeft (sum.associativity A A' T))
                  (Equivalence.trans (functorEquiv A (A' ⊕ T) B)
                    (Equivalence.prod Equivalence.refl (functorEquiv A' T B)))))
              f ≫
            Iso.hom
              ((fun (E : (A ⊕ A') ⊕ T ⥤ B) ↦
                  (Iso.symm (associator (inl_ A (A' ⊕ T)) (Equivalence.inverse (sum.associativity A A' T)) E) ≪≫
                        isoWhiskerRight (sum.inlCompInverseAssociator A A' T) E ≪≫
                          associator (inl_ A A') (inl_ (A ⊕ A') T) E).prod
                    ((isoWhiskerLeft (inl_ A' T)
                            (Iso.symm
                              (associator (inr_ A (A' ⊕ T)) (Equivalence.inverse (sum.associativity A A' T)) E)) ≪≫
                          Iso.symm
                              (associator (inl_ A' T) (inr_ A (A' ⊕ T) ⋙ Equivalence.inverse (sum.associativity A A' T))
                                E) ≪≫
                            isoWhiskerRight (sum.inlCompInrCompInverseAssociator A A' T) E ≪≫
                              associator (inr_ A A') (inl_ (A ⊕ A') T) E).prod
                      (isoWhiskerLeft (inr_ A' T)
                          (Iso.symm
                            (associator (inr_ A (A' ⊕ T)) (Equivalence.inverse (sum.associativity A A' T)) E)) ≪≫
                        Iso.symm
                            (associator (inr_ A' T) (inr_ A (A' ⊕ T) ⋙ Equivalence.inverse (sum.associativity A A' T))
                              E) ≪≫
                          isoWhiskerRight (sum.inrCompInrCompInverseAssociator A A' T) E)))
                Y)).2.1
      x)
    (NatTrans.app
      (Iso.hom
              ((fun (E : (A ⊕ A') ⊕ T ⥤ B) ↦
                  (Iso.symm (associator (inl_ A (A' ⊕ T)) (Equivalence.inverse (sum.associativity A A' T)) E) ≪≫
                        isoWhiskerRight (sum.inlCompInverseAssociator A A' T) E ≪≫
                          associator (inl_ A A') (inl_ (A ⊕ A') T) E).prod
                    ((isoWhiskerLeft (inl_ A' T)
                            (Iso.symm
                              (associator (inr_ A (A' ⊕ T)) (Equivalence.inverse (sum.associativity A A' T)) E)) ≪≫
                          Iso.symm
                              (associator (inl_ A' T) (inr_ A (A' ⊕ T) ⋙ Equivalence.inverse (sum.associativity A A' T))
                                E) ≪≫
                            isoWhiskerRight (sum.inlCompInrCompInverseAssociator A A' T) E ≪≫
                              associator (inr_ A A') (inl_ (A ⊕ A') T) E).prod
                      (isoWhiskerLeft (inr_ A' T)
                          (Iso.symm
                            (associator (inr_ A (A' ⊕ T)) (Equivalence.inverse (sum.associativity A A' T)) E)) ≪≫
                        Iso.symm
                            (associator (inr_ A' T) (inr_ A (A' ⊕ T) ⋙ Equivalence.inverse (sum.associativity A A' T))
                              E) ≪≫
                          isoWhiskerRight (sum.inrCompInrCompInverseAssociator A A' T) E)))
                X) ≫
            map
              (Equivalence.functor
                (Equivalence.trans
                  (Equivalence.trans (functorEquiv (A ⊕ A') T B)
                    (Equivalence.prod (functorEquiv A A' B) Equivalence.refl))
                  (prod.associativity (Functor.{v_1, v, u_1, u} A B) (Functor.{v_2, v, u_2, u} A' B)
                    (Functor.{v_3, v, u_3, u} T B))))
              f).2.1
      x)
have h₂ : f.app (Sum.inl (Sum.inr x)) ≫
    𝟙 (Y.obj (Sum.inl (Sum.inr x))) ≫
      𝟙 (Y.obj (Sum.inl (Sum.inr x))) ≫
        Y.map (NatTrans.app (Iso.hom (sum.inlCompInrCompInverseAssociator A A' T)) x) ≫
          𝟙 (Y.obj (Sum.inl (Sum.inr x))) =
  (𝟙 (X.obj (Sum.inl (Sum.inr x))) ≫
      𝟙 (X.obj (Sum.inl (Sum.inr x))) ≫
        X.map (NatTrans.app (Iso.hom (sum.inlCompInrCompInverseAssociator A A' T)) x) ≫
          𝟙 (X.obj (Sum.inl (Sum.inr x)))) ≫
    f.app (Sum.inl (Sum.inr x))
Tactic: dsimp