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

Tactic:
induction x using Finsupp.induction_linear with
    | zero =>
      simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom]
      rw [map_zero, map_zero, map_zero]
    | add => simp only [map_add, AddHom.toFun_eq_coe, LinearMap.coe_toAddHom] at *; simp only [*]
    | single a b =>
      simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, Finsupp.linearCombination_single,
        map_smul, Derivation.liftKaehlerDifferential_comp_D]
      congr 1
      induction a using MvPolynomial.induction_on
      · simp only [MvPolynomial.derivation_C, map_zero]
      · simp only [map_add, *]
      · simp [*]

Premises used: AddHom.toFun_eq_coe, map_zero, map_add, Derivation.liftKaehlerDifferential_comp_D, MvPolynomial.induction_on, MvPolynomial.derivation_C, Finsupp.linearCombination_single, LinearMap.coe_toAddHom, map_smul