∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Type w} [inst_1 : AddMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] (t : CategoryTheory.TwistShiftData C A) (X : t.Category),
  (CategoryTheory.shiftFunctorZero t.Category A).inv.app X =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorZero C A).inv.app X) ((t.shiftIso 0).inv.app X)