∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] (B : C)
  (a : ℤ),
  CategoryTheory.NatIso.ofComponents
      (fun A =>
        (let __Equiv := Quiver.Hom.opEquiv.trans (CategoryTheory.ShiftedHom.opEquiv' 0 a a ⋯).symm;
          { toEquiv := __Equiv, map_add' := ⋯ }).toAddCommGrpIso)
      ⋯ =
    CategoryTheory.Functor.isoWhiskerRight (CategoryTheory.shiftFunctorZero Cᵒᵖ ℤ)
        (CategoryTheory.preadditiveYoneda.obj ((CategoryTheory.shiftFunctor C a).obj B)) ≪≫
      (CategoryTheory.preadditiveYoneda.obj ((CategoryTheory.shiftFunctor C a).obj B)).leftUnitor