-- Module: Mathlib.RingTheory.Kaehler.Polynomial
Goal:
R : Type u
inst : CommRing R
x : R[X] →₀ R[X]
zero :
  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])
            0)) :
      Ω[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]) 0 :
      Ω[R[X]⁄R])
add :
  ∀ (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])
single :
  ∀ (x y : R[X]),
    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])
              (Finsupp.single 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])
          (Finsupp.single x 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)) :
      Ω[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])

Tactic:
induction x using Finsupp.induction_linear with
    | zero => simp
    | add x y hx hy =>
      simp only [map_add, AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, LinearMap.flip_apply,
        AlgHom.toLinearMap_apply, lsmul_coe] at *; simp only [*]
    | single x y => simp [polynomial_D_apply _ x]

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