-- Module: Mathlib.CategoryTheory.Shift.InducedShiftSequence
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
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)) ≫
      (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)) ≫
          (F' a).map (L.map (NatTrans.app (Iso.inv (shiftFunctorAdd C m n)) K)) ≫
            (F' a).map (L.map (NatTrans.app (Iso.hom (shiftFunctorAdd C m n)) 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)) ≫
      NatTrans.app (Iso.hom (induced.shiftIso L G M F' e' n a a' ha'))
          (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D m) (L.obj K)) ≫
        (F' a').map (NatTrans.app (Iso.inv (commShiftIso L 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)
⊢ NatTrans.app (Iso.hom (induced.shiftIso L G M F' e' (m + n) a a'' ⋯)) (L.obj K) =
    (F' a).map (NatTrans.app (Iso.hom (shiftFunctorAdd D m n)) (L.obj K)) ≫
      𝟙
          ((F' a).obj
            (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n) (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D m) (L.obj K)))) ≫
        NatTrans.app (Iso.hom (induced.shiftIso L G M F' e' n a a' ha'))
            (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D m) (L.obj K)) ≫
          NatTrans.app (Iso.hom (induced.shiftIso L G M F' e' m a' a'' ha'')) (L.obj K)

Tactic:
simp only [id_comp, induced.shiftIso_hom_app_obj,
      G.shiftIso_add_hom_app n m a a' a'' ha' ha'', L.commShiftIso_add,
      comp_obj, CommShift.isoAdd_inv_app, (F' a).map_comp, assoc,
      ← (e' a).hom.naturality_assoc, comp_map]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Functor.CommShift.isoAdd_inv_app, CategoryTheory.Category.assoc, CategoryTheory.Functor.CommShift.commShiftIso_add, CategoryTheory.Functor.shiftIso_add_hom_app, CategoryTheory.Functor.ShiftSequence.induced.shiftIso_hom_app_obj, CategoryTheory.Functor.map_comp, CategoryTheory.Iso.hom, CategoryTheory.Functor.comp_map, CategoryTheory.NatTrans.naturality_assoc, CategoryTheory.Category.id_comp