-- 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 φ
h₂ : d.Universal
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 = φ'
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' = h₂.desc d'
⊢ { desc := @desc, fac := @fac, postcomp_injective := @postcomp_injective : d.Universal } = h₂
have mk : ∀
  (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, fac := @fac, postcomp_injective := @postcomp_injective : d.Universal } =
    { desc := @desc_1, fac := @fac_1, postcomp_injective := @postcomp_injective_1 }
Tactic: cases h₂
Cleared hypotheses: h₂, this