-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Polynomial (goal)
Goal:
R : Type u
inst : CommRing R
σ : Type u_1
f g : MvPolynomial σ R →₀ MvPolynomial σ R
h :
  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])
h_1 :
  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])
have add : HAdd.hAdd (α := Ω[MvPolynomial σ R⁄R]) (β := Ω[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])
        ((Derivation.liftKaehlerDifferential (MvPolynomial.mkDerivation R fun (x : σ) ↦ Finsupp.single x 1) :
            (a : Ω[MvPolynomial σ R⁄R]) → σ →₀ MvPolynomial σ 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])
    ((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])
        ((Derivation.liftKaehlerDifferential (MvPolynomial.mkDerivation R fun (x : σ) ↦ Finsupp.single x 1) :
            (a : Ω[MvPolynomial σ R⁄R]) → σ →₀ MvPolynomial σ 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]) =
  HAdd.hAdd (α := Ω[MvPolynomial σ R⁄R]) (β := Ω[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])
    ((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])
Tactic: simp only [map_add, AddHom.toFun_eq_coe, LinearMap.coe_toAddHom] at *