Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: 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

pp: 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

Tactic:
all_goals
      ext X
      dsimp [shiftFunctorCompIsoId, unitOfTensorIsoUnit,
        shiftFunctorAdd']
      simp only [Category.assoc, eqToHom_map]
      rfl

Goal state after: