-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Polynomial (goal)
Goal:
R : Type u
inst : CommRing R
x y : R[X] →₀ R[X]
hx :
  Eq (α := Ω[R[X]⁄R])
    (((((LinearMap.flip (AlgHom.toLinearMap (lsmul R R Ω[R[X]⁄R]) : R[X] →ₗ[R] End R Ω[R[X]⁄R]) :
                  Ω[R[X]⁄R] →ₗ[R] R[X] →ₗ[R] Ω[R[X]⁄R]) :
                (a : Ω[R[X]⁄R]) → R[X] →ₗ[R] Ω[R[X]⁄R])
              ((D R R[X] : (a : R[X]) → Ω[R[X]⁄R]) X) :
            R[X] →ₗ[R] Ω[R[X]⁄R]) :
          (a : R[X]) → Ω[R[X]⁄R])
        (AddHom.toFun (LinearMap.toAddHom (Derivation.liftKaehlerDifferential derivative'))
          ((Finsupp.linearCombination R[X] (⇑(D R R[X]) : (a : R[X]) → Ω[R[X]⁄R]) : (a : R[X] →₀ R[X]) → Ω[R[X]⁄R])
            x)) :
      Ω[R[X]⁄R])
    ((Finsupp.linearCombination R[X] (⇑(D R R[X]) : (a : R[X]) → Ω[R[X]⁄R]) : (a : R[X] →₀ R[X]) → Ω[R[X]⁄R]) x :
      Ω[R[X]⁄R])
hy :
  Eq (α := Ω[R[X]⁄R])
    (((((LinearMap.flip (AlgHom.toLinearMap (lsmul R R Ω[R[X]⁄R]) : R[X] →ₗ[R] End R Ω[R[X]⁄R]) :
                  Ω[R[X]⁄R] →ₗ[R] R[X] →ₗ[R] Ω[R[X]⁄R]) :
                (a : Ω[R[X]⁄R]) → R[X] →ₗ[R] Ω[R[X]⁄R])
              ((D R R[X] : (a : R[X]) → Ω[R[X]⁄R]) X) :
            R[X] →ₗ[R] Ω[R[X]⁄R]) :
          (a : R[X]) → Ω[R[X]⁄R])
        (AddHom.toFun (LinearMap.toAddHom (Derivation.liftKaehlerDifferential derivative'))
          ((Finsupp.linearCombination R[X] (⇑(D R R[X]) : (a : R[X]) → Ω[R[X]⁄R]) : (a : R[X] →₀ R[X]) → Ω[R[X]⁄R])
            y)) :
      Ω[R[X]⁄R])
    ((Finsupp.linearCombination R[X] (⇑(D R R[X]) : (a : R[X]) → Ω[R[X]⁄R]) : (a : R[X] →₀ R[X]) → Ω[R[X]⁄R]) y :
      Ω[R[X]⁄R])
⊢ Eq (α := Ω[R[X]⁄R])
    (((((LinearMap.flip (AlgHom.toLinearMap (lsmul R R Ω[R[X]⁄R]) : R[X] →ₗ[R] End R Ω[R[X]⁄R]) :
                  Ω[R[X]⁄R] →ₗ[R] R[X] →ₗ[R] Ω[R[X]⁄R]) :
                (a : Ω[R[X]⁄R]) → R[X] →ₗ[R] Ω[R[X]⁄R])
              ((D R R[X] : (a : R[X]) → Ω[R[X]⁄R]) X) :
            R[X] →ₗ[R] Ω[R[X]⁄R]) :
          (a : R[X]) → Ω[R[X]⁄R])
        (AddHom.toFun (LinearMap.toAddHom (Derivation.liftKaehlerDifferential derivative'))
          ((Finsupp.linearCombination R[X] (⇑(D R R[X]) : (a : R[X]) → Ω[R[X]⁄R]) : (a : R[X] →₀ R[X]) → Ω[R[X]⁄R])
            (x + y))) :
      Ω[R[X]⁄R])
    ((Finsupp.linearCombination R[X] (⇑(D R R[X]) : (a : R[X]) → Ω[R[X]⁄R]) : (a : R[X] →₀ R[X]) → Ω[R[X]⁄R]) (x + y) :
      Ω[R[X]⁄R])
have add : HSMul.hSMul (α := R[X]) (β := Ω[R[X]⁄R])
      ((Derivation.liftKaehlerDifferential derivative' : (a : Ω[R[X]⁄R]) → R[X])
          ((Finsupp.linearCombination R[X] (⇑(D R R[X]) : (a : R[X]) → Ω[R[X]⁄R]) : (a : R[X] →₀ R[X]) → Ω[R[X]⁄R]) x) :
        R[X])
      ((D R R[X] : (a : R[X]) → Ω[R[X]⁄R]) X : Ω[R[X]⁄R]) +
    HSMul.hSMul (α := R[X]) (β := Ω[R[X]⁄R])
      ((Derivation.liftKaehlerDifferential derivative' : (a : Ω[R[X]⁄R]) → R[X])
          ((Finsupp.linearCombination R[X] (⇑(D R R[X]) : (a : R[X]) → Ω[R[X]⁄R]) : (a : R[X] →₀ R[X]) → Ω[R[X]⁄R]) y) :
        R[X])
      ((D R R[X] : (a : R[X]) → Ω[R[X]⁄R]) X : Ω[R[X]⁄R]) =
  HAdd.hAdd (α := Ω[R[X]⁄R]) (β := Ω[R[X]⁄R])
    ((Finsupp.linearCombination R[X] (⇑(D R R[X]) : (a : R[X]) → Ω[R[X]⁄R]) : (a : R[X] →₀ R[X]) → Ω[R[X]⁄R]) x :
      Ω[R[X]⁄R])
    ((Finsupp.linearCombination R[X] (⇑(D R R[X]) : (a : R[X]) → Ω[R[X]⁄R]) : (a : R[X] →₀ R[X]) → Ω[R[X]⁄R]) y :
      Ω[R[X]⁄R])
Tactic: simp only [map_add, AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, LinearMap.flip_apply,
        AlgHom.toLinearMap_apply, lsmul_coe] at *