-- 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).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).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)).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).1
      x)
have h₁ : f.app (Sum.inl (Sum.inl x)) ≫
    𝟙 (Y.obj (Sum.inl (Sum.inl x))) ≫
      Y.map (NatTrans.app (Iso.hom (sum.inlCompInverseAssociator A A' T)) x) ≫ 𝟙 (Y.obj (Sum.inl (Sum.inl x))) =
  (𝟙 (X.obj (Sum.inl (Sum.inl x))) ≫
      X.map (NatTrans.app (Iso.hom (sum.inlCompInverseAssociator A A' T)) x) ≫ 𝟙 (X.obj (Sum.inl (Sum.inl x)))) ≫
    f.app (Sum.inl (Sum.inl x))
Tactic: dsimp