-- 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 : C
e_1 :
  (obj.{v, v, u, u} (shiftFunctor C i) X ⟶ obj.{v, v, u, u} (shiftFunctor C i) X) =
    (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 ⟶
      obj.{v, v, u, u}
        (Equivalence.functor
          (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i : Discrete A } { as := j } (Discrete.eqToIso h)
            (Discrete.eqToIso ⋯) ⋯))
        X)
e_3 :
  obj.{v, v, u, u} (shiftFunctor C i) X =
    obj.{v, v, u, u}
      (Equivalence.functor
        (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i : Discrete A } { as := j } (Discrete.eqToIso h)
          (Discrete.eqToIso ⋯) ⋯))
      X
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)) =
    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))
e_7 :
  obj.{v, v, u, u} (shiftFunctor C j) (obj.{v, v, u, u} (shiftFunctor C i) X) =
    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)
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 ⋯) ⋯))
⊢ Eq (α := Iso (C := Functor.{v, v, u, u} C C) (𝟭 C) (shiftFunctor C i ⋙ shiftFunctor C j))
    (Iso.symm (shiftFunctorCompIsoId C i j h))
    (Equivalence.unitIso
      (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i : Discrete A } { as := j } (Discrete.eqToIso h)
        (Discrete.eqToIso ⋯) ⋯))
have h₁ : ∀ (X : C),
  Eq.{v + 1} (α := obj.{v, v, u, u} (𝟭 C) X ⟶ obj.{v, v, u, u} (shiftFunctor C i ⋙ shiftFunctor C j) X)
    (NatTrans.app (Iso.hom (Iso.symm (shiftFunctorCompIsoId C i j h))) X)
    (NatTrans.app
      (Iso.hom
        (Equivalence.unitIso
          (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i : Discrete A } { as := j } (Discrete.eqToIso h)
            (Discrete.eqToIso sorry) sorry)))
      X)
Tactic: ext X