Module: Mathlib.RingTheory.Kaehler.Polynomial

Goal state before:
pp: case add
R : Type u
inst✝ : CommRing R
σ : Type u_1
f✝ g✝ : MvPolynomial σ R →₀ MvPolynomial σ R
a✝¹ :
  (Finsupp.linearCombination (MvPolynomial σ R) fun x ↦ (D R (MvPolynomial σ R)) (MvPolynomial.X x))
      ((MvPolynomial.mkDerivation R fun x ↦ Finsupp.single x 1).liftKaehlerDifferential
        ((Finsupp.linearCombination (MvPolynomial σ R) ⇑(D R (MvPolynomial σ R))) f✝)) =
    (Finsupp.linearCombination (MvPolynomial σ R) ⇑(D R (MvPolynomial σ R))) f✝
a✝ :
  (Finsupp.linearCombination (MvPolynomial σ R) fun x ↦ (D R (MvPolynomial σ R)) (MvPolynomial.X x))
      ((MvPolynomial.mkDerivation R fun x ↦ Finsupp.single x 1).liftKaehlerDifferential
        ((Finsupp.linearCombination (MvPolynomial σ R) ⇑(D R (MvPolynomial σ R))) g✝)) =
    (Finsupp.linearCombination (MvPolynomial σ R) ⇑(D R (MvPolynomial σ R))) g✝
⊢ (Finsupp.linearCombination (MvPolynomial σ R) fun x ↦ (D R (MvPolynomial σ R)) (MvPolynomial.X x))
        ((MvPolynomial.mkDerivation R fun x ↦ Finsupp.single x 1).liftKaehlerDifferential
          ((Finsupp.linearCombination (MvPolynomial σ R) ⇑(D R (MvPolynomial σ R))) f✝)) +
      (Finsupp.linearCombination (MvPolynomial σ R) fun x ↦ (D R (MvPolynomial σ R)) (MvPolynomial.X x))
        ((MvPolynomial.mkDerivation R fun x ↦ Finsupp.single x 1).liftKaehlerDifferential
          ((Finsupp.linearCombination (MvPolynomial σ R) ⇑(D R (MvPolynomial σ R))) g✝)) =
    (Finsupp.linearCombination (MvPolynomial σ R) ⇑(D R (MvPolynomial σ R))) f✝ +
      (Finsupp.linearCombination (MvPolynomial σ R) ⇑(D R (MvPolynomial σ R))) g✝

Tactic:
;

Goal state after:
case add
R : Type u
inst✝ : CommRing R
σ : Type u_1
f✝ g✝ : MvPolynomial σ R →₀ MvPolynomial σ R
a✝¹ :
  (Finsupp.linearCombination (MvPolynomial σ R) fun x ↦ (D R (MvPolynomial σ R)) (MvPolynomial.X x))
      ((MvPolynomial.mkDerivation R fun x ↦ Finsupp.single x 1).liftKaehlerDifferential
        ((Finsupp.linearCombination (MvPolynomial σ R) ⇑(D R (MvPolynomial σ R))) f✝)) =
    (Finsupp.linearCombination (MvPolynomial σ R) ⇑(D R (MvPolynomial σ R))) f✝
a✝ :
  (Finsupp.linearCombination (MvPolynomial σ R) fun x ↦ (D R (MvPolynomial σ R)) (MvPolynomial.X x))
      ((MvPolynomial.mkDerivation R fun x ↦ Finsupp.single x 1).liftKaehlerDifferential
        ((Finsupp.linearCombination (MvPolynomial σ R) ⇑(D R (MvPolynomial σ R))) g✝)) =
    (Finsupp.linearCombination (MvPolynomial σ R) ⇑(D R (MvPolynomial σ R))) g✝
⊢ (Finsupp.linearCombination (MvPolynomial σ R) fun x ↦ (D R (MvPolynomial σ R)) (MvPolynomial.X x))
        ((MvPolynomial.mkDerivation R fun x ↦ Finsupp.single x 1).liftKaehlerDifferential
          ((Finsupp.linearCombination (MvPolynomial σ R) ⇑(D R (MvPolynomial σ R))) f✝)) +
      (Finsupp.linearCombination (MvPolynomial σ R) fun x ↦ (D R (MvPolynomial σ R)) (MvPolynomial.X x))
        ((MvPolynomial.mkDerivation R fun x ↦ Finsupp.single x 1).liftKaehlerDifferential
          ((Finsupp.linearCombination (MvPolynomial σ R) ⇑(D R (MvPolynomial σ R))) g✝)) =
    (Finsupp.linearCombination (MvPolynomial σ R) ⇑(D R (MvPolynomial σ R))) f✝ +
      (Finsupp.linearCombination (MvPolynomial σ R) ⇑(D R (MvPolynomial σ R))) g✝