-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf (goal)
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
⊢ 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))))
have 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 sorry) :
          (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 sorry ≫
              (ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map x))).map (CommRingCat.KaehlerDifferential.map sorry) ≫
                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))) sorry (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))
Tactic: ext