awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
K : Type u_1
L : Type u_2
A : Type u_3
inst : CommRing K
inst_1 : Field L
inst_2 : CommRing A
inst_3 : IsJacobsonRing K
inst_4 : IsNoetherianRing K
inst_5 : Nontrivial A
f : K →+* L
g : L →+* A
hfg : (g.comp f).FiniteType
algInst : Algebra K L := f.toAlgebra
algInst_1 : Algebra K A := (g.comp f).toAlgebra
algebraizeInst : Algebra.FiniteType K A
⊢ f.Finite

Tactic:
exact finite_of_algHom_finiteType_of_isJacobsonRing ⟨g, fun _ ↦ rfl⟩
-- Module: Mathlib.RingTheory.Jacobson.Semiprimary
Goal:
R : Type u_1
M : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsSimpleModule R M
⊢ Eq (α := Submodule R M) (Module.jacobson R M) ⊥

Tactic:
le_bot_iff.mp <| sInf_le isCoatom_bot

Premises used: le_bot_iff, isCoatom_bot, sInf_le, Iff.mp
-- Module: Mathlib.RingTheory.Jacobson.Semiprimary
Goal:
R : Type u_1
M : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsSemisimpleModule R M
⊢ Eq (α := Submodule R M) (Module.jacobson R M) ⊥

Tactic:
have ⟨s, e, simple⟩ := isSemisimpleModule_iff_exists_linearEquiv_dfinsupp.mp ‹_›
  let f : M →ₗ[R] ∀ m : s, m.1 := (LinearMap.pi DFinsupp.lapply).comp e.toLinearMap
  Module.jacobson_eq_bot_of_injective f (DFinsupp.injective_pi_lapply (R := R).comp e.injective)
    (Module.jacobson_pi_eq_bot _ _ fun i ↦ IsSimpleModule.jacobson_eq_bot R _)

Premises used: _private.0.IsSemisimpleModule.jacobson_eq_bot.match_1, Module.jacobson, DFinsupp.injective_pi_lapply, Membership.mem, Subtype, Bot.bot, Module.jacobson_pi_eq_bot, IsSimpleModule.jacobson_eq_bot, Module.jacobson_eq_bot_of_injective, LinearMap.pi, LinearMap.comp, DFinsupp.lapply, LinearEquiv.toLinearMap, Function.Injective.comp, Iff.mp, LinearEquiv.injective, Subtype.val, Eq, isSemisimpleModule_iff_exists_linearEquiv_dfinsupp
-- Module: Mathlib.RingTheory.Jacobson.Semiprimary
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsSemisimpleRing R
⊢ Eq (α := Ideal R) (Ring.jacobson R) ⊥

Tactic:
IsSemisimpleModule.jacobson_eq_bot R R

Premises used: IsSemisimpleModule.jacobson_eq_bot
-- Module: Mathlib.RingTheory.Jacobson.Semiprimary
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst : Ring R
inst_1 : Ring R₂
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
inst_7 : IsSemisimpleModule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
simp_rw : Submodule.comap f ⊥ ≤ f.ker
simp_rw₁ : Submodule.comap f ⊥ ≤ Submodule.comap f ⊥
⊢ Submodule.comap f (Module.jacobson R₂ M₂) ≤ f.ker

Tactic:
simp_rw [jacobson_eq_bot, LinearMap.ker, le_rfl]

Premises used: le_rfl, LinearMap.ker, IsSemisimpleModule.jacobson_eq_bot
-- Module: Mathlib.RingTheory.Jacobson.Semiprimary
Goal:
R : Type u_1
M : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsSemisimpleModule R M
r : R
hr : Membership.mem (γ := Submodule R R) (Ring.jacobson R) r
m : M
⊢ Membership.mem (γ := Submodule R R) (Submodule.comap (LinearMap.toSpanSingleton R M m) (Module.jacobson R M)) r

Tactic:
have := Module.le_comap_jacobson (LinearMap.toSpanSingleton R M m) hr
-- Module: Mathlib.RingTheory.Jacobson.Semiprimary
Goal:
R : Type u_1
M : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsSemisimpleModule R M
r : R
hr : Membership.mem (γ := Submodule R R) (Ring.jacobson R) r
m : M
this : Membership.mem (γ := Submodule R R) (Submodule.comap (LinearMap.toSpanSingleton R M m) (Module.jacobson R M)) r
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (this : Membership.mem (γ := Submodule R R) (Submodule.comap (LinearMap.toSpanSingleton R M m) ⊥) r), r • m = 0
⊢ r • m = 0

Tactic:
rwa [jacobson_eq_bot] at this

Premises used: IsSemisimpleModule.jacobson_eq_bot
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
a : S
⊢ Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) (HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] a) (a ⊗ₜ[R] 1))

Tactic:
simp [RingHom.mem_ker]

Premises used: RingHom.mem_ker
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_1
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
D : Derivation R S M
s t : S
⊢ (D.tensorProductTo : (a : S ⊗[R] S) → M) (s ⊗ₜ[R] t) = HSMul.hSMul (β := M) s ((D : (a : S) → M) t : M)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_1
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
D : Derivation R S M
x y : S ⊗[R] S
⊢ (D.tensorProductTo : (a : S ⊗[R] S) → M) (x * y) =
    HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) x : S)
        ((D.tensorProductTo : (a : S ⊗[R] S) → M) y : M) +
      HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) y : S)
        ((D.tensorProductTo : (a : S ⊗[R] S) → M) x : M)

Tactic:
TensorProduct.induction_on x ?_ ?_ ?_

Premises used: TensorProduct.induction_on
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_1
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
D : Derivation R S M
x y : S ⊗[R] S
refine_1 :
  (D.tensorProductTo : (a : S ⊗[R] S) → M) (0 * y) =
    HSMul.hSMul.{v, u_1, u_1} (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) 0 : S)
        ((D.tensorProductTo : (a : S ⊗[R] S) → M) y : M) +
      HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) y : S)
        ((D.tensorProductTo : (a : S ⊗[R] S) → M) 0 : M)
refine_2 :
  ∀ (x y_1 : S),
    (D.tensorProductTo : (a : S ⊗[R] S) → M) (x ⊗ₜ[R] y_1 * y) =
      HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) (x ⊗ₜ[R] y_1) : S)
          ((D.tensorProductTo : (a : S ⊗[R] S) → M) y : M) +
        HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) y : S)
          ((D.tensorProductTo : (a : S ⊗[R] S) → M) (x ⊗ₜ[R] y_1) : M)
refine_3 :
  ∀ (x y_1 : S ⊗[R] S),
    (D.tensorProductTo : (a : S ⊗[R] S) → M) (x * y) =
        HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) x : S)
            ((D.tensorProductTo : (a : S ⊗[R] S) → M) y : M) +
          HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) y : S)
            ((D.tensorProductTo : (a : S ⊗[R] S) → M) x : M) →
      (D.tensorProductTo : (a : S ⊗[R] S) → M) (y_1 * y) =
          HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) y_1 : S)
              ((D.tensorProductTo : (a : S ⊗[R] S) → M) y : M) +
            HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) y : S)
              ((D.tensorProductTo : (a : S ⊗[R] S) → M) y_1 : M) →
        (D.tensorProductTo : (a : S ⊗[R] S) → M) ((x + y_1) * y) =
          HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) (x + y_1) : S)
              ((D.tensorProductTo : (a : S ⊗[R] S) → M) y : M) +
            HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) y : S)
              ((D.tensorProductTo : (a : S ⊗[R] S) → M) (x + y_1) : M)
⊢ (D.tensorProductTo : (a : S ⊗[R] S) → M) (x * y) =
    HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) x : S)
        ((D.tensorProductTo : (a : S ⊗[R] S) → M) y : M) +
      HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) y : S)
        ((D.tensorProductTo : (a : S ⊗[R] S) → M) x : M)

Tactic:
refine TensorProduct.induction_on x ?_ ?_ ?_
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_1
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
D : Derivation R S M
x y : S ⊗[R] S
refine_1 :
  (D.tensorProductTo : (a : S ⊗[R] S) → M) 0 =
    HSMul.hSMul.{v, u_1, u_1} (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) 0 : S)
        ((D.tensorProductTo : (a : S ⊗[R] S) → M) y : M) +
      HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) y : S)
        ((D.tensorProductTo : (a : S ⊗[R] S) → M) 0 : M)
refine_1₁ :
  0 =
    HSMul.hSMul.{v, u_1, u_1} (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) 0 : S)
        ((D.tensorProductTo : (a : S ⊗[R] S) → M) y : M) +
      HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) y : S) 0
refine_1₂ :
  0 =
    HSMul.hSMul.{v, u_1, u_1} (α := S) (β := M) 0 ((D.tensorProductTo : (a : S ⊗[R] S) → M) y : M) +
      HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) y : S) 0
refine_1₃ : 0 = 0 + HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) y : S) 0
refine_1₄ : 0 = HAdd.hAdd (α := M) 0 0
refine_1₅ refine_1₆ : Eq.{u_1 + 1} (α := M) 0 0
⊢ (D.tensorProductTo : (a : S ⊗[R] S) → M) (0 * y) =
    HSMul.hSMul.{v, u_1, u_1} (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) 0 : S)
        ((D.tensorProductTo : (a : S ⊗[R] S) → M) y : M) +
      HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) y : S)
        ((D.tensorProductTo : (a : S ⊗[R] S) → M) 0 : M)

Tactic:
rw [zero_mul, map_zero, map_zero, zero_smul, smul_zero, add_zero]

Premises used: MulZeroClass.zero_mul, smul_zero, map_zero, zero_smul, add_zero
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_1
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
D : Derivation R S M
x y : S ⊗[R] S
x₁ x₂ : S
⊢ (D.tensorProductTo : (a : S ⊗[R] S) → M) (x₁ ⊗ₜ[R] x₂ * y) =
    HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) (x₁ ⊗ₜ[R] x₂) : S)
        ((D.tensorProductTo : (a : S ⊗[R] S) → M) y : M) +
      HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) y : S)
        ((D.tensorProductTo : (a : S ⊗[R] S) → M) (x₁ ⊗ₜ[R] x₂) : M)

Tactic:
TensorProduct.induction_on y ?_ ?_ ?_

Premises used: TensorProduct.induction_on
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_1
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
D : Derivation R S M
x y : S ⊗[R] S
x₁ x₂ : S
refine_2 :
  (D.tensorProductTo : (a : S ⊗[R] S) → M) (HMul.hMul (α := S ⊗[R] S) (x₁ ⊗ₜ[R] x₂) 0) =
    HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) (x₁ ⊗ₜ[R] x₂) : S)
        ((D.tensorProductTo : (a : S ⊗[R] S) → M) 0 : M) +
      HSMul.hSMul.{v, u_1, u_1} (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) 0 : S)
        ((D.tensorProductTo : (a : S ⊗[R] S) → M) (x₁ ⊗ₜ[R] x₂) : M)
refine_2₁ :
  ∀ (x y : S),
    (D.tensorProductTo : (a : S ⊗[R] S) → M) (HMul.hMul (α := S ⊗[R] S) (x₁ ⊗ₜ[R] x₂) (x ⊗ₜ[R] y)) =
      HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) (x₁ ⊗ₜ[R] x₂) : S)
          ((D.tensorProductTo : (a : S ⊗[R] S) → M) (x ⊗ₜ[R] y) : M) +
        HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) (x ⊗ₜ[R] y) : S)
          ((D.tensorProductTo : (a : S ⊗[R] S) → M) (x₁ ⊗ₜ[R] x₂) : M)
refine_2₂ :
  ∀ (x y : S ⊗[R] S),
    (D.tensorProductTo : (a : S ⊗[R] S) → M) (x₁ ⊗ₜ[R] x₂ * x) =
        HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) (x₁ ⊗ₜ[R] x₂) : S)
            ((D.tensorProductTo : (a : S ⊗[R] S) → M) x : M) +
          HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) x : S)
            ((D.tensorProductTo : (a : S ⊗[R] S) → M) (x₁ ⊗ₜ[R] x₂) : M) →
      (D.tensorProductTo : (a : S ⊗[R] S) → M) (x₁ ⊗ₜ[R] x₂ * y) =
          HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) (x₁ ⊗ₜ[R] x₂) : S)
              ((D.tensorProductTo : (a : S ⊗[R] S) → M) y : M) +
            HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) y : S)
              ((D.tensorProductTo : (a : S ⊗[R] S) → M) (x₁ ⊗ₜ[R] x₂) : M) →
        (D.tensorProductTo : (a : S ⊗[R] S) → M) (x₁ ⊗ₜ[R] x₂ * (x + y)) =
          HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) (x₁ ⊗ₜ[R] x₂) : S)
              ((D.tensorProductTo : (a : S ⊗[R] S) → M) (x + y) : M) +
            HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) (x + y) : S)
              ((D.tensorProductTo : (a : S ⊗[R] S) → M) (x₁ ⊗ₜ[R] x₂) : M)
⊢ (D.tensorProductTo : (a : S ⊗[R] S) → M) (x₁ ⊗ₜ[R] x₂ * y) =
    HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) (x₁ ⊗ₜ[R] x₂) : S)
        ((D.tensorProductTo : (a : S ⊗[R] S) → M) y : M) +
      HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) y : S)
        ((D.tensorProductTo : (a : S ⊗[R] S) → M) (x₁ ⊗ₜ[R] x₂) : M)

Tactic:
refine TensorProduct.induction_on y ?_ ?_ ?_
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_1
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
D : Derivation R S M
x y : S ⊗[R] S
x₁ x₂ : S
refine_2 :
  (D.tensorProductTo : (a : S ⊗[R] S) → M) 0 =
    HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) (x₁ ⊗ₜ[R] x₂) : S)
        ((D.tensorProductTo : (a : S ⊗[R] S) → M) 0 : M) +
      HSMul.hSMul.{v, u_1, u_1} (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) 0 : S)
        ((D.tensorProductTo : (a : S ⊗[R] S) → M) (x₁ ⊗ₜ[R] x₂) : M)
refine_2₁ :
  0 =
    HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) (x₁ ⊗ₜ[R] x₂) : S) 0 +
      HSMul.hSMul.{v, u_1, u_1} (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) 0 : S)
        ((D.tensorProductTo : (a : S ⊗[R] S) → M) (x₁ ⊗ₜ[R] x₂) : M)
refine_2₂ :
  0 =
    HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) (x₁ ⊗ₜ[R] x₂) : S) 0 +
      HSMul.hSMul.{v, u_1, u_1} (α := S) (β := M) 0 ((D.tensorProductTo : (a : S ⊗[R] S) → M) (x₁ ⊗ₜ[R] x₂) : M)
refine_2₃ : 0 = HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) (x₁ ⊗ₜ[R] x₂) : S) 0 + 0
refine_2₄ : 0 = HAdd.hAdd (α := M) 0 0
refine_2₅ refine_2₆ : Eq.{u_1 + 1} (α := M) 0 0
⊢ (D.tensorProductTo : (a : S ⊗[R] S) → M) (HMul.hMul (α := S ⊗[R] S) (x₁ ⊗ₜ[R] x₂) 0) =
    HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) (x₁ ⊗ₜ[R] x₂) : S)
        ((D.tensorProductTo : (a : S ⊗[R] S) → M) 0 : M) +
      HSMul.hSMul.{v, u_1, u_1} (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) 0 : S)
        ((D.tensorProductTo : (a : S ⊗[R] S) → M) (x₁ ⊗ₜ[R] x₂) : M)

Tactic:
rw [mul_zero, map_zero, map_zero, zero_smul, smul_zero, add_zero]

Premises used: smul_zero, map_zero, MulZeroClass.mul_zero, zero_smul, add_zero
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_1
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
D : Derivation R S M
x_1 y_1 : S ⊗[R] S
x₁ x₂ x y : S
refine_2 :
  (x₁ * x) • (HSMul.hSMul (β := M) x₂ ((D : (a : S) → M) y : M) + HSMul.hSMul (β := M) y ((D : (a : S) → M) x₂ : M)) =
    (x₁ * x₂) • HSMul.hSMul (β := M) x ((D : (a : S) → M) y : M) +
      (x * y) • HSMul.hSMul (β := M) x₁ ((D : (a : S) → M) x₂ : M)
⊢ HSMul.hSMul (β := M) (x₁ * x) ((D : (a : S) → M) (x₂ * y) : M) =
    (x₁ * x₂) • HSMul.hSMul (β := M) x ((D : (a : S) → M) y : M) +
      (x * y) • HSMul.hSMul (β := M) x₁ ((D : (a : S) → M) x₂ : M)

Tactic:
rw [D.leibniz]

Premises used: Derivation.leibniz
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_1
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
D : Derivation R S M
x_1 y_1 : S ⊗[R] S
x₁ x₂ x y : S
⊢ (x₁ * x) • (HSMul.hSMul (β := M) x₂ ((D : (a : S) → M) y : M) + HSMul.hSMul (β := M) y ((D : (a : S) → M) x₂ : M)) =
    (x₁ * x₂) • HSMul.hSMul (β := M) x ((D : (a : S) → M) y : M) +
      (x * y) • HSMul.hSMul (β := M) x₁ ((D : (a : S) → M) x₂ : M)

Tactic:
simp only [smul_smul, smul_add, mul_comm (x * y) x₁, mul_right_comm x₁ x₂, ← mul_assoc]

Premises used: HMul.hMul, mul_assoc, smul_smul, mul_right_comm, mul_comm, smul_add
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
a :
  LE.le (α := Submodule S (S ⊗[R] S))
    (Submodule.span S (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)))
    (Submodule.restrictScalars S (ideal R S))
a₁ :
  LE.le (α := Submodule S (S ⊗[R] S)) (Submodule.restrictScalars S (ideal R S))
    (Submodule.span S (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)))
⊢ Eq (α := Submodule S (S ⊗[R] S))
    (Submodule.span S (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)))
    (Submodule.restrictScalars S (ideal R S))

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
a :
  (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)) ⊆
    (↑(Submodule.restrictScalars S (ideal R S)) : Set (S ⊗[R] S))
⊢ LE.le (α := Submodule S (S ⊗[R] S))
    (Submodule.span S (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)))
    (Submodule.restrictScalars S (ideal R S))

Tactic:
rw [Submodule.span_le]

Premises used: Submodule.span_le
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s : S
⊢ (fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)) s ∈
    (↑(Submodule.restrictScalars S (ideal R S)) : Set (S ⊗[R] S))

Tactic:
KaehlerDifferential.one_smul_sub_smul_one_mem_ideal _ _

Premises used: Set.Mem, setOf, KaehlerDifferential.one_smul_sub_smul_one_mem_ideal, Set.preimage, Set.singleton
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s : S
⊢ (fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)) s ∈
    (↑(Submodule.restrictScalars S (ideal R S)) : Set (S ⊗[R] S))

Tactic:
exact KaehlerDifferential.one_smul_sub_smul_one_mem_ideal _ _

Premises used: KaehlerDifferential.one_smul_sub_smul_one_mem_ideal
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S ⊗[R] S
hx : Eq (α := S) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) x : S) (0 : S)
rw : x - 0 ⊗ₜ[R] 1 = x
rw₁ : x - 0 = x
rw₂ rw₃ : x = x
⊢ HSub.hSub (β := S ⊗[R] S) x ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) x ⊗ₜ[R] 1 : S ⊗[R] S) = x

Tactic:
rw [hx, TensorProduct.zero_tmul, sub_zero]

Premises used: sub_zero, TensorProduct.zero_tmul
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S ⊗[R] S
hx : Eq (α := S) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) x : S) (0 : S)
⊢ HSub.hSub (β := S ⊗[R] S) x ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) x ⊗ₜ[R] 1 : S ⊗[R] S) = x

Tactic:
have : x - TensorProduct.lmul' (S := S) R x ⊗ₜ[R] (1 : S) = x := by
      rw [hx, TensorProduct.zero_tmul, sub_zero]
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S ⊗[R] S
hx : Eq (α := S) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) x : S) (0 : S)
this : HSub.hSub (β := S ⊗[R] S) x ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) x ⊗ₜ[R] 1 : S ⊗[R] S) = x
a :
  Membership.mem (γ := Submodule S (S ⊗[R] S))
    (Submodule.span S (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)))
    (HSub.hSub (β := S ⊗[R] S) x ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) x ⊗ₜ[R] 1 : S ⊗[R] S))
⊢ Membership.mem (γ := Submodule S (S ⊗[R] S))
    (Submodule.span S (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1))) x

Tactic:
rw [← this]
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S ⊗[R] S
⊢ Membership.mem (γ := Submodule S (S ⊗[R] S))
    (Submodule.span S (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)))
    (HSub.hSub (β := S ⊗[R] S) x ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) x ⊗ₜ[R] 1 : S ⊗[R] S))

Tactic:
TensorProduct.induction_on x ?_ ?_ ?_

Premises used: TensorProduct.induction_on
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S ⊗[R] S
a :
  Membership.mem (γ := Submodule S (S ⊗[R] S))
    (Submodule.span S (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)))
    (HSub.hSub (α := S ⊗[R] S) (β := S ⊗[R] S) (0 : S ⊗[R] S)
      ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) 0 ⊗ₜ[R] 1 : S ⊗[R] S))
a₁ :
  ∀ (x y : S),
    Membership.mem (γ := Submodule S (S ⊗[R] S))
      (Submodule.span S (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)))
      (HSub.hSub (α := S ⊗[R] S) (β := S ⊗[R] S) (x ⊗ₜ[R] y)
        ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) (x ⊗ₜ[R] y) ⊗ₜ[R] 1 : S ⊗[R] S))
a₂ :
  ∀ (x y : S ⊗[R] S),
    Membership.mem (γ := Submodule S (S ⊗[R] S))
        (Submodule.span S (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)))
        (HSub.hSub (β := S ⊗[R] S) x ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) x ⊗ₜ[R] 1 : S ⊗[R] S)) →
      Membership.mem (γ := Submodule S (S ⊗[R] S))
          (Submodule.span S (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)))
          (HSub.hSub (β := S ⊗[R] S) y ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) y ⊗ₜ[R] 1 : S ⊗[R] S)) →
        Membership.mem (γ := Submodule S (S ⊗[R] S))
          (Submodule.span S (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)))
          (HSub.hSub (β := S ⊗[R] S) (x + y) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) (x + y) ⊗ₜ[R] 1 : S ⊗[R] S))
⊢ Membership.mem (γ := Submodule S (S ⊗[R] S))
    (Submodule.span S (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)))
    (HSub.hSub (β := S ⊗[R] S) x ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) x ⊗ₜ[R] 1 : S ⊗[R] S))

Tactic:
refine TensorProduct.induction_on x ?_ ?_ ?_
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S ⊗[R] S
a :
  Membership.mem (γ := Submodule S (S ⊗[R] S))
    (Submodule.span S (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1))) 0
⊢ Membership.mem (γ := Submodule S (S ⊗[R] S))
    (Submodule.span S (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)))
    (HSub.hSub (α := S ⊗[R] S) (β := S ⊗[R] S) (0 : S ⊗[R] S)
      ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) 0 ⊗ₜ[R] 1 : S ⊗[R] S))

Tactic:
rw [map_zero, TensorProduct.zero_tmul, sub_zero]

Premises used: sub_zero, map_zero, TensorProduct.zero_tmul
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S ⊗[R] S
⊢ Membership.mem (γ := Submodule S (S ⊗[R] S))
    (Submodule.span S (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1))) 0

Tactic:
zero_mem _

Premises used: ZeroMemClass.zero_mem
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S ⊗[R] S
⊢ Membership.mem (γ := Submodule S (S ⊗[R] S))
    (Submodule.span S (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1))) 0

Tactic:
exact zero_mem _

Premises used: ZeroMemClass.zero_mem