awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Kaehler.Polynomial
Goal:
R : Type u
inst : CommRing R
σ : Type u_1
⊢ Eq (α := Derivation R (MvPolynomial σ R) (σ →₀ MvPolynomial σ R))
    ((((↑(Basis.repr (mvPolynomialBasis R σ)) :
                Ω[MvPolynomial σ R⁄R] →ₗ[MvPolynomial σ R] σ →₀ MvPolynomial σ R).compDer :
            LinearMap (R := MvPolynomial σ R) (RingHom.id (MvPolynomial σ R))
              (Derivation R (MvPolynomial σ R) Ω[MvPolynomial σ R⁄R])
              (Derivation R (MvPolynomial σ R) (σ →₀ MvPolynomial σ R))) :
          (a : Derivation R (MvPolynomial σ R) Ω[MvPolynomial σ R⁄R]) →
            Derivation R (MvPolynomial σ R) (σ →₀ MvPolynomial σ R))
        (D R (MvPolynomial σ R)) :
      Derivation R (MvPolynomial σ R) (σ →₀ MvPolynomial σ R))
    (MvPolynomial.mkDerivation R fun (x : σ) ↦ Finsupp.single x 1 :
      Derivation R (MvPolynomial σ R) (σ →₀ MvPolynomial σ R))

Tactic:
Derivation.liftKaehlerDifferential_comp _

Premises used: Derivation.liftKaehlerDifferential, Set.Mem, Derivation.liftKaehlerDifferential_comp
-- Module: Mathlib.RingTheory.Kaehler.Polynomial
Goal:
R : Type u
inst : CommRing R
σ : Type u_1
x : MvPolynomial σ R
⊢ Eq (α := σ →₀ MvPolynomial σ R)
    ((Basis.repr (mvPolynomialBasis R σ) : (a : Ω[MvPolynomial σ R⁄R]) → σ →₀ MvPolynomial σ R)
        ((D R (MvPolynomial σ R) : (a : MvPolynomial σ R) → Ω[MvPolynomial σ R⁄R]) x) :
      σ →₀ MvPolynomial σ R)
    ((MvPolynomial.mkDerivation R fun (x : σ) ↦ Finsupp.single x 1 : (a : MvPolynomial σ R) → σ →₀ MvPolynomial σ R) x :
      σ →₀ MvPolynomial σ R)

Tactic:
Derivation.congr_fun (mvPolynomialBasis_repr_comp_D R σ) x

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, Finsupp.onFinset, Finsupp.zipWith, KaehlerDifferential.mvPolynomialBasis_repr_comp_D, Derivation.congr_fun, FreeAddMonoid.sumAux
-- Module: Mathlib.RingTheory.Kaehler.Polynomial
Goal:
R : Type u
inst : CommRing R
σ : Type u_1
i : σ
⊢ Eq (α := σ →₀ MvPolynomial σ R)
    ((Basis.repr (mvPolynomialBasis R σ) : (a : Ω[MvPolynomial σ R⁄R]) → σ →₀ MvPolynomial σ R)
        ((D R (MvPolynomial σ R) : (a : MvPolynomial σ R) → Ω[MvPolynomial σ R⁄R]) (MvPolynomial.X i)) :
      σ →₀ MvPolynomial σ R)
    (Finsupp.single i 1 : σ →₀ MvPolynomial σ R)

Tactic:
simp [mvPolynomialBasis_repr_D]

Premises used: KaehlerDifferential.mvPolynomialBasis_repr_D
-- Module: Mathlib.RingTheory.Kaehler.Polynomial
Goal:
R : Type u
inst : CommRing R
σ : Type u_1
x : MvPolynomial σ R
i : σ
this :
  Eq (α := Derivation R (MvPolynomial σ R) (MvPolynomial σ R))
    ((((Finsupp.lapply i ∘ₗ
                (↑(Basis.repr (mvPolynomialBasis R σ)) :
                  Ω[MvPolynomial σ R⁄R] →ₗ[MvPolynomial σ R] σ →₀ MvPolynomial σ R)).compDer :
            LinearMap (R := MvPolynomial σ R) (RingHom.id (MvPolynomial σ R))
              (Derivation R (MvPolynomial σ R) Ω[MvPolynomial σ R⁄R])
              (Derivation R (MvPolynomial σ R) (MvPolynomial σ R))) :
          (a : Derivation R (MvPolynomial σ R) Ω[MvPolynomial σ R⁄R]) →
            Derivation R (MvPolynomial σ R) (MvPolynomial σ R))
        (D R (MvPolynomial σ R)) :
      Derivation R (MvPolynomial σ R) (MvPolynomial σ R))
    (MvPolynomial.pderiv i : Derivation R (MvPolynomial σ R) (MvPolynomial σ R))
rw :
  Eq (α := MvPolynomial σ R)
    ((((Basis.repr (mvPolynomialBasis R σ) : (a : Ω[MvPolynomial σ R⁄R]) → σ →₀ MvPolynomial σ R)
              ((D R (MvPolynomial σ R) : (a : MvPolynomial σ R) → Ω[MvPolynomial σ R⁄R]) x) :
            σ →₀ MvPolynomial σ R) :
          (a : σ) → MvPolynomial σ R)
        i :
      MvPolynomial σ R)
    ((((((Finsupp.lapply i ∘ₗ
                      (↑(Basis.repr (mvPolynomialBasis R σ)) :
                        Ω[MvPolynomial σ R⁄R] →ₗ[MvPolynomial σ R] σ →₀ MvPolynomial σ R)).compDer :
                  LinearMap (R := MvPolynomial σ R) (RingHom.id (MvPolynomial σ R))
                    (Derivation R (MvPolynomial σ R) Ω[MvPolynomial σ R⁄R])
                    (Derivation R (MvPolynomial σ R) (MvPolynomial σ R))) :
                (a : Derivation R (MvPolynomial σ R) Ω[MvPolynomial σ R⁄R]) →
                  Derivation R (MvPolynomial σ R) (MvPolynomial σ R))
              (D R (MvPolynomial σ R)) :
            Derivation R (MvPolynomial σ R) (MvPolynomial σ R)) :
          (a : MvPolynomial σ R) → MvPolynomial σ R)
        x :
      MvPolynomial σ R)
⊢ Eq (α := MvPolynomial σ R)
    ((((Basis.repr (mvPolynomialBasis R σ) : (a : Ω[MvPolynomial σ R⁄R]) → σ →₀ MvPolynomial σ R)
              ((D R (MvPolynomial σ R) : (a : MvPolynomial σ R) → Ω[MvPolynomial σ R⁄R]) x) :
            σ →₀ MvPolynomial σ R) :
          (a : σ) → MvPolynomial σ R)
        i :
      MvPolynomial σ R)
    ((MvPolynomial.pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) x : MvPolynomial σ R)

Tactic:
rw [← this]
-- Module: Mathlib.RingTheory.Kaehler.Polynomial
Goal:
R : Type u
inst : CommRing R
σ : Type u_1
x : MvPolynomial σ R
i : σ
this :
  Eq (α := Derivation R (MvPolynomial σ R) (MvPolynomial σ R))
    ((((Finsupp.lapply i ∘ₗ
                (↑(Basis.repr (mvPolynomialBasis R σ)) :
                  Ω[MvPolynomial σ R⁄R] →ₗ[MvPolynomial σ R] σ →₀ MvPolynomial σ R)).compDer :
            LinearMap (R := MvPolynomial σ R) (RingHom.id (MvPolynomial σ R))
              (Derivation R (MvPolynomial σ R) Ω[MvPolynomial σ R⁄R])
              (Derivation R (MvPolynomial σ R) (MvPolynomial σ R))) :
          (a : Derivation R (MvPolynomial σ R) Ω[MvPolynomial σ R⁄R]) →
            Derivation R (MvPolynomial σ R) (MvPolynomial σ R))
        (D R (MvPolynomial σ R)) :
      Derivation R (MvPolynomial σ R) (MvPolynomial σ R))
    (MvPolynomial.pderiv i : Derivation R (MvPolynomial σ R) (MvPolynomial σ R))
⊢ Eq (α := MvPolynomial σ R)
    ((((Basis.repr (mvPolynomialBasis R σ) : (a : Ω[MvPolynomial σ R⁄R]) → σ →₀ MvPolynomial σ R)
              ((D R (MvPolynomial σ R) : (a : MvPolynomial σ R) → Ω[MvPolynomial σ R⁄R]) x) :
            σ →₀ MvPolynomial σ R) :
          (a : σ) → MvPolynomial σ R)
        i :
      MvPolynomial σ R)
    ((((((Finsupp.lapply i ∘ₗ
                      (↑(Basis.repr (mvPolynomialBasis R σ)) :
                        Ω[MvPolynomial σ R⁄R] →ₗ[MvPolynomial σ R] σ →₀ MvPolynomial σ R)).compDer :
                  LinearMap (R := MvPolynomial σ R) (RingHom.id (MvPolynomial σ R))
                    (Derivation R (MvPolynomial σ R) Ω[MvPolynomial σ R⁄R])
                    (Derivation R (MvPolynomial σ R) (MvPolynomial σ R))) :
                (a : Derivation R (MvPolynomial σ R) Ω[MvPolynomial σ R⁄R]) →
                  Derivation R (MvPolynomial σ R) (MvPolynomial σ R))
              (D R (MvPolynomial σ R)) :
            Derivation R (MvPolynomial σ R) (MvPolynomial σ R)) :
          (a : MvPolynomial σ R) → MvPolynomial σ R)
        x :
      MvPolynomial σ R)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Kaehler.Polynomial
Goal:
R : Type u
inst : CommRing R
σ : Type u_1
x : MvPolynomial σ R
i : σ
suffices :
  Eq (α := Derivation R (MvPolynomial σ R) (MvPolynomial σ R))
    ((((Finsupp.lapply i ∘ₗ
                (↑(Basis.repr (mvPolynomialBasis R σ)) :
                  Ω[MvPolynomial σ R⁄R] →ₗ[MvPolynomial σ R] σ →₀ MvPolynomial σ R)).compDer :
            LinearMap (R := MvPolynomial σ R) (RingHom.id (MvPolynomial σ R))
              (Derivation R (MvPolynomial σ R) Ω[MvPolynomial σ R⁄R])
              (Derivation R (MvPolynomial σ R) (MvPolynomial σ R))) :
          (a : Derivation R (MvPolynomial σ R) Ω[MvPolynomial σ R⁄R]) →
            Derivation R (MvPolynomial σ R) (MvPolynomial σ R))
        (D R (MvPolynomial σ R)) :
      Derivation R (MvPolynomial σ R) (MvPolynomial σ R))
    (MvPolynomial.pderiv i : Derivation R (MvPolynomial σ R) (MvPolynomial σ R))
⊢ Eq (α := MvPolynomial σ R)
    ((((Basis.repr (mvPolynomialBasis R σ) : (a : Ω[MvPolynomial σ R⁄R]) → σ →₀ MvPolynomial σ R)
              ((D R (MvPolynomial σ R) : (a : MvPolynomial σ R) → Ω[MvPolynomial σ R⁄R]) x) :
            σ →₀ MvPolynomial σ R) :
          (a : σ) → MvPolynomial σ R)
        i :
      MvPolynomial σ R)
    ((MvPolynomial.pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) x : MvPolynomial σ R)

Tactic:
suffices ((Finsupp.lapply i).comp
    (mvPolynomialBasis R σ).repr.toLinearMap).compDer (D _ _) = MvPolynomial.pderiv i by
    rw [← this]; rfl
-- Module: Mathlib.RingTheory.Kaehler.Polynomial
Goal:
R : Type u
inst : CommRing R
σ : Type u_1
x : MvPolynomial σ R
i : σ
h :
  ∀ (i_1 : σ),
    Eq (α := MvPolynomial σ R)
      ((((((Finsupp.lapply i ∘ₗ
                        (↑(Basis.repr (mvPolynomialBasis R σ)) :
                          Ω[MvPolynomial σ R⁄R] →ₗ[MvPolynomial σ R] σ →₀ MvPolynomial σ R)).compDer :
                    LinearMap (R := MvPolynomial σ R) (RingHom.id (MvPolynomial σ R))
                      (Derivation R (MvPolynomial σ R) Ω[MvPolynomial σ R⁄R])
                      (Derivation R (MvPolynomial σ R) (MvPolynomial σ R))) :
                  (a : Derivation R (MvPolynomial σ R) Ω[MvPolynomial σ R⁄R]) →
                    Derivation R (MvPolynomial σ R) (MvPolynomial σ R))
                (D R (MvPolynomial σ R)) :
              Derivation R (MvPolynomial σ R) (MvPolynomial σ R)) :
            (a : MvPolynomial σ R) → MvPolynomial σ R)
          (MvPolynomial.X i_1) :
        MvPolynomial σ R)
      ((MvPolynomial.pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) (MvPolynomial.X i_1) : MvPolynomial σ R)
⊢ Eq (α := Derivation R (MvPolynomial σ R) (MvPolynomial σ R))
    ((((Finsupp.lapply i ∘ₗ
                (↑(Basis.repr (mvPolynomialBasis R σ)) :
                  Ω[MvPolynomial σ R⁄R] →ₗ[MvPolynomial σ R] σ →₀ MvPolynomial σ R)).compDer :
            LinearMap (R := MvPolynomial σ R) (RingHom.id (MvPolynomial σ R))
              (Derivation R (MvPolynomial σ R) Ω[MvPolynomial σ R⁄R])
              (Derivation R (MvPolynomial σ R) (MvPolynomial σ R))) :
          (a : Derivation R (MvPolynomial σ R) Ω[MvPolynomial σ R⁄R]) →
            Derivation R (MvPolynomial σ R) (MvPolynomial σ R))
        (D R (MvPolynomial σ R)) :
      Derivation R (MvPolynomial σ R) (MvPolynomial σ R))
    (MvPolynomial.pderiv i : Derivation R (MvPolynomial σ R) (MvPolynomial σ R))

Tactic:
apply MvPolynomial.derivation_ext

Premises used: MvPolynomial.derivation_ext
-- Module: Mathlib.RingTheory.Kaehler.Polynomial
Goal:
R : Type u
inst : CommRing R
σ : Type u_1
x : MvPolynomial σ R
i : σ
⊢ ∀ (i_1 : σ),
    Eq (α := MvPolynomial σ R)
      ((((((Finsupp.lapply i ∘ₗ
                        (↑(Basis.repr (mvPolynomialBasis R σ)) :
                          Ω[MvPolynomial σ R⁄R] →ₗ[MvPolynomial σ R] σ →₀ MvPolynomial σ R)).compDer :
                    LinearMap (R := MvPolynomial σ R) (RingHom.id (MvPolynomial σ R))
                      (Derivation R (MvPolynomial σ R) Ω[MvPolynomial σ R⁄R])
                      (Derivation R (MvPolynomial σ R) (MvPolynomial σ R))) :
                  (a : Derivation R (MvPolynomial σ R) Ω[MvPolynomial σ R⁄R]) →
                    Derivation R (MvPolynomial σ R) (MvPolynomial σ R))
                (D R (MvPolynomial σ R)) :
              Derivation R (MvPolynomial σ R) (MvPolynomial σ R)) :
            (a : MvPolynomial σ R) → MvPolynomial σ R)
          (MvPolynomial.X i_1) :
        MvPolynomial σ R)
      ((MvPolynomial.pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) (MvPolynomial.X i_1) : MvPolynomial σ R)

Tactic:
simp [Finsupp.single_apply, Pi.single_apply]

Premises used: Pi.single_apply, Finsupp.single_apply
-- Module: Mathlib.RingTheory.Kaehler.Polynomial
Goal:
R : Type u
inst : CommRing R
σ : Type u_1
x : MvPolynomial σ R
i : σ
suffices suffices₁ suffices₂ :
  Eq (α := Derivation R (MvPolynomial σ R) (MvPolynomial σ R))
    ((((Finsupp.lapply i ∘ₗ
                (↑(Basis.repr (mvPolynomialBasis R σ)) :
                  Ω[MvPolynomial σ R⁄R] →ₗ[MvPolynomial σ R] σ →₀ MvPolynomial σ R)).compDer :
            LinearMap (R := MvPolynomial σ R) (RingHom.id (MvPolynomial σ R))
              (Derivation R (MvPolynomial σ R) Ω[MvPolynomial σ R⁄R])
              (Derivation R (MvPolynomial σ R) (MvPolynomial σ R))) :
          (a : Derivation R (MvPolynomial σ R) Ω[MvPolynomial σ R⁄R]) →
            Derivation R (MvPolynomial σ R) (MvPolynomial σ R))
        (D R (MvPolynomial σ R)) :
      Derivation R (MvPolynomial σ R) (MvPolynomial σ R))
    (MvPolynomial.pderiv i : Derivation R (MvPolynomial σ R) (MvPolynomial σ R))
h :
  ∀ (i_1 : σ),
    Eq (α := MvPolynomial σ R)
      ((((((Finsupp.lapply i ∘ₗ
                        (↑(Basis.repr (mvPolynomialBasis R σ)) :
                          Ω[MvPolynomial σ R⁄R] →ₗ[MvPolynomial σ R] σ →₀ MvPolynomial σ R)).compDer :
                    LinearMap (R := MvPolynomial σ R) (RingHom.id (MvPolynomial σ R))
                      (Derivation R (MvPolynomial σ R) Ω[MvPolynomial σ R⁄R])
                      (Derivation R (MvPolynomial σ R) (MvPolynomial σ R))) :
                  (a : Derivation R (MvPolynomial σ R) Ω[MvPolynomial σ R⁄R]) →
                    Derivation R (MvPolynomial σ R) (MvPolynomial σ R))
                (D R (MvPolynomial σ R)) :
              Derivation R (MvPolynomial σ R) (MvPolynomial σ R)) :
            (a : MvPolynomial σ R) → MvPolynomial σ R)
          (MvPolynomial.X i_1) :
        MvPolynomial σ R)
      ((MvPolynomial.pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) (MvPolynomial.X i_1) : MvPolynomial σ R)
⊢ Eq (α := MvPolynomial σ R)
    ((((Basis.repr (mvPolynomialBasis R σ) : (a : Ω[MvPolynomial σ R⁄R]) → σ →₀ MvPolynomial σ R)
              ((D R (MvPolynomial σ R) : (a : MvPolynomial σ R) → Ω[MvPolynomial σ R⁄R]) x) :
            σ →₀ MvPolynomial σ R) :
          (a : σ) → MvPolynomial σ R)
        i :
      MvPolynomial σ R)
    ((MvPolynomial.pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) x : MvPolynomial σ R)

Tactic:
classical
  suffices ((Finsupp.lapply i).comp
    (mvPolynomialBasis R σ).repr.toLinearMap).compDer (D _ _) = MvPolynomial.pderiv i by
    rw [← this]; rfl
  apply MvPolynomial.derivation_ext
  simp [Finsupp.single_apply, Pi.single_apply]

Premises used: Pi.single_apply, MvPolynomial.derivation_ext, Finsupp.single_apply
-- Module: Mathlib.RingTheory.Kaehler.Polynomial
Goal:
R : Type u
inst : CommRing R
σ : Type u_1
i : σ
x : MvPolynomial σ R
a :
  Eq (α := σ →₀ MvPolynomial σ R)
    ((Basis.repr (mvPolynomialBasis R σ) : (a : Ω[MvPolynomial σ R⁄R]) → σ →₀ MvPolynomial σ R)
        ((LinearEquiv.symm (Basis.repr (mvPolynomialBasis R σ)) : (a : σ →₀ MvPolynomial σ R) → Ω[MvPolynomial σ R⁄R])
          (Finsupp.single i x)) :
      σ →₀ MvPolynomial σ R)
    ((Basis.repr (mvPolynomialBasis R σ) : (a : Ω[MvPolynomial σ R⁄R]) → σ →₀ MvPolynomial σ R)
        (HSMul.hSMul (β := Ω[MvPolynomial σ R⁄R]) x
          ((D R (MvPolynomial σ R) : (a : MvPolynomial σ R) → Ω[MvPolynomial σ R⁄R]) (MvPolynomial.X i) :
            Ω[MvPolynomial σ R⁄R])) :
      σ →₀ MvPolynomial σ R)
⊢ (LinearEquiv.symm (Basis.repr (mvPolynomialBasis R σ)) : (a : σ →₀ MvPolynomial σ R) → Ω[MvPolynomial σ R⁄R])
      (Finsupp.single i x) =
    HSMul.hSMul (β := Ω[MvPolynomial σ R⁄R]) x
      ((D R (MvPolynomial σ R) : (a : MvPolynomial σ R) → Ω[MvPolynomial σ R⁄R]) (MvPolynomial.X i) :
        Ω[MvPolynomial σ R⁄R])

Tactic:
apply (mvPolynomialBasis R σ).repr.injective

Premises used: KaehlerDifferential.mvPolynomialBasis, Module.Basis.repr, LinearEquiv.injective
-- Module: Mathlib.RingTheory.Kaehler.Polynomial
Goal:
R : Type u
inst : CommRing R
σ : Type u_1
i : σ
x : MvPolynomial σ R
⊢ Eq (α := σ →₀ MvPolynomial σ R)
    ((Basis.repr (mvPolynomialBasis R σ) : (a : Ω[MvPolynomial σ R⁄R]) → σ →₀ MvPolynomial σ R)
        ((LinearEquiv.symm (Basis.repr (mvPolynomialBasis R σ)) : (a : σ →₀ MvPolynomial σ R) → Ω[MvPolynomial σ R⁄R])
          (Finsupp.single i x)) :
      σ →₀ MvPolynomial σ R)
    ((Basis.repr (mvPolynomialBasis R σ) : (a : Ω[MvPolynomial σ R⁄R]) → σ →₀ MvPolynomial σ R)
        (HSMul.hSMul (β := Ω[MvPolynomial σ R⁄R]) x
          ((D R (MvPolynomial σ R) : (a : MvPolynomial σ R) → Ω[MvPolynomial σ R⁄R]) (MvPolynomial.X i) :
            Ω[MvPolynomial σ R⁄R])) :
      σ →₀ MvPolynomial σ R)

Tactic:
simp [LinearEquiv.map_smul, -map_smul]

Premises used: LinearEquiv.map_smul, map_smul
-- Module: Mathlib.RingTheory.Kaehler.Polynomial
Goal:
R : Type u
inst : CommRing R
σ : Type u_1
i : σ
⊢ Eq (α := Ω[MvPolynomial σ R⁄R]) ((mvPolynomialBasis R σ : (a : σ) → Ω[MvPolynomial σ R⁄R]) i : Ω[MvPolynomial σ R⁄R])
    ((D R (MvPolynomial σ R) : (a : MvPolynomial σ R) → Ω[MvPolynomial σ R⁄R]) (MvPolynomial.X i) :
      Ω[MvPolynomial σ R⁄R])

Tactic:
(mvPolynomialBasis_repr_symm_single R σ i 1).trans (one_smul _ _)

Premises used: one_smul, KaehlerDifferential.mvPolynomialBasis_repr_symm_single, OfNat.ofNat, Eq.trans
-- Module: Mathlib.RingTheory.Kaehler.Polynomial
Goal:
R : Type u
inst : CommRing R
σ : Type u_1
⊢ Free (MvPolynomial σ R) Ω[MvPolynomial σ R⁄R]

Tactic:
.of_basis (KaehlerDifferential.mvPolynomialBasis R σ)

Premises used: KaehlerDifferential.mvPolynomialBasis, Module.Free.of_basis
-- Module: Mathlib.RingTheory.Kaehler.Polynomial
Goal:
R : Type u
inst : CommRing R
P : R[X]
rw :
  (D R R[X] : (a : R[X]) → Ω[R[X]⁄R]) ((aeval X : (a : R[X]) → R[X]) P) =
    HSMul.hSMul (α := R[X]) (β := Ω[R[X]⁄R]) ((derivative : (a : R[X]) → R[X]) ((aeval X : (a : R[X]) → R[X]) P) : R[X])
      ((D R R[X] : (a : R[X]) → Ω[R[X]⁄R]) X : Ω[R[X]⁄R])
rw₁ :
  HSMul.hSMul (α := R[X]) (β := Ω[R[X]⁄R]) ((aeval X : (a : R[X]) → R[X]) ((derivative : (a : R[X]) → R[X]) P) : R[X])
      ((D R R[X] : (a : R[X]) → Ω[R[X]⁄R]) X : Ω[R[X]⁄R]) =
    HSMul.hSMul (α := R[X]) (β := Ω[R[X]⁄R]) ((derivative : (a : R[X]) → R[X]) ((aeval X : (a : R[X]) → R[X]) P) : R[X])
      ((D R R[X] : (a : R[X]) → Ω[R[X]⁄R]) X : Ω[R[X]⁄R])
rw₂ :
  HSMul.hSMul (α := R[X]) (β := Ω[R[X]⁄R]) ((derivative : (a : R[X]) → R[X]) P : R[X])
      ((D R R[X] : (a : R[X]) → Ω[R[X]⁄R]) X : Ω[R[X]⁄R]) =
    HSMul.hSMul (α := R[X]) (β := Ω[R[X]⁄R]) ((derivative : (a : R[X]) → R[X]) ((aeval X : (a : R[X]) → R[X]) P) : R[X])
      ((D R R[X] : (a : R[X]) → Ω[R[X]⁄R]) X : Ω[R[X]⁄R])
rw₃ rw₄ :
  HSMul.hSMul (α := R[X]) (β := Ω[R[X]⁄R]) ((derivative : (a : R[X]) → R[X]) P : R[X])
      ((D R R[X] : (a : R[X]) → Ω[R[X]⁄R]) X : Ω[R[X]⁄R]) =
    HSMul.hSMul (α := R[X]) (β := Ω[R[X]⁄R]) ((derivative : (a : R[X]) → R[X]) P : R[X])
      ((D R R[X] : (a : R[X]) → Ω[R[X]⁄R]) X : Ω[R[X]⁄R])
⊢ (D R R[X] : (a : R[X]) → Ω[R[X]⁄R]) P =
    HSMul.hSMul (α := R[X]) (β := Ω[R[X]⁄R]) ((derivative : (a : R[X]) → R[X]) P : R[X])
      ((D R R[X] : (a : R[X]) → Ω[R[X]⁄R]) X : Ω[R[X]⁄R])

Tactic:
rw [← aeval_X_left_apply P, (D R R[X]).map_aeval, aeval_X_left_apply, aeval_X_left_apply]

Premises used: Polynomial.aeval_X_left_apply, Polynomial, KaehlerDifferential.D, Derivation.map_aeval
-- Module: Mathlib.RingTheory.Kaehler.Polynomial
Goal:
R : Type u
inst : CommRing R
x : Ω[R[X]⁄R]
obtain :
  ∀ (x : R[X] →₀ R[X]),
    Eq (α := Ω[R[X]⁄R])
      (((((LinearMap.flip (AlgHom.toLinearMap (lsmul R R Ω[R[X]⁄R]) : R[X] →ₗ[R] End R Ω[R[X]⁄R]) :
                    Ω[R[X]⁄R] →ₗ[R] R[X] →ₗ[R] Ω[R[X]⁄R]) :
                  (a : Ω[R[X]⁄R]) → R[X] →ₗ[R] Ω[R[X]⁄R])
                ((D R R[X] : (a : R[X]) → Ω[R[X]⁄R]) X) :
              R[X] →ₗ[R] Ω[R[X]⁄R]) :
            (a : R[X]) → Ω[R[X]⁄R])
          (AddHom.toFun (LinearMap.toAddHom (Derivation.liftKaehlerDifferential derivative'))
            ((Finsupp.linearCombination R[X] (⇑(D R R[X]) : (a : R[X]) → Ω[R[X]⁄R]) : (a : R[X] →₀ R[X]) → Ω[R[X]⁄R])
              x)) :
        Ω[R[X]⁄R])
      ((Finsupp.linearCombination R[X] (⇑(D R R[X]) : (a : R[X]) → Ω[R[X]⁄R]) : (a : R[X] →₀ R[X]) → Ω[R[X]⁄R]) x :
        Ω[R[X]⁄R])
⊢ ((((LinearMap.flip (AlgHom.toLinearMap (lsmul R R Ω[R[X]⁄R]) : R[X] →ₗ[R] End R Ω[R[X]⁄R]) :
                Ω[R[X]⁄R] →ₗ[R] R[X] →ₗ[R] Ω[R[X]⁄R]) :
              (a : Ω[R[X]⁄R]) → R[X] →ₗ[R] Ω[R[X]⁄R])
            ((D R R[X] : (a : R[X]) → Ω[R[X]⁄R]) X) :
          R[X] →ₗ[R] Ω[R[X]⁄R]) :
        (a : R[X]) → Ω[R[X]⁄R])
      (AddHom.toFun (LinearMap.toAddHom (Derivation.liftKaehlerDifferential derivative')) x) =
    x

Tactic:
obtain ⟨x, rfl⟩ := linearCombination_surjective _ _ x

Premises used: rfl, KaehlerDifferential.linearCombination_surjective
-- Module: Mathlib.RingTheory.Kaehler.Polynomial
Goal:
R : Type u
inst : CommRing R
⊢ Eq (α := Ω[R[X]⁄R])
    (((((LinearMap.flip (AlgHom.toLinearMap (lsmul R R Ω[R[X]⁄R]) : R[X] →ₗ[R] End R Ω[R[X]⁄R]) :
                  Ω[R[X]⁄R] →ₗ[R] R[X] →ₗ[R] Ω[R[X]⁄R]) :
                (a : Ω[R[X]⁄R]) → R[X] →ₗ[R] Ω[R[X]⁄R])
              ((D R R[X] : (a : R[X]) → Ω[R[X]⁄R]) X) :
            R[X] →ₗ[R] Ω[R[X]⁄R]) :
          (a : R[X]) → Ω[R[X]⁄R])
        (AddHom.toFun (LinearMap.toAddHom (Derivation.liftKaehlerDifferential derivative'))
          ((Finsupp.linearCombination R[X] (⇑(D R R[X]) : (a : R[X]) → Ω[R[X]⁄R]) : (a : R[X] →₀ R[X]) → Ω[R[X]⁄R])
            0)) :
      Ω[R[X]⁄R])
    ((Finsupp.linearCombination R[X] (⇑(D R R[X]) : (a : R[X]) → Ω[R[X]⁄R]) : (a : R[X] →₀ R[X]) → Ω[R[X]⁄R]) 0 :
      Ω[R[X]⁄R])

Tactic:
simp
-- Module: Mathlib.RingTheory.Kaehler.Polynomial
Goal:
R : Type u
inst : CommRing R
x y : R[X] →₀ R[X]
hx :
  HSMul.hSMul (α := R[X]) (β := Ω[R[X]⁄R])
      ((Derivation.liftKaehlerDifferential derivative' : (a : Ω[R[X]⁄R]) → R[X])
          ((Finsupp.linearCombination R[X] (⇑(D R R[X]) : (a : R[X]) → Ω[R[X]⁄R]) : (a : R[X] →₀ R[X]) → Ω[R[X]⁄R]) x) :
        R[X])
      ((D R R[X] : (a : R[X]) → Ω[R[X]⁄R]) X : Ω[R[X]⁄R]) =
    (Finsupp.linearCombination R[X] (⇑(D R R[X]) : (a : R[X]) → Ω[R[X]⁄R]) : (a : R[X] →₀ R[X]) → Ω[R[X]⁄R]) x
hy :
  HSMul.hSMul (α := R[X]) (β := Ω[R[X]⁄R])
      ((Derivation.liftKaehlerDifferential derivative' : (a : Ω[R[X]⁄R]) → R[X])
          ((Finsupp.linearCombination R[X] (⇑(D R R[X]) : (a : R[X]) → Ω[R[X]⁄R]) : (a : R[X] →₀ R[X]) → Ω[R[X]⁄R]) y) :
        R[X])
      ((D R R[X] : (a : R[X]) → Ω[R[X]⁄R]) X : Ω[R[X]⁄R]) =
    (Finsupp.linearCombination R[X] (⇑(D R R[X]) : (a : R[X]) → Ω[R[X]⁄R]) : (a : R[X] →₀ R[X]) → Ω[R[X]⁄R]) y
⊢ HSMul.hSMul (α := R[X]) (β := Ω[R[X]⁄R])
        ((Derivation.liftKaehlerDifferential derivative' : (a : Ω[R[X]⁄R]) → R[X])
            ((Finsupp.linearCombination R[X] (⇑(D R R[X]) : (a : R[X]) → Ω[R[X]⁄R]) : (a : R[X] →₀ R[X]) → Ω[R[X]⁄R])
              x) :
          R[X])
        ((D R R[X] : (a : R[X]) → Ω[R[X]⁄R]) X : Ω[R[X]⁄R]) +
      HSMul.hSMul (α := R[X]) (β := Ω[R[X]⁄R])
        ((Derivation.liftKaehlerDifferential derivative' : (a : Ω[R[X]⁄R]) → R[X])
            ((Finsupp.linearCombination R[X] (⇑(D R R[X]) : (a : R[X]) → Ω[R[X]⁄R]) : (a : R[X] →₀ R[X]) → Ω[R[X]⁄R])
              y) :
          R[X])
        ((D R R[X] : (a : R[X]) → Ω[R[X]⁄R]) X : Ω[R[X]⁄R]) =
    HAdd.hAdd (α := Ω[R[X]⁄R]) (β := Ω[R[X]⁄R])
      ((Finsupp.linearCombination R[X] (⇑(D R R[X]) : (a : R[X]) → Ω[R[X]⁄R]) : (a : R[X] →₀ R[X]) → Ω[R[X]⁄R]) x :
        Ω[R[X]⁄R])
      ((Finsupp.linearCombination R[X] (⇑(D R R[X]) : (a : R[X]) → Ω[R[X]⁄R]) : (a : R[X] →₀ R[X]) → Ω[R[X]⁄R]) y :
        Ω[R[X]⁄R])

Tactic:
simp only [*]
-- Module: Mathlib.RingTheory.Kaehler.Polynomial
Goal:
R : Type u
inst : CommRing R
x y : R[X]
⊢ Eq (α := Ω[R[X]⁄R])
    (((((LinearMap.flip (AlgHom.toLinearMap (lsmul R R Ω[R[X]⁄R]) : R[X] →ₗ[R] End R Ω[R[X]⁄R]) :
                  Ω[R[X]⁄R] →ₗ[R] R[X] →ₗ[R] Ω[R[X]⁄R]) :
                (a : Ω[R[X]⁄R]) → R[X] →ₗ[R] Ω[R[X]⁄R])
              ((D R R[X] : (a : R[X]) → Ω[R[X]⁄R]) X) :
            R[X] →ₗ[R] Ω[R[X]⁄R]) :
          (a : R[X]) → Ω[R[X]⁄R])
        (AddHom.toFun (LinearMap.toAddHom (Derivation.liftKaehlerDifferential derivative'))
          ((Finsupp.linearCombination R[X] (⇑(D R R[X]) : (a : R[X]) → Ω[R[X]⁄R]) : (a : R[X] →₀ R[X]) → Ω[R[X]⁄R])
            (Finsupp.single x y))) :
      Ω[R[X]⁄R])
    ((Finsupp.linearCombination R[X] (⇑(D R R[X]) : (a : R[X]) → Ω[R[X]⁄R]) : (a : R[X] →₀ R[X]) → Ω[R[X]⁄R])
        (Finsupp.single x y) :
      Ω[R[X]⁄R])

Tactic:
simp [polynomial_D_apply _ x]

Premises used: KaehlerDifferential.polynomial_D_apply