-- Module: Mathlib.RingTheory.Kaehler.Polynomial
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])
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])
⊢ 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])

Tactic:
simp only [map_add, AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, LinearMap.flip_apply,
        AlgHom.toLinearMap_apply, lsmul_coe] at *

Premises used: AlgHom.toLinearMap_apply, AddHom.toFun_eq_coe, map_add, LinearMap.flip_apply, LinearMap.coe_toAddHom, Algebra.lsmul_coe