awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Kaehler.JacobiZariski
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u₃
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
τ : Type w₅
Q : Generators S T ι
P : Generators R S σ
W : Generators R T τ
f : W.Hom Q
change :
  Function.Exact (M := Extension.H1Cotangent (toExtension (Q.comp P))) (N := Q.toExtension.H1Cotangent) (P :=
    T ⊗[S] Ω[S⁄R])
    (⇑((↑T :
              {S : Type u₃} →
                {M : Type (max u₁ w₅)} →
                  {M₂ : Type (max u₂ w₁)} →
                    [inst : Semiring T] →
                      [inst_7 : Semiring S] →
                        [inst_8 : AddCommMonoid M] →
                          [inst_9 : AddCommMonoid M₂] →
                            [inst_10 : Module T M] →
                              [inst_11 : Module T M₂] →
                                [inst_12 : Module S M] →
                                  [inst_13 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ T S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[T] M₂)
            (Extension.H1Cotangent.map f.toExtensionHom) ∘ₗ
          Extension.H1Cotangent.map (Hom.toExtensionHom (defaultHom (Q.comp P) W))) :
      (a : (Q.comp P).toExtension.H1Cotangent) → Q.toExtension.H1Cotangent)
    (⇑(δ Q P) : (a : Q.toExtension.H1Cotangent) → T ⊗[S] Ω[S⁄R])
⊢ Function.Exact (M := Extension.H1Cotangent (toExtension (Q.comp P))) (N := Q.toExtension.H1Cotangent) (P :=
    T ⊗[S] Ω[S⁄R])
    (⇑(Extension.H1Cotangent.map f.toExtensionHom ∘ₗ
          (↑(equiv (Q.comp P) W) : (Q.comp P).toExtension.H1Cotangent →ₗ[T] W.toExtension.H1Cotangent)) :
      (a : (Q.comp P).toExtension.H1Cotangent) → Q.toExtension.H1Cotangent)
    (⇑(δ Q P) : (a : Q.toExtension.H1Cotangent) → T ⊗[S] Ω[S⁄R])

Tactic:
change Function.Exact ((Extension.H1Cotangent.map f.toExtensionHom).restrictScalars T ∘ₗ
    (Extension.H1Cotangent.map _)) (δ Q P)

Premises used: Function.Exact, LinearMap.restrictScalars, Algebra.Extension.H1Cotangent.map, Algebra.Generators.Hom.toExtensionHom, LinearMap.comp, Algebra.Generators.H1Cotangent.δ, DFunLike.coe
-- Module: Mathlib.RingTheory.Kaehler.JacobiZariski
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u₃
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
τ : Type w₅
Q : Generators S T ι
P : Generators R S σ
W : Generators R T τ
f : W.Hom Q
rw :
  Function.Exact (M := Extension.H1Cotangent (toExtension (Q.comp P))) (N := Q.toExtension.H1Cotangent) (P :=
    T ⊗[S] Ω[S⁄R])
    (⇑(Extension.H1Cotangent.map (Hom.toExtensionHom (Q.ofComp P))) :
      (a : (Q.comp P).toExtension.H1Cotangent) → Q.toExtension.H1Cotangent)
    (⇑(δ Q P) : (a : Q.toExtension.H1Cotangent) → T ⊗[S] Ω[S⁄R])
⊢ Function.Exact (M := Extension.H1Cotangent (toExtension (Q.comp P))) (N := Q.toExtension.H1Cotangent) (P :=
    T ⊗[S] Ω[S⁄R])
    (⇑((↑T :
              {S : Type u₃} →
                {M : Type (max u₁ w₅)} →
                  {M₂ : Type (max u₂ w₁)} →
                    [inst : Semiring T] →
                      [inst_7 : Semiring S] →
                        [inst_8 : AddCommMonoid M] →
                          [inst_9 : AddCommMonoid M₂] →
                            [inst_10 : Module T M] →
                              [inst_11 : Module T M₂] →
                                [inst_12 : Module S M] →
                                  [inst_13 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ T S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[T] M₂)
            (Extension.H1Cotangent.map f.toExtensionHom) ∘ₗ
          Extension.H1Cotangent.map (Hom.toExtensionHom (defaultHom (Q.comp P) W))) :
      (a : (Q.comp P).toExtension.H1Cotangent) → Q.toExtension.H1Cotangent)
    (⇑(δ Q P) : (a : Q.toExtension.H1Cotangent) → T ⊗[S] Ω[S⁄R])

Tactic:
rw [← Extension.H1Cotangent.map_comp, Extension.H1Cotangent.map_eq _ (Q.ofComp P).toExtensionHom]

Premises used: Algebra.Extension.H1Cotangent.map_eq, Algebra.Generators.Hom.toExtensionHom, Algebra.Generators.ofComp, Algebra.Extension.H1Cotangent.map_comp
-- Module: Mathlib.RingTheory.Kaehler.JacobiZariski
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u₃
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
τ : Type w₅
Q : Generators S T ι
P : Generators R S σ
W : Generators R T τ
f : W.Hom Q
⊢ Function.Exact (M := Extension.H1Cotangent (toExtension (Q.comp P))) (N := Q.toExtension.H1Cotangent) (P :=
    T ⊗[S] Ω[S⁄R])
    (⇑(Extension.H1Cotangent.map (Hom.toExtensionHom (Q.ofComp P))) :
      (a : (Q.comp P).toExtension.H1Cotangent) → Q.toExtension.H1Cotangent)
    (⇑(δ Q P) : (a : Q.toExtension.H1Cotangent) → T ⊗[S] Ω[S⁄R])

Tactic:
exact_map_δ Q P

Premises used: Algebra.Generators.H1Cotangent.exact_map_δ
-- Module: Mathlib.RingTheory.Kaehler.JacobiZariski
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u₃
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
τ : Type w₅
Q : Generators S T ι
P : Generators R S σ
W : Generators R T τ
f : W.Hom Q
⊢ Function.Exact (M := Extension.H1Cotangent (toExtension (Q.comp P))) (N := Q.toExtension.H1Cotangent) (P :=
    T ⊗[S] Ω[S⁄R])
    (⇑(Extension.H1Cotangent.map (Hom.toExtensionHom (Q.ofComp P))) :
      (a : (Q.comp P).toExtension.H1Cotangent) → Q.toExtension.H1Cotangent)
    (⇑(δ Q P) : (a : Q.toExtension.H1Cotangent) → T ⊗[S] Ω[S⁄R])

Tactic:
exact exact_map_δ Q P

Premises used: Algebra.Generators.H1Cotangent.exact_map_δ
-- Module: Mathlib.RingTheory.Kaehler.JacobiZariski
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u₃
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
⊢ Function.Exact (M := H1Cotangent R T) (N := H1Cotangent S T) (P := T ⊗[S] Ω[S⁄R])
    (⇑(map R S T T) : (a : H1Cotangent R T) → H1Cotangent S T) (⇑(δ R S T) : (a : H1Cotangent S T) → T ⊗[S] Ω[S⁄R])

Tactic:
Generators.H1Cotangent.exact_map_δ' (Generators.self S T)
    (Generators.self R S) (Generators.self R T) (Generators.defaultHom _ _)

Premises used: Algebra.Generators.self, Algebra.Generators.defaultHom, Algebra.Generators.H1Cotangent.exact_map_δ'
-- Module: Mathlib.RingTheory.Kaehler.JacobiZariski
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u₃
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
⊢ Function.Exact (M := H1Cotangent S T) (N := T ⊗[S] Ω[S⁄R]) (P := Ω[T⁄R])
    (⇑(δ R S T) : (a : H1Cotangent S T) → T ⊗[S] Ω[S⁄R]) (⇑(mapBaseChange R S T) : (a : T ⊗[S] Ω[S⁄R]) → Ω[T⁄R])

Tactic:
Generators.H1Cotangent.exact_δ_map (Generators.self S T) (Generators.self R S)

Premises used: Algebra.Generators.self, Algebra.Generators.H1Cotangent.exact_δ_map
-- Module: Mathlib.RingTheory.Kaehler.Polynomial
Goal:
R : Type u
inst : CommRing R
σ : Type u_1
x : Ω[MvPolynomial σ R⁄R]
obtain :
  ∀ (x : 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])
              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])
⊢ (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
        (LinearMap.toAddHom
          (Derivation.liftKaehlerDifferential (MvPolynomial.mkDerivation R fun (x : σ) ↦ Finsupp.single x 1)))
        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
σ : Type u_1
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])
      ((Derivation.liftKaehlerDifferential (MvPolynomial.mkDerivation R fun (x : σ) ↦ Finsupp.single x 1) :
          (a : Ω[MvPolynomial σ R⁄R]) → σ →₀ MvPolynomial σ R)
        0))
    0
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])
      0)
    0
zero₂ zero₃ : Eq (α := Ω[MvPolynomial σ R⁄R]) 0 0
⊢ 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])
      ((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])
          0)))
    ((Finsupp.linearCombination (MvPolynomial σ R)
          (⇑(D R (MvPolynomial σ R)) : (a : MvPolynomial σ R) → Ω[MvPolynomial σ R⁄R]) :
        (a : MvPolynomial σ R →₀ MvPolynomial σ R) → Ω[MvPolynomial σ R⁄R])
      0)

Tactic:
rw [map_zero, map_zero, map_zero]

Premises used: map_zero
-- Module: Mathlib.RingTheory.Kaehler.Polynomial
Goal:
R : Type u
inst : CommRing R
σ : Type u_1
a b : MvPolynomial σ R
single :
  HSMul.hSMul (β := Ω[MvPolynomial σ R⁄R]) b
      ((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]) =
    HSMul.hSMul (β := Ω[MvPolynomial σ R⁄R]) b
      ((D R (MvPolynomial σ R) : (a : MvPolynomial σ R) → Ω[MvPolynomial σ R⁄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])
        (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:
simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, Finsupp.linearCombination_single,
        map_smul, Derivation.liftKaehlerDifferential_comp_D]

Premises used: AddHom.toFun_eq_coe, Derivation.liftKaehlerDifferential_comp_D, Finsupp.linearCombination_single, LinearMap.coe_toAddHom, map_smul
-- Module: Mathlib.RingTheory.Kaehler.Polynomial
Goal:
R : Type u
inst : CommRing R
σ : Type u_1
a b : MvPolynomial σ R
single :
  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])
⊢ HSMul.hSMul (β := Ω[MvPolynomial σ R⁄R]) b
      ((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]) =
    HSMul.hSMul (β := Ω[MvPolynomial σ R⁄R]) b
      ((D R (MvPolynomial σ R) : (a : MvPolynomial σ R) → Ω[MvPolynomial σ R⁄R]) a : Ω[MvPolynomial σ R⁄R])

Tactic:
congr 1
-- Module: Mathlib.RingTheory.Kaehler.Polynomial
Goal:
R : Type u
inst : CommRing R
σ : Type u_1
b : MvPolynomial σ R
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])

Tactic:
simp only [MvPolynomial.derivation_C, map_zero]

Premises used: map_zero, MvPolynomial.derivation_C
-- Module: Mathlib.RingTheory.Kaehler.Polynomial
Goal:
R : Type u
inst : CommRing R
σ : Type u_1
b p q : 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])
        ((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])
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])
        ((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:
simp only [map_add, *]

Premises used: map_add
-- Module: Mathlib.RingTheory.Kaehler.Polynomial
Goal:
R : Type u
inst : CommRing R
σ : Type u_1
b p : MvPolynomial σ R
n : σ
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])
        ((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)
          (p * MvPolynomial.X n)) :
      Ω[MvPolynomial σ R⁄R])
    ((D R (MvPolynomial σ R) : (a : MvPolynomial σ R) → Ω[MvPolynomial σ R⁄R]) (p * MvPolynomial.X n) :
      Ω[MvPolynomial σ R⁄R])

Tactic:
simp [*]
-- Module: Mathlib.RingTheory.Kaehler.Polynomial
Goal:
R : Type u
inst : CommRing R
σ : Type u_1
zero :
  Eq (α := σ →₀ MvPolynomial σ R)
    ((Derivation.liftKaehlerDifferential (MvPolynomial.mkDerivation R fun (x : σ) ↦ Finsupp.single x 1) :
        (a : Ω[MvPolynomial σ R⁄R]) → σ →₀ MvPolynomial σ R)
      0)
    0
zero₁ zero₂ : Eq (α := σ →₀ MvPolynomial σ R) 0 0
⊢ Eq (α := σ →₀ MvPolynomial σ R)
    ((Derivation.liftKaehlerDifferential (MvPolynomial.mkDerivation R fun (x : σ) ↦ Finsupp.single x 1) :
        (a : Ω[MvPolynomial σ R⁄R]) → σ →₀ MvPolynomial σ 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])
        0))
    0

Tactic:
rw [map_zero, map_zero]

Premises used: map_zero
-- Module: Mathlib.RingTheory.Kaehler.Polynomial
Goal:
R : Type u
inst : CommRing R
σ : Type u_1
f g : σ →₀ MvPolynomial σ R
h :
  AddHom.toFun (M := Ω[MvPolynomial σ R⁄R])
      (LinearMap.toAddHom
        (Derivation.liftKaehlerDifferential (MvPolynomial.mkDerivation R fun (x : σ) ↦ Finsupp.single x 1)))
      ((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])
        f) =
    f
h_1 :
  AddHom.toFun (M := Ω[MvPolynomial σ R⁄R])
      (LinearMap.toAddHom
        (Derivation.liftKaehlerDifferential (MvPolynomial.mkDerivation R fun (x : σ) ↦ Finsupp.single x 1)))
      ((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])
        g) =
    g
add :
  HAdd.hAdd (α := σ →₀ MvPolynomial σ R) (β := σ →₀ MvPolynomial σ R)
      ((Derivation.liftKaehlerDifferential (MvPolynomial.mkDerivation R fun (x : σ) ↦ Finsupp.single x 1) :
            (a : Ω[MvPolynomial σ R⁄R]) → σ →₀ MvPolynomial σ 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])
            f) :
        σ →₀ MvPolynomial σ R)
      ((Derivation.liftKaehlerDifferential (MvPolynomial.mkDerivation R fun (x : σ) ↦ Finsupp.single x 1) :
            (a : Ω[MvPolynomial σ R⁄R]) → σ →₀ MvPolynomial σ 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])
            g) :
        σ →₀ MvPolynomial σ R) =
    f + g
⊢ AddHom.toFun (M := Ω[MvPolynomial σ R⁄R])
      (LinearMap.toAddHom
        (Derivation.liftKaehlerDifferential (MvPolynomial.mkDerivation R fun (x : σ) ↦ Finsupp.single x 1)))
      ((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])
        (f + g)) =
    f + g

Tactic:
simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, map_add] at *

Premises used: AddHom.toFun_eq_coe, map_add, LinearMap.coe_toAddHom
-- Module: Mathlib.RingTheory.Kaehler.Polynomial
Goal:
R : Type u
inst : CommRing R
σ : Type u_1
f g : σ →₀ MvPolynomial σ R
h :
  (Derivation.liftKaehlerDifferential (MvPolynomial.mkDerivation R fun (x : σ) ↦ Finsupp.single x 1) :
        (a : Ω[MvPolynomial σ R⁄R]) → σ →₀ MvPolynomial σ 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])
        f) =
    f
h_1 :
  (Derivation.liftKaehlerDifferential (MvPolynomial.mkDerivation R fun (x : σ) ↦ Finsupp.single x 1) :
        (a : Ω[MvPolynomial σ R⁄R]) → σ →₀ MvPolynomial σ 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])
        g) =
    g
⊢ HAdd.hAdd (α := σ →₀ MvPolynomial σ R) (β := σ →₀ MvPolynomial σ R)
      ((Derivation.liftKaehlerDifferential (MvPolynomial.mkDerivation R fun (x : σ) ↦ Finsupp.single x 1) :
            (a : Ω[MvPolynomial σ R⁄R]) → σ →₀ MvPolynomial σ 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])
            f) :
        σ →₀ MvPolynomial σ R)
      ((Derivation.liftKaehlerDifferential (MvPolynomial.mkDerivation R fun (x : σ) ↦ Finsupp.single x 1) :
            (a : Ω[MvPolynomial σ R⁄R]) → σ →₀ MvPolynomial σ 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])
            g) :
        σ →₀ MvPolynomial σ R) =
    f + g

Tactic:
simp only [*]
-- Module: Mathlib.RingTheory.Kaehler.Polynomial
Goal:
R : Type u
inst : CommRing R
σ : Type u_1
a : σ
b : MvPolynomial σ R
⊢ Eq (α := σ →₀ MvPolynomial σ R)
    (AddHom.toFun (M := Ω[MvPolynomial σ R⁄R])
      (LinearMap.toAddHom
        (Derivation.liftKaehlerDifferential (MvPolynomial.mkDerivation R fun (x : σ) ↦ Finsupp.single x 1)))
      ((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])
        (Finsupp.single a b)))
    (Finsupp.single a b)

Tactic:
simp [-map_smul]

Premises used: map_smul