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
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
⊢ (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)
have 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
Tactic: rw [zero_mul, 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
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
⊢ (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)
have refine_1₃ : 0 = 0 + HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) y : S) 0
Tactic: rw [zero_mul, 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
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
⊢ (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)
have refine_1₄ : 0 = HAdd.hAdd (α := M) 0 0
Tactic: rw [zero_mul, 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
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
⊢ (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)
have refine_1₅ : Eq.{u_1 + 1} (α := M) 0 0
Tactic: rw [zero_mul, 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 x₁ y₁ : S ⊗[R] S
h₁ :
  (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)
h₂ :
  (D.tensorProductTo : (a : S ⊗[R] S) → M) (y₁ * y) =
    HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) y₁ : 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₁ : M)
⊢ (D.tensorProductTo : (a : S ⊗[R] S) → M) ((x₁ + y₁) * y) =
    HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) (x₁ + y₁) : 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₁) : M)
have refine_3 : (D.tensorProductTo : (a : S ⊗[R] S) → M) (x₁ * y + y₁ * y) =
  HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) (x₁ + y₁) : 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₁) : M)
Tactic: rw [add_mul, 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 x₁ y₁ : S ⊗[R] S
h₁ :
  (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)
h₂ :
  (D.tensorProductTo : (a : S ⊗[R] S) → M) (y₁ * y) =
    HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) y₁ : 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₁ : M)
refine_3 :
  (D.tensorProductTo : (a : S ⊗[R] S) → M) (x₁ * y + y₁ * y) =
    HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) (x₁ + y₁) : 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₁) : M)
⊢ (D.tensorProductTo : (a : S ⊗[R] S) → M) ((x₁ + y₁) * y) =
    HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) (x₁ + y₁) : 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₁) : M)
have refine_3₁ : HAdd.hAdd (α := M) (β := M) ((D.tensorProductTo : (a : S ⊗[R] S) → M) (x₁ * y) : M)
    ((D.tensorProductTo : (a : S ⊗[R] S) → M) (y₁ * y) : M) =
  HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) (x₁ + y₁) : 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₁) : M)
Tactic: rw [add_mul, 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 x₁ y₁ : S ⊗[R] S
h₁ :
  (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)
h₂ :
  (D.tensorProductTo : (a : S ⊗[R] S) → M) (y₁ * y) =
    HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) y₁ : 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₁ : M)
refine_3 :
  (D.tensorProductTo : (a : S ⊗[R] S) → M) (x₁ * y + y₁ * y) =
    HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) (x₁ + y₁) : 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₁) : M)
refine_3₁ :
  HAdd.hAdd (α := M) (β := M) ((D.tensorProductTo : (a : S ⊗[R] S) → M) (x₁ * y) : M)
      ((D.tensorProductTo : (a : S ⊗[R] S) → M) (y₁ * y) : M) =
    HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) (x₁ + y₁) : 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₁) : M)
⊢ (D.tensorProductTo : (a : S ⊗[R] S) → M) ((x₁ + y₁) * y) =
    HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) (x₁ + y₁) : 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₁) : M)
have refine_3₂ : HAdd.hAdd (α := M) (β := M) ((D.tensorProductTo : (a : S ⊗[R] S) → M) (x₁ * y) : M)
    ((D.tensorProductTo : (a : S ⊗[R] S) → M) (y₁ * y) : M) =
  HSMul.hSMul (β := M)
      (HAdd.hAdd (α := S) (β := S) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) x₁ : S)
        ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) y₁ : 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₁) : M)
Tactic: rw [add_mul, 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₁ 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)
have 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)
Tactic: refine TensorProduct.induction_on y ?_ ?_ ?_
-- 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) (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)
⊢ (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)
have 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)
Tactic: refine TensorProduct.induction_on y ?_ ?_ ?_
-- 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) (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)
⊢ (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)
have 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)
Tactic: refine TensorProduct.induction_on y ?_ ?_ ?_
-- 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
⊢ (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 : (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)
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)
⊢ (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 +
    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]
-- 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)
⊢ (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 +
    HSMul.hSMul.{v, u_1, u_1} (α := S) (β := M) 0 ((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]