Components of pushforwards of morphisms of presheaves of modules

Mathlib's PresheafOfModules.pushforward₀ F R reindexes a presheaf of R-modules along a functor F. On morphisms it keeps the components: TauCeti.PresheafOfModules.pushforward₀_map_app_apply records that the component at X of the pushforward of α is the component of α at the image of X.

theorem TauCeti.PresheafOfModules.pushforward₀_map_app_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {R : CategoryTheory.Functor Dᵒᵖ RingCat} {M N : PresheafOfModules R} (α : M ⟶ N) (X : Cᵒᵖ) (m : ↑(((PresheafOfModules.pushforward₀ F R).obj M).obj X)) : (CategoryTheory.ConcreteCategory.hom (((PresheafOfModules.pushforward₀ F R).map α).app X)) m = (CategoryTheory.ConcreteCategory.hom (α.app (Opposite.op (F.obj (Opposite.unop X))))) m

The pushforward along F of a morphism α of presheaves of modules has, at X, the component of α at the image of X.

The element is taken in the domain of the pushed-forward component, so that the lemma rewrites goals about components of pushed-forward morphisms; an element of M.obj (op (F.obj X.unop)) may be passed as well, since the two modules are definitionally equal.

This is not a simp lemma: simp rewrites the base ring (F.op ⋙ R).obj X of the component to R.obj (op (F.obj X.unop)) inside the implicit arguments of the coercion, so the left-hand side has no simp normal form.