-- 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
⊢ (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)
have refine_2 : 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)
Tactic: dsimp