-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Polynomial (goal)
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])
⊢ 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])
have 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])
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 [*]
Cleared hypotheses: x