∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_2, u_3} C] [inst_1 : CategoryTheory.Limits.HasBinaryProducts C]
  {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} (x : C) (U V : Cᵒᵖ) (f : U ⟶ V),
  CategoryTheory.CategoryStruct.comp (R.val.map f) (R.val.map CategoryTheory.Limits.prod.snd.op) =
    CategoryTheory.CategoryStruct.comp (R.val.map CategoryTheory.Limits.prod.snd.op)
      ((((CategoryTheory.Over.star x).sheafPushforwardContinuous RingCat J (J.over x)).obj (R.over x)).val.map f)