[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁶ : Category.{u_6, u_1} C
inst✝⁵ : Category.{u_5, u_2} D
inst✝⁴ : Category.{?u.20851, u_3} E
F : C ⥤ D
G : D ⥤ E
A : Type u_4
inst✝³ : AddMonoid A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : HasShift E A
a b : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ : shiftFunctor C b ⋙ F ≅ F ⋙ shiftFunctor D b
X : C
⊢ NatTrans.app (isoAdd e₁ e₂).hom X =
    F.map (NatTrans.app (shiftFunctorAdd C a b).hom X) ≫
      NatTrans.app e₂.hom ((shiftFunctor C a).obj X) ≫
        (shiftFunctor D b).map (NatTrans.app e₁.hom X) ≫ NatTrans.app (shiftFunctorAdd D a b).inv (F.obj X)
[PROOFSTEP]
simp only [isoAdd, isoAdd'_hom_app, shiftFunctorAdd'_eq_shiftFunctorAdd]
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁶ : Category.{u_6, u_1} C
inst✝⁵ : Category.{u_5, u_2} D
inst✝⁴ : Category.{?u.24197, u_3} E
F : C ⥤ D
G : D ⥤ E
A : Type u_4
inst✝³ : AddMonoid A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : HasShift E A
a b : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ : shiftFunctor C b ⋙ F ≅ F ⋙ shiftFunctor D b
X : C
⊢ NatTrans.app (isoAdd e₁ e₂).inv X =
    NatTrans.app (shiftFunctorAdd D a b).hom (F.obj X) ≫
      (shiftFunctor D b).map (NatTrans.app e₁.inv X) ≫
        NatTrans.app e₂.inv ((shiftFunctor C a).obj X) ≫ F.map (NatTrans.app (shiftFunctorAdd C a b).inv X)
[PROOFSTEP]
simp only [isoAdd, isoAdd'_inv_app, shiftFunctorAdd'_eq_shiftFunctorAdd]
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁷ : Category.{u_6, u_1} C
inst✝⁶ : Category.{u_5, u_2} D
inst✝⁵ : Category.{?u.38582, u_3} E
F : C ⥤ D
G : D ⥤ E
A : Type u_4
inst✝⁴ : AddMonoid A
inst✝³ : HasShift C A
inst✝² : HasShift D A
inst✝¹ : HasShift E A
inst✝ : CommShift F A
a b c : A
h : a + b = c
⊢ commShiftIso F c = CommShift.isoAdd' h (commShiftIso F a) (commShiftIso F b)
[PROOFSTEP]
subst h
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁷ : Category.{u_6, u_1} C
inst✝⁶ : Category.{u_5, u_2} D
inst✝⁵ : Category.{?u.38582, u_3} E
F : C ⥤ D
G : D ⥤ E
A : Type u_4
inst✝⁴ : AddMonoid A
inst✝³ : HasShift C A
inst✝² : HasShift D A
inst✝¹ : HasShift E A
inst✝ : CommShift F A
a b : A
⊢ commShiftIso F (a + b) = CommShift.isoAdd' (_ : a + b = a + b) (commShiftIso F a) (commShiftIso F b)
[PROOFSTEP]
simp only [commShiftIso_add, CommShift.isoAdd]
