-- 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
X Y Z : Dᵒᵖ
x : X ⟶ Y
x_1 : Y ⟶ Z
h :
  ∀ (b : (↑(R.obj X) : Type u)),
    Eq (α :=
      (↑(Functor.obj (ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map (x ≫ x_1))))
            (CommRingCat.KaehlerDifferential (φ'.app Z))) :
        Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑(R.obj X) : Type u)) ↦
              LinearMap (R := (↑(R.obj X) : Type u)) (RingHom.id (↑(R.obj X) : Type u)) (↑x1 : Type u) (↑x2 : Type u))
              (CC := ModuleCat.carrier) (Y :=
              Functor.obj (ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map (x ≫ x_1))))
                (CommRingCat.KaehlerDifferential (φ'.app Z)))
              (CommRingCat.KaehlerDifferential.map ⋯) :
            (a : (↑(CommRingCat.KaehlerDifferential (φ'.app X)) : Type u)) →
              (↑((ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map (x ≫ x_1)))).obj
                    (CommRingCat.KaehlerDifferential (φ'.app Z))) :
                Type u))
          (CommRingCat.KaehlerDifferential.d b) :
        (↑(Functor.obj (ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map (x ≫ x_1))))
              (CommRingCat.KaehlerDifferential (φ'.app Z))) :
          Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑(R.obj X) : Type u)) ↦
              LinearMap (R := (↑(R.obj X) : Type u)) (RingHom.id (↑(R.obj X) : Type u)) (↑x1 : Type u) (↑x2 : Type u))
              (CC := ModuleCat.carrier) (Y :=
              Functor.obj (ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map (x ≫ x_1))))
                (CommRingCat.KaehlerDifferential (φ'.app Z)))
              (CommRingCat.KaehlerDifferential.map ⋯ ≫
                (ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map x))).map
                    (CommRingCat.KaehlerDifferential.map ⋯) ≫
                  Iso.inv
                    (ModuleCat.restrictScalarsComp'App (CommRingCat.Hom.hom (R.map x)) (CommRingCat.Hom.hom (R.map x_1))
                      (CommRingCat.Hom.hom (R.map (x ≫ x_1))) ⋯ (CommRingCat.KaehlerDifferential (φ'.app Z)))) :
            (a : (↑(CommRingCat.KaehlerDifferential (φ'.app X)) : Type u)) →
              (↑((ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map (x ≫ x_1)))).obj
                    (CommRingCat.KaehlerDifferential (φ'.app Z))) :
                Type u))
          (CommRingCat.KaehlerDifferential.d b) :
        (↑(Functor.obj (ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map (x ≫ x_1))))
              (CommRingCat.KaehlerDifferential (φ'.app Z))) :
          Type u))
⊢ Eq (α :=
    CommRingCat.KaehlerDifferential (φ'.app X) ⟶
      Functor.obj (ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map (x ≫ x_1))))
        (CommRingCat.KaehlerDifferential (φ'.app Z)))
    (CommRingCat.KaehlerDifferential.map ⋯)
    (CommRingCat.KaehlerDifferential.map ⋯ ≫
      (ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map x))).map (CommRingCat.KaehlerDifferential.map ⋯) ≫
        Iso.inv
          (ModuleCat.restrictScalarsComp'App (CommRingCat.Hom.hom (R.map x)) (CommRingCat.Hom.hom (R.map x_1))
            (CommRingCat.Hom.hom (R.map (x ≫ x_1))) ⋯ (CommRingCat.KaehlerDifferential (φ'.app Z))))

Tactic:
ext