-- 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
⊢ (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)
have 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)
Tactic: simp only [TensorProduct.tmul_mul_tmul, Derivation.tensorProductTo,
    TensorProduct.AlgebraTensorModule.lift_apply,
    TensorProduct.lmul'_apply_tmul]