-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
D : Type u_2
inst_1 : Category.{v_1, u_2} D
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_2, u_1} D A
F : Functor.{v, v_1, u, u_2} C D
hF : F.FullyFaithful
s : A → Functor.{v, v, u, u} C C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
m₁ m₂ m₃ : A
X : C
h :
  Eq.{v_1 + 1} (α :=
    obj.{v_1, v_1, u_2, u_2} (shiftFunctor D (m₁ + m₂ + m₃)) (F.obj X) ⟶
      obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₃)
        (obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₁ ⋙ shiftFunctor D m₂) (F.obj X)))
    (NatTrans.app (Iso.hom (shiftFunctorAdd D (m₁ + m₂) m₃)) (F.obj X) ≫
        map (shiftFunctor D m₃) (NatTrans.app (Iso.hom (shiftFunctorAdd D m₁ m₂)) (F.obj X)) :
      obj.{v_1, v_1, u_2, u_2} (shiftFunctor D (m₁ + m₂ + m₃)) (F.obj X) ⟶
        obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₃)
          (obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₁ ⋙ shiftFunctor D m₂) (F.obj X)))
    (NatTrans.app (Iso.hom (shiftFunctorAdd' D m₁ (m₂ + m₃) (m₁ + m₂ + m₃) ⋯)) (F.obj X) ≫
        NatTrans.app (Iso.hom (shiftFunctorAdd D m₂ m₃)) (obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₁) (F.obj X)) :
      obj.{v_1, v_1, u_2, u_2} (shiftFunctor D (m₁ + m₂ + m₃)) (F.obj X) ⟶
        obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₂ ⋙ shiftFunctor D m₃)
          (obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₁) (F.obj X)))
⊢ NatTrans.app (Iso.hom (i (m₁ + m₂ + m₃))) X ≫
      NatTrans.app (Iso.hom (shiftFunctorAdd D (m₁ + m₂) m₃)) (F.obj X) ≫
        map (shiftFunctor D m₃) (NatTrans.app (Iso.inv (i (m₁ + m₂))) X) ≫
          (i m₃).inv.app ((s (m₁ + m₂)).obj X) ≫
            (i m₃).hom.app ((s (m₁ + m₂)).obj X) ≫ (F ⋙ shiftFunctor D m₃).map ((add hF s i m₁ m₂).hom.app X) =
    F.map (eqToHom ⋯) ≫
      NatTrans.app (Iso.hom (i (m₁ + (m₂ + m₃)))) X ≫
        NatTrans.app (Iso.hom (shiftFunctorAdd D m₁ (m₂ + m₃))) (F.obj X) ≫
          NatTrans.app (Iso.hom (shiftFunctorAdd D m₂ m₃)) (obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₁) (F.obj X)) ≫
            map (shiftFunctor D m₃) (map (shiftFunctor D m₂) ((i m₁).inv.app X)) ≫
              map (shiftFunctor D m₃) ((i m₂).inv.app ((s m₁).obj X))
have rw : Eq.{v_1 + 1} (α :=
  F.obj ((s (m₁ + m₂ + m₃)).obj X) ⟶ obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₃) (F.obj ((s m₂).obj ((s m₁).obj X))))
  (CategoryStruct.comp (Y := obj.{v_1, v_1, u_2, u_2} (shiftFunctor D (m₁ + m₂ + m₃)) (F.obj X))
      (CategoryStruct.comp (Y := (s (m₁ + (m₂ + m₃)) ⋙ F).obj X) (eqToHom sorry)
        (NatTrans.app (Iso.hom (i (m₁ + (m₂ + m₃)))) X ≫ eqToHom sorry))
      (NatTrans.app (Iso.hom (shiftFunctorAdd' D m₁ (m₂ + m₃) (m₁ + m₂ + m₃) sorry)) (F.obj X) ≫
        NatTrans.app (Iso.hom (shiftFunctorAdd D m₂ m₃)) (obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₁) (F.obj X)) ≫
          map (shiftFunctor D m₃) (map (shiftFunctor D m₂) ((i m₁).inv.app X) ≫ (i m₂).inv.app ((s m₁).obj X))) :
    F.obj ((s (m₁ + m₂ + m₃)).obj X) ⟶ obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₃) (F.obj ((s m₂).obj ((s m₁).obj X))))
  (F.map (eqToHom sorry) ≫
      NatTrans.app (Iso.hom (i (m₁ + (m₂ + m₃)))) X ≫
        NatTrans.app (Iso.hom (shiftFunctorAdd D m₁ (m₂ + m₃))) (F.obj X) ≫
          NatTrans.app (Iso.hom (shiftFunctorAdd D m₂ m₃)) (obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₁) (F.obj X)) ≫
            map (shiftFunctor D m₃) (map (shiftFunctor D m₂) ((i m₁).inv.app X)) ≫
              map (shiftFunctor D m₃) ((i m₂).inv.app ((s m₁).obj X)) :
    F.obj ((s (m₁ + m₂ + m₃)).obj X) ⟶ obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₃) (F.obj ((s m₂).obj ((s m₁).obj X))))
Tactic: rw [Functor.comp_map, map_add_hom_app,
          Functor.map_comp, Functor.map_comp, Iso.inv_hom_id_app_assoc,
          ← Functor.map_comp_assoc _ ((i (m₁ + m₂)).inv.app X), Iso.inv_hom_id_app,
          Functor.map_id, Category.id_comp, reassoc_of% h,
          dcongr_arg (fun a => (i a).hom.app X) (add_assoc m₁ m₂ m₃)]