Module: Mathlib.CategoryTheory.Shift.Basic

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

Tactic:
dsimp [shiftFunctorCompIsoId, unitOfTensorIsoUnit,
        shiftFunctorAdd']

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