awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Differentials.Basic (hypothesis)
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))
⊢ α - β = 0
have this : ⊤ ≤ (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
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Differentials.Basic (hypothesis)
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
⊢ α - β = 0
have this₁ : ModuleCat.Hom.hom (α - β) = 0
Tactic: rw [top_le_iff, LinearMap.ker_eq_top] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Differentials.Basic (goal)
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
⊢ α - β = 0
have hf : ModuleCat.Hom.hom (α - β) = ModuleCat.Hom.hom 0
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Differentials.Basic (hypothesis)
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) := ⋯
⊢ 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))
have this : IsScalarTower.{u, u, u} (↑A : Type u) (↑B : Type u) (↑B' : Type u)
Tactic: have := IsScalarTower.of_algebraMap_eq' (congrArg Hom.hom fac)
-- 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
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)
⊢ 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))
have 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))
Tactic: rw [h]
-- 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 φ
f : M ⟶ N
X : Cᵒᵖ
a : (↑(S.obj X) : Type u)
⊢ 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))
have 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))
Tactic: dsimp
-- 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 φ
f : M ⟶ N
X : Cᵒᵖ
a : (↑(S.obj X) : Type u)
⊢ 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))
have 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))
Tactic: erw [d_app]
-- 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 φ
f : M ⟶ N
X : Cᵒᵖ
a : (↑(S.obj X) : Type u)
⊢ 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))
have rw : Eq.{v + 1} (α := (↑(N.obj (Opposite.op (F.obj (Opposite.unop X)))) : Type v)) 0 0
Tactic: rw [map_zero]
-- 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₁ 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'
⊢ h₁ = h₂
have 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₂
Tactic: cases h₁
Cleared hypotheses: h₁, this
-- 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₁ h₂ : d.Universal
⊢ h₁ = h₂
have 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'
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
-- 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₁ 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₁.desc d' = h₂.desc d'
have h : d.postcomp (h₁.desc d') = d.postcomp (h₂.desc d')
Tactic: apply h₁.postcomp_injective
-- 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 : Dᵒᵖ
⊢ 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))
have dsimp : CommRingCat.KaehlerDifferential.map sorry =
  Iso.inv
    (ModuleCat.restrictScalarsId'App (CommRingCat.Hom.hom (R.map (𝟙 x))) sorry (CommRingCat.KaehlerDifferential (φ'.app x)))
Tactic: dsimp
-- 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 : Dᵒᵖ
⊢ CommRingCat.KaehlerDifferential.map ⋯ =
    Iso.inv
      (ModuleCat.restrictScalarsId'App (CommRingCat.Hom.hom (R.map (𝟙 x))) ⋯
        (CommRingCat.KaehlerDifferential (φ'.app x)))
have 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 sorry) :
          (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))) sorry
                (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: ext
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.EpiMono (goal)
Goal:
R : Type u
inst : Ring R
X Y : ModuleCat.{v, u} R
f : X ⟶ Y
⊢ Mono f ↔
    Function.Injective (α := (↑X : Type v)) (β := (↑Y : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
            carrier) f) :
        (a : (↑X : Type v)) → (↑Y : Type v))
have rw : (Hom.hom f).ker = ⊥ ↔
  Function.Injective (α := (↑X : Type v)) (β := (↑Y : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
          carrier) f) :
      (a : (↑X : Type v)) → (↑Y : Type v))
Tactic: rw [mono_iff_ker_eq_bot, LinearMap.ker_eq_bot]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.EpiMono (goal)
Goal:
R : Type u
inst : Ring R
X Y : ModuleCat.{v, u} R
f : X ⟶ Y
rw :
  (Hom.hom f).ker = ⊥ ↔
    Function.Injective (α := (↑X : Type v)) (β := (↑Y : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
            carrier) f) :
        (a : (↑X : Type v)) → (↑Y : Type v))
⊢ Mono f ↔
    Function.Injective (α := (↑X : Type v)) (β := (↑Y : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
            carrier) f) :
        (a : (↑X : Type v)) → (↑Y : Type v))
have rw₁ : Function.Injective (α := (↑X : Type v)) (β := (↑Y : Type v)) (⇑(Hom.hom f) : (a : (↑X : Type v)) → (↑Y : Type v)) ↔
  Function.Injective (α := (↑X : Type v)) (β := (↑Y : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
          carrier) f) :
      (a : (↑X : Type v)) → (↑Y : Type v))
Tactic: rw [mono_iff_ker_eq_bot, LinearMap.ker_eq_bot]