-- Lean 4 proof step from Mathlib.CategoryTheory.DifferentialObject (goal)
Goal:
S : Type u_1
inst : AddCommGroupWithOne S
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : HasShift.{v, u, u_1} C S
m n : S
X : DifferentialObject.{v, u, u_1} S C
⊢ Eq (α :=
    Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (m + n)) X.obj ⟶
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 1)
        (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C m) X.obj)))
    ((Functor.map (CategoryTheory.shiftFunctor C (m + n)) X.d ≫
          NatTrans.app (Iso.hom (shiftFunctorComm.{v, u, u_1} C 1 (m + n))) X.obj) ≫
        Functor.map (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 1)
          (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd C m n)) X.obj) :
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (m + n)) X.obj ⟶
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 1)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n)
            (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C m) X.obj)))
    (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd C m n)) X.obj ≫
        CategoryStruct.comp (Y :=
          Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n)
            (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 1)
              (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C m) X.obj)))
          (Functor.map (CategoryTheory.shiftFunctor C n)
            (Functor.map (CategoryTheory.shiftFunctor C m) X.d ≫
              NatTrans.app (Iso.hom (shiftFunctorComm.{v, u, u_1} C 1 m)) X.obj))
          (NatTrans.app (Iso.hom (shiftFunctorComm.{v, u, u_1} C 1 n))
            (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C m) X.obj)) :
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (m + n)) X.obj ⟶
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 1)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n)
            (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C m) X.obj)))
have refine_1 : Eq (α :=
  Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C m ⋙ CategoryTheory.shiftFunctor C n) X.obj ⟶
    Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 1)
      (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n)
        (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C m) X.obj)))
  (NatTrans.app (Iso.inv (CategoryTheory.shiftFunctorAdd C m n)) X.obj ≫
      (Functor.map (CategoryTheory.shiftFunctor C (m + n)) X.d ≫
          NatTrans.app (Iso.hom (shiftFunctorComm.{v, u, u_1} C 1 (m + n))) X.obj) ≫
        Functor.map (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 1)
          (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd C m n)) X.obj) :
    Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C m ⋙ CategoryTheory.shiftFunctor C n) X.obj ⟶
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 1)
        (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C m) X.obj)))
  (NatTrans.app (Iso.inv (CategoryTheory.shiftFunctorAdd C m n)) X.obj ≫
      NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd C m n)) X.obj ≫
        CategoryStruct.comp (Y :=
          Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n)
            (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 1)
              (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C m) X.obj)))
          (Functor.map (CategoryTheory.shiftFunctor C n)
            (Functor.map (CategoryTheory.shiftFunctor C m) X.d ≫
              NatTrans.app (Iso.hom (shiftFunctorComm.{v, u, u_1} C 1 m)) X.obj))
          (NatTrans.app (Iso.hom (shiftFunctorComm.{v, u, u_1} C 1 n))
            (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C m) X.obj)) :
    Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C m ⋙ CategoryTheory.shiftFunctor C n) X.obj ⟶
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor.{v, u, u_1} C (A := S) 1)
        (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C m) X.obj)))
Tactic: rw [← cancel_epi ((shiftFunctorAdd C m n).inv.app X.obj)]