-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddGroup A
inst_2 : HasShift.{v, u, u_1} C A
i j : A
h : i + j = 0
X_1 : C
e_1 :
  (obj.{v, v, u, u} (shiftFunctor C i) X_1 ⟶ obj.{v, v, u, u} (shiftFunctor C i) X_1) =
    (obj.{v, v, u, u}
        (Equivalence.functor
          (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i : Discrete A } { as := j : Discrete A }
            (Discrete.eqToIso h) (Discrete.eqToIso ⋯) ⋯))
        X_1 ⟶
      obj.{v, v, u, u}
        (Equivalence.functor
          (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i : Discrete A } { as := j } (Discrete.eqToIso h)
            (Discrete.eqToIso ⋯) ⋯))
        X_1)
e_3 :
  obj.{v, v, u, u} (shiftFunctor C i) X_1 =
    obj.{v, v, u, u}
      (Equivalence.functor
        (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i : Discrete A } { as := j } (Discrete.eqToIso h)
          (Discrete.eqToIso ⋯) ⋯))
      X_1
e_4 :
  obj.{v, v, u, u} (shiftFunctor C i) (obj.{v, v, u, u} (shiftFunctor C j) (obj.{v, v, u, u} (shiftFunctor C i) X_1)) =
    obj.{v, v, u, u}
      (Equivalence.functor
        (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i : Discrete A } { as := j } (Discrete.eqToIso h)
          (Discrete.eqToIso ⋯) ⋯))
      (obj.{v, v, u, u}
        (Equivalence.inverse
          (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i : Discrete A } { as := j : Discrete A }
            (Discrete.eqToIso h) (Discrete.eqToIso ⋯) ⋯))
        (obj.{v, v, u, u}
          (Equivalence.functor
            (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i : Discrete A } { as := j : Discrete A }
              (Discrete.eqToIso h) (Discrete.eqToIso ⋯) ⋯))
          X_1))
e_7 :
  obj.{v, v, u, u} (shiftFunctor C j) (obj.{v, v, u, u} (shiftFunctor C i) X_1) =
    obj.{v, v, u, u}
      (Equivalence.inverse
        (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i : Discrete A } { as := j } (Discrete.eqToIso h)
          (Discrete.eqToIso ⋯) ⋯))
      (obj.{v, v, u, u}
        (Equivalence.functor
          (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i : Discrete A } { as := j : Discrete A }
            (Discrete.eqToIso h) (Discrete.eqToIso ⋯) ⋯))
        X_1)
e_6 :
  Eq (α := Functor.{v, v, u, u} C C) (shiftFunctor C i ⋙ shiftFunctor C j)
    (Equivalence.functor
        (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i : Discrete A } { as := j : Discrete A }
          (Discrete.eqToIso h) (Discrete.eqToIso ⋯) ⋯) ⋙
      Equivalence.inverse
        (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i : Discrete A } { as := j } (Discrete.eqToIso h)
          (Discrete.eqToIso ⋯) ⋯))
e_4_1 :
  Eq (α := Functor.{v, v, u, u} C C) (shiftFunctor C i ⋙ shiftFunctor C j)
    (Equivalence.functor
        (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i : Discrete A } { as := j : Discrete A }
          (Discrete.eqToIso h) (Discrete.eqToIso ⋯) ⋯) ⋙
      Equivalence.inverse
        (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i : Discrete A } { as := j } (Discrete.eqToIso h)
          (Discrete.eqToIso ⋯) ⋯))
X : C
⊢ Eq.{v + 1} (α := X ⟶ obj.{v, v, u, u} (shiftFunctor C j) (obj.{v, v, u, u} (shiftFunctor C i) X))
    (NatTrans.app (Iso.inv (shiftFunctorZero C A)) X ≫
      NatTrans.app (eqToHom ⋯) X ≫ NatTrans.app (Iso.hom (shiftFunctorAdd C i j)) X)
    (CategoryStruct.comp (Y :=
      obj.{v, v, u, u}
        (obj (shiftMonoidalFunctor C A)
          (MonoidalCategoryStruct.tensorObj (𝒞 := discreteCategory A) { as := i : Discrete A }
            { as := j : Discrete A }))
        X)
      (CategoryStruct.comp (Y :=
        obj.{v, v, u, u}
          (obj (shiftMonoidalFunctor C A) (MonoidalCategoryStruct.tensorUnit (Discrete A) (𝒞 := discreteCategory A))) X)
        (NatTrans.app (LaxMonoidal.ε (shiftMonoidalFunctor C A)) X)
        (NatTrans.app (map (shiftMonoidalFunctor C A) (eqToHom ⋯)) X))
      (NatTrans.app (OplaxMonoidal.δ (shiftMonoidalFunctor C A) { as := i } { as := j }) X))
have h₁ : Eq.{v + 1} (α := X ⟶ obj.{v, v, u, u} (shiftFunctor C j) (obj.{v, v, u, u} (shiftFunctor C i) X))
  (NatTrans.app (Iso.inv (shiftFunctorZero C A)) X ≫
    NatTrans.app (eqToHom sorry) X ≫ NatTrans.app (Iso.hom (shiftFunctorAdd C i j)) X)
  (CategoryStruct.comp (Y :=
    obj.{v, v, u, u}
      (obj (shiftMonoidalFunctor C A) (MonoidalCategoryStruct.tensorUnit (Discrete A) (𝒞 := discreteCategory A))) X)
    (NatTrans.app (LaxMonoidal.ε (shiftMonoidalFunctor C A)) X)
    (NatTrans.app (eqToHom sorry) X ≫ NatTrans.app (OplaxMonoidal.δ (shiftMonoidalFunctor C A) { as := i } { as := j }) X))
Tactic: simp only [Category.assoc, eqToHom_map]