-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Induced (goal)
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)))
⊢ 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))
have a : NatTrans.app (Iso.hom (i (m₁ + m₂ + m₃))) X ≫
    F.map (eqToHom sorry) ≫
      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 sorry) (F.obj X))
    (CategoryStruct.comp (Y := (F ⋙ s (m₁ + m₂ + m₃)).obj X) (eqToHom sorry)
        (NatTrans.app (Iso.hom (i (m₁ + m₂ + m₃))) X ≫ eqToHom sorry) ≫
      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]