-- Module: Mathlib.RingTheory.Kaehler.Polynomial
Goal:
R : Type u
inst : CommRing R
σ : Type u_1
x : σ →₀ MvPolynomial σ R
zero :
  Eq (α := σ →₀ MvPolynomial σ R)
    (AddHom.toFun (M := Ω[MvPolynomial σ R⁄R])
      (LinearMap.toAddHom
        (Derivation.liftKaehlerDifferential (MvPolynomial.mkDerivation R fun (x : σ) ↦ Finsupp.single x 1)))
      ((Finsupp.linearCombination (MvPolynomial σ R) fun (x : σ) ↦
            (D R (MvPolynomial σ R) : (a : MvPolynomial σ R) → Ω[MvPolynomial σ R⁄R]) (MvPolynomial.X x) :
          (a : σ →₀ MvPolynomial σ R) → Ω[MvPolynomial σ R⁄R])
        0))
    0
add :
  ∀ (f g : σ →₀ MvPolynomial σ R),
    AddHom.toFun (M := Ω[MvPolynomial σ R⁄R])
          (LinearMap.toAddHom
            (Derivation.liftKaehlerDifferential (MvPolynomial.mkDerivation R fun (x : σ) ↦ Finsupp.single x 1)))
          ((Finsupp.linearCombination (MvPolynomial σ R) fun (x : σ) ↦
                (D R (MvPolynomial σ R) : (a : MvPolynomial σ R) → Ω[MvPolynomial σ R⁄R]) (MvPolynomial.X x) :
              (a : σ →₀ MvPolynomial σ R) → Ω[MvPolynomial σ R⁄R])
            f) =
        f →
      AddHom.toFun (M := Ω[MvPolynomial σ R⁄R])
            (LinearMap.toAddHom
              (Derivation.liftKaehlerDifferential (MvPolynomial.mkDerivation R fun (x : σ) ↦ Finsupp.single x 1)))
            ((Finsupp.linearCombination (MvPolynomial σ R) fun (x : σ) ↦
                  (D R (MvPolynomial σ R) : (a : MvPolynomial σ R) → Ω[MvPolynomial σ R⁄R]) (MvPolynomial.X x) :
                (a : σ →₀ MvPolynomial σ R) → Ω[MvPolynomial σ R⁄R])
              g) =
          g →
        AddHom.toFun (M := Ω[MvPolynomial σ R⁄R])
            (LinearMap.toAddHom
              (Derivation.liftKaehlerDifferential (MvPolynomial.mkDerivation R fun (x : σ) ↦ Finsupp.single x 1)))
            ((Finsupp.linearCombination (MvPolynomial σ R) fun (x : σ) ↦
                  (D R (MvPolynomial σ R) : (a : MvPolynomial σ R) → Ω[MvPolynomial σ R⁄R]) (MvPolynomial.X x) :
                (a : σ →₀ MvPolynomial σ R) → Ω[MvPolynomial σ R⁄R])
              (f + g)) =
          f + g
single :
  ∀ (a : σ) (b : MvPolynomial σ R),
    Eq (α := σ →₀ MvPolynomial σ R)
      (AddHom.toFun (M := Ω[MvPolynomial σ R⁄R])
        (LinearMap.toAddHom
          (Derivation.liftKaehlerDifferential (MvPolynomial.mkDerivation R fun (x : σ) ↦ Finsupp.single x 1)))
        ((Finsupp.linearCombination (MvPolynomial σ R) fun (x : σ) ↦
              (D R (MvPolynomial σ R) : (a : MvPolynomial σ R) → Ω[MvPolynomial σ R⁄R]) (MvPolynomial.X x) :
            (a : σ →₀ MvPolynomial σ R) → Ω[MvPolynomial σ R⁄R])
          (Finsupp.single a b)))
      (Finsupp.single a b)
⊢ AddHom.toFun (M := Ω[MvPolynomial σ R⁄R])
      (LinearMap.toAddHom
        (Derivation.liftKaehlerDifferential (MvPolynomial.mkDerivation R fun (x : σ) ↦ Finsupp.single x 1)))
      ((Finsupp.linearCombination (MvPolynomial σ R) fun (x : σ) ↦
            (D R (MvPolynomial σ R) : (a : MvPolynomial σ R) → Ω[MvPolynomial σ R⁄R]) (MvPolynomial.X x) :
          (a : σ →₀ MvPolynomial σ R) → Ω[MvPolynomial σ R⁄R])
        x) =
    x

Tactic:
induction x using Finsupp.induction_linear with
    | zero => simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom]; rw [map_zero, map_zero]
    | add => simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, map_add] at *; simp only [*]
    | single a b => simp [-map_smul]

Premises used: AddHom.toFun_eq_coe, map_zero, map_add, LinearMap.coe_toAddHom, map_smul