-- 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 :
  (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
⊢ 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)

Tactic:
simp only [← NatTrans.naturality_assoc, induced.shiftIso_hom_app_obj,
      ← Functor.map_comp_assoc, ← Functor.map_comp, Iso.inv_hom_id_app, comp_obj,
      Functor.map_id, id_comp]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Functor.ShiftSequence.induced.shiftIso_hom_app_obj, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp, CategoryTheory.Iso.inv_hom_id_app, CategoryTheory.NatTrans.naturality_assoc, CategoryTheory.Category.id_comp