-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.SingleFunctors (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
E' : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : Category.{v_4, u_4} E'
A : Type u_5
inst_4 : AddMonoid A
inst_5 : HasShift.{v_2, u_2, u_5} D A
inst_6 : HasShift.{v_3, u_3, u_5} E A
inst_7 : HasShift.{v_4, u_4, u_5} E' A
F G_1 H : SingleFunctors.{v_1, u_1, v_2, u_2, u_5} C D A
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_8 : G.CommShift A
n m a a' a'' : A
ha' : n + a = a'
ha'' : m + a' = a''
X : C
⊢ 𝟙 (obj.{v_3, v_3, u_3, u_3} (shiftFunctor E (m + n)) (G.obj ((F.functor a'').obj X))) ≫
      NatTrans.app (Iso.inv (commShiftIso G (m + n))) ((F.functor a'').obj X) ≫
        𝟙 (G.obj (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (m + n)) ((F.functor a'').obj X))) ≫
          G.map ((F.shiftIso (m + n) a a'' ⋯).hom.app X) =
    NatTrans.app (Iso.hom (shiftFunctorAdd E m n)) (G.obj ((F.functor a'').obj X)) ≫
      𝟙
          (obj.{v_3, v_3, u_3, u_3} (shiftFunctor E n)
            (obj.{v_3, v_3, u_3, u_3} (shiftFunctor E m) (G.obj ((F.functor a'').obj X)))) ≫
        Functor.map (shiftFunctor E n)
            (𝟙 (obj.{v_3, v_3, u_3, u_3} (shiftFunctor E m) (G.obj ((F.functor a'').obj X))) ≫
              NatTrans.app (Iso.inv (commShiftIso G m)) ((F.functor a'').obj X) ≫
                𝟙 (G.obj (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D m) ((F.functor a'').obj X))) ≫
                  G.map ((F.shiftIso m a' a'' ha'').hom.app X)) ≫
          𝟙 (obj.{v_3, v_3, u_3, u_3} (shiftFunctor E n) (G.obj ((F.functor a').obj X))) ≫
            NatTrans.app (Iso.inv (commShiftIso G n)) ((F.functor a').obj X) ≫
              𝟙 (G.obj (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n) ((F.functor a').obj X))) ≫
                G.map ((F.shiftIso n a a' ha').hom.app X)
have w : Eq (α :=
  obj.{v_3, v_3, u_3, u_3} (shiftFunctor E (m + n)) (G.obj ((F.functor a'').obj X)) ⟶ G.obj ((F.functor a).obj X))
  (NatTrans.app (Iso.hom (shiftFunctorAdd E m n)) (G.obj ((F.functor a'').obj X)) ≫
    Functor.map (shiftFunctor E n) (NatTrans.app (Iso.inv (commShiftIso G m)) ((F.functor a'').obj X)) ≫
      NatTrans.app (Iso.inv (commShiftIso G n)) (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D m) ((F.functor a'').obj X)) ≫
        G.map (NatTrans.app (Iso.inv (shiftFunctorAdd D m n)) ((F.functor a'').obj X)) ≫
          G.map (NatTrans.app (Iso.hom (shiftFunctorAdd D m n)) ((F.functor a'').obj X)) ≫
            G.map (Functor.map (shiftFunctor D n) ((F.shiftIso m a' a'' ha'').hom.app X)) ≫
              G.map ((F.shiftIso n a a' ha').hom.app X))
  (NatTrans.app (Iso.hom (shiftFunctorAdd E m n)) (G.obj ((F.functor a'').obj X)) ≫
    Functor.map (shiftFunctor E n) (NatTrans.app (Iso.inv (commShiftIso G m)) ((F.functor a'').obj X)) ≫
      NatTrans.app (Iso.inv (commShiftIso G n)) (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D m) ((F.functor a'').obj X)) ≫
        G.map (Functor.map (shiftFunctor D n) ((F.shiftIso m a' a'' ha'').hom.app X)) ≫
          G.map ((F.shiftIso n a a' ha').hom.app X))
Tactic: simp only [F.shiftIso_add_hom_app n m a a' a'' ha' ha'', Functor.commShiftIso_add,
      Functor.CommShift.isoAdd_inv_app, Functor.map_comp, id_comp, assoc,
      Functor.commShiftIso_inv_naturality_assoc]