awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
d : M.Derivation φ
h₁ h₂ : d.Universal
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 φ), h₁.desc d' = h₂.desc d'
mk :
  ∀
    (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₂
⊢ h₁ = h₂

Tactic:
cases h₁
-- 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
d : M.Derivation φ
h₁ h₂ : d.Universal
suffices :
  ∀
    {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 φ), h₁.desc d' = h₂.desc d'
⊢ h₁ = h₂

Tactic:
suffices ∀ {M' : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)}
      (d' : M'.Derivation φ), h₁.desc d' = h₂.desc d' by
        cases h₁
        cases h₂
        simp only [Universal.mk.injEq]
        ext : 2
        apply this
-- 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
d : M.Derivation φ
h₁ h₂ : d.Universal
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 φ
h : d.postcomp (h₁.desc d') = d.postcomp (h₂.desc d')
⊢ h₁.desc d' = h₂.desc d'

Tactic:
apply h₁.postcomp_injective

Premises used: PresheafOfModules.Derivation.Universal.postcomp_injective
-- 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
d : M.Derivation φ
h₁ h₂ : d.Universal
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 (h₁.desc d') = d.postcomp (h₂.desc d')

Tactic:
simp
-- Module: Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf
Goal:
D : Type u₂
inst : Category.{v₂, u₂} D
S' R : CategoryTheory.Functor.{v₂, u, u₂, u + 1} Dᵒᵖ CommRingCat
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))
φ' : S' ⟶ R
d : M.Derivation' φ'
X : Dᵒᵖ
a : (↑(S'.obj X) : Type u)
⊢ Eq.{v + 1} (α := (↑(M.obj X) : Type v))
    (((d.d : AddMonoidHom.{u, v} (↑(R.obj X) : Type u) (↑(M.obj X) : Type v)) :
          (a : (↑(R.obj X) : Type u)) → (↑(M.obj X) : Type v))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (φ'.app X) :
            (a : (↑(S'.obj X) : Type u)) → (↑(R.obj X) : Type u))
          a) :
      (↑(M.obj X) : Type v))
    (0 : (↑(M.obj X) : Type v))

Tactic:
Derivation.d_app d _

Premises used: PresheafOfModules.Derivation.d_app
-- Module: Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf
Goal:
D : Type u₂
inst : Category.{v₂, u₂} D
S' R : CategoryTheory.Functor.{v₂, u, u₂, u + 1} Dᵒᵖ CommRingCat
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))
φ' : S' ⟶ R
d : M.Derivation' φ'
X : Dᵒᵖ
b : (↑(R.obj X) : Type u)
⊢ (d.app X).d b =
    ((d.d : AddMonoidHom.{u, v} (↑(R.obj X) : Type u) (↑(M.obj X) : Type v)) :
        (a : (↑(R.obj X) : Type u)) → (↑(M.obj X) : Type v))
      b

Tactic:
rfl

Premises used: ModuleCat.Derivation.d, rfl
-- 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
d : (X : Dᵒᵖ) → (M.obj X).Derivation (φ'.app X)
d_map :
  ∀ ⦃X Y : Dᵒᵖ⦄ (f : X ⟶ Y) (x : (↑(R.obj X) : Type u)),
    (d Y).d
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (R.map f) :
            (a : (↑(R.obj X) : Type u)) → (↑(R.obj Y) : Type u))
          x) =
      (ConcreteCategory.hom (FC :=
            fun
              (x1 x2 :
                ModuleCat.{v, u}
                  (↑(Functor.obj
                        (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) :
                    Type u)) ↦
            LinearMap.{u, u, v, v} (R :=
              (↑(Functor.obj
                    (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) :
                Type u))
              (RingHom.id
                (↑(Functor.obj
                      (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) :
                  Type u))
              (↑x1 : Type v) (↑x2 : Type v))
            (CC := ModuleCat.carrier) (M.map f) :
          (a : (↑(M.obj X) : Type v)) →
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom ((R ⋙ forget₂ CommRingCat RingCat).map f))).obj (M.obj Y)) :
              Type v))
        ((d X).d x)
X : Dᵒᵖ
⊢ ∀ (a b : (↑(R.obj X) : Type u)), (d X).d (a + b) = (d X).d a + (d X).d b

Tactic:
simp
-- Module: Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf
Goal:
D : Type u₂
inst : Category.{v₂, u₂} D
S' R : CategoryTheory.Functor.{v₂, u, u₂, u + 1} Dᵒᵖ CommRingCat
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))
φ' : S' ⟶ R
d : (X : Dᵒᵖ) → (M.obj X).Derivation (φ'.app X)
d_map :
  ∀ ⦃X Y : Dᵒᵖ⦄ (f : X ⟶ Y) (x : (↑(R.obj X) : Type u)),
    (d Y).d
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (R.map f) :
            (a : (↑(R.obj X) : Type u)) → (↑(R.obj Y) : Type u))
          x) =
      (ConcreteCategory.hom (FC :=
            fun
              (x1 x2 :
                ModuleCat.{v, u}
                  (↑(Functor.obj
                        (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) :
                    Type u)) ↦
            LinearMap.{u, u, v, v} (R :=
              (↑(Functor.obj
                    (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) :
                Type u))
              (RingHom.id
                (↑(Functor.obj
                      (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) :
                  Type u))
              (↑x1 : Type v) (↑x2 : Type v))
            (CC := ModuleCat.carrier) (M.map f) :
          (a : (↑(M.obj X) : Type v)) →
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom ((R ⋙ forget₂ CommRingCat RingCat).map f))).obj (M.obj Y)) :
              Type v))
        ((d X).d x)
X : Dᵒᵖ
⊢ (mk d d_map).app X = d X

Tactic:
rfl

Premises used: ModuleCat.Derivation.mk, ModuleCat.Derivation, ModuleCat.Derivation.d, rfl, PresheafOfModules.Derivation'.app
-- 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 : Dᵒᵖ
dsimp :
  CommRingCat.KaehlerDifferential.map ⋯ =
    Iso.inv
      (ModuleCat.restrictScalarsId'App (CommRingCat.Hom.hom (R.map (𝟙 x))) ⋯
        (CommRingCat.KaehlerDifferential (φ'.app x)))
⊢ CommRingCat.KaehlerDifferential.map ⋯ =
    NatTrans.app
      (Iso.inv
        (ModuleCat.restrictScalarsId'
          (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 (φ'.app x))

Tactic:
dsimp
-- 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 : Dᵒᵖ
h :
  ∀ (b : (↑(R.obj x) : Type u)),
    Eq (α :=
      (↑((ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map (𝟙 x)))).obj
            (CommRingCat.KaehlerDifferential (φ'.app x))) :
        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) (CommRingCat.KaehlerDifferential.map ⋯) :
            (a : (↑(CommRingCat.KaehlerDifferential (φ'.app x)) : Type u)) →
              (↑((ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map (𝟙 x)))).obj
                    (CommRingCat.KaehlerDifferential (φ'.app x))) :
                Type u))
          (CommRingCat.KaehlerDifferential.d b) :
        (↑((ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map (𝟙 x)))).obj
              (CommRingCat.KaehlerDifferential (φ'.app x))) :
          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) (X := CommRingCat.KaehlerDifferential (φ'.app x))
              (Iso.inv
                (ModuleCat.restrictScalarsId'App (CommRingCat.Hom.hom (R.map (𝟙 x))) ⋯
                  (CommRingCat.KaehlerDifferential (φ'.app x)))) :
            (a : (↑(CommRingCat.KaehlerDifferential (φ'.app x)) : Type u)) →
              (↑((ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map (𝟙 x)))).obj
                    (CommRingCat.KaehlerDifferential (φ'.app x))) :
                Type u))
          (CommRingCat.KaehlerDifferential.d b) :
        (↑((ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map (𝟙 x)))).obj
              (CommRingCat.KaehlerDifferential (φ'.app x))) :
          Type u))
⊢ CommRingCat.KaehlerDifferential.map ⋯ =
    Iso.inv
      (ModuleCat.restrictScalarsId'App (CommRingCat.Hom.hom (R.map (𝟙 x))) ⋯
        (CommRingCat.KaehlerDifferential (φ'.app x)))

Tactic:
ext
-- 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 : Dᵒᵖ
b : (↑(R.obj x) : Type u)
⊢ Eq (α :=
    (↑((ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map (𝟙 x)))).obj
          (CommRingCat.KaehlerDifferential (φ'.app x))) :
      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) (CommRingCat.KaehlerDifferential.map ⋯) :
          (a : (↑(CommRingCat.KaehlerDifferential (φ'.app x)) : Type u)) →
            (↑((ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map (𝟙 x)))).obj
                  (CommRingCat.KaehlerDifferential (φ'.app x))) :
              Type u))
        (CommRingCat.KaehlerDifferential.d b) :
      (↑((ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map (𝟙 x)))).obj
            (CommRingCat.KaehlerDifferential (φ'.app x))) :
        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) (X := CommRingCat.KaehlerDifferential (φ'.app x))
            (Iso.inv
              (ModuleCat.restrictScalarsId'App (CommRingCat.Hom.hom (R.map (𝟙 x))) ⋯
                (CommRingCat.KaehlerDifferential (φ'.app x)))) :
          (a : (↑(CommRingCat.KaehlerDifferential (φ'.app x)) : Type u)) →
            (↑((ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map (𝟙 x)))).obj
                  (CommRingCat.KaehlerDifferential (φ'.app x))) :
              Type u))
        (CommRingCat.KaehlerDifferential.d b) :
      (↑((ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map (𝟙 x)))).obj
            (CommRingCat.KaehlerDifferential (φ'.app x))) :
        Type u))

Tactic:
simp
-- 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
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))

Tactic:
simp