-- Module: Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ CommRingCat
F : CategoryTheory.Functor.{v₁, v₂, u₁, u₂} C D
S' R : CategoryTheory.Functor.{v₂, u, u₂, u + 1} Dᵒᵖ CommRingCat
M N :
  PresheafOfModules.{v, v₂, u₂, u}
    (R ⋙
      forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier) RingCat (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD :=
        RingCat.carrier))
φ : S ⟶ F.op ⋙ R
φ' : S' ⟶ R
d : M.Derivation φ
f : M ⟶ N
X Y : Dᵒᵖ
g : X ⟶ Y
x : (↑(R.obj X) : Type u)
⊢ Eq.{v + 1} (α := (↑(N.obj Y) : Type v))
    (((ModuleCat.Hom.hom (f.app Y)).toAddMonoidHom.comp d.d : (a : (↑(R.obj Y) : Type u)) → (↑(N.obj Y) : Type v))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (R.map g) :
            (a : (↑(R.obj X) : Type u)) → (↑(R.obj Y) : Type u))
          x) :
      (↑(N.obj Y) : Type v))
    ((ConcreteCategory.hom (FC :=
            fun
              (x1 x2 :
                ModuleCat.{v, u}
                  (↑(Functor.obj
                        (R ⋙
                          forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u))
                            (CC := CommRingCat.carrier) RingCat (FD := fun (R S : RingCat.{u}) ↦
                            (↑R : Type u) →+* (↑S : Type u)) (CD := RingCat.carrier))
                        X) :
                    Type u)) ↦
            LinearMap.{u, u, v, v} (R :=
              (↑(Functor.obj
                    (R ⋙
                      forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                        CommRingCat.carrier) RingCat (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u))
                        (CD := RingCat.carrier))
                    X) :
                Type u))
              (RingHom.id
                (↑(Functor.obj
                      (R ⋙
                        forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                          CommRingCat.carrier) RingCat (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u))
                          (CD := RingCat.carrier))
                      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 ⋙ forget₂ CommRingCat RingCat).map g))).obj (N.obj Y)) :
              Type v))
        (((ModuleCat.Hom.hom (f.app X)).toAddMonoidHom.comp d.d : (a : (↑(R.obj X) : Type u)) → (↑(N.obj X) : Type v))
            x :
          (↑(N.obj X) : Type v)) :
      (↑(Functor.obj
            (ModuleCat.restrictScalars
              (RingCat.Hom.hom
                (CategoryTheory.Functor.map
                  (R ⋙
                    forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                      CommRingCat.carrier) RingCat (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u))
                      (CD := RingCat.carrier))
                  g)))
            (N.obj Y)) :
        Type v))

Tactic:
simpa using naturality_apply f g (d.d x)

Premises used: PresheafOfModules.Derivation.d, PresheafOfModules.naturality_apply, DFunLike.coe