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