-- Mathlib/RingTheory/Kaehler/Basic.lean
theorem Derivation.tensorProductTo_mul (D : Derivation R S M) (x y : S ⊗[R] S) :
    D.tensorProductTo (x * y) =
      TensorProduct.lmul' (S := S) R x • D.tensorProductTo y +
        TensorProduct.lmul' (S := S) R y • D.tensorProductTo x

Proof state:
case refine_2.refine_2
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
D : Derivation R S M
x y : S ⊗[R] S
x₁ x₂ : S
⊢ ∀ (x y : S),
    D.tensorProductTo (x₁ ⊗ₜ[R] x₂ * x ⊗ₜ[R] y) =
      (TensorProduct.lmul' R) (x₁ ⊗ₜ[R] x₂) • D.tensorProductTo (x ⊗ₜ[R] y) +
        (TensorProduct.lmul' R) (x ⊗ₜ[R] y) • D.tensorProductTo (x₁ ⊗ₜ[R] x₂)

Tactic:
intro x y

Result:
case refine_2.refine_2
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
D : Derivation R S M
x✝ y✝ : S ⊗[R] S
x₁ x₂ x y : S
⊢ D.tensorProductTo (x₁ ⊗ₜ[R] x₂ * x ⊗ₜ[R] y) =
    (TensorProduct.lmul' R) (x₁ ⊗ₜ[R] x₂) • D.tensorProductTo (x ⊗ₜ[R] y) +
      (TensorProduct.lmul' R) (x ⊗ₜ[R] y) • D.tensorProductTo (x₁ ⊗ₜ[R] x₂)

Proof state:
case refine_2.refine_3
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
D : Derivation R S M
x y : S ⊗[R] S
x₁ x₂ : S
⊢ ∀ (x y : S ⊗[R] S),
    D.tensorProductTo (x₁ ⊗ₜ[R] x₂ * x) =
        (TensorProduct.lmul' R) (x₁ ⊗ₜ[R] x₂) • D.tensorProductTo x +
          (TensorProduct.lmul' R) x • D.tensorProductTo (x₁ ⊗ₜ[R] x₂) →
      D.tensorProductTo (x₁ ⊗ₜ[R] x₂ * y) =
          (TensorProduct.lmul' R) (x₁ ⊗ₜ[R] x₂) • D.tensorProductTo y +
            (TensorProduct.lmul' R) y • D.tensorProductTo (x₁ ⊗ₜ[R] x₂) →
        D.tensorProductTo (x₁ ⊗ₜ[R] x₂ * (x + y)) =
          (TensorProduct.lmul' R) (x₁ ⊗ₜ[R] x₂) • D.tensorProductTo (x + y) +
            (TensorProduct.lmul' R) (x + y) • D.tensorProductTo (x₁ ⊗ₜ[R] x₂)

Tactic:
intro x₁ y₁ h₁ h₂

Result:
case refine_2.refine_3
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
D : Derivation R S M
x y : S ⊗[R] S
x₁✝ x₂ : S
x₁ y₁ : S ⊗[R] S
h₁ :
  D.tensorProductTo (x₁✝ ⊗ₜ[R] x₂ * x₁) =
    (TensorProduct.lmul' R) (x₁✝ ⊗ₜ[R] x₂) • D.tensorProductTo x₁ +
      (TensorProduct.lmul' R) x₁ • D.tensorProductTo (x₁✝ ⊗ₜ[R] x₂)
h₂ :
  D.tensorProductTo (x₁✝ ⊗ₜ[R] x₂ * y₁) =
    (TensorProduct.lmul' R) (x₁✝ ⊗ₜ[R] x₂) • D.tensorProductTo y₁ +
      (TensorProduct.lmul' R) y₁ • D.tensorProductTo (x₁✝ ⊗ₜ[R] x₂)
⊢ D.tensorProductTo (x₁✝ ⊗ₜ[R] x₂ * (x₁ + y₁)) =
    (TensorProduct.lmul' R) (x₁✝ ⊗ₜ[R] x₂) • D.tensorProductTo (x₁ + y₁) +
      (TensorProduct.lmul' R) (x₁ + y₁) • D.tensorProductTo (x₁✝ ⊗ₜ[R] x₂)

Proof state:
case refine_2.refine_3
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
D : Derivation R S M
x y : S ⊗[R] S
x₁✝ x₂ : S
x₁ y₁ : S ⊗[R] S
h₁ :
  D.tensorProductTo (x₁✝ ⊗ₜ[R] x₂ * x₁) =
    (TensorProduct.lmul' R) (x₁✝ ⊗ₜ[R] x₂) • D.tensorProductTo x₁ +
      (TensorProduct.lmul' R) x₁ • D.tensorProductTo (x₁✝ ⊗ₜ[R] x₂)
h₂ :
  D.tensorProductTo (x₁✝ ⊗ₜ[R] x₂ * y₁) =
    (TensorProduct.lmul' R) (x₁✝ ⊗ₜ[R] x₂) • D.tensorProductTo y₁ +
      (TensorProduct.lmul' R) y₁ • D.tensorProductTo (x₁✝ ⊗ₜ[R] x₂)
⊢ D.tensorProductTo (x₁✝ ⊗ₜ[R] x₂ * (x₁ + y₁)) =
    (TensorProduct.lmul' R) (x₁✝ ⊗ₜ[R] x₂) • D.tensorProductTo (x₁ + y₁) +
      (TensorProduct.lmul' R) (x₁ + y₁) • D.tensorProductTo (x₁✝ ⊗ₜ[R] x₂)

Tactic:
rw [mul_add, map_add, map_add, map_add, add_smul, smul_add, h₁, h₂, add_add_add_comm]

Result:
no goals

Proof state:
case refine_3
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
D : Derivation R S M
x y : S ⊗[R] S
⊢ ∀ (x y_1 : S ⊗[R] S),
    D.tensorProductTo (x * y) =
        (TensorProduct.lmul' R) x • D.tensorProductTo y + (TensorProduct.lmul' R) y • D.tensorProductTo x →
      D.tensorProductTo (y_1 * y) =
          (TensorProduct.lmul' R) y_1 • D.tensorProductTo y + (TensorProduct.lmul' R) y • D.tensorProductTo y_1 →
        D.tensorProductTo ((x + y_1) * y) =
          (TensorProduct.lmul' R) (x + y_1) • D.tensorProductTo y +
            (TensorProduct.lmul' R) y • D.tensorProductTo (x + y_1)

Tactic:
intro x₁ y₁ h₁ h₂

Result:
case refine_3
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
D : Derivation R S M
x y x₁ y₁ : S ⊗[R] S
h₁ :
  D.tensorProductTo (x₁ * y) =
    (TensorProduct.lmul' R) x₁ • D.tensorProductTo y + (TensorProduct.lmul' R) y • D.tensorProductTo x₁
h₂ :
  D.tensorProductTo (y₁ * y) =
    (TensorProduct.lmul' R) y₁ • D.tensorProductTo y + (TensorProduct.lmul' R) y • D.tensorProductTo y₁
⊢ D.tensorProductTo ((x₁ + y₁) * y) =
    (TensorProduct.lmul' R) (x₁ + y₁) • D.tensorProductTo y + (TensorProduct.lmul' R) y • D.tensorProductTo (x₁ + y₁)