-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.InducedShiftSequence (goal)
Goal:
C : Type u_1
D : Type u_2
A : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} A
L : Functor.{v_1, v_2, u_1, u_2} C D
F : Functor.{v_2, v_3, u_2, u_3} D A
G : Functor.{v_1, v_3, u_1, u_3} C A
e : L ⋙ F ≅ G
M : Type u_4
inst_3 : AddMonoid M
inst_4 : HasShift.{v_1, u_1, u_4} C M
inst_5 : G.ShiftSequence M
F' : M → Functor.{v_2, v_3, u_2, u_3} D A
e' : (m : M) → L ⋙ F' m ≅ G.shift m
inst_6 : Full (C := Functor.{v_2, v_3, u_2, u_3} D A) (obj (whiskeringLeft C D A) L)
inst_7 : Faithful (C := Functor.{v_2, v_3, u_2, u_3} D A) (obj (whiskeringLeft C D A) L)
inst_8 : HasShift.{v_2, u_2, u_4} D M
inst_9 : L.CommShift M
n m a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
K : C
⊢ (F' a).map
        (NatTrans.app (Iso.hom (shiftFunctorAdd D m n)) (L.obj K) ≫
          map (shiftFunctor D n) (NatTrans.app (Iso.inv (commShiftIso L m)) K) ≫
            NatTrans.app (Iso.inv (commShiftIso L n)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) K)) ≫
      (e' a).hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) K)) ≫
        NatTrans.app (Iso.hom (G.shiftIso n a a' ha')) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) K) ≫
          NatTrans.app (Iso.hom (G.shiftIso m a' a'' ha'')) K ≫ (e' a'').inv.app K =
    (F' a).map (NatTrans.app (Iso.hom (shiftFunctorAdd D m n)) (L.obj K)) ≫
      (shiftFunctor D n ⋙ F' a).map (NatTrans.app (Iso.inv (commShiftIso L m)) K) ≫
        ((F' a).map (NatTrans.app (Iso.inv (commShiftIso L n)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) K)) ≫
            (e' a).hom.app
                (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) K)) ≫
              NatTrans.app (Iso.hom (G.shiftIso n a a' ha')) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) K) ≫
                (e' a').inv.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) K)) ≫
          (e' a').hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) K) ≫
            NatTrans.app (Iso.hom (G.shiftIso m a' a'' ha'')) K ≫ (e' a'').inv.app K
have w : Eq (α := (F' a).obj (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (m + n)) (L.obj K)) ⟶ (F' a'').obj (L.obj K))
  ((F' a).map
      (NatTrans.app (Iso.hom (shiftFunctorAdd D m n)) (L.obj K) ≫
        map (shiftFunctor D n) (NatTrans.app (Iso.inv (commShiftIso L m)) K) ≫
          NatTrans.app (Iso.inv (commShiftIso L n)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) K)) ≫
    (e' a).hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) K)) ≫
      NatTrans.app (Iso.hom (G.shiftIso n a a' ha')) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) K) ≫
        NatTrans.app (Iso.hom (G.shiftIso m a' a'' ha'')) K ≫ (e' a'').inv.app K)
  ((F' a).map (NatTrans.app (Iso.hom (shiftFunctorAdd D m n)) (L.obj K)) ≫
    (F' a).map (map (shiftFunctor D n) (NatTrans.app (Iso.inv (commShiftIso L m)) K)) ≫
      ((F' a).map (NatTrans.app (Iso.inv (commShiftIso L n)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) K)) ≫
          (e' a).hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) K)) ≫
            NatTrans.app (Iso.hom (G.shiftIso n a a' ha')) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) K) ≫
              (e' a').inv.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) K)) ≫
        (e' a').hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) K) ≫
          NatTrans.app (Iso.hom (G.shiftIso m a' a'' ha'')) K ≫ (e' a'').inv.app K)
Tactic: dsimp