-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
M_1 M₁ M₂ M N : PresheafOfModules.{v, v₁, u₁, u} R
f : M ⟶ N
s : M.sections
X Y : Cᵒᵖ
g : X ⟶ Y
⊢ Eq (α := (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map g))).obj (N.obj Y)) : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj X) : Type u)) ↦
            LinearMap.{u, u, v, v} (R := (↑(R.obj X) : Type u)) (RingHom.id (↑(R.obj X) : Type u)) (↑x1 : Type v)
              (↑x2 : Type v))
            (CC := ModuleCat.carrier) (N.map g) :
          (a : (↑(N.obj X) : Type v)) →
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map g))).obj (N.obj Y)) : Type v))
        ((fun (X : Cᵒᵖ) ↦
            ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj X) : Type u)) ↦
                    LinearMap.{u, u, v, v} (R := (↑(R.obj X) : Type u)) (RingHom.id (↑(R.obj X) : Type u))
                      (↑x1 : Type v) (↑x2 : Type v))
                    (CC := ModuleCat.carrier) (f.app X) :
                  (a : (↑(M.obj X) : Type v)) → (↑(N.obj X) : Type v))
                ((↑s : (j : Cᵒᵖ) → (M.presheaf ⋙ forget Ab).obj j) X) :
              (↑(N.obj X) : Type v)))
          X) :
      (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map g))).obj (N.obj Y)) : Type v))
    ((fun (X : Cᵒᵖ) ↦
          ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj X) : Type u)) ↦
                  LinearMap.{u, u, v, v} (R := (↑(R.obj X) : Type u)) (RingHom.id (↑(R.obj X) : Type u)) (↑x1 : Type v)
                    (↑x2 : Type v))
                  (CC := ModuleCat.carrier) (f.app X) :
                (a : (↑(M.obj X) : Type v)) → (↑(N.obj X) : Type v))
              ((↑s : (j : Cᵒᵖ) → (M.presheaf ⋙ forget Ab).obj j) X) :
            (↑(N.obj X) : Type v)))
        Y :
      (↑(N.obj Y) : Type v))
have rw : Eq (α := (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map g))).obj (N.obj Y)) : Type v))
  ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj Y) : Type u)) ↦
          LinearMap.{u, u, v, v} (R := (↑(R.obj Y) : Type u)) (RingHom.id (↑(R.obj Y) : Type u)) (↑x1 : Type v)
            (↑x2 : Type v))
          (CC := ModuleCat.carrier) (f.app Y) :
        (a : (↑(M.obj Y) : Type v)) → (↑(N.obj Y) : Type v))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj X) : Type u)) ↦
              LinearMap.{u, u, v, v} (R := (↑(R.obj X) : Type u)) (RingHom.id (↑(R.obj X) : Type u)) (↑x1 : Type v)
                (↑x2 : Type v))
              (CC := ModuleCat.carrier) (M.map g) :
            (a : (↑(M.obj X) : Type v)) →
              (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map g))).obj (M.obj Y)) : Type v))
          ((↑s : (j : Cᵒᵖ) → (M.presheaf ⋙ forget Ab).obj j) X) :
        (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map g))).obj (M.obj Y)) : Type v)) :
    (↑(N.obj Y) : Type v))
  ((fun (X : Cᵒᵖ) ↦
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj X) : Type u)) ↦
                LinearMap.{u, u, v, v} (R := (↑(R.obj X) : Type u)) (RingHom.id (↑(R.obj X) : Type u)) (↑x1 : Type v)
                  (↑x2 : Type v))
                (CC := ModuleCat.carrier) (f.app X) :
              (a : (↑(M.obj X) : Type v)) → (↑(N.obj X) : Type v))
            ((↑s : (j : Cᵒᵖ) → (M.presheaf ⋙ forget Ab).obj j) X) :
          (↑(N.obj X) : Type v)))
      Y :
    (↑(N.obj Y) : Type v))
Tactic: rw [← naturality_apply, sections_property]