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
X : C
⊢ (shiftFunctorCompIsoId C i j h).symm.hom.app X =
    (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h) (Discrete.eqToIso ⋯)
              ⋯).unitIso.hom.app
      X

Tactic:
dsimp [shiftFunctorCompIsoId, unitOfTensorIsoUnit,
        shiftFunctorAdd']

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
X : C
⊢ (shiftFunctorZero C A).inv.app X ≫ (eqToHom ⋯).app X ≫ (shiftFunctorAdd C i j).hom.app X =
    ((LaxMonoidal.ε (shiftMonoidalFunctor C A)).app X ≫ ((shiftMonoidalFunctor C A).map (eqToHom ⋯)).app X) ≫
      (OplaxMonoidal.δ (shiftMonoidalFunctor C A) { as := i } { as := j }).app X