awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
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)
⊢ (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)
have refine_2₃ : 0 = HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) (x₁ ⊗ₜ[R] x₂) : S) 0 + 0
Tactic: rw [mul_zero, map_zero, map_zero, zero_smul, smul_zero, add_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
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
⊢ (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)
have refine_2₄ : 0 = HAdd.hAdd (α := M) 0 0
Tactic: rw [mul_zero, map_zero, map_zero, zero_smul, smul_zero, add_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
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
⊢ (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)
have refine_2₅ : Eq.{u_1 + 1} (α := M) 0 0
Tactic: rw [mul_zero, map_zero, map_zero, zero_smul, smul_zero, add_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
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₁_1 x₂ : S
x₁ y₁ : S ⊗[R] S
h₁ :
  (D.tensorProductTo : (a : S ⊗[R] S) → M) (x₁_1 ⊗ₜ[R] x₂ * x₁) =
    HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) (x₁_1 ⊗ₜ[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₁_1 ⊗ₜ[R] x₂) : M)
h₂ :
  (D.tensorProductTo : (a : S ⊗[R] S) → M) (x₁_1 ⊗ₜ[R] x₂ * y₁) =
    HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) (x₁_1 ⊗ₜ[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₁_1 ⊗ₜ[R] x₂) : M)
⊢ (D.tensorProductTo : (a : S ⊗[R] S) → M) (x₁_1 ⊗ₜ[R] x₂ * (x₁ + y₁)) =
    HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) (x₁_1 ⊗ₜ[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₁_1 ⊗ₜ[R] x₂) : M)
have refine_2 : (D.tensorProductTo : (a : S ⊗[R] S) → M) (x₁_1 ⊗ₜ[R] x₂ * x₁ + x₁_1 ⊗ₜ[R] x₂ * y₁) =
  HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) (x₁_1 ⊗ₜ[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₁_1 ⊗ₜ[R] x₂) : M)
Tactic: rw [mul_add, map_add, map_add, map_add, add_smul, smul_add, h₁, h₂, add_add_add_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
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₁_1 x₂ : S
x₁ y₁ : S ⊗[R] S
h₁ :
  (D.tensorProductTo : (a : S ⊗[R] S) → M) (x₁_1 ⊗ₜ[R] x₂ * x₁) =
    HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) (x₁_1 ⊗ₜ[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₁_1 ⊗ₜ[R] x₂) : M)
h₂ :
  (D.tensorProductTo : (a : S ⊗[R] S) → M) (x₁_1 ⊗ₜ[R] x₂ * y₁) =
    HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) (x₁_1 ⊗ₜ[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₁_1 ⊗ₜ[R] x₂) : M)
refine_2 :
  (D.tensorProductTo : (a : S ⊗[R] S) → M) (x₁_1 ⊗ₜ[R] x₂ * x₁ + x₁_1 ⊗ₜ[R] x₂ * y₁) =
    HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) (x₁_1 ⊗ₜ[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₁_1 ⊗ₜ[R] x₂) : M)
⊢ (D.tensorProductTo : (a : S ⊗[R] S) → M) (x₁_1 ⊗ₜ[R] x₂ * (x₁ + y₁)) =
    HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) (x₁_1 ⊗ₜ[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₁_1 ⊗ₜ[R] x₂) : M)
have refine_2₁ : HAdd.hAdd (α := M) (β := M) ((D.tensorProductTo : (a : S ⊗[R] S) → M) (x₁_1 ⊗ₜ[R] x₂ * x₁) : M)
    ((D.tensorProductTo : (a : S ⊗[R] S) → M) (x₁_1 ⊗ₜ[R] x₂ * y₁) : M) =
  HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) (x₁_1 ⊗ₜ[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₁_1 ⊗ₜ[R] x₂) : M)
Tactic: rw [mul_add, map_add, map_add, map_add, add_smul, smul_add, h₁, h₂, add_add_add_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
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₁_1 x₂ : S
x₁ y₁ : S ⊗[R] S
h₁ :
  (D.tensorProductTo : (a : S ⊗[R] S) → M) (x₁_1 ⊗ₜ[R] x₂ * x₁) =
    HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) (x₁_1 ⊗ₜ[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₁_1 ⊗ₜ[R] x₂) : M)
h₂ :
  (D.tensorProductTo : (a : S ⊗[R] S) → M) (x₁_1 ⊗ₜ[R] x₂ * y₁) =
    HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) (x₁_1 ⊗ₜ[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₁_1 ⊗ₜ[R] x₂) : M)
refine_2 :
  (D.tensorProductTo : (a : S ⊗[R] S) → M) (x₁_1 ⊗ₜ[R] x₂ * x₁ + x₁_1 ⊗ₜ[R] x₂ * y₁) =
    HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) (x₁_1 ⊗ₜ[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₁_1 ⊗ₜ[R] x₂) : M)
refine_2₁ :
  HAdd.hAdd (α := M) (β := M) ((D.tensorProductTo : (a : S ⊗[R] S) → M) (x₁_1 ⊗ₜ[R] x₂ * x₁) : M)
      ((D.tensorProductTo : (a : S ⊗[R] S) → M) (x₁_1 ⊗ₜ[R] x₂ * y₁) : M) =
    HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) (x₁_1 ⊗ₜ[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₁_1 ⊗ₜ[R] x₂) : M)
⊢ (D.tensorProductTo : (a : S ⊗[R] S) → M) (x₁_1 ⊗ₜ[R] x₂ * (x₁ + y₁)) =
    HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) (x₁_1 ⊗ₜ[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₁_1 ⊗ₜ[R] x₂) : M)
have refine_2₂ : HAdd.hAdd (α := M) (β := M) ((D.tensorProductTo : (a : S ⊗[R] S) → M) (x₁_1 ⊗ₜ[R] x₂ * x₁) : M)
    ((D.tensorProductTo : (a : S ⊗[R] S) → M) (x₁_1 ⊗ₜ[R] x₂ * y₁) : M) =
  HSMul.hSMul (α := S) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) (x₁_1 ⊗ₜ[R] x₂) : S)
      (HAdd.hAdd (α := M) (β := M) ((D.tensorProductTo : (a : S ⊗[R] S) → M) x₁ : M)
        ((D.tensorProductTo : (a : S ⊗[R] S) → M) 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₁_1 ⊗ₜ[R] x₂) : M)
Tactic: rw [mul_add, map_add, map_add, map_add, add_smul, smul_add, h₁, h₂, add_add_add_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
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
⊢ 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)
have 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)
Tactic: rw [D.leibniz]
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
⊢ 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))
have 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))
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
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))
⊢ 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))
have 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)))
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra 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))
have 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))
Tactic: rw [Submodule.span_le]
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
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
have rw : x - 0 ⊗ₜ[R] 1 = x
Tactic: rw [hx, TensorProduct.zero_tmul, sub_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
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
⊢ HSub.hSub (β := S ⊗[R] S) x ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) x ⊗ₜ[R] 1 : S ⊗[R] S) = x
have rw₁ : x - 0 = x
Tactic: rw [hx, TensorProduct.zero_tmul, sub_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
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
⊢ HSub.hSub (β := S ⊗[R] S) x ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) x ⊗ₜ[R] 1 : S ⊗[R] S) = x
have rw₂ : x = x
Tactic: rw [hx, TensorProduct.zero_tmul, sub_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (hypothesis)
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)
⊢ 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
have this : 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]
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
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
⊢ 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
have 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))
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
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))
have 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))
Tactic: refine TensorProduct.induction_on x ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
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))
⊢ 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))
have 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))
Tactic: refine TensorProduct.induction_on x ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
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))
⊢ 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))
have 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))
Tactic: refine TensorProduct.induction_on x ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
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) (β := S ⊗[R] S) (0 : S ⊗[R] S)
      ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) 0 ⊗ₜ[R] 1 : S ⊗[R] S))
have 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
Tactic: rw [map_zero, TensorProduct.zero_tmul, sub_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x_1 : S ⊗[R] S
x y : S
⊢ HSub.hSub (α := S ⊗[R] S) (x ⊗ₜ[R] y) ((x * y) ⊗ₜ[R] 1) = x • HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] y) (y ⊗ₜ[R] 1)
have simp_rw : HSub.hSub (α := S ⊗[R] S) (x ⊗ₜ[R] y) ((x * y) ⊗ₜ[R] 1) =
  HSMul.hSMul (β := S ⊗[R] S) x (1 ⊗ₜ[R] y) - HSMul.hSMul (β := S ⊗[R] S) x (y ⊗ₜ[R] 1)
Tactic: simp_rw [smul_sub, TensorProduct.smul_tmul', smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x_1 : S ⊗[R] S
x y : S
simp_rw :
  HSub.hSub (α := S ⊗[R] S) (x ⊗ₜ[R] y) ((x * y) ⊗ₜ[R] 1) =
    HSMul.hSMul (β := S ⊗[R] S) x (1 ⊗ₜ[R] y) - HSMul.hSMul (β := S ⊗[R] S) x (y ⊗ₜ[R] 1)
⊢ HSub.hSub (α := S ⊗[R] S) (x ⊗ₜ[R] y) ((x * y) ⊗ₜ[R] 1) = x • HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] y) (y ⊗ₜ[R] 1)
have simp_rw₁ : HSub.hSub (α := S ⊗[R] S) (x ⊗ₜ[R] y) ((x * y) ⊗ₜ[R] 1) =
  HSub.hSub (α := S ⊗[R] S) (HSMul.hSMul (β := S) x 1 ⊗ₜ[R] y) ((x • y) ⊗ₜ[R] 1)
Tactic: simp_rw [smul_sub, TensorProduct.smul_tmul', smul_eq_mul, mul_one]