∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Limits.HasBinaryProducts C]
  {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} (x : C),
  CategoryTheory.Functor.whiskerRight (CategoryTheory.NatTrans.op (CategoryTheory.Over.forgetAdjStar x).counit) R.val =
    CategoryTheory.CategoryStruct.comp (SheafOfModules.pushforwardOver x).val
      ((CategoryTheory.Over.star x).op.whiskerLeft (CategoryTheory.CategoryStruct.id (R.over x)).val)