Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
i j : A
h : i + j = 0
X : C
⊢ (shiftFunctor C i).map ((shiftFunctorCompIsoId C i j h).symm.hom.app X) ≫
      (shiftFunctorCompIsoId C j i ⋯).hom.app ((shiftFunctor C i).obj X) =
    𝟙 ((shiftFunctor C i).obj X)

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

Goal state after:
case e'_2.e'_6.e'_8.e'_7.e'_5
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
i j : A
h : i + j = 0
X : C
e_1✝ :
  ((shiftFunctor C i).obj X ⟶ (shiftFunctor C i).obj X) =
    ((equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h) (Discrete.eqToIso ⋯)
              ⋯).functor.obj
        X ⟶
      (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h) (Discrete.eqToIso ⋯)
              ⋯).functor.obj
        X)
e_3✝ :
  (shiftFunctor C i).obj X =
    (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h) (Discrete.eqToIso ⋯)
            ⋯).functor.obj
      X
e_4✝¹ :
  (shiftFunctor C i).obj ((shiftFunctor C j).obj ((shiftFunctor C i).obj X)) =
    (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h) (Discrete.eqToIso ⋯)
            ⋯).functor.obj
      ((equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
              (Discrete.eqToIso ⋯) ⋯).inverse.obj
        ((equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
                (Discrete.eqToIso ⋯) ⋯).functor.obj
          X))
e_7✝ :
  (shiftFunctor C j).obj ((shiftFunctor C i).obj X) =
    (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h) (Discrete.eqToIso ⋯)
            ⋯).inverse.obj
      ((equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
              (Discrete.eqToIso ⋯) ⋯).functor.obj
        X)
e_6✝ :
  shiftFunctor C i ⋙ shiftFunctor C j =
    (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h) (Discrete.eqToIso ⋯)
          ⋯).functor ⋙
      (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h) (Discrete.eqToIso ⋯)
          ⋯).inverse
e_4✝ :
  shiftFunctor C i ⋙ shiftFunctor C j =
    (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h) (Discrete.eqToIso ⋯)
          ⋯).functor ⋙
      (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h) (Discrete.eqToIso ⋯)
          ⋯).inverse
⊢ (shiftFunctorCompIsoId C i j h).symm =
    (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h) (Discrete.eqToIso ⋯)
        ⋯).unitIso

case e'_2.e'_7.e'_7.e'_5
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
i j : A
h : i + j = 0
X : C
e_1✝ :
  ((shiftFunctor C i).obj X ⟶ (shiftFunctor C i).obj X) =
    ((equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h) (Discrete.eqToIso ⋯)
              ⋯).functor.obj
        X ⟶
      (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h) (Discrete.eqToIso ⋯)
              ⋯).functor.obj
        X)
e_4✝ :
  (shiftFunctor C i).obj ((shiftFunctor C j).obj ((shiftFunctor C i).obj X)) =
    (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h) (Discrete.eqToIso ⋯)
            ⋯).functor.obj
      ((equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
              (Discrete.eqToIso ⋯) ⋯).inverse.obj
        ((equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
                (Discrete.eqToIso ⋯) ⋯).functor.obj
          X))
e_5✝¹ :
  (shiftFunctor C i).obj X =
    (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h) (Discrete.eqToIso ⋯)
            ⋯).functor.obj
      X
e_5✝ :
  shiftFunctor C j ⋙ shiftFunctor C i =
    (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h) (Discrete.eqToIso ⋯)
          ⋯).inverse ⋙
      (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h) (Discrete.eqToIso ⋯)
          ⋯).functor
e_3✝ :
  shiftFunctor C j ⋙ shiftFunctor C i =
    (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h) (Discrete.eqToIso ⋯)
          ⋯).inverse ⋙
      (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h) (Discrete.eqToIso ⋯)
          ⋯).functor
⊢ shiftFunctorCompIsoId C j i ⋯ =
    (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h) (Discrete.eqToIso ⋯)
        ⋯).counitIso