[GOAL]
C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
F : A → C ⥤ C
zero : F 0 ≅ 𝟭 C
add : (n m : A) → F (n + m) ≅ F n ⋙ F m
m₁ m₂ m₃ : A
X : C
⊢ (F (m₁ + m₂ + m₃)).obj X = (F (m₁ + (m₂ + m₃))).obj X
[PROOFSTEP]
rw [add_assoc]
[GOAL]
C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
F : A → C ⥤ C
zero : F 0 ≅ 𝟭 C
add : (n m : A) → F (n + m) ≅ F n ⋙ F m
assoc_hom_app :
  autoParam
    (∀ (m₁ m₂ m₃ : A) (X : C),
      NatTrans.app (add (m₁ + m₂) m₃).hom X ≫ (F m₃).map (NatTrans.app (add m₁ m₂).hom X) =
        eqToHom (_ : (F (m₁ + m₂ + m₃)).obj X = (F (m₁ + (m₂ + m₃))).obj X) ≫
          NatTrans.app (add m₁ (m₂ + m₃)).hom X ≫ NatTrans.app (add m₂ m₃).hom ((F m₁).obj X))
    _auto✝
n : A
X : C
⊢ (F (0 + n)).obj X = (F n).obj ((𝟭 C).obj X)
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
F : A → C ⥤ C
zero : F 0 ≅ 𝟭 C
add : (n m : A) → F (n + m) ≅ F n ⋙ F m
assoc_hom_app :
  autoParam
    (∀ (m₁ m₂ m₃ : A) (X : C),
      NatTrans.app (add (m₁ + m₂) m₃).hom X ≫ (F m₃).map (NatTrans.app (add m₁ m₂).hom X) =
        eqToHom (_ : (F (m₁ + m₂ + m₃)).obj X = (F (m₁ + (m₂ + m₃))).obj X) ≫
          NatTrans.app (add m₁ (m₂ + m₃)).hom X ≫ NatTrans.app (add m₂ m₃).hom ((F m₁).obj X))
    _auto✝
n : A
X : C
⊢ (F (0 + n)).obj X = (F n).obj X
[PROOFSTEP]
rw [zero_add]
[GOAL]
C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
F : A → C ⥤ C
zero : F 0 ≅ 𝟭 C
add : (n m : A) → F (n + m) ≅ F n ⋙ F m
assoc_hom_app :
  autoParam
    (∀ (m₁ m₂ m₃ : A) (X : C),
      NatTrans.app (add (m₁ + m₂) m₃).hom X ≫ (F m₃).map (NatTrans.app (add m₁ m₂).hom X) =
        eqToHom (_ : (F (m₁ + m₂ + m₃)).obj X = (F (m₁ + (m₂ + m₃))).obj X) ≫
          NatTrans.app (add m₁ (m₂ + m₃)).hom X ≫ NatTrans.app (add m₂ m₃).hom ((F m₁).obj X))
    _auto✝
zero_add_hom_app :
  autoParam
    (∀ (n : A) (X : C),
      NatTrans.app (add 0 n).hom X =
        eqToHom (_ : (F (0 + n)).obj X = (F n).obj ((𝟭 C).obj X)) ≫ (F n).map (NatTrans.app zero.inv X))
    _auto✝
n : A
X : C
⊢ (F (n + 0)).obj X = (𝟭 C).obj ((F n).obj X)
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
F : A → C ⥤ C
zero : F 0 ≅ 𝟭 C
add : (n m : A) → F (n + m) ≅ F n ⋙ F m
assoc_hom_app :
  autoParam
    (∀ (m₁ m₂ m₃ : A) (X : C),
      NatTrans.app (add (m₁ + m₂) m₃).hom X ≫ (F m₃).map (NatTrans.app (add m₁ m₂).hom X) =
        eqToHom (_ : (F (m₁ + m₂ + m₃)).obj X = (F (m₁ + (m₂ + m₃))).obj X) ≫
          NatTrans.app (add m₁ (m₂ + m₃)).hom X ≫ NatTrans.app (add m₂ m₃).hom ((F m₁).obj X))
    _auto✝
zero_add_hom_app :
  autoParam
    (∀ (n : A) (X : C),
      NatTrans.app (add 0 n).hom X =
        eqToHom (_ : (F (0 + n)).obj X = (F n).obj ((𝟭 C).obj X)) ≫ (F n).map (NatTrans.app zero.inv X))
    _auto✝
n : A
X : C
⊢ (F (n + 0)).obj X = (F n).obj X
[PROOFSTEP]
rw [add_zero]
[GOAL]
C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
h : ShiftMkCore C A
m₁ m₂ m₃ : A
X : C
⊢ (F h (m₁ + (m₂ + m₃))).obj X = (F h (m₁ + m₂ + m₃)).obj X
[PROOFSTEP]
rw [add_assoc]
[GOAL]
C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
h : ShiftMkCore C A
m₁ m₂ m₃ : A
X : C
⊢ (F h m₃).map (NatTrans.app (add h m₁ m₂).inv X) ≫ NatTrans.app (add h (m₁ + m₂) m₃).inv X =
    NatTrans.app (add h m₂ m₃).inv ((F h m₁).obj X) ≫
      NatTrans.app (add h m₁ (m₂ + m₃)).inv X ≫ eqToHom (_ : (F h (m₁ + (m₂ + m₃))).obj X = (F h (m₁ + m₂ + m₃)).obj X)
[PROOFSTEP]
rw [← cancel_mono ((h.add (m₁ + m₂) m₃).hom.app X ≫ (h.F m₃).map ((h.add m₁ m₂).hom.app X)), Category.assoc,
  Category.assoc, Category.assoc, Iso.inv_hom_id_app_assoc, ← Functor.map_comp, Iso.inv_hom_id_app, Functor.map_id,
  h.assoc_hom_app, eqToHom_trans_assoc, eqToHom_refl, Category.id_comp, Iso.inv_hom_id_app_assoc, Iso.inv_hom_id_app]
[GOAL]
C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
h : ShiftMkCore C A
m₁ m₂ m₃ : A
X : C
⊢ 𝟙 ((F h m₃).obj ((F h m₁ ⋙ F h m₂).obj X)) = 𝟙 ((F h m₂ ⋙ F h m₃).obj ((F h m₁).obj X))
[PROOFSTEP]
rfl
[GOAL]
C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
h : ShiftMkCore C A
n : A
X : C
⊢ (F h n).obj ((𝟭 C).obj X) = (F h (0 + n)).obj X
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
h : ShiftMkCore C A
n : A
X : C
⊢ (F h n).obj X = (F h (0 + n)).obj X
[PROOFSTEP]
rw [zero_add]
[GOAL]
C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
h : ShiftMkCore C A
n : A
X : C
⊢ NatTrans.app (add h 0 n).inv X =
    (F h n).map (NatTrans.app h.zero.hom X) ≫ eqToHom (_ : (F h n).obj ((𝟭 C).obj X) = (F h (0 + n)).obj X)
[PROOFSTEP]
rw [← cancel_epi ((h.add 0 n).hom.app X), Iso.hom_inv_id_app, h.zero_add_hom_app, Category.assoc, ←
  Functor.map_comp_assoc, Iso.inv_hom_id_app, Functor.map_id, Category.id_comp, eqToHom_trans, eqToHom_refl]
[GOAL]
C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
h : ShiftMkCore C A
n : A
X : C
⊢ (𝟭 C).obj ((F h n).obj X) = (F h (n + 0)).obj X
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
h : ShiftMkCore C A
n : A
X : C
⊢ (F h n).obj X = (F h (n + 0)).obj X
[PROOFSTEP]
rw [add_zero]
[GOAL]
C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
h : ShiftMkCore C A
n : A
X : C
⊢ NatTrans.app (add h n 0).inv X =
    NatTrans.app h.zero.hom ((F h n).obj X) ≫ eqToHom (_ : (𝟭 C).obj ((F h n).obj X) = (F h (n + 0)).obj X)
[PROOFSTEP]
rw [← cancel_epi ((h.add n 0).hom.app X), Iso.hom_inv_id_app, h.add_zero_hom_app, Category.assoc,
  Iso.inv_hom_id_app_assoc, eqToHom_trans, eqToHom_refl]
[GOAL]
C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
h : ShiftMkCore C A
src✝ : Discrete A ⥤ C ⥤ C := Discrete.functor h.F
⊢ ∀ {X Y X' Y' : Discrete A} (f : X ⟶ Y) (g : X' ⟶ Y'),
    MonoidalCategory.tensorHom ((Functor.mk src✝.toPrefunctor).map f) ((Functor.mk src✝.toPrefunctor).map g) ≫
        (fun m n => (ShiftMkCore.add h m.as n.as).inv) Y Y' =
      (fun m n => (ShiftMkCore.add h m.as n.as).inv) X X' ≫
        (Functor.mk src✝.toPrefunctor).map (MonoidalCategory.tensorHom f g)
[PROOFSTEP]
rintro ⟨X⟩ ⟨Y⟩ ⟨X'⟩ ⟨Y'⟩ ⟨⟨⟨rfl⟩⟩⟩ ⟨⟨⟨rfl⟩⟩⟩
[GOAL]
case mk.mk.mk.mk.up.up.refl.up.up.refl
C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
h : ShiftMkCore C A
src✝ : Discrete A ⥤ C ⥤ C := Discrete.functor h.F
X X' : A
⊢ MonoidalCategory.tensorHom
        ((Functor.mk src✝.toPrefunctor).map { down := { down := (_ : { as := X }.as = { as := X }.as) } })
        ((Functor.mk src✝.toPrefunctor).map { down := { down := (_ : { as := X' }.as = { as := X' }.as) } }) ≫
      (fun m n => (ShiftMkCore.add h m.as n.as).inv) { as := X } { as := X' } =
    (fun m n => (ShiftMkCore.add h m.as n.as).inv) { as := X } { as := X' } ≫
      (Functor.mk src✝.toPrefunctor).map
        (MonoidalCategory.tensorHom { down := { down := (_ : { as := X }.as = { as := X }.as) } }
          { down := { down := (_ : { as := X' }.as = { as := X' }.as) } })
[PROOFSTEP]
ext
[GOAL]
case mk.mk.mk.mk.up.up.refl.up.up.refl.w.h
C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
h : ShiftMkCore C A
src✝ : Discrete A ⥤ C ⥤ C := Discrete.functor h.F
X X' : A
x✝ : C
⊢ NatTrans.app
      (MonoidalCategory.tensorHom
          ((Functor.mk src✝.toPrefunctor).map { down := { down := (_ : { as := X }.as = { as := X }.as) } })
          ((Functor.mk src✝.toPrefunctor).map { down := { down := (_ : { as := X' }.as = { as := X' }.as) } }) ≫
        (fun m n => (ShiftMkCore.add h m.as n.as).inv) { as := X } { as := X' })
      x✝ =
    NatTrans.app
      ((fun m n => (ShiftMkCore.add h m.as n.as).inv) { as := X } { as := X' } ≫
        (Functor.mk src✝.toPrefunctor).map
          (MonoidalCategory.tensorHom { down := { down := (_ : { as := X }.as = { as := X }.as) } }
            { down := { down := (_ : { as := X' }.as = { as := X' }.as) } }))
      x✝
[PROOFSTEP]
dsimp
[GOAL]
case mk.mk.mk.mk.up.up.refl.up.up.refl.w.h
C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
h : ShiftMkCore C A
src✝ : Discrete A ⥤ C ⥤ C := Discrete.functor h.F
X X' : A
x✝ : C
⊢ (NatTrans.app ((Discrete.functor h.F).map { down := { down := (_ : X' = X') } }) ((ShiftMkCore.F h X).obj x✝) ≫
        (ShiftMkCore.F h X').map (NatTrans.app ((Discrete.functor h.F).map { down := { down := (_ : X = X) } }) x✝)) ≫
      NatTrans.app (ShiftMkCore.add h X X').inv x✝ =
    NatTrans.app (ShiftMkCore.add h X X').inv x✝ ≫
      NatTrans.app
        ((Discrete.functor h.F).map
          (MonoidalCategory.tensorHom { down := { down := (_ : X = X) } } { down := { down := (_ : X' = X') } }))
        x✝
[PROOFSTEP]
simp
[GOAL]
C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
h : ShiftMkCore C A
src✝ : Discrete A ⥤ C ⥤ C := Discrete.functor h.F
⊢ ∀ (X Y Z : Discrete A),
    MonoidalCategory.tensorHom ((fun m n => (ShiftMkCore.add h m.as n.as).inv) X Y)
          (𝟙 ((Functor.mk src✝.toPrefunctor).obj Z)) ≫
        (fun m n => (ShiftMkCore.add h m.as n.as).inv) (MonoidalCategory.tensorObj X Y) Z ≫
          (Functor.mk src✝.toPrefunctor).map (MonoidalCategory.associator X Y Z).hom =
      (MonoidalCategory.associator ((Functor.mk src✝.toPrefunctor).obj X) ((Functor.mk src✝.toPrefunctor).obj Y)
            ((Functor.mk src✝.toPrefunctor).obj Z)).hom ≫
        MonoidalCategory.tensorHom (𝟙 ((Functor.mk src✝.toPrefunctor).obj X))
            ((fun m n => (ShiftMkCore.add h m.as n.as).inv) Y Z) ≫
          (fun m n => (ShiftMkCore.add h m.as n.as).inv) X (MonoidalCategory.tensorObj Y Z)
[PROOFSTEP]
rintro ⟨m₁⟩ ⟨m₂⟩ ⟨m₃⟩
[GOAL]
case mk.mk.mk
C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
h : ShiftMkCore C A
src✝ : Discrete A ⥤ C ⥤ C := Discrete.functor h.F
m₁ m₂ m₃ : A
⊢ MonoidalCategory.tensorHom ((fun m n => (ShiftMkCore.add h m.as n.as).inv) { as := m₁ } { as := m₂ })
        (𝟙 ((Functor.mk src✝.toPrefunctor).obj { as := m₃ })) ≫
      (fun m n => (ShiftMkCore.add h m.as n.as).inv) (MonoidalCategory.tensorObj { as := m₁ } { as := m₂ })
          { as := m₃ } ≫
        (Functor.mk src✝.toPrefunctor).map (MonoidalCategory.associator { as := m₁ } { as := m₂ } { as := m₃ }).hom =
    (MonoidalCategory.associator ((Functor.mk src✝.toPrefunctor).obj { as := m₁ })
          ((Functor.mk src✝.toPrefunctor).obj { as := m₂ }) ((Functor.mk src✝.toPrefunctor).obj { as := m₃ })).hom ≫
      MonoidalCategory.tensorHom (𝟙 ((Functor.mk src✝.toPrefunctor).obj { as := m₁ }))
          ((fun m n => (ShiftMkCore.add h m.as n.as).inv) { as := m₂ } { as := m₃ }) ≫
        (fun m n => (ShiftMkCore.add h m.as n.as).inv) { as := m₁ }
          (MonoidalCategory.tensorObj { as := m₂ } { as := m₃ })
[PROOFSTEP]
ext X
[GOAL]
case mk.mk.mk.w.h
C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
h : ShiftMkCore C A
src✝ : Discrete A ⥤ C ⥤ C := Discrete.functor h.F
m₁ m₂ m₃ : A
X : C
⊢ NatTrans.app
      (MonoidalCategory.tensorHom ((fun m n => (ShiftMkCore.add h m.as n.as).inv) { as := m₁ } { as := m₂ })
          (𝟙 ((Functor.mk src✝.toPrefunctor).obj { as := m₃ })) ≫
        (fun m n => (ShiftMkCore.add h m.as n.as).inv) (MonoidalCategory.tensorObj { as := m₁ } { as := m₂ })
            { as := m₃ } ≫
          (Functor.mk src✝.toPrefunctor).map (MonoidalCategory.associator { as := m₁ } { as := m₂ } { as := m₃ }).hom)
      X =
    NatTrans.app
      ((MonoidalCategory.associator ((Functor.mk src✝.toPrefunctor).obj { as := m₁ })
            ((Functor.mk src✝.toPrefunctor).obj { as := m₂ }) ((Functor.mk src✝.toPrefunctor).obj { as := m₃ })).hom ≫
        MonoidalCategory.tensorHom (𝟙 ((Functor.mk src✝.toPrefunctor).obj { as := m₁ }))
            ((fun m n => (ShiftMkCore.add h m.as n.as).inv) { as := m₂ } { as := m₃ }) ≫
          (fun m n => (ShiftMkCore.add h m.as n.as).inv) { as := m₁ }
            (MonoidalCategory.tensorObj { as := m₂ } { as := m₃ }))
      X
[PROOFSTEP]
simp [endofunctorMonoidalCategory, h.assoc_inv_app_assoc]
[GOAL]
C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
h : ShiftMkCore C A
src✝ : Discrete A ⥤ C ⥤ C := Discrete.functor h.F
⊢ ∀ (X : Discrete A),
    (MonoidalCategory.leftUnitor ((Functor.mk src✝.toPrefunctor).obj X)).hom =
      MonoidalCategory.tensorHom h.zero.inv (𝟙 ((Functor.mk src✝.toPrefunctor).obj X)) ≫
        (fun m n => (ShiftMkCore.add h m.as n.as).inv) (MonoidalCategory.tensorUnit (Discrete A)) X ≫
          (Functor.mk src✝.toPrefunctor).map (MonoidalCategory.leftUnitor X).hom
[PROOFSTEP]
rintro ⟨n⟩
[GOAL]
case mk
C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
h : ShiftMkCore C A
src✝ : Discrete A ⥤ C ⥤ C := Discrete.functor h.F
n : A
⊢ (MonoidalCategory.leftUnitor ((Functor.mk src✝.toPrefunctor).obj { as := n })).hom =
    MonoidalCategory.tensorHom h.zero.inv (𝟙 ((Functor.mk src✝.toPrefunctor).obj { as := n })) ≫
      (fun m n => (ShiftMkCore.add h m.as n.as).inv) (MonoidalCategory.tensorUnit (Discrete A)) { as := n } ≫
        (Functor.mk src✝.toPrefunctor).map (MonoidalCategory.leftUnitor { as := n }).hom
[PROOFSTEP]
ext X
[GOAL]
case mk.w.h
C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
h : ShiftMkCore C A
src✝ : Discrete A ⥤ C ⥤ C := Discrete.functor h.F
n : A
X : C
⊢ NatTrans.app (MonoidalCategory.leftUnitor ((Functor.mk src✝.toPrefunctor).obj { as := n })).hom X =
    NatTrans.app
      (MonoidalCategory.tensorHom h.zero.inv (𝟙 ((Functor.mk src✝.toPrefunctor).obj { as := n })) ≫
        (fun m n => (ShiftMkCore.add h m.as n.as).inv) (MonoidalCategory.tensorUnit (Discrete A)) { as := n } ≫
          (Functor.mk src✝.toPrefunctor).map (MonoidalCategory.leftUnitor { as := n }).hom)
      X
[PROOFSTEP]
simp [endofunctorMonoidalCategory, h.zero_add_inv_app, ← Functor.map_comp]
[GOAL]
C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
h : ShiftMkCore C A
src✝ : Discrete A ⥤ C ⥤ C := Discrete.functor h.F
⊢ ∀ (X : Discrete A),
    (MonoidalCategory.rightUnitor ((Functor.mk src✝.toPrefunctor).obj X)).hom =
      MonoidalCategory.tensorHom (𝟙 ((Functor.mk src✝.toPrefunctor).obj X)) h.zero.inv ≫
        (fun m n => (ShiftMkCore.add h m.as n.as).inv) X (MonoidalCategory.tensorUnit (Discrete A)) ≫
          (Functor.mk src✝.toPrefunctor).map (MonoidalCategory.rightUnitor X).hom
[PROOFSTEP]
rintro ⟨n⟩
[GOAL]
case mk
C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
h : ShiftMkCore C A
src✝ : Discrete A ⥤ C ⥤ C := Discrete.functor h.F
n : A
⊢ (MonoidalCategory.rightUnitor ((Functor.mk src✝.toPrefunctor).obj { as := n })).hom =
    MonoidalCategory.tensorHom (𝟙 ((Functor.mk src✝.toPrefunctor).obj { as := n })) h.zero.inv ≫
      (fun m n => (ShiftMkCore.add h m.as n.as).inv) { as := n } (MonoidalCategory.tensorUnit (Discrete A)) ≫
        (Functor.mk src✝.toPrefunctor).map (MonoidalCategory.rightUnitor { as := n }).hom
[PROOFSTEP]
ext X
[GOAL]
case mk.w.h
C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
h : ShiftMkCore C A
src✝ : Discrete A ⥤ C ⥤ C := Discrete.functor h.F
n : A
X : C
⊢ NatTrans.app (MonoidalCategory.rightUnitor ((Functor.mk src✝.toPrefunctor).obj { as := n })).hom X =
    NatTrans.app
      (MonoidalCategory.tensorHom (𝟙 ((Functor.mk src✝.toPrefunctor).obj { as := n })) h.zero.inv ≫
        (fun m n => (ShiftMkCore.add h m.as n.as).inv) { as := n } (MonoidalCategory.tensorUnit (Discrete A)) ≫
          (Functor.mk src✝.toPrefunctor).map (MonoidalCategory.rightUnitor { as := n }).hom)
      X
[PROOFSTEP]
simp [endofunctorMonoidalCategory, h.add_zero_inv_app]
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
i j k : A
h : i + j = k
⊢ shiftFunctor C k = shiftFunctor C (i + j)
[PROOFSTEP]
rw [h]
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
i j : A
⊢ shiftFunctorAdd' C i j (i + j) (_ : i + j = i + j) = shiftFunctorAdd C i j
[PROOFSTEP]
ext1
[GOAL]
case w
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
i j : A
⊢ (shiftFunctorAdd' C i j (i + j) (_ : i + j = i + j)).hom = (shiftFunctorAdd C i j).hom
[PROOFSTEP]
apply Category.id_comp
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
h : ShiftMkCore C A
a : A
⊢ shiftFunctor C a = F h a
[PROOFSTEP]
rfl
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
h : ShiftMkCore C A
⊢ shiftFunctorZero C A = h.zero
[PROOFSTEP]
letI := hasShiftMk C A h
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
h : ShiftMkCore C A
this : HasShift C A := hasShiftMk C A h
⊢ shiftFunctorZero C A = h.zero
[PROOFSTEP]
dsimp [shiftFunctorZero]
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
h : ShiftMkCore C A
this : HasShift C A := hasShiftMk C A h
⊢ (MonoidalFunctor.εIso (shiftMonoidalFunctor C A)).symm = h.zero
[PROOFSTEP]
change (shiftFunctorZero C A).symm.symm = h.zero.symm.symm
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
h : ShiftMkCore C A
this : HasShift C A := hasShiftMk C A h
⊢ (shiftFunctorZero C A).symm.symm = h.zero.symm.symm
[PROOFSTEP]
congr 1
[GOAL]
case e_I
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
h : ShiftMkCore C A
this : HasShift C A := hasShiftMk C A h
⊢ (shiftFunctorZero C A).symm = h.zero.symm
[PROOFSTEP]
ext
[GOAL]
case e_I.w.w.h
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
h : ShiftMkCore C A
this : HasShift C A := hasShiftMk C A h
x✝ : C
⊢ NatTrans.app (shiftFunctorZero C A).symm.hom x✝ = NatTrans.app h.zero.symm.hom x✝
[PROOFSTEP]
rfl
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
h : ShiftMkCore C A
a b : A
⊢ shiftFunctorAdd C a b = add h a b
[PROOFSTEP]
letI := hasShiftMk C A h
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
h : ShiftMkCore C A
a b : A
this : HasShift C A := hasShiftMk C A h
⊢ shiftFunctorAdd C a b = add h a b
[PROOFSTEP]
change (shiftFunctorAdd C a b).symm.symm = (h.add a b).symm.symm
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
h : ShiftMkCore C A
a b : A
this : HasShift C A := hasShiftMk C A h
⊢ (shiftFunctorAdd C a b).symm.symm = (add h a b).symm.symm
[PROOFSTEP]
congr 1
[GOAL]
case e_I
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
h : ShiftMkCore C A
a b : A
this : HasShift C A := hasShiftMk C A h
⊢ (shiftFunctorAdd C a b).symm = (add h a b).symm
[PROOFSTEP]
ext
[GOAL]
case e_I.w.w.h
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
h : ShiftMkCore C A
a b : A
this : HasShift C A := hasShiftMk C A h
x✝ : C
⊢ NatTrans.app (shiftFunctorAdd C a b).symm.hom x✝ = NatTrans.app (add h a b).symm.hom x✝
[PROOFSTEP]
rfl
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a : A
⊢ shiftFunctorAdd' C 0 a a (_ : 0 + a = a) =
    (Functor.leftUnitor (shiftFunctor C a)).symm ≪≫ isoWhiskerRight (shiftFunctorZero C A).symm (shiftFunctor C a)
[PROOFSTEP]
ext X
[GOAL]
case w.w.h
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a : A
X : C
⊢ NatTrans.app (shiftFunctorAdd' C 0 a a (_ : 0 + a = a)).hom X =
    NatTrans.app
      ((Functor.leftUnitor (shiftFunctor C a)).symm ≪≫
          isoWhiskerRight (shiftFunctorZero C A).symm (shiftFunctor C a)).hom
      X
[PROOFSTEP]
dsimp [shiftFunctorAdd', shiftFunctorZero, shiftFunctor]
[GOAL]
case w.w.h
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a : A
X : C
⊢ NatTrans.app (eqToHom (_ : shiftFunctor C a = shiftFunctor C (0 + a))) X ≫
      NatTrans.app (shiftFunctorAdd C 0 a).hom X =
    𝟙 (((shiftMonoidalFunctor C A).toLaxMonoidalFunctor.toFunctor.obj { as := a }).obj X) ≫
      ((shiftMonoidalFunctor C A).toLaxMonoidalFunctor.toFunctor.obj { as := a }).map
        (NatTrans.app (shiftMonoidalFunctor C A).toLaxMonoidalFunctor.ε X)
[PROOFSTEP]
simp only [eqToHom_app, obj_ε_app, Discrete.addMonoidal_leftUnitor, eqToIso.inv, eqToHom_map, Category.id_comp]
[GOAL]
case w.w.h
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a : A
X : C
⊢ eqToHom
        (_ :
          ((shiftMonoidalFunctor C A).toLaxMonoidalFunctor.toFunctor.obj { as := a }).obj X =
            ((shiftMonoidalFunctor C A).toLaxMonoidalFunctor.toFunctor.obj { as := 0 + a }).obj X) ≫
      NatTrans.app (shiftFunctorAdd C 0 a).hom X =
    eqToHom
        (_ :
          ((shiftMonoidalFunctor C A).toLaxMonoidalFunctor.toFunctor.obj { as := a }).obj X =
            ((shiftMonoidalFunctor C A).toLaxMonoidalFunctor.toFunctor.obj
                  (MonoidalCategory.tensorObj MonoidalCategory.tensorUnit' { as := a })).obj
              X) ≫
      NatTrans.app
        (MonoidalFunctor.μIso (shiftMonoidalFunctor C A) (MonoidalCategory.tensorUnit (Discrete A)) { as := a }).inv X
[PROOFSTEP]
rfl
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a : A
⊢ shiftFunctorAdd' C a 0 a (_ : a + 0 = a) =
    (Functor.rightUnitor (shiftFunctor C a)).symm ≪≫ isoWhiskerLeft (shiftFunctor C a) (shiftFunctorZero C A).symm
[PROOFSTEP]
ext
[GOAL]
case w.w.h
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a : A
x✝ : C
⊢ NatTrans.app (shiftFunctorAdd' C a 0 a (_ : a + 0 = a)).hom x✝ =
    NatTrans.app
      ((Functor.rightUnitor (shiftFunctor C a)).symm ≪≫
          isoWhiskerLeft (shiftFunctor C a) (shiftFunctorZero C A).symm).hom
      x✝
[PROOFSTEP]
dsimp [shiftFunctorAdd', shiftFunctorZero, shiftFunctor]
[GOAL]
case w.w.h
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a : A
x✝ : C
⊢ NatTrans.app (eqToHom (_ : shiftFunctor C a = shiftFunctor C (a + 0))) x✝ ≫
      NatTrans.app (shiftFunctorAdd C a 0).hom x✝ =
    𝟙 (((shiftMonoidalFunctor C A).toLaxMonoidalFunctor.toFunctor.obj { as := a }).obj x✝) ≫
      NatTrans.app (shiftMonoidalFunctor C A).toLaxMonoidalFunctor.ε
        (((shiftMonoidalFunctor C A).toLaxMonoidalFunctor.toFunctor.obj { as := a }).obj x✝)
[PROOFSTEP]
simp only [eqToHom_app, ε_app_obj, Discrete.addMonoidal_rightUnitor, eqToIso.inv, eqToHom_map, Category.id_comp]
[GOAL]
case w.w.h
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a : A
x✝ : C
⊢ eqToHom
        (_ :
          ((shiftMonoidalFunctor C A).toLaxMonoidalFunctor.toFunctor.obj { as := a }).obj x✝ =
            ((shiftMonoidalFunctor C A).toLaxMonoidalFunctor.toFunctor.obj { as := a + 0 }).obj x✝) ≫
      NatTrans.app (shiftFunctorAdd C a 0).hom x✝ =
    eqToHom
        (_ :
          ((shiftMonoidalFunctor C A).toLaxMonoidalFunctor.toFunctor.obj { as := a }).obj x✝ =
            ((shiftMonoidalFunctor C A).toLaxMonoidalFunctor.toFunctor.obj
                  (MonoidalCategory.tensorObj { as := a } MonoidalCategory.tensorUnit')).obj
              x✝) ≫
      NatTrans.app
        (MonoidalFunctor.μIso (shiftMonoidalFunctor C A) { as := a } (MonoidalCategory.tensorUnit (Discrete A))).inv x✝
[PROOFSTEP]
rfl
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a₁ a₂ a₃ a₁₂ a₂₃ a₁₂₃ : A
h₁₂ : a₁ + a₂ = a₁₂
h₂₃ : a₂ + a₃ = a₂₃
h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃
⊢ a₁₂ + a₃ = a₁₂₃
[PROOFSTEP]
rw [← h₁₂, h₁₂₃]
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a₁ a₂ a₃ a₁₂ a₂₃ a₁₂₃ : A
h₁₂ : a₁ + a₂ = a₁₂
h₂₃ : a₂ + a₃ = a₂₃
h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃
⊢ a₁ + a₂₃ = a₁₂₃
[PROOFSTEP]
rw [← h₂₃, ← add_assoc, h₁₂₃]
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a₁ a₂ a₃ a₁₂ a₂₃ a₁₂₃ : A
h₁₂ : a₁ + a₂ = a₁₂
h₂₃ : a₂ + a₃ = a₂₃
h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃
⊢ shiftFunctorAdd' C a₁₂ a₃ a₁₂₃ (_ : a₁₂ + a₃ = a₁₂₃) ≪≫
      isoWhiskerRight (shiftFunctorAdd' C a₁ a₂ a₁₂ h₁₂) (shiftFunctor C a₃) ≪≫
        Functor.associator (shiftFunctor C a₁) (shiftFunctor C a₂) (shiftFunctor C a₃) =
    shiftFunctorAdd' C a₁ a₂₃ a₁₂₃ (_ : a₁ + a₂₃ = a₁₂₃) ≪≫
      isoWhiskerLeft (shiftFunctor C a₁) (shiftFunctorAdd' C a₂ a₃ a₂₃ h₂₃)
[PROOFSTEP]
subst h₁₂ h₂₃ h₁₂₃
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a₁ a₂ a₃ : A
⊢ shiftFunctorAdd' C (a₁ + a₂) a₃ (a₁ + a₂ + a₃) (_ : a₁ + a₂ + a₃ = a₁ + a₂ + a₃) ≪≫
      isoWhiskerRight (shiftFunctorAdd' C a₁ a₂ (a₁ + a₂) (_ : a₁ + a₂ = a₁ + a₂)) (shiftFunctor C a₃) ≪≫
        Functor.associator (shiftFunctor C a₁) (shiftFunctor C a₂) (shiftFunctor C a₃) =
    shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) (_ : a₁ + (a₂ + a₃) = a₁ + a₂ + a₃) ≪≫
      isoWhiskerLeft (shiftFunctor C a₁) (shiftFunctorAdd' C a₂ a₃ (a₂ + a₃) (_ : a₂ + a₃ = a₂ + a₃))
[PROOFSTEP]
ext X
[GOAL]
case w.w.h
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a₁ a₂ a₃ : A
X : C
⊢ NatTrans.app
      (shiftFunctorAdd' C (a₁ + a₂) a₃ (a₁ + a₂ + a₃) (_ : a₁ + a₂ + a₃ = a₁ + a₂ + a₃) ≪≫
          isoWhiskerRight (shiftFunctorAdd' C a₁ a₂ (a₁ + a₂) (_ : a₁ + a₂ = a₁ + a₂)) (shiftFunctor C a₃) ≪≫
            Functor.associator (shiftFunctor C a₁) (shiftFunctor C a₂) (shiftFunctor C a₃)).hom
      X =
    NatTrans.app
      (shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) (_ : a₁ + (a₂ + a₃) = a₁ + a₂ + a₃) ≪≫
          isoWhiskerLeft (shiftFunctor C a₁) (shiftFunctorAdd' C a₂ a₃ (a₂ + a₃) (_ : a₂ + a₃ = a₂ + a₃))).hom
      X
[PROOFSTEP]
dsimp
[GOAL]
case w.w.h
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a₁ a₂ a₃ : A
X : C
⊢ NatTrans.app (shiftFunctorAdd' C (a₁ + a₂) a₃ (a₁ + a₂ + a₃) (_ : a₁ + a₂ + a₃ = a₁ + a₂ + a₃)).hom X ≫
      (shiftFunctor C a₃).map (NatTrans.app (shiftFunctorAdd' C a₁ a₂ (a₁ + a₂) (_ : a₁ + a₂ = a₁ + a₂)).hom X) ≫
        𝟙 ((shiftFunctor C a₃).obj ((shiftFunctor C a₂).obj ((shiftFunctor C a₁).obj X))) =
    NatTrans.app (shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) (_ : a₁ + (a₂ + a₃) = a₁ + a₂ + a₃)).hom X ≫
      NatTrans.app (shiftFunctorAdd' C a₂ a₃ (a₂ + a₃) (_ : a₂ + a₃ = a₂ + a₃)).hom ((shiftFunctor C a₁).obj X)
[PROOFSTEP]
simp only [shiftFunctorAdd'_eq_shiftFunctorAdd, Category.comp_id]
[GOAL]
case w.w.h
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a₁ a₂ a₃ : A
X : C
⊢ NatTrans.app (shiftFunctorAdd C (a₁ + a₂) a₃).hom X ≫
      (shiftFunctor C a₃).map (NatTrans.app (shiftFunctorAdd C a₁ a₂).hom X) =
    NatTrans.app (shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) (_ : a₁ + (a₂ + a₃) = a₁ + a₂ + a₃)).hom X ≫
      NatTrans.app (shiftFunctorAdd C a₂ a₃).hom ((shiftFunctor C a₁).obj X)
[PROOFSTEP]
dsimp [shiftFunctorAdd']
[GOAL]
case w.w.h
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a₁ a₂ a₃ : A
X : C
⊢ NatTrans.app (shiftFunctorAdd C (a₁ + a₂) a₃).hom X ≫
      (shiftFunctor C a₃).map (NatTrans.app (shiftFunctorAdd C a₁ a₂).hom X) =
    (NatTrans.app (eqToHom (_ : shiftFunctor C (a₁ + a₂ + a₃) = shiftFunctor C (a₁ + (a₂ + a₃)))) X ≫
        NatTrans.app (shiftFunctorAdd C a₁ (a₂ + a₃)).hom X) ≫
      NatTrans.app (shiftFunctorAdd C a₂ a₃).hom ((shiftFunctor C a₁).obj X)
[PROOFSTEP]
simp only [eqToHom_app]
[GOAL]
case w.w.h
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a₁ a₂ a₃ : A
X : C
⊢ NatTrans.app (shiftFunctorAdd C (a₁ + a₂) a₃).hom X ≫
      (shiftFunctor C a₃).map (NatTrans.app (shiftFunctorAdd C a₁ a₂).hom X) =
    (eqToHom (_ : (shiftFunctor C (a₁ + a₂ + a₃)).obj X = (shiftFunctor C (a₁ + (a₂ + a₃))).obj X) ≫
        NatTrans.app (shiftFunctorAdd C a₁ (a₂ + a₃)).hom X) ≫
      NatTrans.app (shiftFunctorAdd C a₂ a₃).hom ((shiftFunctor C a₁).obj X)
[PROOFSTEP]
dsimp [shiftFunctorAdd, shiftFunctor]
[GOAL]
case w.w.h
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a₁ a₂ a₃ : A
X : C
⊢ NatTrans.app (MonoidalFunctor.μIso (shiftMonoidalFunctor C A) { as := a₁ + a₂ } { as := a₃ }).inv X ≫
      ((shiftMonoidalFunctor C A).toLaxMonoidalFunctor.toFunctor.obj { as := a₃ }).map
        (NatTrans.app (MonoidalFunctor.μIso (shiftMonoidalFunctor C A) { as := a₁ } { as := a₂ }).inv X) =
    (eqToHom
          (_ :
            ((shiftMonoidalFunctor C A).toLaxMonoidalFunctor.toFunctor.obj { as := a₁ + a₂ + a₃ }).obj X =
              ((shiftMonoidalFunctor C A).toLaxMonoidalFunctor.toFunctor.obj { as := a₁ + (a₂ + a₃) }).obj X) ≫
        NatTrans.app (MonoidalFunctor.μIso (shiftMonoidalFunctor C A) { as := a₁ } { as := a₂ + a₃ }).inv X) ≫
      NatTrans.app (MonoidalFunctor.μIso (shiftMonoidalFunctor C A) { as := a₂ } { as := a₃ }).inv
        (((shiftMonoidalFunctor C A).toLaxMonoidalFunctor.toFunctor.obj { as := a₁ }).obj X)
[PROOFSTEP]
simp only [obj_μ_inv_app, Discrete.addMonoidal_associator, eqToIso.hom, eqToHom_map, eqToHom_app]
[GOAL]
case w.w.h
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a₁ a₂ a₃ : A
X : C
⊢ NatTrans.app (MonoidalFunctor.μIso (shiftMonoidalFunctor C A) { as := a₁ + a₂ } { as := a₃ }).inv X ≫
      NatTrans.app
          (LaxMonoidalFunctor.μ (shiftMonoidalFunctor C A).toLaxMonoidalFunctor
            (MonoidalCategory.tensorObj { as := a₁ } { as := a₂ }) { as := a₃ })
          X ≫
        eqToHom
            (_ :
              ((shiftMonoidalFunctor C A).toLaxMonoidalFunctor.toFunctor.obj
                      (MonoidalCategory.tensorObj (MonoidalCategory.tensorObj { as := a₁ } { as := a₂ })
                        { as := a₃ })).obj
                  X =
                ((shiftMonoidalFunctor C A).toLaxMonoidalFunctor.toFunctor.obj
                      (MonoidalCategory.tensorObj { as := a₁ }
                        (MonoidalCategory.tensorObj { as := a₂ } { as := a₃ }))).obj
                  X) ≫
          NatTrans.app
              (MonoidalFunctor.μIso (shiftMonoidalFunctor C A) { as := a₁ }
                  (MonoidalCategory.tensorObj { as := a₂ } { as := a₃ })).inv
              X ≫
            NatTrans.app (MonoidalFunctor.μIso (shiftMonoidalFunctor C A) { as := a₂ } { as := a₃ }).inv
              (((shiftMonoidalFunctor C A).toLaxMonoidalFunctor.toFunctor.obj { as := a₁ }).obj X) =
    (eqToHom
          (_ :
            ((shiftMonoidalFunctor C A).toLaxMonoidalFunctor.toFunctor.obj { as := a₁ + a₂ + a₃ }).obj X =
              ((shiftMonoidalFunctor C A).toLaxMonoidalFunctor.toFunctor.obj { as := a₁ + (a₂ + a₃) }).obj X) ≫
        NatTrans.app (MonoidalFunctor.μIso (shiftMonoidalFunctor C A) { as := a₁ } { as := a₂ + a₃ }).inv X) ≫
      NatTrans.app (MonoidalFunctor.μIso (shiftMonoidalFunctor C A) { as := a₂ } { as := a₃ }).inv
        (((shiftMonoidalFunctor C A).toLaxMonoidalFunctor.toFunctor.obj { as := a₁ }).obj X)
[PROOFSTEP]
erw [Iso.inv_hom_id_app_assoc, Category.assoc]
[GOAL]
case w.w.h
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a₁ a₂ a₃ : A
X : C
⊢ eqToHom
        (_ :
          ((shiftMonoidalFunctor C A).toLaxMonoidalFunctor.toFunctor.obj
                  (MonoidalCategory.tensorObj (MonoidalCategory.tensorObj { as := a₁ } { as := a₂ }) { as := a₃ })).obj
              X =
            ((shiftMonoidalFunctor C A).toLaxMonoidalFunctor.toFunctor.obj
                  (MonoidalCategory.tensorObj { as := a₁ } (MonoidalCategory.tensorObj { as := a₂ } { as := a₃ }))).obj
              X) ≫
      NatTrans.app
          (MonoidalFunctor.μIso (shiftMonoidalFunctor C A) { as := a₁ }
              (MonoidalCategory.tensorObj { as := a₂ } { as := a₃ })).inv
          X ≫
        NatTrans.app (MonoidalFunctor.μIso (shiftMonoidalFunctor C A) { as := a₂ } { as := a₃ }).inv
          (((shiftMonoidalFunctor C A).toLaxMonoidalFunctor.toFunctor.obj { as := a₁ }).obj X) =
    eqToHom
        (_ :
          ((shiftMonoidalFunctor C A).toLaxMonoidalFunctor.toFunctor.obj { as := a₁ + a₂ + a₃ }).obj X =
            ((shiftMonoidalFunctor C A).toLaxMonoidalFunctor.toFunctor.obj { as := a₁ + (a₂ + a₃) }).obj X) ≫
      NatTrans.app (MonoidalFunctor.μIso (shiftMonoidalFunctor C A) { as := a₁ } { as := a₂ + a₃ }).inv X ≫
        NatTrans.app (MonoidalFunctor.μIso (shiftMonoidalFunctor C A) { as := a₂ } { as := a₃ }).inv
          (((shiftMonoidalFunctor C A).toLaxMonoidalFunctor.toFunctor.obj { as := a₁ }).obj X)
[PROOFSTEP]
rfl
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a₁ a₂ a₃ : A
⊢ shiftFunctorAdd C (a₁ + a₂) a₃ ≪≫
      isoWhiskerRight (shiftFunctorAdd C a₁ a₂) (shiftFunctor C a₃) ≪≫
        Functor.associator (shiftFunctor C a₁) (shiftFunctor C a₂) (shiftFunctor C a₃) =
    shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) (_ : a₁ + (a₂ + a₃) = a₁ + a₂ + a₃) ≪≫
      isoWhiskerLeft (shiftFunctor C a₁) (shiftFunctorAdd C a₂ a₃)
[PROOFSTEP]
ext X
[GOAL]
case w.w.h
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a₁ a₂ a₃ : A
X : C
⊢ NatTrans.app
      (shiftFunctorAdd C (a₁ + a₂) a₃ ≪≫
          isoWhiskerRight (shiftFunctorAdd C a₁ a₂) (shiftFunctor C a₃) ≪≫
            Functor.associator (shiftFunctor C a₁) (shiftFunctor C a₂) (shiftFunctor C a₃)).hom
      X =
    NatTrans.app
      (shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) (_ : a₁ + (a₂ + a₃) = a₁ + a₂ + a₃) ≪≫
          isoWhiskerLeft (shiftFunctor C a₁) (shiftFunctorAdd C a₂ a₃)).hom
      X
[PROOFSTEP]
simpa [shiftFunctorAdd'_eq_shiftFunctorAdd] using
  NatTrans.congr_app (congr_arg Iso.hom (shiftFunctorAdd'_assoc C a₁ a₂ a₃ _ _ _ rfl rfl rfl)) X
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a : A
X : C
⊢ NatTrans.app (shiftFunctorAdd' C 0 a a (_ : 0 + a = a)).hom X =
    (shiftFunctor C a).map (NatTrans.app (shiftFunctorZero C A).inv X)
[PROOFSTEP]
simpa using NatTrans.congr_app (congr_arg Iso.hom (shiftFunctorAdd'_zero_add C a)) X
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a : A
X : C
⊢ (shiftFunctor C (0 + a)).obj X = (shiftFunctor C a).obj ((𝟭 C).obj X)
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a : A
X : C
⊢ (shiftFunctor C (0 + a)).obj X = (shiftFunctor C a).obj X
[PROOFSTEP]
rw [zero_add]
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a : A
X : C
⊢ NatTrans.app (shiftFunctorAdd C 0 a).hom X =
    eqToHom (_ : (shiftFunctor C (0 + a)).obj X = (shiftFunctor C a).obj ((𝟭 C).obj X)) ≫
      (shiftFunctor C a).map (NatTrans.app (shiftFunctorZero C A).inv X)
[PROOFSTEP]
simp [← shiftFunctorAdd'_zero_add_hom_app, shiftFunctorAdd']
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a : A
X : C
⊢ NatTrans.app (shiftFunctorAdd' C 0 a a (_ : 0 + a = a)).inv X =
    (shiftFunctor C a).map (NatTrans.app (shiftFunctorZero C A).hom X)
[PROOFSTEP]
simpa using NatTrans.congr_app (congr_arg Iso.inv (shiftFunctorAdd'_zero_add C a)) X
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a : A
X : C
⊢ (shiftFunctor C a).obj ((𝟭 C).obj X) = (shiftFunctor C (0 + a)).obj X
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a : A
X : C
⊢ (shiftFunctor C a).obj X = (shiftFunctor C (0 + a)).obj X
[PROOFSTEP]
rw [zero_add]
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a : A
X : C
⊢ NatTrans.app (shiftFunctorAdd C 0 a).inv X =
    (shiftFunctor C a).map (NatTrans.app (shiftFunctorZero C A).hom X) ≫
      eqToHom (_ : (shiftFunctor C a).obj ((𝟭 C).obj X) = (shiftFunctor C (0 + a)).obj X)
[PROOFSTEP]
simp [← shiftFunctorAdd'_zero_add_inv_app, shiftFunctorAdd']
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a : A
X : C
⊢ NatTrans.app (shiftFunctorAdd' C a 0 a (_ : a + 0 = a)).hom X =
    NatTrans.app (shiftFunctorZero C A).inv ((shiftFunctor C a).obj X)
[PROOFSTEP]
simpa using NatTrans.congr_app (congr_arg Iso.hom (shiftFunctorAdd'_add_zero C a)) X
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a : A
X : C
⊢ (shiftFunctor C (a + 0)).obj X = (𝟭 C).obj ((shiftFunctor C a).obj X)
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a : A
X : C
⊢ (shiftFunctor C (a + 0)).obj X = (shiftFunctor C a).obj X
[PROOFSTEP]
rw [add_zero]
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a : A
X : C
⊢ NatTrans.app (shiftFunctorAdd C a 0).hom X =
    eqToHom (_ : (shiftFunctor C (a + 0)).obj X = (𝟭 C).obj ((shiftFunctor C a).obj X)) ≫
      NatTrans.app (shiftFunctorZero C A).inv ((shiftFunctor C a).obj X)
[PROOFSTEP]
simp [← shiftFunctorAdd'_add_zero_hom_app, shiftFunctorAdd']
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a : A
X : C
⊢ NatTrans.app (shiftFunctorAdd' C a 0 a (_ : a + 0 = a)).inv X =
    NatTrans.app (shiftFunctorZero C A).hom ((shiftFunctor C a).obj X)
[PROOFSTEP]
simpa using NatTrans.congr_app (congr_arg Iso.inv (shiftFunctorAdd'_add_zero C a)) X
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a : A
X : C
⊢ (𝟭 C).obj ((shiftFunctor C a).obj X) = (shiftFunctor C (a + 0)).obj X
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a : A
X : C
⊢ (shiftFunctor C a).obj X = (shiftFunctor C (a + 0)).obj X
[PROOFSTEP]
rw [add_zero]
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a : A
X : C
⊢ NatTrans.app (shiftFunctorAdd C a 0).inv X =
    NatTrans.app (shiftFunctorZero C A).hom ((shiftFunctor C a).obj X) ≫
      eqToHom (_ : (𝟭 C).obj ((shiftFunctor C a).obj X) = (shiftFunctor C (a + 0)).obj X)
[PROOFSTEP]
simp [← shiftFunctorAdd'_add_zero_inv_app, shiftFunctorAdd']
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a₁ a₂ a₃ a₁₂ a₂₃ a₁₂₃ : A
h₁₂ : a₁ + a₂ = a₁₂
h₂₃ : a₂ + a₃ = a₂₃
h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃
X : C
⊢ a₁₂ + a₃ = a₁₂₃
[PROOFSTEP]
rw [← h₁₂, h₁₂₃]
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a₁ a₂ a₃ a₁₂ a₂₃ a₁₂₃ : A
h₁₂ : a₁ + a₂ = a₁₂
h₂₃ : a₂ + a₃ = a₂₃
h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃
X : C
⊢ a₁ + a₂₃ = a₁₂₃
[PROOFSTEP]
rw [← h₂₃, ← add_assoc, h₁₂₃]
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a₁ a₂ a₃ a₁₂ a₂₃ a₁₂₃ : A
h₁₂ : a₁ + a₂ = a₁₂
h₂₃ : a₂ + a₃ = a₂₃
h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃
X : C
⊢ NatTrans.app (shiftFunctorAdd' C a₁₂ a₃ a₁₂₃ (_ : a₁₂ + a₃ = a₁₂₃)).hom X ≫
      (shiftFunctor C a₃).map (NatTrans.app (shiftFunctorAdd' C a₁ a₂ a₁₂ h₁₂).hom X) =
    NatTrans.app (shiftFunctorAdd' C a₁ a₂₃ a₁₂₃ (_ : a₁ + a₂₃ = a₁₂₃)).hom X ≫
      NatTrans.app (shiftFunctorAdd' C a₂ a₃ a₂₃ h₂₃).hom ((shiftFunctor C a₁).obj X)
[PROOFSTEP]
simpa using NatTrans.congr_app (congr_arg Iso.hom (shiftFunctorAdd'_assoc C _ _ _ _ _ _ h₁₂ h₂₃ h₁₂₃)) X
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a₁ a₂ a₃ a₁₂ a₂₃ a₁₂₃ : A
h₁₂ : a₁ + a₂ = a₁₂
h₂₃ : a₂ + a₃ = a₂₃
h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃
X : C
⊢ a₁₂ + a₃ = a₁₂₃
[PROOFSTEP]
rw [← h₁₂, h₁₂₃]
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a₁ a₂ a₃ a₁₂ a₂₃ a₁₂₃ : A
h₁₂ : a₁ + a₂ = a₁₂
h₂₃ : a₂ + a₃ = a₂₃
h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃
X : C
⊢ a₁ + a₂₃ = a₁₂₃
[PROOFSTEP]
rw [← h₂₃, ← add_assoc, h₁₂₃]
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a₁ a₂ a₃ a₁₂ a₂₃ a₁₂₃ : A
h₁₂ : a₁ + a₂ = a₁₂
h₂₃ : a₂ + a₃ = a₂₃
h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃
X : C
⊢ (shiftFunctor C a₃).map (NatTrans.app (shiftFunctorAdd' C a₁ a₂ a₁₂ h₁₂).inv X) ≫
      NatTrans.app (shiftFunctorAdd' C a₁₂ a₃ a₁₂₃ (_ : a₁₂ + a₃ = a₁₂₃)).inv X =
    NatTrans.app (shiftFunctorAdd' C a₂ a₃ a₂₃ h₂₃).inv ((shiftFunctor C a₁).obj X) ≫
      NatTrans.app (shiftFunctorAdd' C a₁ a₂₃ a₁₂₃ (_ : a₁ + a₂₃ = a₁₂₃)).inv X
[PROOFSTEP]
simpa using NatTrans.congr_app (congr_arg Iso.inv (shiftFunctorAdd'_assoc C _ _ _ _ _ _ h₁₂ h₂₃ h₁₂₃)) X
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a₁ a₂ a₃ : A
X : C
⊢ NatTrans.app (shiftFunctorAdd C (a₁ + a₂) a₃).hom X ≫
      (shiftFunctor C a₃).map (NatTrans.app (shiftFunctorAdd C a₁ a₂).hom X) =
    NatTrans.app (shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) (_ : a₁ + (a₂ + a₃) = a₁ + a₂ + a₃)).hom X ≫
      NatTrans.app (shiftFunctorAdd C a₂ a₃).hom ((shiftFunctor C a₁).obj X)
[PROOFSTEP]
simpa using NatTrans.congr_app (congr_arg Iso.hom (shiftFunctorAdd_assoc C a₁ a₂ a₃)) X
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a₁ a₂ a₃ : A
X : C
⊢ (shiftFunctor C a₃).map (NatTrans.app (shiftFunctorAdd C a₁ a₂).inv X) ≫
      NatTrans.app (shiftFunctorAdd C (a₁ + a₂) a₃).inv X =
    NatTrans.app (shiftFunctorAdd C a₂ a₃).inv ((shiftFunctor C a₁).obj X) ≫
      NatTrans.app (shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) (_ : a₁ + (a₂ + a₃) = a₁ + a₂ + a₃)).inv X
[PROOFSTEP]
simpa using NatTrans.congr_app (congr_arg Iso.inv (shiftFunctorAdd_assoc C a₁ a₂ a₃)) X
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
X Y : C
f : X ⟶ Y
i j : A
⊢ (shiftFunctor C j).map ((shiftFunctor C i).map f) =
    (shiftAdd X i j).inv ≫ (shiftFunctor C (i + j)).map f ≫ (shiftAdd Y i j).hom
[PROOFSTEP]
symm
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
X Y : C
f : X ⟶ Y
i j : A
⊢ (shiftAdd X i j).inv ≫ (shiftFunctor C (i + j)).map f ≫ (shiftAdd Y i j).hom =
    (shiftFunctor C j).map ((shiftFunctor C i).map f)
[PROOFSTEP]
apply NatIso.naturality_1
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
X Y : C
f : X ⟶ Y
⊢ (shiftFunctor C 0).map f = (shiftZero A X).hom ≫ f ≫ (shiftZero A Y).inv
[PROOFSTEP]
symm
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
X Y : C
f : X ⟶ Y
⊢ (shiftZero A X).hom ≫ f ≫ (shiftZero A Y).inv = (shiftFunctor C 0).map f
[PROOFSTEP]
apply NatIso.naturality_2
[GOAL]
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
⊢ j + i = 0
[PROOFSTEP]
rw [← add_left_inj j, add_assoc, h, zero_add, add_zero]
[GOAL]
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 (NatTrans.app (shiftFunctorCompIsoId C i j h).symm.hom X) ≫
      NatTrans.app (shiftFunctorCompIsoId C j i (_ : j + i = 0)).hom ((shiftFunctor C i).obj X) =
    𝟙 ((shiftFunctor C i).obj X)
[PROOFSTEP]
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]
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
⊢ (MonoidalCategory.tensorObj { as := j } { as := i }).as = (MonoidalCategory.tensorUnit (Discrete A)).as
[PROOFSTEP]
dsimp
[GOAL]
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
⊢ j + i = 0
[PROOFSTEP]
rw [← add_left_inj j, add_assoc, h, zero_add, add_zero]
[GOAL]
case h.e'_2.h.h.e'_6.h.h.e'_8.h.h.e'_7.h.h.e'_5.h
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 ((𝟭 C).obj X) ⟶ (𝟭 C).obj ((shiftFunctor C i).obj X)) =
    ((equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
              (Discrete.eqToIso
                (_ :
                  (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                    (MonoidalCategory.tensorUnit (Discrete A)).as))
              (_ :
                MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                    (MonoidalCategory.leftUnitor { as := i }).hom =
                  (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                    MonoidalCategory.tensorHom (𝟙 { as := i })
                        (Discrete.eqToIso
                            (_ :
                              (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                                (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                      (MonoidalCategory.rightUnitor { as := i }).hom)).functor.obj
        ((𝟭 C).obj X) ⟶
      (𝟭 C).obj
        ((equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
                (Discrete.eqToIso
                  (_ :
                    (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                      (MonoidalCategory.tensorUnit (Discrete A)).as))
                (_ :
                  MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                      (MonoidalCategory.leftUnitor { as := i }).hom =
                    (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                      MonoidalCategory.tensorHom (𝟙 { as := i })
                          (Discrete.eqToIso
                              (_ :
                                (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                                  (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                        (MonoidalCategory.rightUnitor { as := i }).hom)).functor.obj
          X))
e_3✝ :
  (shiftFunctor C i).obj ((𝟭 C).obj X) =
    (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
            (Discrete.eqToIso
              (_ :
                (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                  (MonoidalCategory.tensorUnit (Discrete A)).as))
            (_ :
              MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                  (MonoidalCategory.leftUnitor { as := i }).hom =
                (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                  MonoidalCategory.tensorHom (𝟙 { as := i })
                      (Discrete.eqToIso
                          (_ :
                            (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                              (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                    (MonoidalCategory.rightUnitor { as := i }).hom)).functor.obj
      ((𝟭 C).obj X)
e_4✝¹ :
  (shiftFunctor C i).obj ((shiftFunctor C i ⋙ shiftFunctor C j).obj X) =
    (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
            (Discrete.eqToIso
              (_ :
                (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                  (MonoidalCategory.tensorUnit (Discrete A)).as))
            (_ :
              MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                  (MonoidalCategory.leftUnitor { as := i }).hom =
                (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                  MonoidalCategory.tensorHom (𝟙 { as := i })
                      (Discrete.eqToIso
                          (_ :
                            (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                              (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                    (MonoidalCategory.rightUnitor { as := i }).hom)).functor.obj
      (((equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
                (Discrete.eqToIso
                  (_ :
                    (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                      (MonoidalCategory.tensorUnit (Discrete A)).as))
                (_ :
                  MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                      (MonoidalCategory.leftUnitor { as := i }).hom =
                    (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                      MonoidalCategory.tensorHom (𝟙 { as := i })
                          (Discrete.eqToIso
                              (_ :
                                (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                                  (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                        (MonoidalCategory.rightUnitor { as := i }).hom)).functor ⋙
            (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
                (Discrete.eqToIso
                  (_ :
                    (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                      (MonoidalCategory.tensorUnit (Discrete A)).as))
                (_ :
                  MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                      (MonoidalCategory.leftUnitor { as := i }).hom =
                    (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                      MonoidalCategory.tensorHom (𝟙 { as := i })
                          (Discrete.eqToIso
                              (_ :
                                (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                                  (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                        (MonoidalCategory.rightUnitor { as := i }).hom)).inverse).obj
        X)
e_7✝ :
  (shiftFunctor C i ⋙ shiftFunctor C j).obj X =
    ((equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
              (Discrete.eqToIso
                (_ :
                  (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                    (MonoidalCategory.tensorUnit (Discrete A)).as))
              (_ :
                MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                    (MonoidalCategory.leftUnitor { as := i }).hom =
                  (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                    MonoidalCategory.tensorHom (𝟙 { as := i })
                        (Discrete.eqToIso
                            (_ :
                              (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                                (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                      (MonoidalCategory.rightUnitor { as := i }).hom)).functor ⋙
          (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
              (Discrete.eqToIso
                (_ :
                  (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                    (MonoidalCategory.tensorUnit (Discrete A)).as))
              (_ :
                MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                    (MonoidalCategory.leftUnitor { as := i }).hom =
                  (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                    MonoidalCategory.tensorHom (𝟙 { as := i })
                        (Discrete.eqToIso
                            (_ :
                              (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                                (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                      (MonoidalCategory.rightUnitor { as := i }).hom)).inverse).obj
      X
e_6✝ :
  shiftFunctor C i ⋙ shiftFunctor C j =
    (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
          (Discrete.eqToIso
            (_ :
              (MonoidalCategory.tensorObj { as := j } { as := i }).as = (MonoidalCategory.tensorUnit (Discrete A)).as))
          (_ :
            MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                (MonoidalCategory.leftUnitor { as := i }).hom =
              (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                MonoidalCategory.tensorHom (𝟙 { as := i })
                    (Discrete.eqToIso
                        (_ :
                          (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                            (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                  (MonoidalCategory.rightUnitor { as := i }).hom)).functor ⋙
      (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
          (Discrete.eqToIso
            (_ :
              (MonoidalCategory.tensorObj { as := j } { as := i }).as = (MonoidalCategory.tensorUnit (Discrete A)).as))
          (_ :
            MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                (MonoidalCategory.leftUnitor { as := i }).hom =
              (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                MonoidalCategory.tensorHom (𝟙 { as := i })
                    (Discrete.eqToIso
                        (_ :
                          (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                            (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                  (MonoidalCategory.rightUnitor { as := i }).hom)).inverse
e_4✝ :
  shiftFunctor C i ⋙ shiftFunctor C j =
    (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
          (Discrete.eqToIso
            (_ :
              (MonoidalCategory.tensorObj { as := j } { as := i }).as = (MonoidalCategory.tensorUnit (Discrete A)).as))
          (_ :
            MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                (MonoidalCategory.leftUnitor { as := i }).hom =
              (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                MonoidalCategory.tensorHom (𝟙 { as := i })
                    (Discrete.eqToIso
                        (_ :
                          (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                            (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                  (MonoidalCategory.rightUnitor { as := i }).hom)).functor ⋙
      (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
          (Discrete.eqToIso
            (_ :
              (MonoidalCategory.tensorObj { as := j } { as := i }).as = (MonoidalCategory.tensorUnit (Discrete A)).as))
          (_ :
            MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                (MonoidalCategory.leftUnitor { as := i }).hom =
              (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                MonoidalCategory.tensorHom (𝟙 { as := i })
                    (Discrete.eqToIso
                        (_ :
                          (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                            (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                  (MonoidalCategory.rightUnitor { as := i }).hom)).inverse
⊢ (shiftFunctorCompIsoId C i j h).symm =
    (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
        (Discrete.eqToIso
          (_ : (MonoidalCategory.tensorObj { as := j } { as := i }).as = (MonoidalCategory.tensorUnit (Discrete A)).as))
        (_ :
          MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
              (MonoidalCategory.leftUnitor { as := i }).hom =
            (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
              MonoidalCategory.tensorHom (𝟙 { as := i })
                  (Discrete.eqToIso
                      (_ :
                        (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                          (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                (MonoidalCategory.rightUnitor { as := i }).hom)).unitIso
case h.e'_2.h.h.e'_7.h.h.e'_7.h.h.e'_5.h
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 ((𝟭 C).obj X) ⟶ (𝟭 C).obj ((shiftFunctor C i).obj X)) =
    ((equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
              (Discrete.eqToIso
                (_ :
                  (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                    (MonoidalCategory.tensorUnit (Discrete A)).as))
              (_ :
                MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                    (MonoidalCategory.leftUnitor { as := i }).hom =
                  (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                    MonoidalCategory.tensorHom (𝟙 { as := i })
                        (Discrete.eqToIso
                            (_ :
                              (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                                (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                      (MonoidalCategory.rightUnitor { as := i }).hom)).functor.obj
        ((𝟭 C).obj X) ⟶
      (𝟭 C).obj
        ((equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
                (Discrete.eqToIso
                  (_ :
                    (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                      (MonoidalCategory.tensorUnit (Discrete A)).as))
                (_ :
                  MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                      (MonoidalCategory.leftUnitor { as := i }).hom =
                    (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                      MonoidalCategory.tensorHom (𝟙 { as := i })
                          (Discrete.eqToIso
                              (_ :
                                (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                                  (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                        (MonoidalCategory.rightUnitor { as := i }).hom)).functor.obj
          X))
e_4✝ :
  (shiftFunctor C i).obj ((shiftFunctor C i ⋙ shiftFunctor C j).obj X) =
    (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
            (Discrete.eqToIso
              (_ :
                (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                  (MonoidalCategory.tensorUnit (Discrete A)).as))
            (_ :
              MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                  (MonoidalCategory.leftUnitor { as := i }).hom =
                (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                  MonoidalCategory.tensorHom (𝟙 { as := i })
                      (Discrete.eqToIso
                          (_ :
                            (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                              (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                    (MonoidalCategory.rightUnitor { as := i }).hom)).functor.obj
      (((equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
                (Discrete.eqToIso
                  (_ :
                    (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                      (MonoidalCategory.tensorUnit (Discrete A)).as))
                (_ :
                  MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                      (MonoidalCategory.leftUnitor { as := i }).hom =
                    (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                      MonoidalCategory.tensorHom (𝟙 { as := i })
                          (Discrete.eqToIso
                              (_ :
                                (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                                  (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                        (MonoidalCategory.rightUnitor { as := i }).hom)).functor ⋙
            (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
                (Discrete.eqToIso
                  (_ :
                    (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                      (MonoidalCategory.tensorUnit (Discrete A)).as))
                (_ :
                  MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                      (MonoidalCategory.leftUnitor { as := i }).hom =
                    (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                      MonoidalCategory.tensorHom (𝟙 { as := i })
                          (Discrete.eqToIso
                              (_ :
                                (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                                  (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                        (MonoidalCategory.rightUnitor { as := i }).hom)).inverse).obj
        X)
e_5✝¹ :
  (𝟭 C).obj ((shiftFunctor C i).obj X) =
    (𝟭 C).obj
      ((equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
              (Discrete.eqToIso
                (_ :
                  (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                    (MonoidalCategory.tensorUnit (Discrete A)).as))
              (_ :
                MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                    (MonoidalCategory.leftUnitor { as := i }).hom =
                  (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                    MonoidalCategory.tensorHom (𝟙 { as := i })
                        (Discrete.eqToIso
                            (_ :
                              (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                                (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                      (MonoidalCategory.rightUnitor { as := i }).hom)).functor.obj
        X)
e_5✝ :
  shiftFunctor C j ⋙ shiftFunctor C i =
    (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
          (Discrete.eqToIso
            (_ :
              (MonoidalCategory.tensorObj { as := j } { as := i }).as = (MonoidalCategory.tensorUnit (Discrete A)).as))
          (_ :
            MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                (MonoidalCategory.leftUnitor { as := i }).hom =
              (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                MonoidalCategory.tensorHom (𝟙 { as := i })
                    (Discrete.eqToIso
                        (_ :
                          (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                            (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                  (MonoidalCategory.rightUnitor { as := i }).hom)).inverse ⋙
      (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
          (Discrete.eqToIso
            (_ :
              (MonoidalCategory.tensorObj { as := j } { as := i }).as = (MonoidalCategory.tensorUnit (Discrete A)).as))
          (_ :
            MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                (MonoidalCategory.leftUnitor { as := i }).hom =
              (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                MonoidalCategory.tensorHom (𝟙 { as := i })
                    (Discrete.eqToIso
                        (_ :
                          (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                            (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                  (MonoidalCategory.rightUnitor { as := i }).hom)).functor
e_3✝ :
  shiftFunctor C j ⋙ shiftFunctor C i =
    (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
          (Discrete.eqToIso
            (_ :
              (MonoidalCategory.tensorObj { as := j } { as := i }).as = (MonoidalCategory.tensorUnit (Discrete A)).as))
          (_ :
            MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                (MonoidalCategory.leftUnitor { as := i }).hom =
              (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                MonoidalCategory.tensorHom (𝟙 { as := i })
                    (Discrete.eqToIso
                        (_ :
                          (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                            (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                  (MonoidalCategory.rightUnitor { as := i }).hom)).inverse ⋙
      (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
          (Discrete.eqToIso
            (_ :
              (MonoidalCategory.tensorObj { as := j } { as := i }).as = (MonoidalCategory.tensorUnit (Discrete A)).as))
          (_ :
            MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                (MonoidalCategory.leftUnitor { as := i }).hom =
              (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                MonoidalCategory.tensorHom (𝟙 { as := i })
                    (Discrete.eqToIso
                        (_ :
                          (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                            (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                  (MonoidalCategory.rightUnitor { as := i }).hom)).functor
⊢ shiftFunctorCompIsoId C j i (_ : j + i = 0) =
    (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
        (Discrete.eqToIso
          (_ : (MonoidalCategory.tensorObj { as := j } { as := i }).as = (MonoidalCategory.tensorUnit (Discrete A)).as))
        (_ :
          MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
              (MonoidalCategory.leftUnitor { as := i }).hom =
            (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
              MonoidalCategory.tensorHom (𝟙 { as := i })
                  (Discrete.eqToIso
                      (_ :
                        (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                          (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                (MonoidalCategory.rightUnitor { as := i }).hom)).counitIso
[PROOFSTEP]
all_goals
  ext X
  dsimp [shiftFunctorCompIsoId, unitOfTensorIsoUnit, shiftFunctorAdd']
  simp only [Category.assoc, eqToHom_map]
  rfl
[GOAL]
case h.e'_2.h.h.e'_6.h.h.e'_8.h.h.e'_7.h.h.e'_5.h
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 ((𝟭 C).obj X) ⟶ (𝟭 C).obj ((shiftFunctor C i).obj X)) =
    ((equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
              (Discrete.eqToIso
                (_ :
                  (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                    (MonoidalCategory.tensorUnit (Discrete A)).as))
              (_ :
                MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                    (MonoidalCategory.leftUnitor { as := i }).hom =
                  (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                    MonoidalCategory.tensorHom (𝟙 { as := i })
                        (Discrete.eqToIso
                            (_ :
                              (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                                (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                      (MonoidalCategory.rightUnitor { as := i }).hom)).functor.obj
        ((𝟭 C).obj X) ⟶
      (𝟭 C).obj
        ((equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
                (Discrete.eqToIso
                  (_ :
                    (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                      (MonoidalCategory.tensorUnit (Discrete A)).as))
                (_ :
                  MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                      (MonoidalCategory.leftUnitor { as := i }).hom =
                    (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                      MonoidalCategory.tensorHom (𝟙 { as := i })
                          (Discrete.eqToIso
                              (_ :
                                (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                                  (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                        (MonoidalCategory.rightUnitor { as := i }).hom)).functor.obj
          X))
e_3✝ :
  (shiftFunctor C i).obj ((𝟭 C).obj X) =
    (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
            (Discrete.eqToIso
              (_ :
                (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                  (MonoidalCategory.tensorUnit (Discrete A)).as))
            (_ :
              MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                  (MonoidalCategory.leftUnitor { as := i }).hom =
                (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                  MonoidalCategory.tensorHom (𝟙 { as := i })
                      (Discrete.eqToIso
                          (_ :
                            (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                              (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                    (MonoidalCategory.rightUnitor { as := i }).hom)).functor.obj
      ((𝟭 C).obj X)
e_4✝¹ :
  (shiftFunctor C i).obj ((shiftFunctor C i ⋙ shiftFunctor C j).obj X) =
    (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
            (Discrete.eqToIso
              (_ :
                (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                  (MonoidalCategory.tensorUnit (Discrete A)).as))
            (_ :
              MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                  (MonoidalCategory.leftUnitor { as := i }).hom =
                (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                  MonoidalCategory.tensorHom (𝟙 { as := i })
                      (Discrete.eqToIso
                          (_ :
                            (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                              (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                    (MonoidalCategory.rightUnitor { as := i }).hom)).functor.obj
      (((equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
                (Discrete.eqToIso
                  (_ :
                    (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                      (MonoidalCategory.tensorUnit (Discrete A)).as))
                (_ :
                  MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                      (MonoidalCategory.leftUnitor { as := i }).hom =
                    (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                      MonoidalCategory.tensorHom (𝟙 { as := i })
                          (Discrete.eqToIso
                              (_ :
                                (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                                  (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                        (MonoidalCategory.rightUnitor { as := i }).hom)).functor ⋙
            (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
                (Discrete.eqToIso
                  (_ :
                    (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                      (MonoidalCategory.tensorUnit (Discrete A)).as))
                (_ :
                  MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                      (MonoidalCategory.leftUnitor { as := i }).hom =
                    (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                      MonoidalCategory.tensorHom (𝟙 { as := i })
                          (Discrete.eqToIso
                              (_ :
                                (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                                  (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                        (MonoidalCategory.rightUnitor { as := i }).hom)).inverse).obj
        X)
e_7✝ :
  (shiftFunctor C i ⋙ shiftFunctor C j).obj X =
    ((equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
              (Discrete.eqToIso
                (_ :
                  (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                    (MonoidalCategory.tensorUnit (Discrete A)).as))
              (_ :
                MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                    (MonoidalCategory.leftUnitor { as := i }).hom =
                  (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                    MonoidalCategory.tensorHom (𝟙 { as := i })
                        (Discrete.eqToIso
                            (_ :
                              (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                                (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                      (MonoidalCategory.rightUnitor { as := i }).hom)).functor ⋙
          (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
              (Discrete.eqToIso
                (_ :
                  (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                    (MonoidalCategory.tensorUnit (Discrete A)).as))
              (_ :
                MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                    (MonoidalCategory.leftUnitor { as := i }).hom =
                  (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                    MonoidalCategory.tensorHom (𝟙 { as := i })
                        (Discrete.eqToIso
                            (_ :
                              (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                                (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                      (MonoidalCategory.rightUnitor { as := i }).hom)).inverse).obj
      X
e_6✝ :
  shiftFunctor C i ⋙ shiftFunctor C j =
    (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
          (Discrete.eqToIso
            (_ :
              (MonoidalCategory.tensorObj { as := j } { as := i }).as = (MonoidalCategory.tensorUnit (Discrete A)).as))
          (_ :
            MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                (MonoidalCategory.leftUnitor { as := i }).hom =
              (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                MonoidalCategory.tensorHom (𝟙 { as := i })
                    (Discrete.eqToIso
                        (_ :
                          (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                            (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                  (MonoidalCategory.rightUnitor { as := i }).hom)).functor ⋙
      (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
          (Discrete.eqToIso
            (_ :
              (MonoidalCategory.tensorObj { as := j } { as := i }).as = (MonoidalCategory.tensorUnit (Discrete A)).as))
          (_ :
            MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                (MonoidalCategory.leftUnitor { as := i }).hom =
              (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                MonoidalCategory.tensorHom (𝟙 { as := i })
                    (Discrete.eqToIso
                        (_ :
                          (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                            (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                  (MonoidalCategory.rightUnitor { as := i }).hom)).inverse
e_4✝ :
  shiftFunctor C i ⋙ shiftFunctor C j =
    (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
          (Discrete.eqToIso
            (_ :
              (MonoidalCategory.tensorObj { as := j } { as := i }).as = (MonoidalCategory.tensorUnit (Discrete A)).as))
          (_ :
            MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                (MonoidalCategory.leftUnitor { as := i }).hom =
              (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                MonoidalCategory.tensorHom (𝟙 { as := i })
                    (Discrete.eqToIso
                        (_ :
                          (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                            (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                  (MonoidalCategory.rightUnitor { as := i }).hom)).functor ⋙
      (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
          (Discrete.eqToIso
            (_ :
              (MonoidalCategory.tensorObj { as := j } { as := i }).as = (MonoidalCategory.tensorUnit (Discrete A)).as))
          (_ :
            MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                (MonoidalCategory.leftUnitor { as := i }).hom =
              (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                MonoidalCategory.tensorHom (𝟙 { as := i })
                    (Discrete.eqToIso
                        (_ :
                          (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                            (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                  (MonoidalCategory.rightUnitor { as := i }).hom)).inverse
⊢ (shiftFunctorCompIsoId C i j h).symm =
    (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
        (Discrete.eqToIso
          (_ : (MonoidalCategory.tensorObj { as := j } { as := i }).as = (MonoidalCategory.tensorUnit (Discrete A)).as))
        (_ :
          MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
              (MonoidalCategory.leftUnitor { as := i }).hom =
            (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
              MonoidalCategory.tensorHom (𝟙 { as := i })
                  (Discrete.eqToIso
                      (_ :
                        (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                          (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                (MonoidalCategory.rightUnitor { as := i }).hom)).unitIso
[PROOFSTEP]
ext X
[GOAL]
case h.e'_2.h.h.e'_6.h.h.e'_8.h.h.e'_7.h.h.e'_5.h.w.w.h
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 ((𝟭 C).obj X✝) ⟶ (𝟭 C).obj ((shiftFunctor C i).obj X✝)) =
    ((equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
              (Discrete.eqToIso
                (_ :
                  (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                    (MonoidalCategory.tensorUnit (Discrete A)).as))
              (_ :
                MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                    (MonoidalCategory.leftUnitor { as := i }).hom =
                  (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                    MonoidalCategory.tensorHom (𝟙 { as := i })
                        (Discrete.eqToIso
                            (_ :
                              (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                                (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                      (MonoidalCategory.rightUnitor { as := i }).hom)).functor.obj
        ((𝟭 C).obj X✝) ⟶
      (𝟭 C).obj
        ((equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
                (Discrete.eqToIso
                  (_ :
                    (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                      (MonoidalCategory.tensorUnit (Discrete A)).as))
                (_ :
                  MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                      (MonoidalCategory.leftUnitor { as := i }).hom =
                    (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                      MonoidalCategory.tensorHom (𝟙 { as := i })
                          (Discrete.eqToIso
                              (_ :
                                (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                                  (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                        (MonoidalCategory.rightUnitor { as := i }).hom)).functor.obj
          X✝))
e_3✝ :
  (shiftFunctor C i).obj ((𝟭 C).obj X✝) =
    (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
            (Discrete.eqToIso
              (_ :
                (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                  (MonoidalCategory.tensorUnit (Discrete A)).as))
            (_ :
              MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                  (MonoidalCategory.leftUnitor { as := i }).hom =
                (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                  MonoidalCategory.tensorHom (𝟙 { as := i })
                      (Discrete.eqToIso
                          (_ :
                            (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                              (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                    (MonoidalCategory.rightUnitor { as := i }).hom)).functor.obj
      ((𝟭 C).obj X✝)
e_4✝¹ :
  (shiftFunctor C i).obj ((shiftFunctor C i ⋙ shiftFunctor C j).obj X✝) =
    (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
            (Discrete.eqToIso
              (_ :
                (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                  (MonoidalCategory.tensorUnit (Discrete A)).as))
            (_ :
              MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                  (MonoidalCategory.leftUnitor { as := i }).hom =
                (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                  MonoidalCategory.tensorHom (𝟙 { as := i })
                      (Discrete.eqToIso
                          (_ :
                            (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                              (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                    (MonoidalCategory.rightUnitor { as := i }).hom)).functor.obj
      (((equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
                (Discrete.eqToIso
                  (_ :
                    (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                      (MonoidalCategory.tensorUnit (Discrete A)).as))
                (_ :
                  MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                      (MonoidalCategory.leftUnitor { as := i }).hom =
                    (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                      MonoidalCategory.tensorHom (𝟙 { as := i })
                          (Discrete.eqToIso
                              (_ :
                                (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                                  (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                        (MonoidalCategory.rightUnitor { as := i }).hom)).functor ⋙
            (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
                (Discrete.eqToIso
                  (_ :
                    (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                      (MonoidalCategory.tensorUnit (Discrete A)).as))
                (_ :
                  MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                      (MonoidalCategory.leftUnitor { as := i }).hom =
                    (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                      MonoidalCategory.tensorHom (𝟙 { as := i })
                          (Discrete.eqToIso
                              (_ :
                                (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                                  (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                        (MonoidalCategory.rightUnitor { as := i }).hom)).inverse).obj
        X✝)
e_7✝ :
  (shiftFunctor C i ⋙ shiftFunctor C j).obj X✝ =
    ((equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
              (Discrete.eqToIso
                (_ :
                  (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                    (MonoidalCategory.tensorUnit (Discrete A)).as))
              (_ :
                MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                    (MonoidalCategory.leftUnitor { as := i }).hom =
                  (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                    MonoidalCategory.tensorHom (𝟙 { as := i })
                        (Discrete.eqToIso
                            (_ :
                              (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                                (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                      (MonoidalCategory.rightUnitor { as := i }).hom)).functor ⋙
          (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
              (Discrete.eqToIso
                (_ :
                  (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                    (MonoidalCategory.tensorUnit (Discrete A)).as))
              (_ :
                MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                    (MonoidalCategory.leftUnitor { as := i }).hom =
                  (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                    MonoidalCategory.tensorHom (𝟙 { as := i })
                        (Discrete.eqToIso
                            (_ :
                              (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                                (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                      (MonoidalCategory.rightUnitor { as := i }).hom)).inverse).obj
      X✝
e_6✝ :
  shiftFunctor C i ⋙ shiftFunctor C j =
    (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
          (Discrete.eqToIso
            (_ :
              (MonoidalCategory.tensorObj { as := j } { as := i }).as = (MonoidalCategory.tensorUnit (Discrete A)).as))
          (_ :
            MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                (MonoidalCategory.leftUnitor { as := i }).hom =
              (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                MonoidalCategory.tensorHom (𝟙 { as := i })
                    (Discrete.eqToIso
                        (_ :
                          (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                            (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                  (MonoidalCategory.rightUnitor { as := i }).hom)).functor ⋙
      (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
          (Discrete.eqToIso
            (_ :
              (MonoidalCategory.tensorObj { as := j } { as := i }).as = (MonoidalCategory.tensorUnit (Discrete A)).as))
          (_ :
            MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                (MonoidalCategory.leftUnitor { as := i }).hom =
              (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                MonoidalCategory.tensorHom (𝟙 { as := i })
                    (Discrete.eqToIso
                        (_ :
                          (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                            (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                  (MonoidalCategory.rightUnitor { as := i }).hom)).inverse
e_4✝ :
  shiftFunctor C i ⋙ shiftFunctor C j =
    (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
          (Discrete.eqToIso
            (_ :
              (MonoidalCategory.tensorObj { as := j } { as := i }).as = (MonoidalCategory.tensorUnit (Discrete A)).as))
          (_ :
            MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                (MonoidalCategory.leftUnitor { as := i }).hom =
              (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                MonoidalCategory.tensorHom (𝟙 { as := i })
                    (Discrete.eqToIso
                        (_ :
                          (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                            (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                  (MonoidalCategory.rightUnitor { as := i }).hom)).functor ⋙
      (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
          (Discrete.eqToIso
            (_ :
              (MonoidalCategory.tensorObj { as := j } { as := i }).as = (MonoidalCategory.tensorUnit (Discrete A)).as))
          (_ :
            MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                (MonoidalCategory.leftUnitor { as := i }).hom =
              (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                MonoidalCategory.tensorHom (𝟙 { as := i })
                    (Discrete.eqToIso
                        (_ :
                          (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                            (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                  (MonoidalCategory.rightUnitor { as := i }).hom)).inverse
X : C
⊢ NatTrans.app (shiftFunctorCompIsoId C i j h).symm.hom X =
    NatTrans.app
      (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
            (Discrete.eqToIso
              (_ :
                (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                  (MonoidalCategory.tensorUnit (Discrete A)).as))
            (_ :
              MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                  (MonoidalCategory.leftUnitor { as := i }).hom =
                (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                  MonoidalCategory.tensorHom (𝟙 { as := i })
                      (Discrete.eqToIso
                          (_ :
                            (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                              (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                    (MonoidalCategory.rightUnitor { as := i }).hom)).unitIso.hom
      X
[PROOFSTEP]
dsimp [shiftFunctorCompIsoId, unitOfTensorIsoUnit, shiftFunctorAdd']
[GOAL]
case h.e'_2.h.h.e'_6.h.h.e'_8.h.h.e'_7.h.h.e'_5.h.w.w.h
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 ((𝟭 C).obj X✝) ⟶ (𝟭 C).obj ((shiftFunctor C i).obj X✝)) =
    ((equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
              (Discrete.eqToIso
                (_ :
                  (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                    (MonoidalCategory.tensorUnit (Discrete A)).as))
              (_ :
                MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                    (MonoidalCategory.leftUnitor { as := i }).hom =
                  (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                    MonoidalCategory.tensorHom (𝟙 { as := i })
                        (Discrete.eqToIso
                            (_ :
                              (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                                (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                      (MonoidalCategory.rightUnitor { as := i }).hom)).functor.obj
        ((𝟭 C).obj X✝) ⟶
      (𝟭 C).obj
        ((equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
                (Discrete.eqToIso
                  (_ :
                    (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                      (MonoidalCategory.tensorUnit (Discrete A)).as))
                (_ :
                  MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                      (MonoidalCategory.leftUnitor { as := i }).hom =
                    (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                      MonoidalCategory.tensorHom (𝟙 { as := i })
                          (Discrete.eqToIso
                              (_ :
                                (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                                  (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                        (MonoidalCategory.rightUnitor { as := i }).hom)).functor.obj
          X✝))
e_3✝ :
  (shiftFunctor C i).obj ((𝟭 C).obj X✝) =
    (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
            (Discrete.eqToIso
              (_ :
                (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                  (MonoidalCategory.tensorUnit (Discrete A)).as))
            (_ :
              MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                  (MonoidalCategory.leftUnitor { as := i }).hom =
                (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                  MonoidalCategory.tensorHom (𝟙 { as := i })
                      (Discrete.eqToIso
                          (_ :
                            (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                              (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                    (MonoidalCategory.rightUnitor { as := i }).hom)).functor.obj
      ((𝟭 C).obj X✝)
e_4✝¹ :
  (shiftFunctor C i).obj ((shiftFunctor C i ⋙ shiftFunctor C j).obj X✝) =
    (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
            (Discrete.eqToIso
              (_ :
                (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                  (MonoidalCategory.tensorUnit (Discrete A)).as))
            (_ :
              MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                  (MonoidalCategory.leftUnitor { as := i }).hom =
                (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                  MonoidalCategory.tensorHom (𝟙 { as := i })
                      (Discrete.eqToIso
                          (_ :
                            (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                              (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                    (MonoidalCategory.rightUnitor { as := i }).hom)).functor.obj
      (((equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
                (Discrete.eqToIso
                  (_ :
                    (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                      (MonoidalCategory.tensorUnit (Discrete A)).as))
                (_ :
                  MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                      (MonoidalCategory.leftUnitor { as := i }).hom =
                    (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                      MonoidalCategory.tensorHom (𝟙 { as := i })
                          (Discrete.eqToIso
                              (_ :
                                (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                                  (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                        (MonoidalCategory.rightUnitor { as := i }).hom)).functor ⋙
            (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
                (Discrete.eqToIso
                  (_ :
                    (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                      (MonoidalCategory.tensorUnit (Discrete A)).as))
                (_ :
                  MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                      (MonoidalCategory.leftUnitor { as := i }).hom =
                    (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                      MonoidalCategory.tensorHom (𝟙 { as := i })
                          (Discrete.eqToIso
                              (_ :
                                (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                                  (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                        (MonoidalCategory.rightUnitor { as := i }).hom)).inverse).obj
        X✝)
e_7✝ :
  (shiftFunctor C i ⋙ shiftFunctor C j).obj X✝ =
    ((equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
              (Discrete.eqToIso
                (_ :
                  (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                    (MonoidalCategory.tensorUnit (Discrete A)).as))
              (_ :
                MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                    (MonoidalCategory.leftUnitor { as := i }).hom =
                  (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                    MonoidalCategory.tensorHom (𝟙 { as := i })
                        (Discrete.eqToIso
                            (_ :
                              (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                                (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                      (MonoidalCategory.rightUnitor { as := i }).hom)).functor ⋙
          (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
              (Discrete.eqToIso
                (_ :
                  (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                    (MonoidalCategory.tensorUnit (Discrete A)).as))
              (_ :
                MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                    (MonoidalCategory.leftUnitor { as := i }).hom =
                  (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                    MonoidalCategory.tensorHom (𝟙 { as := i })
                        (Discrete.eqToIso
                            (_ :
                              (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                                (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                      (MonoidalCategory.rightUnitor { as := i }).hom)).inverse).obj
      X✝
e_6✝ :
  shiftFunctor C i ⋙ shiftFunctor C j =
    (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
          (Discrete.eqToIso
            (_ :
              (MonoidalCategory.tensorObj { as := j } { as := i }).as = (MonoidalCategory.tensorUnit (Discrete A)).as))
          (_ :
            MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                (MonoidalCategory.leftUnitor { as := i }).hom =
              (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                MonoidalCategory.tensorHom (𝟙 { as := i })
                    (Discrete.eqToIso
                        (_ :
                          (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                            (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                  (MonoidalCategory.rightUnitor { as := i }).hom)).functor ⋙
      (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
          (Discrete.eqToIso
            (_ :
              (MonoidalCategory.tensorObj { as := j } { as := i }).as = (MonoidalCategory.tensorUnit (Discrete A)).as))
          (_ :
            MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                (MonoidalCategory.leftUnitor { as := i }).hom =
              (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                MonoidalCategory.tensorHom (𝟙 { as := i })
                    (Discrete.eqToIso
                        (_ :
                          (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                            (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                  (MonoidalCategory.rightUnitor { as := i }).hom)).inverse
e_4✝ :
  shiftFunctor C i ⋙ shiftFunctor C j =
    (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
          (Discrete.eqToIso
            (_ :
              (MonoidalCategory.tensorObj { as := j } { as := i }).as = (MonoidalCategory.tensorUnit (Discrete A)).as))
          (_ :
            MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                (MonoidalCategory.leftUnitor { as := i }).hom =
              (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                MonoidalCategory.tensorHom (𝟙 { as := i })
                    (Discrete.eqToIso
                        (_ :
                          (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                            (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                  (MonoidalCategory.rightUnitor { as := i }).hom)).functor ⋙
      (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
          (Discrete.eqToIso
            (_ :
              (MonoidalCategory.tensorObj { as := j } { as := i }).as = (MonoidalCategory.tensorUnit (Discrete A)).as))
          (_ :
            MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                (MonoidalCategory.leftUnitor { as := i }).hom =
              (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                MonoidalCategory.tensorHom (𝟙 { as := i })
                    (Discrete.eqToIso
                        (_ :
                          (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                            (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                  (MonoidalCategory.rightUnitor { as := i }).hom)).inverse
X : C
⊢ NatTrans.app (shiftFunctorZero C A).inv X ≫
      NatTrans.app (eqToHom (_ : shiftFunctor C 0 = shiftFunctor C (i + j))) X ≫
        NatTrans.app (shiftFunctorAdd C i j).hom X =
    (NatTrans.app (shiftMonoidalFunctor C A).toLaxMonoidalFunctor.ε X ≫
        NatTrans.app
          ((shiftMonoidalFunctor C A).toLaxMonoidalFunctor.toFunctor.map
            (eqToHom
              (_ : MonoidalCategory.tensorUnit (Discrete A) = MonoidalCategory.tensorObj { as := i } { as := j })))
          X) ≫
      NatTrans.app (MonoidalFunctor.μIso (shiftMonoidalFunctor C A) { as := i } { as := j }).inv X
[PROOFSTEP]
simp only [Category.assoc, eqToHom_map]
[GOAL]
case h.e'_2.h.h.e'_6.h.h.e'_8.h.h.e'_7.h.h.e'_5.h.w.w.h
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 ((𝟭 C).obj X✝) ⟶ (𝟭 C).obj ((shiftFunctor C i).obj X✝)) =
    ((equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
              (Discrete.eqToIso
                (_ :
                  (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                    (MonoidalCategory.tensorUnit (Discrete A)).as))
              (_ :
                MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                    (MonoidalCategory.leftUnitor { as := i }).hom =
                  (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                    MonoidalCategory.tensorHom (𝟙 { as := i })
                        (Discrete.eqToIso
                            (_ :
                              (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                                (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                      (MonoidalCategory.rightUnitor { as := i }).hom)).functor.obj
        ((𝟭 C).obj X✝) ⟶
      (𝟭 C).obj
        ((equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
                (Discrete.eqToIso
                  (_ :
                    (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                      (MonoidalCategory.tensorUnit (Discrete A)).as))
                (_ :
                  MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                      (MonoidalCategory.leftUnitor { as := i }).hom =
                    (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                      MonoidalCategory.tensorHom (𝟙 { as := i })
                          (Discrete.eqToIso
                              (_ :
                                (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                                  (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                        (MonoidalCategory.rightUnitor { as := i }).hom)).functor.obj
          X✝))
e_3✝ :
  (shiftFunctor C i).obj ((𝟭 C).obj X✝) =
    (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
            (Discrete.eqToIso
              (_ :
                (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                  (MonoidalCategory.tensorUnit (Discrete A)).as))
            (_ :
              MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                  (MonoidalCategory.leftUnitor { as := i }).hom =
                (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                  MonoidalCategory.tensorHom (𝟙 { as := i })
                      (Discrete.eqToIso
                          (_ :
                            (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                              (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                    (MonoidalCategory.rightUnitor { as := i }).hom)).functor.obj
      ((𝟭 C).obj X✝)
e_4✝¹ :
  (shiftFunctor C i).obj ((shiftFunctor C i ⋙ shiftFunctor C j).obj X✝) =
    (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
            (Discrete.eqToIso
              (_ :
                (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                  (MonoidalCategory.tensorUnit (Discrete A)).as))
            (_ :
              MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                  (MonoidalCategory.leftUnitor { as := i }).hom =
                (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                  MonoidalCategory.tensorHom (𝟙 { as := i })
                      (Discrete.eqToIso
                          (_ :
                            (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                              (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                    (MonoidalCategory.rightUnitor { as := i }).hom)).functor.obj
      (((equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
                (Discrete.eqToIso
                  (_ :
                    (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                      (MonoidalCategory.tensorUnit (Discrete A)).as))
                (_ :
                  MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                      (MonoidalCategory.leftUnitor { as := i }).hom =
                    (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                      MonoidalCategory.tensorHom (𝟙 { as := i })
                          (Discrete.eqToIso
                              (_ :
                                (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                                  (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                        (MonoidalCategory.rightUnitor { as := i }).hom)).functor ⋙
            (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
                (Discrete.eqToIso
                  (_ :
                    (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                      (MonoidalCategory.tensorUnit (Discrete A)).as))
                (_ :
                  MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                      (MonoidalCategory.leftUnitor { as := i }).hom =
                    (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                      MonoidalCategory.tensorHom (𝟙 { as := i })
                          (Discrete.eqToIso
                              (_ :
                                (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                                  (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                        (MonoidalCategory.rightUnitor { as := i }).hom)).inverse).obj
        X✝)
e_7✝ :
  (shiftFunctor C i ⋙ shiftFunctor C j).obj X✝ =
    ((equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
              (Discrete.eqToIso
                (_ :
                  (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                    (MonoidalCategory.tensorUnit (Discrete A)).as))
              (_ :
                MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                    (MonoidalCategory.leftUnitor { as := i }).hom =
                  (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                    MonoidalCategory.tensorHom (𝟙 { as := i })
                        (Discrete.eqToIso
                            (_ :
                              (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                                (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                      (MonoidalCategory.rightUnitor { as := i }).hom)).functor ⋙
          (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
              (Discrete.eqToIso
                (_ :
                  (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                    (MonoidalCategory.tensorUnit (Discrete A)).as))
              (_ :
                MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                    (MonoidalCategory.leftUnitor { as := i }).hom =
                  (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                    MonoidalCategory.tensorHom (𝟙 { as := i })
                        (Discrete.eqToIso
                            (_ :
                              (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                                (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                      (MonoidalCategory.rightUnitor { as := i }).hom)).inverse).obj
      X✝
e_6✝ :
  shiftFunctor C i ⋙ shiftFunctor C j =
    (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
          (Discrete.eqToIso
            (_ :
              (MonoidalCategory.tensorObj { as := j } { as := i }).as = (MonoidalCategory.tensorUnit (Discrete A)).as))
          (_ :
            MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                (MonoidalCategory.leftUnitor { as := i }).hom =
              (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                MonoidalCategory.tensorHom (𝟙 { as := i })
                    (Discrete.eqToIso
                        (_ :
                          (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                            (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                  (MonoidalCategory.rightUnitor { as := i }).hom)).functor ⋙
      (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
          (Discrete.eqToIso
            (_ :
              (MonoidalCategory.tensorObj { as := j } { as := i }).as = (MonoidalCategory.tensorUnit (Discrete A)).as))
          (_ :
            MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                (MonoidalCategory.leftUnitor { as := i }).hom =
              (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                MonoidalCategory.tensorHom (𝟙 { as := i })
                    (Discrete.eqToIso
                        (_ :
                          (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                            (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                  (MonoidalCategory.rightUnitor { as := i }).hom)).inverse
e_4✝ :
  shiftFunctor C i ⋙ shiftFunctor C j =
    (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
          (Discrete.eqToIso
            (_ :
              (MonoidalCategory.tensorObj { as := j } { as := i }).as = (MonoidalCategory.tensorUnit (Discrete A)).as))
          (_ :
            MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                (MonoidalCategory.leftUnitor { as := i }).hom =
              (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                MonoidalCategory.tensorHom (𝟙 { as := i })
                    (Discrete.eqToIso
                        (_ :
                          (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                            (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                  (MonoidalCategory.rightUnitor { as := i }).hom)).functor ⋙
      (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
          (Discrete.eqToIso
            (_ :
              (MonoidalCategory.tensorObj { as := j } { as := i }).as = (MonoidalCategory.tensorUnit (Discrete A)).as))
          (_ :
            MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                (MonoidalCategory.leftUnitor { as := i }).hom =
              (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                MonoidalCategory.tensorHom (𝟙 { as := i })
                    (Discrete.eqToIso
                        (_ :
                          (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                            (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                  (MonoidalCategory.rightUnitor { as := i }).hom)).inverse
X : C
⊢ NatTrans.app (shiftFunctorZero C A).inv X ≫
      NatTrans.app (eqToHom (_ : shiftFunctor C 0 = shiftFunctor C (i + j))) X ≫
        NatTrans.app (shiftFunctorAdd C i j).hom X =
    NatTrans.app (shiftMonoidalFunctor C A).toLaxMonoidalFunctor.ε X ≫
      NatTrans.app
          (eqToHom
            (_ :
              (shiftMonoidalFunctor C A).toLaxMonoidalFunctor.toFunctor.obj (MonoidalCategory.tensorUnit (Discrete A)) =
                (shiftMonoidalFunctor C A).toLaxMonoidalFunctor.toFunctor.obj
                  (MonoidalCategory.tensorObj { as := i } { as := j })))
          X ≫
        NatTrans.app (MonoidalFunctor.μIso (shiftMonoidalFunctor C A) { as := i } { as := j }).inv X
[PROOFSTEP]
rfl
[GOAL]
case h.e'_2.h.h.e'_7.h.h.e'_7.h.h.e'_5.h
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 ((𝟭 C).obj X) ⟶ (𝟭 C).obj ((shiftFunctor C i).obj X)) =
    ((equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
              (Discrete.eqToIso
                (_ :
                  (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                    (MonoidalCategory.tensorUnit (Discrete A)).as))
              (_ :
                MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                    (MonoidalCategory.leftUnitor { as := i }).hom =
                  (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                    MonoidalCategory.tensorHom (𝟙 { as := i })
                        (Discrete.eqToIso
                            (_ :
                              (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                                (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                      (MonoidalCategory.rightUnitor { as := i }).hom)).functor.obj
        ((𝟭 C).obj X) ⟶
      (𝟭 C).obj
        ((equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
                (Discrete.eqToIso
                  (_ :
                    (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                      (MonoidalCategory.tensorUnit (Discrete A)).as))
                (_ :
                  MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                      (MonoidalCategory.leftUnitor { as := i }).hom =
                    (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                      MonoidalCategory.tensorHom (𝟙 { as := i })
                          (Discrete.eqToIso
                              (_ :
                                (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                                  (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                        (MonoidalCategory.rightUnitor { as := i }).hom)).functor.obj
          X))
e_4✝ :
  (shiftFunctor C i).obj ((shiftFunctor C i ⋙ shiftFunctor C j).obj X) =
    (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
            (Discrete.eqToIso
              (_ :
                (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                  (MonoidalCategory.tensorUnit (Discrete A)).as))
            (_ :
              MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                  (MonoidalCategory.leftUnitor { as := i }).hom =
                (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                  MonoidalCategory.tensorHom (𝟙 { as := i })
                      (Discrete.eqToIso
                          (_ :
                            (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                              (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                    (MonoidalCategory.rightUnitor { as := i }).hom)).functor.obj
      (((equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
                (Discrete.eqToIso
                  (_ :
                    (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                      (MonoidalCategory.tensorUnit (Discrete A)).as))
                (_ :
                  MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                      (MonoidalCategory.leftUnitor { as := i }).hom =
                    (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                      MonoidalCategory.tensorHom (𝟙 { as := i })
                          (Discrete.eqToIso
                              (_ :
                                (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                                  (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                        (MonoidalCategory.rightUnitor { as := i }).hom)).functor ⋙
            (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
                (Discrete.eqToIso
                  (_ :
                    (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                      (MonoidalCategory.tensorUnit (Discrete A)).as))
                (_ :
                  MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                      (MonoidalCategory.leftUnitor { as := i }).hom =
                    (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                      MonoidalCategory.tensorHom (𝟙 { as := i })
                          (Discrete.eqToIso
                              (_ :
                                (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                                  (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                        (MonoidalCategory.rightUnitor { as := i }).hom)).inverse).obj
        X)
e_5✝¹ :
  (𝟭 C).obj ((shiftFunctor C i).obj X) =
    (𝟭 C).obj
      ((equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
              (Discrete.eqToIso
                (_ :
                  (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                    (MonoidalCategory.tensorUnit (Discrete A)).as))
              (_ :
                MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                    (MonoidalCategory.leftUnitor { as := i }).hom =
                  (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                    MonoidalCategory.tensorHom (𝟙 { as := i })
                        (Discrete.eqToIso
                            (_ :
                              (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                                (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                      (MonoidalCategory.rightUnitor { as := i }).hom)).functor.obj
        X)
e_5✝ :
  shiftFunctor C j ⋙ shiftFunctor C i =
    (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
          (Discrete.eqToIso
            (_ :
              (MonoidalCategory.tensorObj { as := j } { as := i }).as = (MonoidalCategory.tensorUnit (Discrete A)).as))
          (_ :
            MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                (MonoidalCategory.leftUnitor { as := i }).hom =
              (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                MonoidalCategory.tensorHom (𝟙 { as := i })
                    (Discrete.eqToIso
                        (_ :
                          (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                            (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                  (MonoidalCategory.rightUnitor { as := i }).hom)).inverse ⋙
      (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
          (Discrete.eqToIso
            (_ :
              (MonoidalCategory.tensorObj { as := j } { as := i }).as = (MonoidalCategory.tensorUnit (Discrete A)).as))
          (_ :
            MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                (MonoidalCategory.leftUnitor { as := i }).hom =
              (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                MonoidalCategory.tensorHom (𝟙 { as := i })
                    (Discrete.eqToIso
                        (_ :
                          (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                            (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                  (MonoidalCategory.rightUnitor { as := i }).hom)).functor
e_3✝ :
  shiftFunctor C j ⋙ shiftFunctor C i =
    (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
          (Discrete.eqToIso
            (_ :
              (MonoidalCategory.tensorObj { as := j } { as := i }).as = (MonoidalCategory.tensorUnit (Discrete A)).as))
          (_ :
            MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                (MonoidalCategory.leftUnitor { as := i }).hom =
              (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                MonoidalCategory.tensorHom (𝟙 { as := i })
                    (Discrete.eqToIso
                        (_ :
                          (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                            (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                  (MonoidalCategory.rightUnitor { as := i }).hom)).inverse ⋙
      (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
          (Discrete.eqToIso
            (_ :
              (MonoidalCategory.tensorObj { as := j } { as := i }).as = (MonoidalCategory.tensorUnit (Discrete A)).as))
          (_ :
            MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                (MonoidalCategory.leftUnitor { as := i }).hom =
              (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                MonoidalCategory.tensorHom (𝟙 { as := i })
                    (Discrete.eqToIso
                        (_ :
                          (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                            (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                  (MonoidalCategory.rightUnitor { as := i }).hom)).functor
⊢ shiftFunctorCompIsoId C j i (_ : j + i = 0) =
    (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
        (Discrete.eqToIso
          (_ : (MonoidalCategory.tensorObj { as := j } { as := i }).as = (MonoidalCategory.tensorUnit (Discrete A)).as))
        (_ :
          MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
              (MonoidalCategory.leftUnitor { as := i }).hom =
            (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
              MonoidalCategory.tensorHom (𝟙 { as := i })
                  (Discrete.eqToIso
                      (_ :
                        (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                          (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                (MonoidalCategory.rightUnitor { as := i }).hom)).counitIso
[PROOFSTEP]
ext X
[GOAL]
case h.e'_2.h.h.e'_7.h.h.e'_7.h.h.e'_5.h.w.w.h
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 ((𝟭 C).obj X✝) ⟶ (𝟭 C).obj ((shiftFunctor C i).obj X✝)) =
    ((equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
              (Discrete.eqToIso
                (_ :
                  (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                    (MonoidalCategory.tensorUnit (Discrete A)).as))
              (_ :
                MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                    (MonoidalCategory.leftUnitor { as := i }).hom =
                  (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                    MonoidalCategory.tensorHom (𝟙 { as := i })
                        (Discrete.eqToIso
                            (_ :
                              (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                                (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                      (MonoidalCategory.rightUnitor { as := i }).hom)).functor.obj
        ((𝟭 C).obj X✝) ⟶
      (𝟭 C).obj
        ((equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
                (Discrete.eqToIso
                  (_ :
                    (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                      (MonoidalCategory.tensorUnit (Discrete A)).as))
                (_ :
                  MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                      (MonoidalCategory.leftUnitor { as := i }).hom =
                    (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                      MonoidalCategory.tensorHom (𝟙 { as := i })
                          (Discrete.eqToIso
                              (_ :
                                (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                                  (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                        (MonoidalCategory.rightUnitor { as := i }).hom)).functor.obj
          X✝))
e_4✝ :
  (shiftFunctor C i).obj ((shiftFunctor C i ⋙ shiftFunctor C j).obj X✝) =
    (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
            (Discrete.eqToIso
              (_ :
                (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                  (MonoidalCategory.tensorUnit (Discrete A)).as))
            (_ :
              MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                  (MonoidalCategory.leftUnitor { as := i }).hom =
                (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                  MonoidalCategory.tensorHom (𝟙 { as := i })
                      (Discrete.eqToIso
                          (_ :
                            (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                              (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                    (MonoidalCategory.rightUnitor { as := i }).hom)).functor.obj
      (((equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
                (Discrete.eqToIso
                  (_ :
                    (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                      (MonoidalCategory.tensorUnit (Discrete A)).as))
                (_ :
                  MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                      (MonoidalCategory.leftUnitor { as := i }).hom =
                    (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                      MonoidalCategory.tensorHom (𝟙 { as := i })
                          (Discrete.eqToIso
                              (_ :
                                (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                                  (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                        (MonoidalCategory.rightUnitor { as := i }).hom)).functor ⋙
            (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
                (Discrete.eqToIso
                  (_ :
                    (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                      (MonoidalCategory.tensorUnit (Discrete A)).as))
                (_ :
                  MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                      (MonoidalCategory.leftUnitor { as := i }).hom =
                    (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                      MonoidalCategory.tensorHom (𝟙 { as := i })
                          (Discrete.eqToIso
                              (_ :
                                (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                                  (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                        (MonoidalCategory.rightUnitor { as := i }).hom)).inverse).obj
        X✝)
e_5✝¹ :
  (𝟭 C).obj ((shiftFunctor C i).obj X✝) =
    (𝟭 C).obj
      ((equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
              (Discrete.eqToIso
                (_ :
                  (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                    (MonoidalCategory.tensorUnit (Discrete A)).as))
              (_ :
                MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                    (MonoidalCategory.leftUnitor { as := i }).hom =
                  (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                    MonoidalCategory.tensorHom (𝟙 { as := i })
                        (Discrete.eqToIso
                            (_ :
                              (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                                (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                      (MonoidalCategory.rightUnitor { as := i }).hom)).functor.obj
        X✝)
e_5✝ :
  shiftFunctor C j ⋙ shiftFunctor C i =
    (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
          (Discrete.eqToIso
            (_ :
              (MonoidalCategory.tensorObj { as := j } { as := i }).as = (MonoidalCategory.tensorUnit (Discrete A)).as))
          (_ :
            MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                (MonoidalCategory.leftUnitor { as := i }).hom =
              (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                MonoidalCategory.tensorHom (𝟙 { as := i })
                    (Discrete.eqToIso
                        (_ :
                          (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                            (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                  (MonoidalCategory.rightUnitor { as := i }).hom)).inverse ⋙
      (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
          (Discrete.eqToIso
            (_ :
              (MonoidalCategory.tensorObj { as := j } { as := i }).as = (MonoidalCategory.tensorUnit (Discrete A)).as))
          (_ :
            MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                (MonoidalCategory.leftUnitor { as := i }).hom =
              (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                MonoidalCategory.tensorHom (𝟙 { as := i })
                    (Discrete.eqToIso
                        (_ :
                          (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                            (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                  (MonoidalCategory.rightUnitor { as := i }).hom)).functor
e_3✝ :
  shiftFunctor C j ⋙ shiftFunctor C i =
    (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
          (Discrete.eqToIso
            (_ :
              (MonoidalCategory.tensorObj { as := j } { as := i }).as = (MonoidalCategory.tensorUnit (Discrete A)).as))
          (_ :
            MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                (MonoidalCategory.leftUnitor { as := i }).hom =
              (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                MonoidalCategory.tensorHom (𝟙 { as := i })
                    (Discrete.eqToIso
                        (_ :
                          (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                            (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                  (MonoidalCategory.rightUnitor { as := i }).hom)).inverse ⋙
      (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
          (Discrete.eqToIso
            (_ :
              (MonoidalCategory.tensorObj { as := j } { as := i }).as = (MonoidalCategory.tensorUnit (Discrete A)).as))
          (_ :
            MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                (MonoidalCategory.leftUnitor { as := i }).hom =
              (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                MonoidalCategory.tensorHom (𝟙 { as := i })
                    (Discrete.eqToIso
                        (_ :
                          (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                            (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                  (MonoidalCategory.rightUnitor { as := i }).hom)).functor
X : C
⊢ NatTrans.app (shiftFunctorCompIsoId C j i (_ : j + i = 0)).hom X =
    NatTrans.app
      (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
            (Discrete.eqToIso
              (_ :
                (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                  (MonoidalCategory.tensorUnit (Discrete A)).as))
            (_ :
              MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                  (MonoidalCategory.leftUnitor { as := i }).hom =
                (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                  MonoidalCategory.tensorHom (𝟙 { as := i })
                      (Discrete.eqToIso
                          (_ :
                            (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                              (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                    (MonoidalCategory.rightUnitor { as := i }).hom)).counitIso.hom
      X
[PROOFSTEP]
dsimp [shiftFunctorCompIsoId, unitOfTensorIsoUnit, shiftFunctorAdd']
[GOAL]
case h.e'_2.h.h.e'_7.h.h.e'_7.h.h.e'_5.h.w.w.h
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 ((𝟭 C).obj X✝) ⟶ (𝟭 C).obj ((shiftFunctor C i).obj X✝)) =
    ((equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
              (Discrete.eqToIso
                (_ :
                  (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                    (MonoidalCategory.tensorUnit (Discrete A)).as))
              (_ :
                MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                    (MonoidalCategory.leftUnitor { as := i }).hom =
                  (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                    MonoidalCategory.tensorHom (𝟙 { as := i })
                        (Discrete.eqToIso
                            (_ :
                              (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                                (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                      (MonoidalCategory.rightUnitor { as := i }).hom)).functor.obj
        ((𝟭 C).obj X✝) ⟶
      (𝟭 C).obj
        ((equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
                (Discrete.eqToIso
                  (_ :
                    (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                      (MonoidalCategory.tensorUnit (Discrete A)).as))
                (_ :
                  MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                      (MonoidalCategory.leftUnitor { as := i }).hom =
                    (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                      MonoidalCategory.tensorHom (𝟙 { as := i })
                          (Discrete.eqToIso
                              (_ :
                                (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                                  (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                        (MonoidalCategory.rightUnitor { as := i }).hom)).functor.obj
          X✝))
e_4✝ :
  (shiftFunctor C i).obj ((shiftFunctor C i ⋙ shiftFunctor C j).obj X✝) =
    (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
            (Discrete.eqToIso
              (_ :
                (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                  (MonoidalCategory.tensorUnit (Discrete A)).as))
            (_ :
              MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                  (MonoidalCategory.leftUnitor { as := i }).hom =
                (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                  MonoidalCategory.tensorHom (𝟙 { as := i })
                      (Discrete.eqToIso
                          (_ :
                            (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                              (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                    (MonoidalCategory.rightUnitor { as := i }).hom)).functor.obj
      (((equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
                (Discrete.eqToIso
                  (_ :
                    (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                      (MonoidalCategory.tensorUnit (Discrete A)).as))
                (_ :
                  MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                      (MonoidalCategory.leftUnitor { as := i }).hom =
                    (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                      MonoidalCategory.tensorHom (𝟙 { as := i })
                          (Discrete.eqToIso
                              (_ :
                                (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                                  (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                        (MonoidalCategory.rightUnitor { as := i }).hom)).functor ⋙
            (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
                (Discrete.eqToIso
                  (_ :
                    (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                      (MonoidalCategory.tensorUnit (Discrete A)).as))
                (_ :
                  MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                      (MonoidalCategory.leftUnitor { as := i }).hom =
                    (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                      MonoidalCategory.tensorHom (𝟙 { as := i })
                          (Discrete.eqToIso
                              (_ :
                                (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                                  (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                        (MonoidalCategory.rightUnitor { as := i }).hom)).inverse).obj
        X✝)
e_5✝¹ :
  (𝟭 C).obj ((shiftFunctor C i).obj X✝) =
    (𝟭 C).obj
      ((equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
              (Discrete.eqToIso
                (_ :
                  (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                    (MonoidalCategory.tensorUnit (Discrete A)).as))
              (_ :
                MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                    (MonoidalCategory.leftUnitor { as := i }).hom =
                  (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                    MonoidalCategory.tensorHom (𝟙 { as := i })
                        (Discrete.eqToIso
                            (_ :
                              (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                                (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                      (MonoidalCategory.rightUnitor { as := i }).hom)).functor.obj
        X✝)
e_5✝ :
  shiftFunctor C j ⋙ shiftFunctor C i =
    (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
          (Discrete.eqToIso
            (_ :
              (MonoidalCategory.tensorObj { as := j } { as := i }).as = (MonoidalCategory.tensorUnit (Discrete A)).as))
          (_ :
            MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                (MonoidalCategory.leftUnitor { as := i }).hom =
              (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                MonoidalCategory.tensorHom (𝟙 { as := i })
                    (Discrete.eqToIso
                        (_ :
                          (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                            (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                  (MonoidalCategory.rightUnitor { as := i }).hom)).inverse ⋙
      (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
          (Discrete.eqToIso
            (_ :
              (MonoidalCategory.tensorObj { as := j } { as := i }).as = (MonoidalCategory.tensorUnit (Discrete A)).as))
          (_ :
            MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                (MonoidalCategory.leftUnitor { as := i }).hom =
              (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                MonoidalCategory.tensorHom (𝟙 { as := i })
                    (Discrete.eqToIso
                        (_ :
                          (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                            (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                  (MonoidalCategory.rightUnitor { as := i }).hom)).functor
e_3✝ :
  shiftFunctor C j ⋙ shiftFunctor C i =
    (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
          (Discrete.eqToIso
            (_ :
              (MonoidalCategory.tensorObj { as := j } { as := i }).as = (MonoidalCategory.tensorUnit (Discrete A)).as))
          (_ :
            MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                (MonoidalCategory.leftUnitor { as := i }).hom =
              (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                MonoidalCategory.tensorHom (𝟙 { as := i })
                    (Discrete.eqToIso
                        (_ :
                          (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                            (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                  (MonoidalCategory.rightUnitor { as := i }).hom)).inverse ⋙
      (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
          (Discrete.eqToIso
            (_ :
              (MonoidalCategory.tensorObj { as := j } { as := i }).as = (MonoidalCategory.tensorUnit (Discrete A)).as))
          (_ :
            MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                (MonoidalCategory.leftUnitor { as := i }).hom =
              (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                MonoidalCategory.tensorHom (𝟙 { as := i })
                    (Discrete.eqToIso
                        (_ :
                          (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                            (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                  (MonoidalCategory.rightUnitor { as := i }).hom)).functor
X : C
⊢ (NatTrans.app (shiftFunctorAdd C j i).inv X ≫
        NatTrans.app (eqToHom (_ : shiftFunctor C (j + i) = shiftFunctor C 0)) X) ≫
      NatTrans.app (shiftFunctorZero C A).hom X =
    NatTrans.app (LaxMonoidalFunctor.μ (shiftMonoidalFunctor C A).toLaxMonoidalFunctor { as := j } { as := i }) X ≫
      NatTrans.app
          ((shiftMonoidalFunctor C A).toLaxMonoidalFunctor.toFunctor.map
            (eqToHom
              (_ : MonoidalCategory.tensorObj { as := j } { as := i } = MonoidalCategory.tensorUnit (Discrete A))))
          X ≫
        NatTrans.app (MonoidalFunctor.εIso (shiftMonoidalFunctor C A)).inv X
[PROOFSTEP]
simp only [Category.assoc, eqToHom_map]
[GOAL]
case h.e'_2.h.h.e'_7.h.h.e'_7.h.h.e'_5.h.w.w.h
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 ((𝟭 C).obj X✝) ⟶ (𝟭 C).obj ((shiftFunctor C i).obj X✝)) =
    ((equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
              (Discrete.eqToIso
                (_ :
                  (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                    (MonoidalCategory.tensorUnit (Discrete A)).as))
              (_ :
                MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                    (MonoidalCategory.leftUnitor { as := i }).hom =
                  (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                    MonoidalCategory.tensorHom (𝟙 { as := i })
                        (Discrete.eqToIso
                            (_ :
                              (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                                (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                      (MonoidalCategory.rightUnitor { as := i }).hom)).functor.obj
        ((𝟭 C).obj X✝) ⟶
      (𝟭 C).obj
        ((equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
                (Discrete.eqToIso
                  (_ :
                    (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                      (MonoidalCategory.tensorUnit (Discrete A)).as))
                (_ :
                  MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                      (MonoidalCategory.leftUnitor { as := i }).hom =
                    (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                      MonoidalCategory.tensorHom (𝟙 { as := i })
                          (Discrete.eqToIso
                              (_ :
                                (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                                  (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                        (MonoidalCategory.rightUnitor { as := i }).hom)).functor.obj
          X✝))
e_4✝ :
  (shiftFunctor C i).obj ((shiftFunctor C i ⋙ shiftFunctor C j).obj X✝) =
    (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
            (Discrete.eqToIso
              (_ :
                (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                  (MonoidalCategory.tensorUnit (Discrete A)).as))
            (_ :
              MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                  (MonoidalCategory.leftUnitor { as := i }).hom =
                (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                  MonoidalCategory.tensorHom (𝟙 { as := i })
                      (Discrete.eqToIso
                          (_ :
                            (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                              (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                    (MonoidalCategory.rightUnitor { as := i }).hom)).functor.obj
      (((equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
                (Discrete.eqToIso
                  (_ :
                    (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                      (MonoidalCategory.tensorUnit (Discrete A)).as))
                (_ :
                  MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                      (MonoidalCategory.leftUnitor { as := i }).hom =
                    (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                      MonoidalCategory.tensorHom (𝟙 { as := i })
                          (Discrete.eqToIso
                              (_ :
                                (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                                  (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                        (MonoidalCategory.rightUnitor { as := i }).hom)).functor ⋙
            (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
                (Discrete.eqToIso
                  (_ :
                    (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                      (MonoidalCategory.tensorUnit (Discrete A)).as))
                (_ :
                  MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                      (MonoidalCategory.leftUnitor { as := i }).hom =
                    (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                      MonoidalCategory.tensorHom (𝟙 { as := i })
                          (Discrete.eqToIso
                              (_ :
                                (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                                  (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                        (MonoidalCategory.rightUnitor { as := i }).hom)).inverse).obj
        X✝)
e_5✝¹ :
  (𝟭 C).obj ((shiftFunctor C i).obj X✝) =
    (𝟭 C).obj
      ((equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
              (Discrete.eqToIso
                (_ :
                  (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                    (MonoidalCategory.tensorUnit (Discrete A)).as))
              (_ :
                MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                    (MonoidalCategory.leftUnitor { as := i }).hom =
                  (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                    MonoidalCategory.tensorHom (𝟙 { as := i })
                        (Discrete.eqToIso
                            (_ :
                              (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                                (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                      (MonoidalCategory.rightUnitor { as := i }).hom)).functor.obj
        X✝)
e_5✝ :
  shiftFunctor C j ⋙ shiftFunctor C i =
    (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
          (Discrete.eqToIso
            (_ :
              (MonoidalCategory.tensorObj { as := j } { as := i }).as = (MonoidalCategory.tensorUnit (Discrete A)).as))
          (_ :
            MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                (MonoidalCategory.leftUnitor { as := i }).hom =
              (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                MonoidalCategory.tensorHom (𝟙 { as := i })
                    (Discrete.eqToIso
                        (_ :
                          (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                            (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                  (MonoidalCategory.rightUnitor { as := i }).hom)).inverse ⋙
      (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
          (Discrete.eqToIso
            (_ :
              (MonoidalCategory.tensorObj { as := j } { as := i }).as = (MonoidalCategory.tensorUnit (Discrete A)).as))
          (_ :
            MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                (MonoidalCategory.leftUnitor { as := i }).hom =
              (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                MonoidalCategory.tensorHom (𝟙 { as := i })
                    (Discrete.eqToIso
                        (_ :
                          (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                            (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                  (MonoidalCategory.rightUnitor { as := i }).hom)).functor
e_3✝ :
  shiftFunctor C j ⋙ shiftFunctor C i =
    (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
          (Discrete.eqToIso
            (_ :
              (MonoidalCategory.tensorObj { as := j } { as := i }).as = (MonoidalCategory.tensorUnit (Discrete A)).as))
          (_ :
            MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                (MonoidalCategory.leftUnitor { as := i }).hom =
              (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                MonoidalCategory.tensorHom (𝟙 { as := i })
                    (Discrete.eqToIso
                        (_ :
                          (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                            (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                  (MonoidalCategory.rightUnitor { as := i }).hom)).inverse ⋙
      (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
          (Discrete.eqToIso
            (_ :
              (MonoidalCategory.tensorObj { as := j } { as := i }).as = (MonoidalCategory.tensorUnit (Discrete A)).as))
          (_ :
            MonoidalCategory.tensorHom (Discrete.eqToIso h).hom (𝟙 { as := i }) ≫
                (MonoidalCategory.leftUnitor { as := i }).hom =
              (MonoidalCategory.associator { as := i } { as := j } { as := i }).hom ≫
                MonoidalCategory.tensorHom (𝟙 { as := i })
                    (Discrete.eqToIso
                        (_ :
                          (MonoidalCategory.tensorObj { as := j } { as := i }).as =
                            (MonoidalCategory.tensorUnit (Discrete A)).as)).hom ≫
                  (MonoidalCategory.rightUnitor { as := i }).hom)).functor
X : C
⊢ NatTrans.app (shiftFunctorAdd C j i).inv X ≫
      NatTrans.app (eqToHom (_ : shiftFunctor C (j + i) = shiftFunctor C 0)) X ≫
        NatTrans.app (shiftFunctorZero C A).hom X =
    NatTrans.app (LaxMonoidalFunctor.μ (shiftMonoidalFunctor C A).toLaxMonoidalFunctor { as := j } { as := i }) X ≫
      NatTrans.app
          (eqToHom
            (_ :
              (shiftMonoidalFunctor C A).toLaxMonoidalFunctor.toFunctor.obj
                  (MonoidalCategory.tensorObj { as := j } { as := i }) =
                (shiftMonoidalFunctor C A).toLaxMonoidalFunctor.toFunctor.obj
                  (MonoidalCategory.tensorUnit (Discrete A))))
          X ≫
        NatTrans.app (MonoidalFunctor.εIso (shiftMonoidalFunctor C A)).inv X
[PROOFSTEP]
rfl
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X Y : C
f : X ⟶ Y
i : A
⊢ IsEquivalence (shiftFunctor C i)
[PROOFSTEP]
change IsEquivalence (shiftEquiv C i).functor
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X Y : C
f : X ⟶ Y
i : A
⊢ IsEquivalence (shiftEquiv C i).functor
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X✝ Y : C
f : X✝ ⟶ Y
n m : A
h : n + m = 0
X : C
⊢ m + n = 0
[PROOFSTEP]
rw [← neg_eq_of_add_eq_zero_left h, add_right_neg]
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X✝ Y : C
f : X✝ ⟶ Y
n m : A
h : n + m = 0
X : C
⊢ (shiftFunctor C n).map (NatTrans.app (shiftFunctorCompIsoId C n m h).hom X) =
    NatTrans.app (shiftFunctorCompIsoId C m n (_ : m + n = 0)).hom ((shiftFunctor C n).obj X)
[PROOFSTEP]
dsimp [shiftFunctorCompIsoId]
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X✝ Y : C
f : X✝ ⟶ Y
n m : A
h : n + m = 0
X : C
⊢ (shiftFunctor C n).map (NatTrans.app (shiftFunctorAdd' C n m 0 h).inv X ≫ NatTrans.app (shiftFunctorZero C A).hom X) =
    NatTrans.app (shiftFunctorAdd' C m n 0 (_ : m + n = 0)).inv ((shiftFunctor C n).obj X) ≫
      NatTrans.app (shiftFunctorZero C A).hom ((shiftFunctor C n).obj X)
[PROOFSTEP]
simpa only [Functor.map_comp, ← shiftFunctorAdd'_zero_add_inv_app n X, ← shiftFunctorAdd'_add_zero_inv_app n X] using
  shiftFunctorAdd'_assoc_inv_app n m n 0 0 n h (by rw [← neg_eq_of_add_eq_zero_left h, add_right_neg])
    (by rw [h, zero_add]) X
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X✝ Y : C
f : X✝ ⟶ Y
n m : A
h : n + m = 0
X : C
⊢ m + n = 0
[PROOFSTEP]
rw [← neg_eq_of_add_eq_zero_left h, add_right_neg]
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X✝ Y : C
f : X✝ ⟶ Y
n m : A
h : n + m = 0
X : C
⊢ n + m + n = n
[PROOFSTEP]
rw [h, zero_add]
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X✝ Y : C
f : X✝ ⟶ Y
n m : A
h : n + m = 0
X : C
⊢ m + n = 0
[PROOFSTEP]
rw [← neg_eq_of_add_eq_zero_left h, add_right_neg]
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X✝ Y : C
f : X✝ ⟶ Y
n m : A
h : n + m = 0
X : C
⊢ (shiftFunctor C n).map (NatTrans.app (shiftFunctorCompIsoId C n m h).inv X) =
    NatTrans.app (shiftFunctorCompIsoId C m n (_ : m + n = 0)).inv ((shiftFunctor C n).obj X)
[PROOFSTEP]
rw [← cancel_mono (((shiftFunctorCompIsoId C n m h).hom.app X)⟦n⟧'), ← Functor.map_comp, Iso.inv_hom_id_app,
  Functor.map_id, shift_shiftFunctorCompIsoId_hom_app, Iso.inv_hom_id_app]
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X✝ Y : C
f : X✝ ⟶ Y
n m : A
h : n + m = 0
X : C
⊢ 𝟙 ((shiftFunctor C n).obj ((𝟭 C).obj X)) = 𝟙 ((𝟭 C).obj ((shiftFunctor C n).obj X))
[PROOFSTEP]
rfl
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X✝ Y : C
f : X✝ ⟶ Y
n : A
X : C
⊢ (shiftFunctor C n).map (NatTrans.app (shiftFunctorCompIsoId C n (-n) (_ : n + -n = 0)).hom X) =
    NatTrans.app (shiftFunctorCompIsoId C (-n) n (_ : -n + n = 0)).hom ((shiftFunctor C n).obj X)
[PROOFSTEP]
apply shift_shiftFunctorCompIsoId_hom_app
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X✝ Y : C
f : X✝ ⟶ Y
n : A
X : C
⊢ (shiftFunctor C n).map (NatTrans.app (shiftFunctorCompIsoId C n (-n) (_ : n + -n = 0)).inv X) =
    NatTrans.app (shiftFunctorCompIsoId C (-n) n (_ : -n + n = 0)).inv ((shiftFunctor C n).obj X)
[PROOFSTEP]
apply shift_shiftFunctorCompIsoId_inv_app
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X✝ Y : C
f : X✝ ⟶ Y
n : A
X : C
⊢ (shiftFunctor C (-n)).map (NatTrans.app (shiftFunctorCompIsoId C (-n) n (_ : -n + n = 0)).hom X) =
    NatTrans.app (shiftFunctorCompIsoId C n (-n) (_ : n + -n = 0)).hom ((shiftFunctor C (-n)).obj X)
[PROOFSTEP]
apply shift_shiftFunctorCompIsoId_hom_app
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X✝ Y : C
f : X✝ ⟶ Y
n : A
X : C
⊢ (shiftFunctor C (-n)).map (NatTrans.app (shiftFunctorCompIsoId C (-n) n (_ : -n + n = 0)).inv X) =
    NatTrans.app (shiftFunctorCompIsoId C n (-n) (_ : n + -n = 0)).inv ((shiftFunctor C (-n)).obj X)
[PROOFSTEP]
apply shift_shiftFunctorCompIsoId_inv_app
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
i j k : A
h : i + j = k
⊢ j + i = k
[PROOFSTEP]
rw [add_comm j i, h]
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
i j k : A
h : i + j = k
⊢ shiftFunctorComm C i j = (shiftFunctorAdd' C i j k h).symm ≪≫ shiftFunctorAdd' C j i k (_ : j + i = k)
[PROOFSTEP]
subst h
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
i j : A
⊢ shiftFunctorComm C i j =
    (shiftFunctorAdd' C i j (i + j) (_ : i + j = i + j)).symm ≪≫ shiftFunctorAdd' C j i (i + j) (_ : j + i = i + j)
[PROOFSTEP]
rw [shiftFunctorAdd'_eq_shiftFunctorAdd]
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
i j : A
⊢ shiftFunctorComm C i j = (shiftFunctorAdd C i j).symm ≪≫ shiftFunctorAdd' C j i (i + j) (_ : j + i = i + j)
[PROOFSTEP]
rfl
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
i j : A
⊢ (shiftFunctorComm C i j).symm = shiftFunctorComm C j i
[PROOFSTEP]
ext1
[GOAL]
case w
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
i j : A
⊢ (shiftFunctorComm C i j).symm.hom = (shiftFunctorComm C j i).hom
[PROOFSTEP]
dsimp
[GOAL]
case w
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
i j : A
⊢ (shiftFunctorComm C i j).inv = (shiftFunctorComm C j i).hom
[PROOFSTEP]
rw [shiftFunctorComm_eq C i j (i + j) rfl, shiftFunctorComm_eq C j i (i + j) (add_comm j i)]
[GOAL]
case w
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
i j : A
⊢ ((shiftFunctorAdd' C i j (i + j) (_ : i + j = i + j)).symm ≪≫
        shiftFunctorAdd' C j i (i + j) (_ : j + i = i + j)).inv =
    ((shiftFunctorAdd' C j i (i + j) (_ : j + i = i + j)).symm ≪≫
        shiftFunctorAdd' C i j (i + j) (_ : i + j = i + j)).hom
[PROOFSTEP]
rfl
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
X Y : C
f : X ⟶ Y
i j : A
⊢ (shiftComm X i j).symm = shiftComm X j i
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
X Y : C
f : X ⟶ Y
i j : A
⊢ (shiftComm X i j).symm.hom = (shiftComm X j i).hom
[PROOFSTEP]
exact NatTrans.congr_app (congr_arg Iso.hom (shiftFunctorComm_symm C i j)) X
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
X Y : C
f : X ⟶ Y
i j : A
⊢ (shiftFunctor C j).map ((shiftFunctor C i).map f) =
    (shiftComm X i j).hom ≫ (shiftFunctor C i).map ((shiftFunctor C j).map f) ≫ (shiftComm Y j i).hom
[PROOFSTEP]
erw [← shiftComm_symm Y i j, ← ((shiftFunctorComm C i j).hom.naturality_assoc f)]
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
X Y : C
f : X ⟶ Y
i j : A
⊢ (shiftFunctor C j).map ((shiftFunctor C i).map f) =
    (shiftFunctor C i ⋙ shiftFunctor C j).map f ≫
      NatTrans.app (shiftFunctorComm C i j).hom Y ≫ (shiftComm Y i j).symm.hom
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
X Y : C
f : X ⟶ Y
i j : A
⊢ (shiftFunctor C j).map ((shiftFunctor C i).map f) =
    (shiftFunctor C j).map ((shiftFunctor C i).map f) ≫
      NatTrans.app (shiftFunctorComm C i j).hom Y ≫ NatTrans.app (shiftFunctorComm C i j).inv Y
[PROOFSTEP]
simp only [Iso.hom_inv_id_app, Functor.comp_obj, Category.comp_id]
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
X Y : C
f : X ⟶ Y
i j : A
⊢ (shiftComm X i j).hom ≫ (shiftFunctor C i).map ((shiftFunctor C j).map f) =
    (shiftFunctor C j).map ((shiftFunctor C i).map f) ≫ (shiftComm Y i j).hom
[PROOFSTEP]
rw [shiftComm', ← shiftComm_symm, Iso.symm_hom, Iso.inv_hom_id_assoc]
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
X Y : C
f : X ⟶ Y
n : A
⊢ NatTrans.app (shiftFunctorZero C A).hom ((shiftFunctor C n).obj X) =
    NatTrans.app (shiftFunctorComm C n 0).hom X ≫ (shiftFunctor C n).map (NatTrans.app (shiftFunctorZero C A).hom X)
[PROOFSTEP]
rw [← shiftFunctorAdd'_zero_add_inv_app n X, shiftFunctorComm_eq C n 0 n (add_zero n)]
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
X Y : C
f : X ⟶ Y
n : A
⊢ NatTrans.app (shiftFunctorZero C A).hom ((shiftFunctor C n).obj X) =
    NatTrans.app ((shiftFunctorAdd' C n 0 n (_ : n + 0 = n)).symm ≪≫ shiftFunctorAdd' C 0 n n (_ : 0 + n = n)).hom X ≫
      NatTrans.app (shiftFunctorAdd' C 0 n n (_ : 0 + n = n)).inv X
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
X Y : C
f : X ⟶ Y
n : A
⊢ NatTrans.app (shiftFunctorZero C A).hom ((shiftFunctor C n).obj X) =
    (NatTrans.app (shiftFunctorAdd' C n 0 n (_ : n + 0 = n)).inv X ≫
        NatTrans.app (shiftFunctorAdd' C 0 n n (_ : 0 + n = n)).hom X) ≫
      NatTrans.app (shiftFunctorAdd' C 0 n n (_ : 0 + n = n)).inv X
[PROOFSTEP]
rw [Category.assoc, Iso.hom_inv_id_app, Category.comp_id, shiftFunctorAdd'_add_zero_inv_app]
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
X Y : C
f : X ⟶ Y
n : A
⊢ NatTrans.app (shiftFunctorZero C A).inv ((shiftFunctor C n).obj X) =
    (shiftFunctor C n).map (NatTrans.app (shiftFunctorZero C A).inv X) ≫ NatTrans.app (shiftFunctorComm C n 0).inv X
[PROOFSTEP]
rw [← cancel_mono ((shiftFunctorZero C A).hom.app (X⟦n⟧)), Category.assoc, Iso.inv_hom_id_app,
  shiftFunctorZero_hom_app_shift, Iso.inv_hom_id_app_assoc, ← Functor.map_comp, Iso.inv_hom_id_app]
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
X Y : C
f : X ⟶ Y
n : A
⊢ 𝟙 ((𝟭 C).obj ((shiftFunctor C n).obj X)) = (shiftFunctor C n).map (𝟙 ((𝟭 C).obj X))
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
X Y : C
f : X ⟶ Y
n : A
⊢ 𝟙 ((shiftFunctor C n).obj X) = (shiftFunctor C n).map (𝟙 X)
[PROOFSTEP]
rw [Functor.map_id]
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
X✝ Y : C
f : X✝ ⟶ Y
m₁ m₂ m₃ : A
X : C
⊢ NatTrans.app (shiftFunctorComm C m₁ (m₂ + m₃)).hom X ≫
      (shiftFunctor C m₁).map (NatTrans.app (shiftFunctorAdd C m₂ m₃).hom X) =
    NatTrans.app (shiftFunctorAdd C m₂ m₃).hom ((shiftFunctor C m₁).obj X) ≫
      (shiftFunctor C m₃).map (NatTrans.app (shiftFunctorComm C m₁ m₂).hom X) ≫
        NatTrans.app (shiftFunctorComm C m₁ m₃).hom ((shiftFunctor C m₂).obj X)
[PROOFSTEP]
rw [← cancel_mono ((shiftFunctorComm C m₁ m₃).inv.app (X⟦m₂⟧)), ←
  cancel_mono (((shiftFunctorComm C m₁ m₂).inv.app X)⟦m₃⟧')]
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
X✝ Y : C
f : X✝ ⟶ Y
m₁ m₂ m₃ : A
X : C
⊢ ((NatTrans.app (shiftFunctorComm C m₁ (m₂ + m₃)).hom X ≫
          (shiftFunctor C m₁).map (NatTrans.app (shiftFunctorAdd C m₂ m₃).hom X)) ≫
        NatTrans.app (shiftFunctorComm C m₁ m₃).inv ((shiftFunctor C m₂).obj X)) ≫
      (shiftFunctor C m₃).map (NatTrans.app (shiftFunctorComm C m₁ m₂).inv X) =
    ((NatTrans.app (shiftFunctorAdd C m₂ m₃).hom ((shiftFunctor C m₁).obj X) ≫
          (shiftFunctor C m₃).map (NatTrans.app (shiftFunctorComm C m₁ m₂).hom X) ≫
            NatTrans.app (shiftFunctorComm C m₁ m₃).hom ((shiftFunctor C m₂).obj X)) ≫
        NatTrans.app (shiftFunctorComm C m₁ m₃).inv ((shiftFunctor C m₂).obj X)) ≫
      (shiftFunctor C m₃).map (NatTrans.app (shiftFunctorComm C m₁ m₂).inv X)
[PROOFSTEP]
simp only [Category.assoc, Iso.hom_inv_id_app]
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
X✝ Y : C
f : X✝ ⟶ Y
m₁ m₂ m₃ : A
X : C
⊢ NatTrans.app (shiftFunctorComm C m₁ (m₂ + m₃)).hom X ≫
      (shiftFunctor C m₁).map (NatTrans.app (shiftFunctorAdd C m₂ m₃).hom X) ≫
        NatTrans.app (shiftFunctorComm C m₁ m₃).inv ((shiftFunctor C m₂).obj X) ≫
          (shiftFunctor C m₃).map (NatTrans.app (shiftFunctorComm C m₁ m₂).inv X) =
    NatTrans.app (shiftFunctorAdd C m₂ m₃).hom ((shiftFunctor C m₁).obj X) ≫
      (shiftFunctor C m₃).map (NatTrans.app (shiftFunctorComm C m₁ m₂).hom X) ≫
        𝟙 ((shiftFunctor C m₁ ⋙ shiftFunctor C m₃).obj ((shiftFunctor C m₂).obj X)) ≫
          (shiftFunctor C m₃).map (NatTrans.app (shiftFunctorComm C m₁ m₂).inv X)
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
X✝ Y : C
f : X✝ ⟶ Y
m₁ m₂ m₃ : A
X : C
⊢ NatTrans.app (shiftFunctorComm C m₁ (m₂ + m₃)).hom X ≫
      (shiftFunctor C m₁).map (NatTrans.app (shiftFunctorAdd C m₂ m₃).hom X) ≫
        NatTrans.app (shiftFunctorComm C m₁ m₃).inv ((shiftFunctor C m₂).obj X) ≫
          (shiftFunctor C m₃).map (NatTrans.app (shiftFunctorComm C m₁ m₂).inv X) =
    NatTrans.app (shiftFunctorAdd C m₂ m₃).hom ((shiftFunctor C m₁).obj X) ≫
      (shiftFunctor C m₃).map (NatTrans.app (shiftFunctorComm C m₁ m₂).hom X) ≫
        𝟙 ((shiftFunctor C m₃).obj ((shiftFunctor C m₁).obj ((shiftFunctor C m₂).obj X))) ≫
          (shiftFunctor C m₃).map (NatTrans.app (shiftFunctorComm C m₁ m₂).inv X)
[PROOFSTEP]
simp only [Category.id_comp, ← Functor.map_comp, Iso.hom_inv_id_app]
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
X✝ Y : C
f : X✝ ⟶ Y
m₁ m₂ m₃ : A
X : C
⊢ NatTrans.app (shiftFunctorComm C m₁ (m₂ + m₃)).hom X ≫
      (shiftFunctor C m₁).map (NatTrans.app (shiftFunctorAdd C m₂ m₃).hom X) ≫
        NatTrans.app (shiftFunctorComm C m₁ m₃).inv ((shiftFunctor C m₂).obj X) ≫
          (shiftFunctor C m₃).map (NatTrans.app (shiftFunctorComm C m₁ m₂).inv X) =
    NatTrans.app (shiftFunctorAdd C m₂ m₃).hom ((shiftFunctor C m₁).obj X) ≫
      (shiftFunctor C m₃).map (𝟙 ((shiftFunctor C m₁ ⋙ shiftFunctor C m₂).obj X))
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
X✝ Y : C
f : X✝ ⟶ Y
m₁ m₂ m₃ : A
X : C
⊢ NatTrans.app (shiftFunctorComm C m₁ (m₂ + m₃)).hom X ≫
      (shiftFunctor C m₁).map (NatTrans.app (shiftFunctorAdd C m₂ m₃).hom X) ≫
        NatTrans.app (shiftFunctorComm C m₁ m₃).inv ((shiftFunctor C m₂).obj X) ≫
          (shiftFunctor C m₃).map (NatTrans.app (shiftFunctorComm C m₁ m₂).inv X) =
    NatTrans.app (shiftFunctorAdd C m₂ m₃).hom ((shiftFunctor C m₁).obj X) ≫
      (shiftFunctor C m₃).map (𝟙 ((shiftFunctor C m₂).obj ((shiftFunctor C m₁).obj X)))
[PROOFSTEP]
simp only [Functor.map_id, Category.comp_id, shiftFunctorComm_eq C _ _ _ rfl, ← shiftFunctorAdd'_eq_shiftFunctorAdd]
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
X✝ Y : C
f : X✝ ⟶ Y
m₁ m₂ m₃ : A
X : C
⊢ NatTrans.app
        ((shiftFunctorAdd' C m₁ (m₂ + m₃) (m₁ + (m₂ + m₃)) (_ : m₁ + (m₂ + m₃) = m₁ + (m₂ + m₃))).symm ≪≫
            shiftFunctorAdd' C (m₂ + m₃) m₁ (m₁ + (m₂ + m₃)) (_ : m₂ + m₃ + m₁ = m₁ + (m₂ + m₃))).hom
        X ≫
      (shiftFunctor C m₁).map (NatTrans.app (shiftFunctorAdd' C m₂ m₃ (m₂ + m₃) (_ : m₂ + m₃ = m₂ + m₃)).hom X) ≫
        NatTrans.app
            ((shiftFunctorAdd' C m₁ m₃ (m₁ + m₃) (_ : m₁ + m₃ = m₁ + m₃)).symm ≪≫
                shiftFunctorAdd' C m₃ m₁ (m₁ + m₃) (_ : m₃ + m₁ = m₁ + m₃)).inv
            ((shiftFunctor C m₂).obj X) ≫
          (shiftFunctor C m₃).map
            (NatTrans.app
              ((shiftFunctorAdd' C m₁ m₂ (m₁ + m₂) (_ : m₁ + m₂ = m₁ + m₂)).symm ≪≫
                  shiftFunctorAdd' C m₂ m₁ (m₁ + m₂) (_ : m₂ + m₁ = m₁ + m₂)).inv
              X) =
    NatTrans.app (shiftFunctorAdd' C m₂ m₃ (m₂ + m₃) (_ : m₂ + m₃ = m₂ + m₃)).hom ((shiftFunctor C m₁).obj X)
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
X✝ Y : C
f : X✝ ⟶ Y
m₁ m₂ m₃ : A
X : C
⊢ (NatTrans.app (shiftFunctorAdd' C m₁ (m₂ + m₃) (m₁ + (m₂ + m₃)) (_ : m₁ + (m₂ + m₃) = m₁ + (m₂ + m₃))).inv X ≫
        NatTrans.app (shiftFunctorAdd' C (m₂ + m₃) m₁ (m₁ + (m₂ + m₃)) (_ : m₂ + m₃ + m₁ = m₁ + (m₂ + m₃))).hom X) ≫
      (shiftFunctor C m₁).map (NatTrans.app (shiftFunctorAdd' C m₂ m₃ (m₂ + m₃) (_ : m₂ + m₃ = m₂ + m₃)).hom X) ≫
        (NatTrans.app (shiftFunctorAdd' C m₃ m₁ (m₁ + m₃) (_ : m₃ + m₁ = m₁ + m₃)).inv ((shiftFunctor C m₂).obj X) ≫
            NatTrans.app (shiftFunctorAdd' C m₁ m₃ (m₁ + m₃) (_ : m₁ + m₃ = m₁ + m₃)).hom ((shiftFunctor C m₂).obj X)) ≫
          (shiftFunctor C m₃).map
            (NatTrans.app (shiftFunctorAdd' C m₂ m₁ (m₁ + m₂) (_ : m₂ + m₁ = m₁ + m₂)).inv X ≫
              NatTrans.app (shiftFunctorAdd' C m₁ m₂ (m₁ + m₂) (_ : m₁ + m₂ = m₁ + m₂)).hom X) =
    NatTrans.app (shiftFunctorAdd' C m₂ m₃ (m₂ + m₃) (_ : m₂ + m₃ = m₂ + m₃)).hom ((shiftFunctor C m₁).obj X)
[PROOFSTEP]
simp only [Category.assoc, Iso.hom_inv_id_app_assoc, Iso.inv_hom_id_app_assoc, ← Functor.map_comp,
  shiftFunctorAdd'_assoc_hom_app_assoc m₂ m₃ m₁ (m₂ + m₃) (m₁ + m₃) (m₁ + (m₂ + m₃)) rfl (add_comm m₃ m₁)
    (add_comm _ m₁) X,
  ←
  shiftFunctorAdd'_assoc_hom_app_assoc m₂ m₁ m₃ (m₁ + m₂) (m₁ + m₃) (m₁ + (m₂ + m₃)) (add_comm _ _) rfl
    (by rw [add_comm m₂ m₁, add_assoc]) X,
  shiftFunctorAdd'_assoc_hom_app m₁ m₂ m₃ (m₁ + m₂) (m₂ + m₃) (m₁ + (m₂ + m₃)) rfl rfl (add_assoc _ _ _) X]
[GOAL]
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
X✝ Y : C
f : X✝ ⟶ Y
m₁ m₂ m₃ : A
X : C
⊢ m₂ + m₁ + m₃ = m₁ + (m₂ + m₃)
[PROOFSTEP]
rw [add_comm m₂ m₁, add_assoc]
[GOAL]
C : Type u
A : Type u_1
inst✝⁵ : Category.{v, u} C
D : Type u_2
inst✝⁴ : Category.{u_3, u_2} D
inst✝³ : AddMonoid A
inst✝² : HasShift D A
F : C ⥤ D
inst✝¹ : Full F
inst✝ : Faithful F
s : A → C ⥤ C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
X : C
⊢ F.map (NatTrans.app (hasShiftOfFullyFaithful_zero F s i).hom X) =
    NatTrans.app (i 0).hom X ≫ NatTrans.app (shiftFunctorZero D A).hom (F.obj X)
[PROOFSTEP]
simp [hasShiftOfFullyFaithful_zero]
[GOAL]
C : Type u
A : Type u_1
inst✝⁵ : Category.{v, u} C
D : Type u_2
inst✝⁴ : Category.{u_3, u_2} D
inst✝³ : AddMonoid A
inst✝² : HasShift D A
F : C ⥤ D
inst✝¹ : Full F
inst✝ : Faithful F
s : A → C ⥤ C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
X : C
⊢ F.map (NatTrans.app (hasShiftOfFullyFaithful_zero F s i).inv X) =
    NatTrans.app (shiftFunctorZero D A).inv (F.obj X) ≫ NatTrans.app (i 0).inv X
[PROOFSTEP]
simp [hasShiftOfFullyFaithful_zero]
[GOAL]
C : Type u
A : Type u_1
inst✝⁵ : Category.{v, u} C
D : Type u_2
inst✝⁴ : Category.{u_3, u_2} D
inst✝³ : AddMonoid A
inst✝² : HasShift D A
F : C ⥤ D
inst✝¹ : Full F
inst✝ : Faithful F
s : A → C ⥤ C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
a b : A
X : C
⊢ F.map (NatTrans.app (hasShiftOfFullyFaithful_add F s i a b).hom X) =
    NatTrans.app (i (a + b)).hom X ≫
      NatTrans.app (shiftFunctorAdd D a b).hom (F.obj X) ≫
        (shiftFunctor D b).map (NatTrans.app (i a).inv X) ≫ NatTrans.app (i b).inv ((s a).obj X)
[PROOFSTEP]
dsimp [hasShiftOfFullyFaithful_add]
[GOAL]
C : Type u
A : Type u_1
inst✝⁵ : Category.{v, u} C
D : Type u_2
inst✝⁴ : Category.{u_3, u_2} D
inst✝³ : AddMonoid A
inst✝² : HasShift D A
F : C ⥤ D
inst✝¹ : Full F
inst✝ : Faithful F
s : A → C ⥤ C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
a b : A
X : C
⊢ F.map
      (F.preimage
        (NatTrans.app (i (a + b)).hom X ≫
          NatTrans.app (shiftFunctorAdd D a b).hom (F.obj X) ≫
            𝟙 ((shiftFunctor D b).obj ((shiftFunctor D a).obj (F.obj X))) ≫
              (shiftFunctor D b).map (NatTrans.app (i a).inv X) ≫
                𝟙 ((shiftFunctor D b).obj (F.obj ((s a).obj X))) ≫
                  NatTrans.app (i b).inv ((s a).obj X) ≫ 𝟙 (F.obj ((s b).obj ((s a).obj X))))) =
    NatTrans.app (i (a + b)).hom X ≫
      NatTrans.app (shiftFunctorAdd D a b).hom (F.obj X) ≫
        (shiftFunctor D b).map (NatTrans.app (i a).inv X) ≫ NatTrans.app (i b).inv ((s a).obj X)
[PROOFSTEP]
simp
[GOAL]
C : Type u
A : Type u_1
inst✝⁵ : Category.{v, u} C
D : Type u_2
inst✝⁴ : Category.{u_3, u_2} D
inst✝³ : AddMonoid A
inst✝² : HasShift D A
F : C ⥤ D
inst✝¹ : Full F
inst✝ : Faithful F
s : A → C ⥤ C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
a b : A
X : C
⊢ F.map (NatTrans.app (hasShiftOfFullyFaithful_add F s i a b).inv X) =
    NatTrans.app (i b).hom ((s a).obj X) ≫
      (shiftFunctor D b).map (NatTrans.app (i a).hom X) ≫
        NatTrans.app (shiftFunctorAdd D a b).inv (F.obj X) ≫ NatTrans.app (i (a + b)).inv X
[PROOFSTEP]
dsimp [hasShiftOfFullyFaithful_add]
[GOAL]
C : Type u
A : Type u_1
inst✝⁵ : Category.{v, u} C
D : Type u_2
inst✝⁴ : Category.{u_3, u_2} D
inst✝³ : AddMonoid A
inst✝² : HasShift D A
F : C ⥤ D
inst✝¹ : Full F
inst✝ : Faithful F
s : A → C ⥤ C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
a b : A
X : C
⊢ F.map
      (F.preimage
        ((((((𝟙 (F.obj ((s b).obj ((s a).obj X))) ≫ NatTrans.app (i b).hom ((s a).obj X)) ≫
                  𝟙 ((shiftFunctor D b).obj (F.obj ((s a).obj X)))) ≫
                (shiftFunctor D b).map (NatTrans.app (i a).hom X)) ≫
              𝟙 ((shiftFunctor D b).obj ((shiftFunctor D a).obj (F.obj X)))) ≫
            NatTrans.app (shiftFunctorAdd D a b).inv (F.obj X)) ≫
          NatTrans.app (i (a + b)).inv X)) =
    NatTrans.app (i b).hom ((s a).obj X) ≫
      (shiftFunctor D b).map (NatTrans.app (i a).hom X) ≫
        NatTrans.app (shiftFunctorAdd D a b).inv (F.obj X) ≫ NatTrans.app (i (a + b)).inv X
[PROOFSTEP]
simp
[GOAL]
C : Type u
A : Type u_1
inst✝⁵ : Category.{v, u} C
D : Type u_2
inst✝⁴ : Category.{?u.291249, u_2} D
inst✝³ : AddMonoid A
inst✝² : HasShift D A
F : C ⥤ D
inst✝¹ : Full F
inst✝ : Faithful F
s : A → C ⥤ C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
m₁ m₂ m₃ : A
X : C
⊢ F.map
      (NatTrans.app (hasShiftOfFullyFaithful_add F s i (m₁ + m₂) m₃).hom X ≫
        (s m₃).map (NatTrans.app (hasShiftOfFullyFaithful_add F s i m₁ m₂).hom X)) =
    F.map
      (eqToHom (_ : (s (m₁ + m₂ + m₃)).obj X = (s (m₁ + (m₂ + m₃))).obj X) ≫
        NatTrans.app (hasShiftOfFullyFaithful_add F s i m₁ (m₂ + m₃)).hom X ≫
          NatTrans.app (hasShiftOfFullyFaithful_add F s i m₂ m₃).hom ((s m₁).obj X))
[PROOFSTEP]
have h := shiftFunctorAdd'_assoc_hom_app m₁ m₂ m₃ _ _ (m₁ + m₂ + m₃) rfl rfl rfl (F.obj X)
[GOAL]
C : Type u
A : Type u_1
inst✝⁵ : Category.{v, u} C
D : Type u_2
inst✝⁴ : Category.{?u.291249, u_2} D
inst✝³ : AddMonoid A
inst✝² : HasShift D A
F : C ⥤ D
inst✝¹ : Full F
inst✝ : Faithful F
s : A → C ⥤ C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
m₁ m₂ m₃ : A
X : C
h :
  NatTrans.app (shiftFunctorAdd' D (m₁ + m₂) m₃ (m₁ + m₂ + m₃) (_ : m₁ + m₂ + m₃ = m₁ + m₂ + m₃)).hom (F.obj X) ≫
      (shiftFunctor D m₃).map
        (NatTrans.app (shiftFunctorAdd' D m₁ m₂ (m₁ + m₂) (_ : m₁ + m₂ = m₁ + m₂)).hom (F.obj X)) =
    NatTrans.app (shiftFunctorAdd' D m₁ (m₂ + m₃) (m₁ + m₂ + m₃) (_ : m₁ + (m₂ + m₃) = m₁ + m₂ + m₃)).hom (F.obj X) ≫
      NatTrans.app (shiftFunctorAdd' D m₂ m₃ (m₂ + m₃) (_ : m₂ + m₃ = m₂ + m₃)).hom ((shiftFunctor D m₁).obj (F.obj X))
⊢ F.map
      (NatTrans.app (hasShiftOfFullyFaithful_add F s i (m₁ + m₂) m₃).hom X ≫
        (s m₃).map (NatTrans.app (hasShiftOfFullyFaithful_add F s i m₁ m₂).hom X)) =
    F.map
      (eqToHom (_ : (s (m₁ + m₂ + m₃)).obj X = (s (m₁ + (m₂ + m₃))).obj X) ≫
        NatTrans.app (hasShiftOfFullyFaithful_add F s i m₁ (m₂ + m₃)).hom X ≫
          NatTrans.app (hasShiftOfFullyFaithful_add F s i m₂ m₃).hom ((s m₁).obj X))
[PROOFSTEP]
simp only [shiftFunctorAdd'_eq_shiftFunctorAdd] at h 
[GOAL]
C : Type u
A : Type u_1
inst✝⁵ : Category.{v, u} C
D : Type u_2
inst✝⁴ : Category.{?u.291249, u_2} D
inst✝³ : AddMonoid A
inst✝² : HasShift D A
F : C ⥤ D
inst✝¹ : Full F
inst✝ : Faithful F
s : A → C ⥤ C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
m₁ m₂ m₃ : A
X : C
h :
  NatTrans.app (shiftFunctorAdd D (m₁ + m₂) m₃).hom (F.obj X) ≫
      (shiftFunctor D m₃).map (NatTrans.app (shiftFunctorAdd D m₁ m₂).hom (F.obj X)) =
    NatTrans.app (shiftFunctorAdd' D m₁ (m₂ + m₃) (m₁ + m₂ + m₃) (_ : m₁ + (m₂ + m₃) = m₁ + m₂ + m₃)).hom (F.obj X) ≫
      NatTrans.app (shiftFunctorAdd D m₂ m₃).hom ((shiftFunctor D m₁).obj (F.obj X))
⊢ F.map
      (NatTrans.app (hasShiftOfFullyFaithful_add F s i (m₁ + m₂) m₃).hom X ≫
        (s m₃).map (NatTrans.app (hasShiftOfFullyFaithful_add F s i m₁ m₂).hom X)) =
    F.map
      (eqToHom (_ : (s (m₁ + m₂ + m₃)).obj X = (s (m₁ + (m₂ + m₃))).obj X) ≫
        NatTrans.app (hasShiftOfFullyFaithful_add F s i m₁ (m₂ + m₃)).hom X ≫
          NatTrans.app (hasShiftOfFullyFaithful_add F s i m₂ m₃).hom ((s m₁).obj X))
[PROOFSTEP]
rw [← cancel_mono ((i m₃).hom.app ((s m₂).obj ((s m₁).obj X)))]
[GOAL]
C : Type u
A : Type u_1
inst✝⁵ : Category.{v, u} C
D : Type u_2
inst✝⁴ : Category.{?u.291249, u_2} D
inst✝³ : AddMonoid A
inst✝² : HasShift D A
F : C ⥤ D
inst✝¹ : Full F
inst✝ : Faithful F
s : A → C ⥤ C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
m₁ m₂ m₃ : A
X : C
h :
  NatTrans.app (shiftFunctorAdd D (m₁ + m₂) m₃).hom (F.obj X) ≫
      (shiftFunctor D m₃).map (NatTrans.app (shiftFunctorAdd D m₁ m₂).hom (F.obj X)) =
    NatTrans.app (shiftFunctorAdd' D m₁ (m₂ + m₃) (m₁ + m₂ + m₃) (_ : m₁ + (m₂ + m₃) = m₁ + m₂ + m₃)).hom (F.obj X) ≫
      NatTrans.app (shiftFunctorAdd D m₂ m₃).hom ((shiftFunctor D m₁).obj (F.obj X))
⊢ F.map
        (NatTrans.app (hasShiftOfFullyFaithful_add F s i (m₁ + m₂) m₃).hom X ≫
          (s m₃).map (NatTrans.app (hasShiftOfFullyFaithful_add F s i m₁ m₂).hom X)) ≫
      NatTrans.app (i m₃).hom ((s m₂).obj ((s m₁).obj X)) =
    F.map
        (eqToHom (_ : (s (m₁ + m₂ + m₃)).obj X = (s (m₁ + (m₂ + m₃))).obj X) ≫
          NatTrans.app (hasShiftOfFullyFaithful_add F s i m₁ (m₂ + m₃)).hom X ≫
            NatTrans.app (hasShiftOfFullyFaithful_add F s i m₂ m₃).hom ((s m₁).obj X)) ≫
      NatTrans.app (i m₃).hom ((s m₂).obj ((s m₁).obj X))
[PROOFSTEP]
simp only [Functor.comp_obj, Functor.map_comp, map_hasShiftOfFullyFaithful_add_hom_app, Category.assoc,
  Iso.inv_hom_id_app_assoc, NatTrans.naturality_assoc, Functor.comp_map, Iso.inv_hom_id_app, Category.comp_id]
[GOAL]
C : Type u
A : Type u_1
inst✝⁵ : Category.{v, u} C
D : Type u_2
inst✝⁴ : Category.{?u.291249, u_2} D
inst✝³ : AddMonoid A
inst✝² : HasShift D A
F : C ⥤ D
inst✝¹ : Full F
inst✝ : Faithful F
s : A → C ⥤ C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
m₁ m₂ m₃ : A
X : C
h :
  NatTrans.app (shiftFunctorAdd D (m₁ + m₂) m₃).hom (F.obj X) ≫
      (shiftFunctor D m₃).map (NatTrans.app (shiftFunctorAdd D m₁ m₂).hom (F.obj X)) =
    NatTrans.app (shiftFunctorAdd' D m₁ (m₂ + m₃) (m₁ + m₂ + m₃) (_ : m₁ + (m₂ + m₃) = m₁ + m₂ + m₃)).hom (F.obj X) ≫
      NatTrans.app (shiftFunctorAdd D m₂ m₃).hom ((shiftFunctor D m₁).obj (F.obj X))
⊢ NatTrans.app (i (m₁ + m₂ + m₃)).hom X ≫
      NatTrans.app (shiftFunctorAdd D (m₁ + m₂) m₃).hom (F.obj X) ≫
        (shiftFunctor D m₃).map (NatTrans.app (i (m₁ + m₂)).inv X) ≫
          NatTrans.app (i m₃).inv ((s (m₁ + m₂)).obj X) ≫
            F.map ((s m₃).map (NatTrans.app (hasShiftOfFullyFaithful_add F s i m₁ m₂).hom X)) ≫
              NatTrans.app (i m₃).hom ((s m₂).obj ((s m₁).obj X)) =
    F.map (eqToHom (_ : (s (m₁ + m₂ + m₃)).obj X = (s (m₁ + (m₂ + m₃))).obj X)) ≫
      NatTrans.app (i (m₁ + (m₂ + m₃))).hom X ≫
        NatTrans.app (shiftFunctorAdd D m₁ (m₂ + m₃)).hom (F.obj X) ≫
          NatTrans.app (shiftFunctorAdd D m₂ m₃).hom ((shiftFunctor D m₁).obj (F.obj X)) ≫
            (shiftFunctor D m₃).map ((shiftFunctor D m₂).map (NatTrans.app (i m₁).inv X)) ≫
              (shiftFunctor D m₃).map (NatTrans.app (i m₂).inv ((s m₁).obj X))
[PROOFSTEP]
erw [(i m₃).hom.naturality]
[GOAL]
C : Type u
A : Type u_1
inst✝⁵ : Category.{v, u} C
D : Type u_2
inst✝⁴ : Category.{?u.291249, u_2} D
inst✝³ : AddMonoid A
inst✝² : HasShift D A
F : C ⥤ D
inst✝¹ : Full F
inst✝ : Faithful F
s : A → C ⥤ C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
m₁ m₂ m₃ : A
X : C
h :
  NatTrans.app (shiftFunctorAdd D (m₁ + m₂) m₃).hom (F.obj X) ≫
      (shiftFunctor D m₃).map (NatTrans.app (shiftFunctorAdd D m₁ m₂).hom (F.obj X)) =
    NatTrans.app (shiftFunctorAdd' D m₁ (m₂ + m₃) (m₁ + m₂ + m₃) (_ : m₁ + (m₂ + m₃) = m₁ + m₂ + m₃)).hom (F.obj X) ≫
      NatTrans.app (shiftFunctorAdd D m₂ m₃).hom ((shiftFunctor D m₁).obj (F.obj X))
⊢ NatTrans.app (i (m₁ + m₂ + m₃)).hom X ≫
      NatTrans.app (shiftFunctorAdd D (m₁ + m₂) m₃).hom (F.obj X) ≫
        (shiftFunctor D m₃).map (NatTrans.app (i (m₁ + m₂)).inv X) ≫
          NatTrans.app (i m₃).inv ((s (m₁ + m₂)).obj X) ≫
            NatTrans.app (i m₃).hom ((s (m₁ + m₂)).obj X) ≫
              (F ⋙ shiftFunctor D m₃).map (NatTrans.app (hasShiftOfFullyFaithful_add F s i m₁ m₂).hom X) =
    F.map (eqToHom (_ : (s (m₁ + m₂ + m₃)).obj X = (s (m₁ + (m₂ + m₃))).obj X)) ≫
      NatTrans.app (i (m₁ + (m₂ + m₃))).hom X ≫
        NatTrans.app (shiftFunctorAdd D m₁ (m₂ + m₃)).hom (F.obj X) ≫
          NatTrans.app (shiftFunctorAdd D m₂ m₃).hom ((shiftFunctor D m₁).obj (F.obj X)) ≫
            (shiftFunctor D m₃).map ((shiftFunctor D m₂).map (NatTrans.app (i m₁).inv X)) ≫
              (shiftFunctor D m₃).map (NatTrans.app (i m₂).inv ((s m₁).obj X))
[PROOFSTEP]
rw [Functor.comp_map, map_hasShiftOfFullyFaithful_add_hom_app, Functor.map_comp, Functor.map_comp,
  Iso.inv_hom_id_app_assoc, ← Functor.map_comp_assoc _ ((i (m₁ + m₂)).inv.app X), Iso.inv_hom_id_app, Functor.map_id,
  Category.id_comp, reassoc_of% h, dcongr_arg (fun a => (i a).hom.app X) (add_assoc m₁ m₂ m₃)]
[GOAL]
C : Type u
A : Type u_1
inst✝⁵ : Category.{v, u} C
D : Type u_2
inst✝⁴ : Category.{?u.291249, u_2} D
inst✝³ : AddMonoid A
inst✝² : HasShift D A
F : C ⥤ D
inst✝¹ : Full F
inst✝ : Faithful F
s : A → C ⥤ C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
m₁ m₂ m₃ : A
X : C
h :
  NatTrans.app (shiftFunctorAdd D (m₁ + m₂) m₃).hom (F.obj X) ≫
      (shiftFunctor D m₃).map (NatTrans.app (shiftFunctorAdd D m₁ m₂).hom (F.obj X)) =
    NatTrans.app (shiftFunctorAdd' D m₁ (m₂ + m₃) (m₁ + m₂ + m₃) (_ : m₁ + (m₂ + m₃) = m₁ + m₂ + m₃)).hom (F.obj X) ≫
      NatTrans.app (shiftFunctorAdd D m₂ m₃).hom ((shiftFunctor D m₁).obj (F.obj X))
⊢ (eqToHom (_ : (s (m₁ + m₂ + m₃) ⋙ F).obj X = (s (m₁ + (m₂ + m₃)) ⋙ F).obj X) ≫
        NatTrans.app (i (m₁ + (m₂ + m₃))).hom X ≫
          eqToHom (_ : (F ⋙ shiftFunctor D (m₁ + (m₂ + m₃))).obj X = (F ⋙ shiftFunctor D (m₁ + m₂ + m₃)).obj X)) ≫
      NatTrans.app (shiftFunctorAdd' D m₁ (m₂ + m₃) (m₁ + m₂ + m₃) (_ : m₁ + (m₂ + m₃) = m₁ + m₂ + m₃)).hom (F.obj X) ≫
        NatTrans.app (shiftFunctorAdd D m₂ m₃).hom ((shiftFunctor D m₁).obj (F.obj X)) ≫
          (shiftFunctor D m₃).map
            ((shiftFunctor D m₂).map (NatTrans.app (i m₁).inv X) ≫ NatTrans.app (i m₂).inv ((s m₁).obj X)) =
    F.map (eqToHom (_ : (s (m₁ + m₂ + m₃)).obj X = (s (m₁ + (m₂ + m₃))).obj X)) ≫
      NatTrans.app (i (m₁ + (m₂ + m₃))).hom X ≫
        NatTrans.app (shiftFunctorAdd D m₁ (m₂ + m₃)).hom (F.obj X) ≫
          NatTrans.app (shiftFunctorAdd D m₂ m₃).hom ((shiftFunctor D m₁).obj (F.obj X)) ≫
            (shiftFunctor D m₃).map ((shiftFunctor D m₂).map (NatTrans.app (i m₁).inv X)) ≫
              (shiftFunctor D m₃).map (NatTrans.app (i m₂).inv ((s m₁).obj X))
[PROOFSTEP]
simp [shiftFunctorAdd', eqToHom_map]
[GOAL]
C : Type u
A : Type u_1
inst✝⁵ : Category.{v, u} C
D : Type u_2
inst✝⁴ : Category.{?u.291249, u_2} D
inst✝³ : AddMonoid A
inst✝² : HasShift D A
F : C ⥤ D
inst✝¹ : Full F
inst✝ : Faithful F
s : A → C ⥤ C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
n : A
X : C
⊢ F.map (NatTrans.app (hasShiftOfFullyFaithful_add F s i 0 n).hom X) =
    F.map
      (eqToHom (_ : (s (0 + n)).obj X = (s n).obj ((𝟭 C).obj X)) ≫
        (s n).map (NatTrans.app (hasShiftOfFullyFaithful_zero F s i).inv X))
[PROOFSTEP]
have this := dcongr_arg (fun a => (i a).hom.app X) (zero_add n)
[GOAL]
C : Type u
A : Type u_1
inst✝⁵ : Category.{v, u} C
D : Type u_2
inst✝⁴ : Category.{?u.291249, u_2} D
inst✝³ : AddMonoid A
inst✝² : HasShift D A
F : C ⥤ D
inst✝¹ : Full F
inst✝ : Faithful F
s : A → C ⥤ C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
n : A
X : C
this :
  NatTrans.app (i (0 + n)).hom X =
    eqToHom (_ : (s (0 + n) ⋙ F).obj X = (s n ⋙ F).obj X) ≫
      NatTrans.app (i n).hom X ≫ eqToHom (_ : (F ⋙ shiftFunctor D n).obj X = (F ⋙ shiftFunctor D (0 + n)).obj X)
⊢ F.map (NatTrans.app (hasShiftOfFullyFaithful_add F s i 0 n).hom X) =
    F.map
      (eqToHom (_ : (s (0 + n)).obj X = (s n).obj ((𝟭 C).obj X)) ≫
        (s n).map (NatTrans.app (hasShiftOfFullyFaithful_zero F s i).inv X))
[PROOFSTEP]
rw [← cancel_mono ((i n).hom.app ((s 0).obj X))]
[GOAL]
C : Type u
A : Type u_1
inst✝⁵ : Category.{v, u} C
D : Type u_2
inst✝⁴ : Category.{?u.291249, u_2} D
inst✝³ : AddMonoid A
inst✝² : HasShift D A
F : C ⥤ D
inst✝¹ : Full F
inst✝ : Faithful F
s : A → C ⥤ C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
n : A
X : C
this :
  NatTrans.app (i (0 + n)).hom X =
    eqToHom (_ : (s (0 + n) ⋙ F).obj X = (s n ⋙ F).obj X) ≫
      NatTrans.app (i n).hom X ≫ eqToHom (_ : (F ⋙ shiftFunctor D n).obj X = (F ⋙ shiftFunctor D (0 + n)).obj X)
⊢ F.map (NatTrans.app (hasShiftOfFullyFaithful_add F s i 0 n).hom X) ≫ NatTrans.app (i n).hom ((s 0).obj X) =
    F.map
        (eqToHom (_ : (s (0 + n)).obj X = (s n).obj ((𝟭 C).obj X)) ≫
          (s n).map (NatTrans.app (hasShiftOfFullyFaithful_zero F s i).inv X)) ≫
      NatTrans.app (i n).hom ((s 0).obj X)
[PROOFSTEP]
simp [this, map_hasShiftOfFullyFaithful_add_hom_app, shiftFunctorAdd_zero_add_hom_app, eqToHom_map]
[GOAL]
C : Type u
A : Type u_1
inst✝⁵ : Category.{v, u} C
D : Type u_2
inst✝⁴ : Category.{?u.291249, u_2} D
inst✝³ : AddMonoid A
inst✝² : HasShift D A
F : C ⥤ D
inst✝¹ : Full F
inst✝ : Faithful F
s : A → C ⥤ C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
n : A
X : C
this :
  NatTrans.app (i (0 + n)).hom X =
    eqToHom (_ : (s (0 + n) ⋙ F).obj X = (s n ⋙ F).obj X) ≫
      NatTrans.app (i n).hom X ≫ eqToHom (_ : (F ⋙ shiftFunctor D n).obj X = (F ⋙ shiftFunctor D (0 + n)).obj X)
⊢ eqToHom (_ : (s (0 + n) ⋙ F).obj X = (s n ⋙ F).obj X) ≫
      NatTrans.app (i n).hom X ≫
        (shiftFunctor D n).map (NatTrans.app (shiftFunctorZero D A).inv (F.obj X)) ≫
          (shiftFunctor D n).map (NatTrans.app (i 0).inv X) =
    eqToHom (_ : F.obj ((s (0 + n)).obj X) = F.obj ((s n).obj X)) ≫
      F.map ((s n).map (NatTrans.app (hasShiftOfFullyFaithful_zero F s i).inv X)) ≫ NatTrans.app (i n).hom ((s 0).obj X)
[PROOFSTEP]
congr 1
[GOAL]
case e_a
C : Type u
A : Type u_1
inst✝⁵ : Category.{v, u} C
D : Type u_2
inst✝⁴ : Category.{?u.291249, u_2} D
inst✝³ : AddMonoid A
inst✝² : HasShift D A
F : C ⥤ D
inst✝¹ : Full F
inst✝ : Faithful F
s : A → C ⥤ C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
n : A
X : C
this :
  NatTrans.app (i (0 + n)).hom X =
    eqToHom (_ : (s (0 + n) ⋙ F).obj X = (s n ⋙ F).obj X) ≫
      NatTrans.app (i n).hom X ≫ eqToHom (_ : (F ⋙ shiftFunctor D n).obj X = (F ⋙ shiftFunctor D (0 + n)).obj X)
⊢ NatTrans.app (i n).hom X ≫
      (shiftFunctor D n).map (NatTrans.app (shiftFunctorZero D A).inv (F.obj X)) ≫
        (shiftFunctor D n).map (NatTrans.app (i 0).inv X) =
    F.map ((s n).map (NatTrans.app (hasShiftOfFullyFaithful_zero F s i).inv X)) ≫ NatTrans.app (i n).hom ((s 0).obj X)
[PROOFSTEP]
erw [(i n).hom.naturality]
[GOAL]
case e_a
C : Type u
A : Type u_1
inst✝⁵ : Category.{v, u} C
D : Type u_2
inst✝⁴ : Category.{?u.291249, u_2} D
inst✝³ : AddMonoid A
inst✝² : HasShift D A
F : C ⥤ D
inst✝¹ : Full F
inst✝ : Faithful F
s : A → C ⥤ C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
n : A
X : C
this :
  NatTrans.app (i (0 + n)).hom X =
    eqToHom (_ : (s (0 + n) ⋙ F).obj X = (s n ⋙ F).obj X) ≫
      NatTrans.app (i n).hom X ≫ eqToHom (_ : (F ⋙ shiftFunctor D n).obj X = (F ⋙ shiftFunctor D (0 + n)).obj X)
⊢ NatTrans.app (i n).hom X ≫
      (shiftFunctor D n).map (NatTrans.app (shiftFunctorZero D A).inv (F.obj X)) ≫
        (shiftFunctor D n).map (NatTrans.app (i 0).inv X) =
    NatTrans.app (i n).hom X ≫ (F ⋙ shiftFunctor D n).map (NatTrans.app (hasShiftOfFullyFaithful_zero F s i).inv X)
[PROOFSTEP]
dsimp
[GOAL]
case e_a
C : Type u
A : Type u_1
inst✝⁵ : Category.{v, u} C
D : Type u_2
inst✝⁴ : Category.{?u.291249, u_2} D
inst✝³ : AddMonoid A
inst✝² : HasShift D A
F : C ⥤ D
inst✝¹ : Full F
inst✝ : Faithful F
s : A → C ⥤ C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
n : A
X : C
this :
  NatTrans.app (i (0 + n)).hom X =
    eqToHom (_ : (s (0 + n) ⋙ F).obj X = (s n ⋙ F).obj X) ≫
      NatTrans.app (i n).hom X ≫ eqToHom (_ : (F ⋙ shiftFunctor D n).obj X = (F ⋙ shiftFunctor D (0 + n)).obj X)
⊢ NatTrans.app (i n).hom X ≫
      (shiftFunctor D n).map (NatTrans.app (shiftFunctorZero D A).inv (F.obj X)) ≫
        (shiftFunctor D n).map (NatTrans.app (i 0).inv X) =
    NatTrans.app (i n).hom X ≫ (shiftFunctor D n).map (F.map (NatTrans.app (hasShiftOfFullyFaithful_zero F s i).inv X))
[PROOFSTEP]
simp
[GOAL]
C : Type u
A : Type u_1
inst✝⁵ : Category.{v, u} C
D : Type u_2
inst✝⁴ : Category.{?u.291249, u_2} D
inst✝³ : AddMonoid A
inst✝² : HasShift D A
F : C ⥤ D
inst✝¹ : Full F
inst✝ : Faithful F
s : A → C ⥤ C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
n : A
X : C
⊢ F.map (NatTrans.app (hasShiftOfFullyFaithful_add F s i n 0).hom X) =
    F.map
      (eqToHom (_ : (s (n + 0)).obj X = (𝟭 C).obj ((s n).obj X)) ≫
        NatTrans.app (hasShiftOfFullyFaithful_zero F s i).inv ((s n).obj X))
[PROOFSTEP]
have := dcongr_arg (fun a => (i a).hom.app X) (add_zero n)
[GOAL]
C : Type u
A : Type u_1
inst✝⁵ : Category.{v, u} C
D : Type u_2
inst✝⁴ : Category.{?u.291249, u_2} D
inst✝³ : AddMonoid A
inst✝² : HasShift D A
F : C ⥤ D
inst✝¹ : Full F
inst✝ : Faithful F
s : A → C ⥤ C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
n : A
X : C
this :
  NatTrans.app (i (n + 0)).hom X =
    eqToHom (_ : (s (n + 0) ⋙ F).obj X = (s n ⋙ F).obj X) ≫
      NatTrans.app (i n).hom X ≫ eqToHom (_ : (F ⋙ shiftFunctor D n).obj X = (F ⋙ shiftFunctor D (n + 0)).obj X)
⊢ F.map (NatTrans.app (hasShiftOfFullyFaithful_add F s i n 0).hom X) =
    F.map
      (eqToHom (_ : (s (n + 0)).obj X = (𝟭 C).obj ((s n).obj X)) ≫
        NatTrans.app (hasShiftOfFullyFaithful_zero F s i).inv ((s n).obj X))
[PROOFSTEP]
simp [this, ← NatTrans.naturality_assoc, eqToHom_map, shiftFunctorAdd_add_zero_hom_app]
