-- Module: Mathlib.CategoryTheory.Shift.Induced
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
s : A → Functor.{v_2, v_2, u_2, u_2} D D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst_4 : Full (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
inst_5 : Faithful (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
m₁ m₂ m₃ : A
X : C
eq :
  Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (m₁ + m₂ + m₃)) X) ⟶
      F.obj
        (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₃)
          (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₂) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₁) X))))
    (F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C (m₁ + m₂) m₃)) X) ≫
      F.map (map (shiftFunctor C m₃) (NatTrans.app (Iso.hom (shiftFunctorAdd C m₁ m₂)) X)))
    (F.map (eqToHom ⋯) ≫
      F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C m₁ (m₂ + m₃))) X) ≫
        F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C m₂ m₃)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₁) X)))
a :
  NatTrans.app (Iso.hom (i (m₁ + m₂ + m₃))) X ≫
      F.map (eqToHom ⋯) ≫
        F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C m₁ (m₂ + m₃))) X) ≫
          F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C m₂ m₃)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₁) X)) ≫
            (i m₃).inv.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₁ ⋙ shiftFunctor C m₂) X) ≫
              (s m₃).map ((i m₂).inv.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₁) X)) =
    CategoryStruct.comp (Y := (s (m₁ + (m₂ + m₃))).obj (F.obj X)) (NatTrans.app (eqToHom ⋯) (F.obj X))
      (CategoryStruct.comp (Y := (F ⋙ s (m₁ + m₂ + m₃)).obj X) (eqToHom ⋯)
          (NatTrans.app (Iso.hom (i (m₁ + m₂ + m₃))) X ≫ eqToHom ⋯) ≫
        F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C m₁ (m₂ + m₃))) X) ≫
          NatTrans.app (Iso.inv (i (m₂ + m₃))) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₁) X) ≫
            (s (m₂ + m₃)).map ((i m₁).inv.app X) ≫
              (Induced.add F s i m₂ m₃).hom.app ((s m₁).obj (F.obj X)) ≫ (s m₃).map ((s m₂).map ((i m₁).hom.app X)))
⊢ NatTrans.app (Iso.hom (i (m₁ + m₂ + m₃))) X ≫
      F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C (m₁ + m₂) m₃)) X) ≫
        (i m₃).inv.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (m₁ + m₂)) X) ≫
          (s m₃).map (F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C m₁ m₂)) X)) ≫
            (s m₃).map ((i m₂).inv.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₁) X)) ≫
              𝟙 ((s m₃).obj ((F ⋙ s m₂).obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₁) X))) =
    NatTrans.app (eqToHom ⋯) (F.obj X) ≫
      NatTrans.app (Iso.hom (i (m₁ + (m₂ + m₃)))) X ≫
        F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C m₁ (m₂ + m₃))) X) ≫
          NatTrans.app (Iso.inv (i (m₂ + m₃))) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₁) X) ≫
            (s (m₂ + m₃)).map ((i m₁).inv.app X) ≫
              (Induced.add F s i m₂ m₃).hom.app ((s m₁).obj (F.obj X)) ≫ (s m₃).map ((s m₂).map ((i m₁).hom.app X))

Tactic:
erw [Category.comp_id, ← NatTrans.naturality_assoc, reassoc_of% eq,
          dcongr_arg (fun a => (i a).hom.app X) (add_assoc m₁ m₂ m₃).symm]

Premises used: add_assoc, CategoryTheory.Category.comp_id, Eq.symm, CategoryTheory.Iso.hom, CategoryTheory.NatTrans.app, CategoryTheory.NatTrans.naturality_assoc, CategoryTheory.dcongr_arg