-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Polynomial (goal)
Goal:
R : Type u
inst : CommRing R
σ : Type u_1
a b : MvPolynomial σ R
single :
  ∀ (a : 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])
          ((MvPolynomial.mkDerivation R fun (x : σ) ↦ Finsupp.single x 1 :
              (a : MvPolynomial σ R) → σ →₀ MvPolynomial σ R)
            ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)) :
        Ω[MvPolynomial σ R⁄R])
      ((D R (MvPolynomial σ R) : (a : MvPolynomial σ R) → Ω[MvPolynomial σ R⁄R])
          ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a) :
        Ω[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])
        ((MvPolynomial.mkDerivation R fun (x : σ) ↦ Finsupp.single x 1 : (a : MvPolynomial σ R) → σ →₀ MvPolynomial σ R)
          a) :
      Ω[MvPolynomial σ R⁄R])
    ((D R (MvPolynomial σ R) : (a : MvPolynomial σ R) → Ω[MvPolynomial σ R⁄R]) a : Ω[MvPolynomial σ R⁄R])
have single₁ : ∀ (p q : 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])
          ((MvPolynomial.mkDerivation R fun (x : σ) ↦ Finsupp.single x 1 :
              (a : MvPolynomial σ R) → σ →₀ MvPolynomial σ R)
            p) :
        Ω[MvPolynomial σ R⁄R])
      ((D R (MvPolynomial σ R) : (a : MvPolynomial σ R) → Ω[MvPolynomial σ R⁄R]) p : Ω[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])
            ((MvPolynomial.mkDerivation R fun (x : σ) ↦ Finsupp.single x 1 :
                (a : MvPolynomial σ R) → σ →₀ MvPolynomial σ R)
              q) :
          Ω[MvPolynomial σ R⁄R])
        ((D R (MvPolynomial σ R) : (a : MvPolynomial σ R) → Ω[MvPolynomial σ R⁄R]) q : Ω[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])
            ((MvPolynomial.mkDerivation R fun (x : σ) ↦ Finsupp.single x 1 :
                (a : MvPolynomial σ R) → σ →₀ MvPolynomial σ R)
              (p + q)) :
          Ω[MvPolynomial σ R⁄R])
        ((D R (MvPolynomial σ R) : (a : MvPolynomial σ R) → Ω[MvPolynomial σ R⁄R]) (p + q) : Ω[MvPolynomial σ R⁄R])
Tactic: induction a using MvPolynomial.induction_on
Cleared hypotheses: a