-- 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
d : M.Derivation φ
desc :
  {M' :
      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))} →
    (d' : M'.Derivation φ) → M ⟶ M'
fac :
  ∀
    {M' :
      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))}
    (d' : M'.Derivation φ), d.postcomp (desc d') = d'
postcomp_injective :
  ∀
    {M' :
      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))}
    (φ_1 φ' : M ⟶ M') (h : d.postcomp φ_1 = d.postcomp φ'), φ_1 = φ'
desc_1 :
  {M' :
      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))} →
    (d' : M'.Derivation φ) → M ⟶ M'
fac_1 :
  ∀
    {M' :
      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))}
    (d' : M'.Derivation φ), d.postcomp (desc_1 d') = d'
postcomp_injective_1 :
  ∀
    {M' :
      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))}
    (φ_1 φ' : M ⟶ M') (h : d.postcomp φ_1 = d.postcomp φ'), φ_1 = φ'
this :
  ∀
    {M' :
      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))}
    (d' : M'.Derivation φ),
    { desc := @desc, fac := @fac, postcomp_injective := @postcomp_injective : d.Universal }.desc d' =
      { desc := @desc_1, fac := @fac_1, postcomp_injective := @postcomp_injective_1 : d.Universal }.desc d'
⊢ @desc = @desc_1
have mk : ∀
  (x :
    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)))
  (x_1 : x.Derivation φ), desc x_1 = desc_1 x_1
Tactic: ext : 2