-- 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
          (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))
              (x ≫ x_1))))
        (CommRingCat.KaehlerDifferential (φ'.app Z)))
    (CommRingCat.KaehlerDifferential.map ⋯)
    (CommRingCat.KaehlerDifferential.map ⋯ ≫
      CategoryStruct.comp (Y :=
        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))
                x)))
          (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))
                  x_1)))
            (CommRingCat.KaehlerDifferential (φ'.app Z))))
        (CategoryTheory.Functor.map
          (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))
                x)))
          (CommRingCat.KaehlerDifferential.map ⋯))
        (NatTrans.app
          (Iso.inv
            (ModuleCat.restrictScalarsComp'
              (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))
                  x))
              (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))
                  x_1))
              (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))
                  (x ≫ x_1)))
              ⋯))
          (CommRingCat.KaehlerDifferential (φ'.app Z))))
have dsimp : Eq (α :=
  CommRingCat.KaehlerDifferential (φ'.app X) ⟶
    Functor.obj (ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map (x ≫ x_1))))
      (CommRingCat.KaehlerDifferential (φ'.app Z)))
  (CommRingCat.KaehlerDifferential.map sorry)
  (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))))
Tactic: dsimp