-- 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₁_1 x₂ : S
x₁ y₁ : S ⊗[R] S
h₁ :
  (D.tensorProductTo : (a : S ⊗[R] S) → M) (x₁_1 ⊗ₜ[R] x₂ * x₁) =
    HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) (x₁_1 ⊗ₜ[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₁_1 ⊗ₜ[R] x₂) : M)
h₂ :
  (D.tensorProductTo : (a : S ⊗[R] S) → M) (x₁_1 ⊗ₜ[R] x₂ * y₁) =
    HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) (x₁_1 ⊗ₜ[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₁_1 ⊗ₜ[R] x₂) : M)
refine_2 :
  (D.tensorProductTo : (a : S ⊗[R] S) → M) (x₁_1 ⊗ₜ[R] x₂ * x₁ + x₁_1 ⊗ₜ[R] x₂ * y₁) =
    HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) (x₁_1 ⊗ₜ[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₁_1 ⊗ₜ[R] x₂) : M)
refine_2₁ :
  HAdd.hAdd (α := M) (β := M) ((D.tensorProductTo : (a : S ⊗[R] S) → M) (x₁_1 ⊗ₜ[R] x₂ * x₁) : M)
      ((D.tensorProductTo : (a : S ⊗[R] S) → M) (x₁_1 ⊗ₜ[R] x₂ * y₁) : M) =
    HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) (x₁_1 ⊗ₜ[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₁_1 ⊗ₜ[R] x₂) : M)
refine_2₂ :
  HAdd.hAdd (α := M) (β := M) ((D.tensorProductTo : (a : S ⊗[R] S) → M) (x₁_1 ⊗ₜ[R] x₂ * x₁) : M)
      ((D.tensorProductTo : (a : S ⊗[R] S) → M) (x₁_1 ⊗ₜ[R] x₂ * y₁) : M) =
    HSMul.hSMul (α := S) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) (x₁_1 ⊗ₜ[R] x₂) : S)
        (HAdd.hAdd (α := M) (β := M) ((D.tensorProductTo : (a : S ⊗[R] S) → M) x₁ : M)
          ((D.tensorProductTo : (a : S ⊗[R] S) → M) 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₁_1 ⊗ₜ[R] x₂) : M)
⊢ (D.tensorProductTo : (a : S ⊗[R] S) → M) (x₁_1 ⊗ₜ[R] x₂ * (x₁ + y₁)) =
    HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) (x₁_1 ⊗ₜ[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₁_1 ⊗ₜ[R] x₂) : M)
have refine_2₃ : HAdd.hAdd (α := M) (β := M) ((D.tensorProductTo : (a : S ⊗[R] S) → M) (x₁_1 ⊗ₜ[R] x₂ * x₁) : M)
    ((D.tensorProductTo : (a : S ⊗[R] S) → M) (x₁_1 ⊗ₜ[R] x₂ * y₁) : M) =
  HSMul.hSMul (α := S) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) (x₁_1 ⊗ₜ[R] x₂) : S)
      (HAdd.hAdd (α := M) (β := M) ((D.tensorProductTo : (a : S ⊗[R] S) → M) x₁ : M)
        ((D.tensorProductTo : (a : S ⊗[R] S) → M) 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) (x₁_1 ⊗ₜ[R] x₂) : M)
Tactic: rw [mul_add, map_add, map_add, map_add, add_smul, smul_add, h₁, h₂, add_add_add_comm]