awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.ModuleCat.Differentials.Basic
Goal:
A B : CommRingCat
f : A ⟶ B
M : ModuleCat (↑B : Type u)
α β : KaehlerDifferential f ⟶ M
h :
  ∀ (b : (↑B : Type u)),
    Eq (α := (↑M : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑B : Type u)) ↦
              LinearMap (R := (↑B : Type u)) (RingHom.id (↑B : Type u)) (↑x1 : Type u) (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) α :
            (a : (↑(KaehlerDifferential f) : Type u)) → (↑M : Type u))
          (d b) :
        (↑M : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑B : Type u)) ↦
              LinearMap (R := (↑B : Type u)) (RingHom.id (↑B : Type u)) (↑x1 : Type u) (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) β :
            (a : (↑(KaehlerDifferential f) : Type u)) → (↑M : Type u))
          (d b) :
        (↑M : Type u))
⊢ ⊤ ≤ (ModuleCat.Hom.hom (α - β)).ker

Tactic:
have : ⊤ ≤ LinearMap.ker (α - β).hom := by
    rw [← KaehlerDifferential.span_range_derivation, Submodule.span_le]
    rintro _ ⟨y, rfl⟩
    rw [SetLike.mem_coe, LinearMap.mem_ker, ModuleCat.hom_sub, LinearMap.sub_apply, sub_eq_zero]
    apply h
-- Module: Mathlib.Algebra.Category.ModuleCat.Differentials.Basic
Goal:
A B : CommRingCat
f : A ⟶ B
M : ModuleCat (↑B : Type u)
α β : KaehlerDifferential f ⟶ M
h :
  ∀ (b : (↑B : Type u)),
    Eq (α := (↑M : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑B : Type u)) ↦
              LinearMap (R := (↑B : Type u)) (RingHom.id (↑B : Type u)) (↑x1 : Type u) (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) α :
            (a : (↑(KaehlerDifferential f) : Type u)) → (↑M : Type u))
          (d b) :
        (↑M : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑B : Type u)) ↦
              LinearMap (R := (↑B : Type u)) (RingHom.id (↑B : Type u)) (↑x1 : Type u) (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) β :
            (a : (↑(KaehlerDifferential f) : Type u)) → (↑M : Type u))
          (d b) :
        (↑M : Type u))
this : ⊤ ≤ (ModuleCat.Hom.hom (α - β)).ker
⊢ ModuleCat.Hom.hom (α - β) = 0

Tactic:
rw [top_le_iff, LinearMap.ker_eq_top] at this

Premises used: LinearMap.ker_eq_top, top_le_iff
-- Module: Mathlib.Algebra.Category.ModuleCat.Differentials.Basic
Goal:
A B : CommRingCat
f : A ⟶ B
M : ModuleCat (↑B : Type u)
α β : KaehlerDifferential f ⟶ M
h :
  ∀ (b : (↑B : Type u)),
    Eq (α := (↑M : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑B : Type u)) ↦
              LinearMap (R := (↑B : Type u)) (RingHom.id (↑B : Type u)) (↑x1 : Type u) (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) α :
            (a : (↑(KaehlerDifferential f) : Type u)) → (↑M : Type u))
          (d b) :
        (↑M : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑B : Type u)) ↦
              LinearMap (R := (↑B : Type u)) (RingHom.id (↑B : Type u)) (↑x1 : Type u) (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) β :
            (a : (↑(KaehlerDifferential f) : Type u)) → (↑M : Type u))
          (d b) :
        (↑M : Type u))
this : ModuleCat.Hom.hom (α - β) = 0
hf : ModuleCat.Hom.hom (α - β) = ModuleCat.Hom.hom 0
⊢ α - β = 0

Tactic:
ext : 1
-- Module: Mathlib.Algebra.Category.ModuleCat.Differentials.Basic
Goal:
A B : CommRingCat
f : A ⟶ B
M : ModuleCat (↑B : Type u)
α β : KaehlerDifferential f ⟶ M
h :
  ∀ (b : (↑B : Type u)),
    Eq (α := (↑M : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑B : Type u)) ↦
              LinearMap (R := (↑B : Type u)) (RingHom.id (↑B : Type u)) (↑x1 : Type u) (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) α :
            (a : (↑(KaehlerDifferential f) : Type u)) → (↑M : Type u))
          (d b) :
        (↑M : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑B : Type u)) ↦
              LinearMap (R := (↑B : Type u)) (RingHom.id (↑B : Type u)) (↑x1 : Type u) (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) β :
            (a : (↑(KaehlerDifferential f) : Type u)) → (↑M : Type u))
          (d b) :
        (↑M : Type u))
this : ModuleCat.Hom.hom (α - β) = 0
⊢ ModuleCat.Hom.hom (α - β) = ModuleCat.Hom.hom 0

Tactic:
this
-- Module: Mathlib.Algebra.Category.ModuleCat.Differentials.Basic
Goal:
A B : CommRingCat
f : A ⟶ B
M : ModuleCat (↑B : Type u)
α β : KaehlerDifferential f ⟶ M
h :
  ∀ (b : (↑B : Type u)),
    Eq (α := (↑M : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑B : Type u)) ↦
              LinearMap (R := (↑B : Type u)) (RingHom.id (↑B : Type u)) (↑x1 : Type u) (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) α :
            (a : (↑(KaehlerDifferential f) : Type u)) → (↑M : Type u))
          (d b) :
        (↑M : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑B : Type u)) ↦
              LinearMap (R := (↑B : Type u)) (RingHom.id (↑B : Type u)) (↑x1 : Type u) (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) β :
            (a : (↑(KaehlerDifferential f) : Type u)) → (↑M : Type u))
          (d b) :
        (↑M : Type u))
this : ModuleCat.Hom.hom (α - β) = 0
⊢ ModuleCat.Hom.hom (α - β) = ModuleCat.Hom.hom 0

Tactic:
exact this
-- Module: Mathlib.Algebra.Category.ModuleCat.Differentials.Basic
Goal:
A B A' B' : CommRingCat
f : A ⟶ B
f' : A' ⟶ B'
g : A ⟶ A'
g' : B ⟶ B'
fac : g ≫ f' = f ≫ g'
this_1 : Algebra (↑A : Type u) (↑B : Type u) := (Hom.hom f).toAlgebra
this_2 : Algebra (↑A' : Type u) (↑B' : Type u) := (Hom.hom f').toAlgebra
this_3 : Algebra (↑A : Type u) (↑A' : Type u) := (Hom.hom g).toAlgebra
this_4 : Algebra (↑B : Type u) (↑B' : Type u) := (Hom.hom g').toAlgebra
this_5 : Algebra (↑A : Type u) (↑B' : Type u) := (Hom.hom (g ≫ f')).toAlgebra
this_6 : IsScalarTower.{u, u, u} (↑A : Type u) (↑A' : Type u) (↑B' : Type u)
this : IsScalarTower.{u, u, u} (↑A : Type u) (↑B : Type u) (↑B' : Type u)
⊢ ∀ (x y : Ω[(↑B : Type u)⁄(↑A : Type u)]),
    (_root_.KaehlerDifferential.map (↑A : Type u) (↑A' : Type u) (↑B : Type u) (↑B' : Type u) :
          (a : Ω[(↑B : Type u)⁄(↑A : Type u)]) → Ω[(↑B' : Type u)⁄(↑A' : Type u)])
        (x + y) =
      HAdd.hAdd (α := (↑((ModuleCat.restrictScalars (Hom.hom g')).obj (KaehlerDifferential f')) : Type u)) (β :=
        (↑((ModuleCat.restrictScalars (Hom.hom g')).obj (KaehlerDifferential f')) : Type u))
        ((_root_.KaehlerDifferential.map (↑A : Type u) (↑A' : Type u) (↑B : Type u) (↑B' : Type u) :
              (a : Ω[(↑B : Type u)⁄(↑A : Type u)]) → Ω[(↑B' : Type u)⁄(↑A' : Type u)])
            x :
          Ω[(↑B' : Type u)⁄(↑A' : Type u)])
        ((_root_.KaehlerDifferential.map (↑A : Type u) (↑A' : Type u) (↑B : Type u) (↑B' : Type u) :
              (a : Ω[(↑B : Type u)⁄(↑A : Type u)]) → Ω[(↑B' : Type u)⁄(↑A' : Type u)])
            y :
          Ω[(↑B' : Type u)⁄(↑A' : Type u)])

Tactic:
simp
-- Module: Mathlib.Algebra.Category.ModuleCat.Differentials.Basic
Goal:
A B A' B' : CommRingCat
f : A ⟶ B
f' : A' ⟶ B'
g : A ⟶ A'
g' : B ⟶ B'
fac : g ≫ f' = f ≫ g'
this_1 : Algebra (↑A : Type u) (↑B : Type u) := (Hom.hom f).toAlgebra
this_2 : Algebra (↑A' : Type u) (↑B' : Type u) := (Hom.hom f').toAlgebra
this_3 : Algebra (↑A : Type u) (↑A' : Type u) := (Hom.hom g).toAlgebra
this_4 : Algebra (↑B : Type u) (↑B' : Type u) := (Hom.hom g').toAlgebra
this_5 : Algebra (↑A : Type u) (↑B' : Type u) := (Hom.hom (g ≫ f')).toAlgebra
this_6 : IsScalarTower.{u, u, u} (↑A : Type u) (↑A' : Type u) (↑B' : Type u)
this : IsScalarTower.{u, u, u} (↑A : Type u) (↑B : Type u) (↑B' : Type u)
⊢ ∀ (m : (↑B : Type u)) (x : Ω[(↑B : Type u)⁄(↑A : Type u)]),
    (_root_.KaehlerDifferential.map (↑A : Type u) (↑A' : Type u) (↑B : Type u) (↑B' : Type u) :
          (a : Ω[(↑B : Type u)⁄(↑A : Type u)]) → Ω[(↑B' : Type u)⁄(↑A' : Type u)])
        (m • x) =
      HSMul.hSMul (α := (↑B : Type u)) (β :=
        (↑((ModuleCat.restrictScalars (Hom.hom g')).obj (KaehlerDifferential f')) : Type u))
        ((RingHom.id (↑B : Type u) : (a : (↑B : Type u)) → (↑B : Type u)) m : (↑B : Type u))
        ((_root_.KaehlerDifferential.map (↑A : Type u) (↑A' : Type u) (↑B : Type u) (↑B' : Type u) :
              (a : Ω[(↑B : Type u)⁄(↑A : Type u)]) → Ω[(↑B' : Type u)⁄(↑A' : Type u)])
            x :
          Ω[(↑B' : Type u)⁄(↑A' : Type u)])

Tactic:
simp
-- Module: Mathlib.Algebra.Category.ModuleCat.Differentials.Basic
Goal:
A B A' B' : CommRingCat
f : A ⟶ B
f' : A' ⟶ B'
g : A ⟶ A'
g' : B ⟶ B'
fac : g ≫ f' = f ≫ g'
b : (↑B : Type u)
algInst : Algebra (↑A : Type u) (↑B : Type u) := (Hom.hom f).toAlgebra
algInst_1 : Algebra (↑A' : Type u) (↑B' : Type u) := (Hom.hom f').toAlgebra
algInst_2 : Algebra (↑A : Type u) (↑A' : Type u) := (Hom.hom g).toAlgebra
algInst_3 : Algebra (↑B : Type u) (↑B' : Type u) := (Hom.hom g').toAlgebra
algInst_4 : Algebra (↑A : Type u) (↑B' : Type u) := ((Hom.hom f').comp (Hom.hom g)).toAlgebra
scalarTowerInst : IsScalarTower.{u, u, u} (↑A : Type u) (↑A' : Type u) (↑B' : Type u) := ⋯
⊢ IsScalarTower.{u, u, u} (↑A : Type u) (↑B : Type u) (↑B' : Type u)

Tactic:
have := IsScalarTower.of_algebraMap_eq' (congrArg Hom.hom fac)
-- Module: Mathlib.Algebra.Category.ModuleCat.Differentials.Basic
Goal:
A B A' B' : CommRingCat
f : A ⟶ B
f' : A' ⟶ B'
g : A ⟶ A'
g' : B ⟶ B'
fac : g ≫ f' = f ≫ g'
b : (↑B : Type u)
algInst : Algebra (↑A : Type u) (↑B : Type u) := (Hom.hom f).toAlgebra
algInst_1 : Algebra (↑A' : Type u) (↑B' : Type u) := (Hom.hom f').toAlgebra
algInst_2 : Algebra (↑A : Type u) (↑A' : Type u) := (Hom.hom g).toAlgebra
algInst_3 : Algebra (↑B : Type u) (↑B' : Type u) := (Hom.hom g').toAlgebra
algInst_4 : Algebra (↑A : Type u) (↑B' : Type u) := ((Hom.hom f').comp (Hom.hom g)).toAlgebra
scalarTowerInst : IsScalarTower.{u, u, u} (↑A : Type u) (↑A' : Type u) (↑B' : Type u) := ⋯
this : IsScalarTower.{u, u, u} (↑A : Type u) (↑B : Type u) (↑B' : Type u)
⊢ Eq (α := (↑((ModuleCat.restrictScalars (Hom.hom g')).obj (KaehlerDifferential f')) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑B : Type u)) ↦
            LinearMap (R := (↑B : Type u)) (RingHom.id (↑B : Type u)) (↑x1 : Type u) (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (map fac) :
          (a : (↑(KaehlerDifferential f) : Type u)) →
            (↑((ModuleCat.restrictScalars (Hom.hom g')).obj (KaehlerDifferential f')) : Type u))
        (d b) :
      (↑((ModuleCat.restrictScalars (Hom.hom g')).obj (KaehlerDifferential f')) : Type u))
    (d
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
              g' :
            (a : (↑B : Type u)) → (↑B' : Type u))
          b) :
      (↑(KaehlerDifferential f') : Type u))

Tactic:
_root_.KaehlerDifferential.map_D A A' B B' b

Premises used: CommRingCat.carrier, Quotient.liftOn', Set.Mem, AddCon.liftOn, Submodule.Quotient.mk, Ideal.Cotangent, List.foldl, KaehlerDifferential, KaehlerDifferential.map_D, FreeAddMonoid.sumAux, ModuleCat.Derivation.d
-- Module: Mathlib.Algebra.Category.ModuleCat.Differentials.Basic
Goal:
A B A' B' : CommRingCat
f : A ⟶ B
f' : A' ⟶ B'
g : A ⟶ A'
g' : B ⟶ B'
fac : g ≫ f' = f ≫ g'
b : (↑B : Type u)
algInst : Algebra (↑A : Type u) (↑B : Type u) := (Hom.hom f).toAlgebra
algInst_1 : Algebra (↑A' : Type u) (↑B' : Type u) := (Hom.hom f').toAlgebra
algInst_2 : Algebra (↑A : Type u) (↑A' : Type u) := (Hom.hom g).toAlgebra
algInst_3 : Algebra (↑B : Type u) (↑B' : Type u) := (Hom.hom g').toAlgebra
algInst_4 : Algebra (↑A : Type u) (↑B' : Type u) := ((Hom.hom f').comp (Hom.hom g)).toAlgebra
scalarTowerInst : IsScalarTower.{u, u, u} (↑A : Type u) (↑A' : Type u) (↑B' : Type u) := ⋯
this : IsScalarTower.{u, u, u} (↑A : Type u) (↑B : Type u) (↑B' : Type u)
⊢ Eq (α := (↑((ModuleCat.restrictScalars (Hom.hom g')).obj (KaehlerDifferential f')) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑B : Type u)) ↦
            LinearMap (R := (↑B : Type u)) (RingHom.id (↑B : Type u)) (↑x1 : Type u) (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (map fac) :
          (a : (↑(KaehlerDifferential f) : Type u)) →
            (↑((ModuleCat.restrictScalars (Hom.hom g')).obj (KaehlerDifferential f')) : Type u))
        (d b) :
      (↑((ModuleCat.restrictScalars (Hom.hom g')).obj (KaehlerDifferential f')) : Type u))
    (d
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
              g' :
            (a : (↑B : Type u)) → (↑B' : Type u))
          b) :
      (↑(KaehlerDifferential f') : Type u))

Tactic:
exact _root_.KaehlerDifferential.map_D A A' B B' b

Premises used: CommRingCat.carrier, KaehlerDifferential.map_D
-- Module: Mathlib.Algebra.Category.ModuleCat.Differentials.Basic
Goal:
A B : CommRingCat
f : A ⟶ B
M : ModuleCat (↑B : Type u)
D : M.Derivation f
b : (↑B : Type u)
this_1 : Algebra (↑A : Type u) (↑B : Type u) := (CommRingCat.Hom.hom f).toAlgebra
this : Module (↑A : Type u) (↑M : Type u) := Module.compHom (↑M : Type u) (CommRingCat.Hom.hom f)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑B : Type u)) ↦
          LinearMap (R := (↑B : Type u)) (RingHom.id (↑B : Type u)) (↑x1 : Type u) (↑x2 : Type u)) (CC := carrier)
          D.desc :
        (a : (↑(CommRingCat.KaehlerDifferential f) : Type u)) → (↑M : Type u))
      (CommRingCat.KaehlerDifferential.d b) =
    D.d b

Tactic:
apply D.liftKaehlerDifferential_comp_D

Premises used: Derivation.liftKaehlerDifferential_comp_D
-- 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
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 ⟶ F.op ⋙ R
d d' : M.Derivation φ
h : d = d'
X : Dᵒᵖ
b : (↑(R.obj X) : Type u)
rw rw₁ :
  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))
        b :
      (↑(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))
        b :
      (↑(M.obj X) : Type v))
⊢ 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))
        b :
      (↑(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))
        b :
      (↑(M.obj X) : Type v))

Tactic:
rw [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
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 ⟶ F.op ⋙ R
d : M.Derivation φ
X : Dᵒᵖ
⊢ 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))
      1)
    0

Tactic:
simpa using d.d_mul (X := X) 1 1

Premises used: PresheafOfModules.Derivation.d_mul, OfNat.ofNat
-- 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 φ
f : M ⟶ N
X : Cᵒᵖ
a : (↑(S.obj X) : Type u)
dsimp :
  Eq (α := (↑(N.obj (Opposite.op (F.obj (Opposite.unop X)))) : Type v))
    ((ModuleCat.Hom.hom (f.app (Opposite.op (F.obj (Opposite.unop X)))) :
          (a : (↑(M.obj (Opposite.op (F.obj (Opposite.unop X)))) : Type v)) →
            (↑(N.obj (Opposite.op (F.obj (Opposite.unop X)))) : Type v))
        (((d.d :
                AddMonoidHom.{u, v} (↑(R.obj (Opposite.op (F.obj (Opposite.unop X)))) : Type u)
                  (↑(M.obj (Opposite.op (F.obj (Opposite.unop X)))) : Type v)) :
              (a : (↑(R.obj (Opposite.op (F.obj (Opposite.unop X)))) : Type u)) →
                (↑(M.obj (Opposite.op (F.obj (Opposite.unop 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 (Opposite.op (F.obj (Opposite.unop X)))) : Type u))
              a) :
          (↑(M.obj (Opposite.op (F.obj (Opposite.unop X)))) : Type v)) :
      (↑(N.obj (Opposite.op (F.obj (Opposite.unop X)))) : Type v))
    (0 : (↑(N.obj (F.op.obj X)) : Type v))
⊢ Eq.{v + 1} (α := (↑(N.obj (F.op.obj X)) : Type v))
    (((AddMonoidHom.comp (LinearMap.toAddMonoidHom (ModuleCat.Hom.hom (f.app (F.op.obj X)))) d.d :
            AddMonoidHom.{u, v} (↑(R.obj (F.op.obj X)) : Type u) (↑(N.obj (F.op.obj X)) : Type v)) :
          (a : (↑(R.obj (F.op.obj X)) : Type u)) → (↑(N.obj (F.op.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)) → (↑((F.op ⋙ R).obj X) : Type u))
          a) :
      (↑(N.obj (F.op.obj X)) : Type v))
    (0 : (↑(N.obj (F.op.obj X)) : Type v))

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
d : M.Derivation φ
f : M ⟶ N
X : Cᵒᵖ
a : (↑(S.obj X) : Type u)
erw :
  Eq (α := (↑(N.obj (Opposite.op (F.obj (Opposite.unop X)))) : Type v))
    ((ModuleCat.Hom.hom (f.app (Opposite.op (F.obj (Opposite.unop X)))) :
          (a : (↑(M.obj (Opposite.op (F.obj (Opposite.unop X)))) : Type v)) →
            (↑(N.obj (Opposite.op (F.obj (Opposite.unop X)))) : Type v))
        0 :
      (↑(N.obj (Opposite.op (F.obj (Opposite.unop X)))) : Type v))
    (0 : (↑(N.obj (F.op.obj X)) : Type v))
⊢ Eq (α := (↑(N.obj (Opposite.op (F.obj (Opposite.unop X)))) : Type v))
    ((ModuleCat.Hom.hom (f.app (Opposite.op (F.obj (Opposite.unop X)))) :
          (a : (↑(M.obj (Opposite.op (F.obj (Opposite.unop X)))) : Type v)) →
            (↑(N.obj (Opposite.op (F.obj (Opposite.unop X)))) : Type v))
        (((d.d :
                AddMonoidHom.{u, v} (↑(R.obj (Opposite.op (F.obj (Opposite.unop X)))) : Type u)
                  (↑(M.obj (Opposite.op (F.obj (Opposite.unop X)))) : Type v)) :
              (a : (↑(R.obj (Opposite.op (F.obj (Opposite.unop X)))) : Type u)) →
                (↑(M.obj (Opposite.op (F.obj (Opposite.unop 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 (Opposite.op (F.obj (Opposite.unop X)))) : Type u))
              a) :
          (↑(M.obj (Opposite.op (F.obj (Opposite.unop X)))) : Type v)) :
      (↑(N.obj (Opposite.op (F.obj (Opposite.unop X)))) : Type v))
    (0 : (↑(N.obj (F.op.obj X)) : Type v))

Tactic:
erw [d_app]

Premises used: PresheafOfModules.Derivation.d_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
d : M.Derivation φ
f : M ⟶ N
X : Cᵒᵖ
a : (↑(S.obj X) : Type u)
rw rw₁ : Eq.{v + 1} (α := (↑(N.obj (Opposite.op (F.obj (Opposite.unop X)))) : Type v)) 0 0
⊢ Eq (α := (↑(N.obj (Opposite.op (F.obj (Opposite.unop X)))) : Type v))
    ((ModuleCat.Hom.hom (f.app (Opposite.op (F.obj (Opposite.unop X)))) :
          (a : (↑(M.obj (Opposite.op (F.obj (Opposite.unop X)))) : Type v)) →
            (↑(N.obj (Opposite.op (F.obj (Opposite.unop X)))) : Type v))
        0 :
      (↑(N.obj (Opposite.op (F.obj (Opposite.unop X)))) : Type v))
    (0 : (↑(N.obj (F.op.obj X)) : Type v))

Tactic:
rw [map_zero]

Premises used: map_zero