-- 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_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_5 :
  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_5_1 :
  Eq (α := Functor.{v, v, u, u} C C) (shiftFunctor C j ⋙ shiftFunctor C i)
    (Equivalence.inverse
        (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i : Discrete A } { as := j : Discrete A }
          (Discrete.eqToIso h) (Discrete.eqToIso ⋯) ⋯) ⋙
      Equivalence.functor
        (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i : Discrete A } { as := j } (Discrete.eqToIso h)
          (Discrete.eqToIso ⋯) ⋯))
e_3 :
  Eq (α := Functor.{v, v, u, u} C C) (shiftFunctor C j ⋙ shiftFunctor C i)
    (Equivalence.inverse
        (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i : Discrete A } { as := j : Discrete A }
          (Discrete.eqToIso h) (Discrete.eqToIso ⋯) ⋯) ⋙
      Equivalence.functor
        (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i : Discrete A } { as := j } (Discrete.eqToIso h)
          (Discrete.eqToIso ⋯) ⋯))
X : C
⊢ Eq.{v + 1} (α := obj.{v, v, u, u} (shiftFunctor C j ⋙ shiftFunctor C i) X ⟶ obj.{v, v, u, u} (𝟭 C) X)
    (NatTrans.app (Iso.hom (shiftFunctorCompIsoId C j i ⋯)) X)
    (NatTrans.app
      (Iso.hom
        (Equivalence.counitIso
          (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i : Discrete A } { as := j } (Discrete.eqToIso h)
            (Discrete.eqToIso ⋯) ⋯)))
      X)
have h₁ : Eq.{v + 1} (α := obj.{v, v, u, u} (shiftFunctor C i) (obj.{v, v, u, u} (shiftFunctor C j) X) ⟶ X)
  ((NatTrans.app (Iso.inv (shiftFunctorAdd C j i)) X ≫ NatTrans.app (eqToHom sorry) X) ≫
    NatTrans.app (Iso.hom (shiftFunctorZero C A)) X)
  (CategoryStruct.comp (Y :=
    obj.{v, v, u, u}
      (obj (shiftMonoidalFunctor C A)
        (MonoidalCategoryStruct.tensorObj (𝒞 := discreteCategory A) { as := j : Discrete A } { as := i : Discrete A }))
      X)
    (NatTrans.app (LaxMonoidal.μ (shiftMonoidalFunctor C A) { as := j } { as := i }) X)
    (CategoryStruct.comp (Y :=
      obj.{v, v, u, u}
        (obj (shiftMonoidalFunctor C A) (MonoidalCategoryStruct.tensorUnit (Discrete A) (𝒞 := discreteCategory A))) X)
      (NatTrans.app (map (shiftMonoidalFunctor C A) (eqToHom sorry)) X)
      (NatTrans.app (OplaxMonoidal.η (shiftMonoidalFunctor C A)) X)))
Tactic: dsimp [shiftFunctorCompIsoId, unitOfTensorIsoUnit,
        shiftFunctorAdd']