∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D}
  {F G : CategoryTheory.Functor C D} {T : CategoryTheory.Sheaf J RingCat} {S : CategoryTheory.Sheaf K RingCat}
  [inst_2 : F.IsContinuous J K] [inst_3 : F.IsContinuous J K] [inst_4 : G.IsContinuous J K]
  [inst_5 : G.IsContinuous J K] (φ : T ⟶ (G.sheafPushforwardContinuous RingCat J K).obj S) (α : F ⟶ G)
  (X : SheafOfModules S) (U : Cᵒᵖ) (x : ↑(((SheafOfModules.pushforward φ).obj X).val.obj U)),
  (CategoryTheory.ConcreteCategory.hom (((SheafOfModules.pushforwardNatTrans φ α).app X).val.app U)) x =
    (CategoryTheory.ConcreteCategory.hom (X.val.map (α.app (Opposite.unop U)).op)) x