awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.ModuleCat.Colimits
Goal:
R_1 : Type w
inst : Ring R_1
J : Type u
inst_1 : Category.{v, u} J
F : J ⥤ ModuleCat.{w', w} R_1
R : Type w
inst_2 : CommRing R
M ι : Type u
inst_3 : AddCommGroup M
inst_4 : Module R M
s : Cocone (J := Discrete ι) (C := ModuleCat.{u, w} R) (Discrete.functor fun (x : ι) ↦ of R M)
f : Cocone.pt (F := Discrete.functor fun (x : ι) ↦ of R M) (finsuppCocone R M ι) ⟶ s.pt
h : ∀ (j : Discrete ι), NatTrans.app (Cocone.ι (finsuppCocone R M ι)) j ≫ f = s.ι.app j
⊢ Hom.hom f =
    Hom.hom
      (↟((Finsupp.lsum R : (a : ι → M →ₗ[R] (↑s.pt : Type u)) → (ι →₀ M) →ₗ[R] (↑s.pt : Type u)) fun (i : ι) ↦
          Hom.hom (s.ι.app { as := i })))

Tactic:
exact Finsupp.lhom_ext' fun i ↦ LinearMap.ext fun x ↦ by simpa using congr($(h ⟨i⟩) (x : M))

Premises used: LinearMap.ext, Finsupp.lhom_ext'
-- Module: Mathlib.Algebra.Category.ModuleCat.Descent
Goal:
A B : Type u
inst : CommRing A
inst_1 : CommRing B
f : A →+* B
hf : f.Flat
⊢ Module.Flat A B

Tactic:
algebraize [f]
-- Module: Mathlib.Algebra.Category.ModuleCat.Descent
Goal:
A B : Type u
inst : CommRing A
inst_1 : CommRing B
f : A →+* B
hf : f.Flat
algInst : Algebra A B := f.toAlgebra
algebraizeInst : Module.Flat A B
change : PreservesFiniteLimits (C := ModuleCat A) (tensorLeft (of A B))
⊢ PreservesFiniteLimits (tensorLeft ((restrictScalars f).obj (of B B)))

Tactic:
change PreservesFiniteLimits <| tensorLeft (ModuleCat.of A B)

Premises used: CategoryTheory.Limits.PreservesFiniteLimits, CategoryTheory.MonoidalCategory.tensorLeft, ModuleCat.of
-- Module: Mathlib.Algebra.Category.ModuleCat.Descent
Goal:
A B : Type u
inst : CommRing A
inst_1 : CommRing B
f : A →+* B
hf : f.Flat
algInst : Algebra A B := f.toAlgebra
algebraizeInst : Module.Flat A B
⊢ PreservesFiniteLimits (C := ModuleCat A) (tensorLeft (of A B))

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Category.ModuleCat.Descent
Goal:
A B : Type u
inst : CommRing A
inst_1 : CommRing B
f : A →+* B
hf : f.Flat
⊢ PreservesFiniteLimits (extendScalars f ⋙ restrictScalars f)

Tactic:
have : PreservesFiniteLimits (extendScalars.{_, _, u} f ⋙ restrictScalars.{_, _, u} f) :=
    ModuleCat.preservesFiniteLimits_tensorLeft_of_ringHomFlat hf
-- Module: Mathlib.Algebra.Category.ModuleCat.Descent
Goal:
A B : Type u
inst : CommRing A
inst_1 : CommRing B
f : A →+* B
hf : f.Flat
this : PreservesFiniteLimits (extendScalars f ⋙ restrictScalars f)
⊢ PreservesFiniteLimits (extendScalars f)

Tactic:
preservesFiniteLimits_of_reflects_of_preserves (extendScalars f) (restrictScalars f)

Premises used: CategoryTheory.Limits.preservesFiniteLimits_of_reflects_of_preserves, ModuleCat.restrictScalars, ModuleCat.extendScalars
-- Module: Mathlib.Algebra.Category.ModuleCat.Descent
Goal:
A B : Type u
inst : CommRing A
inst_1 : CommRing B
f : A →+* B
hf : f.Flat
this : PreservesFiniteLimits (extendScalars f ⋙ restrictScalars f)
⊢ PreservesFiniteLimits (extendScalars f)

Tactic:
exact preservesFiniteLimits_of_reflects_of_preserves (extendScalars f) (restrictScalars f)

Premises used: CategoryTheory.Limits.preservesFiniteLimits_of_reflects_of_preserves, ModuleCat.restrictScalars, ModuleCat.extendScalars
-- Module: Mathlib.Algebra.Category.ModuleCat.Descent
Goal:
A B : Type u
inst : CommRing A
inst_1 : CommRing B
f : A →+* B
hf : f.FaithfullyFlat
⊢ (extendScalars f).ReflectsIsomorphisms

Tactic:
⟨fun {M N} g h ↦ ?_⟩

Premises used: CategoryTheory.Functor.ReflectsIsomorphisms.mk
-- Module: Mathlib.Algebra.Category.ModuleCat.Descent
Goal:
A B : Type u
inst : CommRing A
inst_1 : CommRing B
f : A →+* B
hf : f.FaithfullyFlat
refine : ∀ {M N : ModuleCat A} (g : M ⟶ N) (h : IsIso ((extendScalars f).map g)), IsIso g
⊢ (extendScalars f).ReflectsIsomorphisms

Tactic:
refine ⟨fun {M N} g h ↦ ?_⟩
-- Module: Mathlib.Algebra.Category.ModuleCat.Descent
Goal:
A B : Type u
inst : CommRing A
inst_1 : CommRing B
f : A →+* B
hf : f.FaithfullyFlat
M N : ModuleCat A
g : M ⟶ N
h : IsIso ((extendScalars f).map g)
⊢ Module.FaithfullyFlat A B

Tactic:
algebraize [f]
-- Module: Mathlib.Algebra.Category.ModuleCat.Descent
Goal:
A B : Type u
inst : CommRing A
inst_1 : CommRing B
f : A →+* B
hf : f.FaithfullyFlat
M N : ModuleCat A
g : M ⟶ N
h : IsIso ((extendScalars f).map g)
algInst : Algebra A B := f.toAlgebra
algebraizeInst : Module.FaithfullyFlat A B
rw :
  ∀
    (h :
      Function.Bijective (α := (↑((extendScalars f).obj M) : Type u)) (β := (↑((extendScalars f).obj N) : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat B) ↦ (↑x1 : Type u) →ₗ[B] (↑x2 : Type u)) (CC := carrier)
              ((extendScalars f).map g)) :
          (a : (↑((extendScalars f).obj M) : Type u)) → (↑((extendScalars f).obj N) : Type u))),
    Module.FaithfullyFlat A B →
      Function.Bijective (α := (↑M : Type u)) (β := (↑N : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat A) ↦ (↑x1 : Type u) →ₗ[A] (↑x2 : Type u)) (CC := carrier)
              g) :
          (a : (↑M : Type u)) → (↑N : Type u))
⊢ IsIso g

Tactic:
rw [ConcreteCategory.isIso_iff_bijective] at h ⊢

Premises used: CategoryTheory.ConcreteCategory.isIso_iff_bijective
-- Module: Mathlib.Algebra.Category.ModuleCat.Descent
Goal:
A B : Type u
inst : CommRing A
inst_1 : CommRing B
f : A →+* B
hf : f.FaithfullyFlat
M N : ModuleCat A
g : M ⟶ N
h :
  Function.Bijective (α := (↑((extendScalars f).obj M) : Type u)) (β := (↑((extendScalars f).obj N) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat B) ↦ (↑x1 : Type u) →ₗ[B] (↑x2 : Type u)) (CC := carrier)
          ((extendScalars f).map g)) :
      (a : (↑((extendScalars f).obj M) : Type u)) → (↑((extendScalars f).obj N) : Type u))
algInst : Algebra A B := f.toAlgebra
algebraizeInst : Module.FaithfullyFlat A B
⊢ Function.Bijective (α := TensorProduct A B (↑M : Type u)) (β := TensorProduct A B (↑N : Type u))
    (⇑(LinearMap.lTensor B (Hom.hom g)) : (a : TensorProduct A B (↑M : Type u)) → TensorProduct A B (↑N : Type u))

Tactic:
replace h : Function.Bijective (LinearMap.lTensor B g.hom) := h
-- Module: Mathlib.Algebra.Category.ModuleCat.Descent
Goal:
A B : Type u
inst : CommRing A
inst_1 : CommRing B
f : A →+* B
hf : f.FaithfullyFlat
M N : ModuleCat A
g : M ⟶ N
algInst : Algebra A B := f.toAlgebra
algebraizeInst : Module.FaithfullyFlat A B
h :
  Function.Bijective (α := TensorProduct A B (↑M : Type u)) (β := TensorProduct A B (↑N : Type u))
    (⇑(LinearMap.lTensor B (Hom.hom g)) : (a : TensorProduct A B (↑M : Type u)) → TensorProduct A B (↑N : Type u))
rwa rwa₁ rwa₂ rwa₃ :
  ∀
    (h :
      Function.Bijective (α := (↑M : Type u)) (β := (↑N : Type u))
        (⇑(Hom.hom g) : (a : (↑M : Type u)) → (↑N : Type u))),
    Function.Bijective (α := (↑M : Type u)) (β := (↑N : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat A) ↦ (↑x1 : Type u) →ₗ[A] (↑x2 : Type u)) (CC := carrier)
            g) :
        (a : (↑M : Type u)) → (↑N : Type u))
⊢ Function.Bijective (α := (↑M : Type u)) (β := (↑N : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat A) ↦ (↑x1 : Type u) →ₗ[A] (↑x2 : Type u)) (CC := carrier) g) :
      (a : (↑M : Type u)) → (↑N : Type u))

Tactic:
rwa [Module.FaithfullyFlat.lTensor_bijective_iff_bijective] at h

Premises used: Module.FaithfullyFlat.lTensor_bijective_iff_bijective
-- Module: Mathlib.Algebra.Category.ModuleCat.Descent
Goal:
A B : Type u
inst : CommRing A
inst_1 : CommRing B
f : A →+* B
hf : f.FaithfullyFlat
⊢ PreservesFiniteLimits (extendScalars f)

Tactic:
have := preservesFiniteLimits_extendScalars_of_flat hf.flat
-- Module: Mathlib.Algebra.Category.ModuleCat.Descent
Goal:
A B : Type u
inst : CommRing A
inst_1 : CommRing B
f : A →+* B
hf : f.FaithfullyFlat
this : PreservesFiniteLimits (extendScalars f)
⊢ (extendScalars f).ReflectsIsomorphisms

Tactic:
have := reflectsIsomorphisms_extendScalars_of_faithfullyFlat hf
-- Module: Mathlib.Algebra.Category.ModuleCat.Descent
Goal:
A B : Type u
inst : CommRing A
inst_1 : CommRing B
f : A →+* B
hf : f.FaithfullyFlat
this_1 : PreservesFiniteLimits (extendScalars f)
this : (extendScalars f).ReflectsIsomorphisms
convert_1 : HasEqualizerOfIsCosplitPair (extendScalars f)
convert_2 : PreservesLimitOfIsCosplitPair (extendScalars f)
⊢ ComonadicLeftAdjoint (extendScalars f)

Tactic:
convert!
    Comonad.comonadicOfHasPreservesFSplitEqualizersOfReflectsIsomorphisms
      (extendRestrictScalarsAdj f)
-- Module: Mathlib.Algebra.Category.ModuleCat.Descent
Goal:
A B : Type u
inst : CommRing A
inst_1 : CommRing B
f : A →+* B
hf : f.FaithfullyFlat
this_1 : PreservesFiniteLimits (extendScalars f)
this : (extendScalars f).ReflectsIsomorphisms
⊢ HasEqualizerOfIsCosplitPair (extendScalars f)

Tactic:
⟨inferInstance⟩

Premises used: inferInstance, CategoryTheory.Comonad.HasEqualizerOfIsCosplitPair.mk
-- Module: Mathlib.Algebra.Category.ModuleCat.Descent
Goal:
A B : Type u
inst : CommRing A
inst_1 : CommRing B
f : A →+* B
hf : f.FaithfullyFlat
this_1 : PreservesFiniteLimits (extendScalars f)
this : (extendScalars f).ReflectsIsomorphisms
⊢ HasEqualizerOfIsCosplitPair (extendScalars f)

Tactic:
exact ⟨inferInstance⟩
-- Module: Mathlib.Algebra.Category.ModuleCat.Descent
Goal:
A B : Type u
inst : CommRing A
inst_1 : CommRing B
f : A →+* B
hf : f.FaithfullyFlat
this_1 : PreservesFiniteLimits (extendScalars f)
this : (extendScalars f).ReflectsIsomorphisms
⊢ PreservesLimitOfIsCosplitPair (extendScalars f)

Tactic:
⟨inferInstance⟩

Premises used: inferInstance, CategoryTheory.Comonad.PreservesLimitOfIsCosplitPair.mk
-- Module: Mathlib.Algebra.Category.ModuleCat.Descent
Goal:
A B : Type u
inst : CommRing A
inst_1 : CommRing B
f : A →+* B
hf : f.FaithfullyFlat
this_1 : PreservesFiniteLimits (extendScalars f)
this : (extendScalars f).ReflectsIsomorphisms
⊢ PreservesLimitOfIsCosplitPair (extendScalars f)

Tactic:
exact ⟨inferInstance⟩
-- Module: Mathlib.Algebra.Category.ModuleCat.Differentials.Basic
Goal:
A B : CommRingCat
M : ModuleCat.{v, u} (↑B : Type u)
f : A ⟶ B
d : (↑B : Type u) → (↑M : Type v)
d_add : ∀ (b b' : (↑B : Type u)), d (b + b') = d b + d b'
d_mul : ∀ (b b' : (↑B : Type u)), d (b * b') = b • d b' + b' • d b
d_map :
  ∀ (a : (↑A : Type u)),
    d
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) f :
            (a : (↑A : Type u)) → (↑B : Type u))
          a) =
      0
this_1 : Algebra (↑A : Type u) (↑B : Type u) := (CommRingCat.Hom.hom f).toAlgebra
this : Module.{u, v} (↑A : Type u) (↑M : Type v) := Module.compHom (↑M : Type v) (CommRingCat.Hom.hom f)
a : (↑A : Type u)
b : (↑B : Type u)
dsimp : d (a • b) = a • d b
⊢ d (a • b) =
    HSMul.hSMul (α := (↑A : Type u))
      ((RingHom.id (↑A : Type u) : (a : (↑A : Type u)) → (↑A : Type u)) a : (↑A : Type u)) (d b)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Category.ModuleCat.Differentials.Basic
Goal:
A B : CommRingCat
M : ModuleCat.{v, u} (↑B : Type u)
f : A ⟶ B
d : (↑B : Type u) → (↑M : Type v)
d_add : ∀ (b b' : (↑B : Type u)), d (b + b') = d b + d b'
d_mul : ∀ (b b' : (↑B : Type u)), d (b * b') = b • d b' + b' • d b
d_map :
  ∀ (a : (↑A : Type u)),
    d
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) f :
            (a : (↑A : Type u)) → (↑B : Type u))
          a) =
      0
this_1 : Algebra (↑A : Type u) (↑B : Type u) := (CommRingCat.Hom.hom f).toAlgebra
this : Module.{u, v} (↑A : Type u) (↑M : Type v) := Module.compHom (↑M : Type v) (CommRingCat.Hom.hom f)
a : (↑A : Type u)
b : (↑B : Type u)
rw :
  HSMul.hSMul (α := (↑B : Type u)) ((CommRingCat.Hom.hom f : (a : (↑A : Type u)) → (↑B : Type u)) a : (↑B : Type u))
      (d b) =
    a • d b
⊢ d (a • b) = a • d b

Tactic:
rw [RingHom.smul_toAlgebra, d_mul, d_map, smul_zero, add_zero]

Premises used: smul_zero, RingHom.smul_toAlgebra, add_zero
-- Module: Mathlib.Algebra.Category.ModuleCat.Differentials.Basic
Goal:
A B : CommRingCat
M : ModuleCat.{v, u} (↑B : Type u)
f : A ⟶ B
d : (↑B : Type u) → (↑M : Type v)
d_add : ∀ (b b' : (↑B : Type u)), d (b + b') = d b + d b'
d_mul : ∀ (b b' : (↑B : Type u)), d (b * b') = b • d b' + b' • d b
d_map :
  ∀ (a : (↑A : Type u)),
    d
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) f :
            (a : (↑A : Type u)) → (↑B : Type u))
          a) =
      0
this_1 : Algebra (↑A : Type u) (↑B : Type u) := (CommRingCat.Hom.hom f).toAlgebra
this : Module.{u, v} (↑A : Type u) (↑M : Type v) := Module.compHom (↑M : Type v) (CommRingCat.Hom.hom f)
a : (↑A : Type u)
b : (↑B : Type u)
⊢ HSMul.hSMul (α := (↑B : Type u)) ((CommRingCat.Hom.hom f : (a : (↑A : Type u)) → (↑B : Type u)) a : (↑B : Type u))
      (d b) =
    a • d b

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Differentials.Basic
Goal:
A B : CommRingCat
M : ModuleCat.{v, u} (↑B : Type u)
f : A ⟶ B
d : (↑B : Type u) → (↑M : Type v)
d_add : ∀ (b b' : (↑B : Type u)), d (b + b') = d b + d b'
d_mul : ∀ (b b' : (↑B : Type u)), d (b * b') = b • d b' + b' • d b
d_map :
  ∀ (a : (↑A : Type u)),
    d
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) f :
            (a : (↑A : Type u)) → (↑B : Type u))
          a) =
      0
this_1 : Algebra (↑A : Type u) (↑B : Type u) := (CommRingCat.Hom.hom f).toAlgebra
this : Module.{u, v} (↑A : Type u) (↑M : Type v) := Module.compHom (↑M : Type v) (CommRingCat.Hom.hom f)
dsimp : d 1 = 0
⊢ Eq.{v + 1} (α := (↑M : Type v))
    ((({ toFun := d, map_add' := d_add, map_smul' := ⋯ } :
          LinearMap.{u, u, u, v} (R := (↑A : Type u)) (RingHom.id (↑A : Type u)) (↑B : Type u) (↑M : Type v)) :
        (a : (↑B : Type u)) → (↑M : Type v))
      1)
    0

Tactic:
dsimp
-- Module: Mathlib.Algebra.Category.ModuleCat.Differentials.Basic
Goal:
A B : CommRingCat
M : ModuleCat.{v, u} (↑B : Type u)
f : A ⟶ B
d : (↑B : Type u) → (↑M : Type v)
d_add : ∀ (b b' : (↑B : Type u)), d (b + b') = d b + d b'
d_mul : ∀ (b b' : (↑B : Type u)), d (b * b') = b • d b' + b' • d b
d_map :
  ∀ (a : (↑A : Type u)),
    d
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) f :
            (a : (↑A : Type u)) → (↑B : Type u))
          a) =
      0
this_1 : Algebra (↑A : Type u) (↑B : Type u) := (CommRingCat.Hom.hom f).toAlgebra
this : Module.{u, v} (↑A : Type u) (↑M : Type v) := Module.compHom (↑M : Type v) (CommRingCat.Hom.hom f)
rw : d ((CommRingCat.Hom.hom f : (a : (↑A : Type u)) → (↑B : Type u)) 1) = 0
rw₁ rw₂ : Eq.{v + 1} (α := (↑M : Type v)) 0 0
⊢ d 1 = 0

Tactic:
rw [← f.hom.map_one, d_map]

Premises used: CommRingCat.Hom.hom, RingHom.map_one
-- Module: Mathlib.Algebra.Category.ModuleCat.Differentials.Basic
Goal:
A B : CommRingCat
M : ModuleCat.{v, u} (↑B : Type u)
f : A ⟶ B
D : M.Derivation f
b b' : (↑B : Type u)
⊢ D.d (b + b') = D.d b + D.d b'

Tactic:
simp [d]

Premises used: ModuleCat.Derivation.d
-- Module: Mathlib.Algebra.Category.ModuleCat.Differentials.Basic
Goal:
A B : CommRingCat
M : ModuleCat.{v, u} (↑B : Type u)
f : A ⟶ B
D : M.Derivation f
b b' : (↑B : Type u)
⊢ D.d (b * b') = b • D.d b' + b' • D.d b

Tactic:
simp [d]

Premises used: ModuleCat.Derivation.d
-- Module: Mathlib.Algebra.Category.ModuleCat.Differentials.Basic
Goal:
A B : CommRingCat
M : ModuleCat.{v, u} (↑B : Type u)
f : A ⟶ B
D : M.Derivation f
a : (↑A : Type u)
⊢ D.d
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) f :
          (a : (↑A : Type u)) → (↑B : Type u))
        a) =
    0

Tactic:
letI := f.hom.toAlgebra
  letI := Module.compHom M f.hom
  D.map_algebraMap a

Premises used: Derivation.map_algebraMap, 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'
this : Algebra (↑A : Type u) (↑B : Type u) := (Hom.hom f).toAlgebra
⊢ ∀ (b b' : (↑B : Type u)),
    (fun (b : (↑B : Type u)) ↦
          ((_root_.KaehlerDifferential.D (↑A : Type u) (↑B : Type u) :
                (a : (↑B : Type u)) → Ω[(↑B : Type u)⁄(↑A : Type u)])
              b :
            Ω[(↑B : Type u)⁄(↑A : Type u)]))
        (b + b') =
      HAdd.hAdd (α := (↑(KaehlerDifferential f) : Type u))
        ((fun (b : (↑B : Type u)) ↦
            ((_root_.KaehlerDifferential.D (↑A : Type u) (↑B : Type u) :
                  (a : (↑B : Type u)) → Ω[(↑B : Type u)⁄(↑A : Type u)])
                b :
              Ω[(↑B : Type u)⁄(↑A : Type u)]))
          b)
        ((fun (b : (↑B : Type u)) ↦
            ((_root_.KaehlerDifferential.D (↑A : Type u) (↑B : Type u) :
                  (a : (↑B : Type u)) → Ω[(↑B : Type u)⁄(↑A : Type u)])
                b :
              Ω[(↑B : Type u)⁄(↑A : Type u)]))
          b')

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 : Algebra (↑A : Type u) (↑B : Type u) := (Hom.hom f).toAlgebra
⊢ ∀ (b b' : (↑B : Type u)),
    (fun (b : (↑B : Type u)) ↦
          ((_root_.KaehlerDifferential.D (↑A : Type u) (↑B : Type u) :
                (a : (↑B : Type u)) → Ω[(↑B : Type u)⁄(↑A : Type u)])
              b :
            Ω[(↑B : Type u)⁄(↑A : Type u)]))
        (b * b') =
      HSMul.hSMul (β := (↑(KaehlerDifferential f) : Type u)) b
          ((fun (b : (↑B : Type u)) ↦
              ((_root_.KaehlerDifferential.D (↑A : Type u) (↑B : Type u) :
                    (a : (↑B : Type u)) → Ω[(↑B : Type u)⁄(↑A : Type u)])
                  b :
                Ω[(↑B : Type u)⁄(↑A : Type u)]))
            b') +
        HSMul.hSMul (β := (↑(KaehlerDifferential f) : Type u)) b'
          ((fun (b : (↑B : Type u)) ↦
              ((_root_.KaehlerDifferential.D (↑A : Type u) (↑B : Type u) :
                    (a : (↑B : Type u)) → Ω[(↑B : Type u)⁄(↑A : Type u)])
                  b :
                Ω[(↑B : Type u)⁄(↑A : Type u)]))
            b)

Tactic:
simp
-- 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))
rw : α - β = 0
⊢ α = β

Tactic:
rw [← sub_eq_zero]

Premises used: sub_eq_zero
-- 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))
rw :
  Set.range (ι := (↑B : Type u))
      (⇑(_root_.KaehlerDifferential.D (↑A : Type u) (↑B : Type u)) :
        (a : (↑B : Type u)) → Ω[(↑B : Type u)⁄(↑A : Type u)]) ⊆
    (↑(ModuleCat.Hom.hom (α - β)).ker : Set Ω[(↑B : Type u)⁄(↑A : Type u)])
⊢ ⊤ ≤ (ModuleCat.Hom.hom (α - β)).ker

Tactic:
rw [← KaehlerDifferential.span_range_derivation, Submodule.span_le]

Premises used: KaehlerDifferential.span_range_derivation, Submodule.span_le
-- 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))
y : (↑B : Type u)
rw :
  Eq (α := (↑M : Type u))
    ((ModuleCat.Hom.hom α : (a : Ω[(↑B : Type u)⁄(↑A : Type u)]) → (↑M : Type u))
        ((_root_.KaehlerDifferential.D (↑A : Type u) (↑B : Type u) :
              (a : (↑B : Type u)) → Ω[(↑B : Type u)⁄(↑A : Type u)])
            y :
          Ω[(↑B : Type u)⁄(↑A : Type u)]) :
      (↑M : Type u))
    ((ModuleCat.Hom.hom β : (a : Ω[(↑B : Type u)⁄(↑A : Type u)]) → (↑M : Type u))
        ((_root_.KaehlerDifferential.D (↑A : Type u) (↑B : Type u) :
              (a : (↑B : Type u)) → Ω[(↑B : Type u)⁄(↑A : Type u)])
            y :
          Ω[(↑B : Type u)⁄(↑A : Type u)]) :
      (↑M : Type u))
⊢ Membership.mem (α := Ω[(↑B : Type u)⁄(↑A : Type u)])
    (↑(ModuleCat.Hom.hom (α - β)).ker : Set Ω[(↑B : Type u)⁄(↑A : Type u)])
    ((_root_.KaehlerDifferential.D (↑A : Type u) (↑B : Type u) : (a : (↑B : Type u)) → Ω[(↑B : Type u)⁄(↑A : Type u)])
        y :
      Ω[(↑B : Type u)⁄(↑A : Type u)])

Tactic:
rw [SetLike.mem_coe, LinearMap.mem_ker, ModuleCat.hom_sub, LinearMap.sub_apply, sub_eq_zero]

Premises used: sub_eq_zero, LinearMap.mem_ker, SetLike.mem_coe, LinearMap.sub_apply, ModuleCat.hom_sub
-- 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))
y : (↑B : Type u)
⊢ Eq (α := (↑M : Type u))
    ((ModuleCat.Hom.hom α : (a : Ω[(↑B : Type u)⁄(↑A : Type u)]) → (↑M : Type u))
        ((_root_.KaehlerDifferential.D (↑A : Type u) (↑B : Type u) :
              (a : (↑B : Type u)) → Ω[(↑B : Type u)⁄(↑A : Type u)])
            y :
          Ω[(↑B : Type u)⁄(↑A : Type u)]) :
      (↑M : Type u))
    ((ModuleCat.Hom.hom β : (a : Ω[(↑B : Type u)⁄(↑A : Type u)]) → (↑M : Type u))
        ((_root_.KaehlerDifferential.D (↑A : Type u) (↑B : Type u) :
              (a : (↑B : Type u)) → Ω[(↑B : Type u)⁄(↑A : Type u)])
            y :
          Ω[(↑B : Type u)⁄(↑A : Type u)]) :
      (↑M : Type u))

Tactic:
apply h