-- 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 :
  (TensorProduct.lift
          ((↑R :
              {S M : Type v} →
                {M₂ : Type (max u_1 v)} →
                  [inst : Semiring R] →
                    [inst_7 : Semiring S] →
                      [inst_8 : AddCommMonoid M] →
                        [inst_9 : AddCommMonoid M₂] →
                          [inst_10 : Module R M] →
                            [inst_11 : Module R M₂] →
                              [inst_12 : Module S M] →
                                [inst_13 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            (S := S)
            ((LinearMap.flip (LinearMap.lsmul S (S →ₗ[R] M)) : (a : S →ₗ[R] M) → S →ₗ[S] S →ₗ[R] M) (↑D : S →ₗ[R] M))) :
        (a : S ⊗[R] S) → M)
      ((x₁ * x) ⊗ₜ[R] (x₂ * y)) =
    HSMul.hSMul (β := M) (x₁ * x₂)
        ((TensorProduct.lift
                ((↑R :
                    {S M : Type v} →
                      {M₂ : Type (max u_1 v)} →
                        [inst : Semiring R] →
                          [inst_7 : Semiring S] →
                            [inst_8 : AddCommMonoid M] →
                              [inst_9 : AddCommMonoid M₂] →
                                [inst_10 : Module R M] →
                                  [inst_11 : Module R M₂] →
                                    [inst_12 : Module S M] →
                                      [inst_13 : Module S M₂] →
                                        [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                  (S := S)
                  ((LinearMap.flip (LinearMap.lsmul S (S →ₗ[R] M)) : (a : S →ₗ[R] M) → S →ₗ[S] S →ₗ[R] M)
                    (↑D : S →ₗ[R] M))) :
              (a : S ⊗[R] S) → M)
            (x ⊗ₜ[R] y) :
          M) +
      HSMul.hSMul (β := M) (x * y)
        ((TensorProduct.lift
                ((↑R :
                    {S M : Type v} →
                      {M₂ : Type (max u_1 v)} →
                        [inst : Semiring R] →
                          [inst_7 : Semiring S] →
                            [inst_8 : AddCommMonoid M] →
                              [inst_9 : AddCommMonoid M₂] →
                                [inst_10 : Module R M] →
                                  [inst_11 : Module R M₂] →
                                    [inst_12 : Module S M] →
                                      [inst_13 : Module S M₂] →
                                        [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                  (S := S)
                  ((LinearMap.flip (LinearMap.lsmul S (S →ₗ[R] M)) : (a : S →ₗ[R] M) → S →ₗ[S] S →ₗ[R] M)
                    (↑D : S →ₗ[R] M))) :
              (a : S ⊗[R] S) → M)
            (x₁ ⊗ₜ[R] x₂) :
          M)
⊢ (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:
simp only [TensorProduct.tmul_mul_tmul, Derivation.tensorProductTo,
    TensorProduct.AlgebraTensorModule.lift_apply,
    TensorProduct.lmul'_apply_tmul]

Premises used: Algebra.TensorProduct.lmul'_apply_tmul, Derivation.tensorProductTo, Algebra.TensorProduct.tmul_mul_tmul, TensorProduct.AlgebraTensorModule.lift_apply