-- 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
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 ⋯) ⋯))
          X ⟶
        obj.{v, v, u, u}
          (Equivalence.functor
            (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i : Discrete A } { as := j } (Discrete.eqToIso h)
              (Discrete.eqToIso ⋯) ⋯))
          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 ⋯) ⋯))
          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 ⋯) ⋯))
            (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)) →
        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) →
          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 (α := 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 ⋯) ⋯))
⊢ 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) (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 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 →
      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 sorry) sorry) ⋙
            Equivalence.functor
              (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 j ⋙ shiftFunctor C i)
            (Equivalence.inverse
                (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i : Discrete A } { as := j : Discrete A }
                  (Discrete.eqToIso h) (Discrete.eqToIso sorry) sorry) ⋙
              Equivalence.functor
                (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) (shiftFunctor C j ⋙ shiftFunctor C i) (𝟭 C))
            (shiftFunctorCompIsoId C j i sorry)
            (Equivalence.counitIso
              (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