-- 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
⊢ Eq.{v + 1} (α := obj.{v, v, u, u} (shiftFunctor C i) X ⟶ obj.{v, v, u, u} (shiftFunctor C i) X)
    (map (shiftFunctor C i) (NatTrans.app (Iso.hom (Iso.symm (shiftFunctorCompIsoId C i j h))) X) ≫
        NatTrans.app (Iso.hom (shiftFunctorCompIsoId C j i ⋯)) (obj.{v, v, u, u} (shiftFunctor C i) X) :
      obj.{v, v, u, u} (shiftFunctor C i) X ⟶ obj.{v, v, u, u} (shiftFunctor C i) X)
    (𝟙 (obj.{v, v, u, u} (shiftFunctor C i) X) :
      obj.{v, v, u, u} (shiftFunctor C i) X ⟶ obj.{v, v, u, u} (shiftFunctor C i) X)
have h₁ : (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 sorry) sorry))
        X ⟶
      obj.{v, v, u, u}
        (Equivalence.functor
          (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i : Discrete A } { as := j } (Discrete.eqToIso h)
            (Discrete.eqToIso sorry) sorry))
        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.eqToIso h)
            (Discrete.eqToIso sorry) sorry))
        X →
    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 sorry) sorry))
          (obj.{v, v, u, u}
            (Equivalence.inverse
              (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i : Discrete A } { as := j : Discrete A }
                (Discrete.eqToIso h) (Discrete.eqToIso sorry) sorry))
            (obj.{v, v, u, u}
              (Equivalence.functor
                (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i : Discrete A } { as := j : Discrete A }
                  (Discrete.eqToIso h) (Discrete.eqToIso sorry) sorry))
              X)) →
      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 sorry) sorry))
            (obj.{v, v, u, u}
              (Equivalence.functor
                (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i : Discrete A } { as := j : Discrete A }
                  (Discrete.eqToIso h) (Discrete.eqToIso sorry) sorry))
              X) →
        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 sorry) sorry) ⋙
              Equivalence.inverse
                (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i : Discrete A } { as := j }
                  (Discrete.eqToIso h) (Discrete.eqToIso sorry) sorry)) →
          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 sorry) sorry) ⋙
                Equivalence.inverse
                  (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i : Discrete A } { as := j }
                    (Discrete.eqToIso h) (Discrete.eqToIso sorry) sorry)) →
            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 sorry) sorry))
Tactic: convert!
      (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) ⟨i⟩ ⟨j⟩ (Discrete.eqToIso h)
            (Discrete.eqToIso (by dsimp; rw [← add_left_inj j, add_assoc, h, zero_add, add_zero]))
            (Subsingleton.elim _ _)).functor_unitIso_comp
        X