awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Polynomial (goal)
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)
    ((MvPolynomial.pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) x : MvPolynomial σ R)
have 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)
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Polynomial (goal)
Goal:
R : Type u
inst : CommRing R
σ : Type u_1
x : MvPolynomial σ R
i : σ
⊢ 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)
have 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))
Tactic: suffices ((Finsupp.lapply i).comp
    (mvPolynomialBasis R σ).repr.toLinearMap).compDer (D _ _) = MvPolynomial.pderiv i by
    rw [← this]; rfl
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Polynomial (goal)
Goal:
R : Type u
inst : CommRing R
σ : Type u_1
x : MvPolynomial σ R
i : σ
⊢ 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))
have 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)
Tactic: apply MvPolynomial.derivation_ext
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Polynomial (goal)
Goal:
R : Type u
inst : CommRing R
σ : Type u_1
x : MvPolynomial σ R
i : σ
⊢ 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)
have 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))
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]
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Polynomial (goal)
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))
⊢ 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)
have 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)
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]
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Polynomial (goal)
Goal:
R : Type u
inst : CommRing R
σ : Type u_1
i : σ
x : 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])
have 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)
Tactic: apply (mvPolynomialBasis R σ).repr.injective
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Polynomial (goal)
Goal:
R : Type u
inst : CommRing R
P : R[X]
⊢ (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])
have 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])
Tactic: rw [← aeval_X_left_apply P, (D R R[X]).map_aeval, aeval_X_left_apply, aeval_X_left_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Polynomial (goal)
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])
⊢ (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])
have 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])
Tactic: rw [← aeval_X_left_apply P, (D R R[X]).map_aeval, aeval_X_left_apply, aeval_X_left_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Polynomial (goal)
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])
⊢ (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])
have 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])
Tactic: rw [← aeval_X_left_apply P, (D R R[X]).map_aeval, aeval_X_left_apply, aeval_X_left_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Polynomial (goal)
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])
⊢ (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])
have 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])
Tactic: rw [← aeval_X_left_apply P, (D R R[X]).map_aeval, aeval_X_left_apply, aeval_X_left_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Polynomial (goal)
Goal:
R : Type u
inst : CommRing 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
have 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])
Tactic: obtain ⟨x, rfl⟩ := linearCombination_surjective _ _ x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Polynomial (goal)
Goal:
R : Type u
inst : CommRing R
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])
have zero : 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: induction x using Finsupp.induction_linear with
    | zero => simp
    | add x y hx hy =>
      simp only [map_add, AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, LinearMap.flip_apply,
        AlgHom.toLinearMap_apply, lsmul_coe] at *; simp only [*]
    | single x y => simp [polynomial_D_apply _ x]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.TensorProduct (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing A
inst_4 : Algebra R A
a : A
⊢ HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) a 0 = 0
have rw : HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) a (0 ⊗ₜ[R] 0) = 0 ⊗ₜ[R] 0
Tactic: rw [← zero_tmul _ (0 : Ω[A⁄R]), mulActionBaseChange_smul_tmul, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.TensorProduct (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing A
inst_4 : Algebra R A
a : A
rw : HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) a (0 ⊗ₜ[R] 0) = 0 ⊗ₜ[R] 0
⊢ HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) a 0 = 0
have rw₁ : Eq (α := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) (0 ⊗ₜ[R] HSMul.hSMul (β := Ω[A⁄R]) a 0) (0 ⊗ₜ[R] 0)
Tactic: rw [← zero_tmul _ (0 : Ω[A⁄R]), mulActionBaseChange_smul_tmul, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.TensorProduct (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing A
inst_4 : Algebra R A
a : A
rw : HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) a (0 ⊗ₜ[R] 0) = 0 ⊗ₜ[R] 0
rw₁ : Eq (α := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) (0 ⊗ₜ[R] HSMul.hSMul (β := Ω[A⁄R]) a 0) (0 ⊗ₜ[R] 0)
⊢ HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) a 0 = 0
have rw₂ : Eq (α := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) (0 ⊗ₜ[R] 0) (0 ⊗ₜ[R] 0)
Tactic: rw [← zero_tmul _ (0 : Ω[A⁄R]), mulActionBaseChange_smul_tmul, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.TensorProduct (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing A
inst_4 : Algebra R A
a : A
x y : TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]
⊢ a • (x + y) = a • x + a • y
have change : (LinearEquiv.symm (TensorProduct.comm R S Ω[A⁄R]) : (a : Ω[A⁄R] ⊗[R] S) → S ⊗[R] Ω[A⁄R])
    (HSMul.hSMul (β := TensorProduct.{u_1, u_3, u_2} R Ω[A⁄R] S) a
      ((TensorProduct.comm R S Ω[A⁄R] : (a : S ⊗[R] Ω[A⁄R]) → Ω[A⁄R] ⊗[R] S) (x + y) :
        TensorProduct.{u_1, u_3, u_2} R Ω[A⁄R] S)) =
  a • x + a • y
Tactic: change (TensorProduct.comm R S Ω[A⁄R]).symm (a • (TensorProduct.comm R S Ω[A⁄R]) (x + y)) = _
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.TensorProduct (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing A
inst_4 : Algebra R A
a : A
x y : TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]
⊢ (LinearEquiv.symm (TensorProduct.comm R S Ω[A⁄R]) : (a : Ω[A⁄R] ⊗[R] S) → S ⊗[R] Ω[A⁄R])
      (HSMul.hSMul (β := TensorProduct.{u_1, u_3, u_2} R Ω[A⁄R] S) a
        ((TensorProduct.comm R S Ω[A⁄R] : (a : S ⊗[R] Ω[A⁄R]) → Ω[A⁄R] ⊗[R] S) (x + y) :
          TensorProduct.{u_1, u_3, u_2} R Ω[A⁄R] S)) =
    a • x + a • y
have rw : HAdd.hAdd (α := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])
    ((LinearEquiv.symm (TensorProduct.comm R S Ω[A⁄R]) : (a : Ω[A⁄R] ⊗[R] S) → S ⊗[R] Ω[A⁄R])
        (HSMul.hSMul (β := TensorProduct.{u_1, u_3, u_2} R Ω[A⁄R] S) a
          ((TensorProduct.comm R S Ω[A⁄R] : (a : S ⊗[R] Ω[A⁄R]) → Ω[A⁄R] ⊗[R] S) x :
            TensorProduct.{u_1, u_3, u_2} R Ω[A⁄R] S)) :
      TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])
    ((LinearEquiv.symm (TensorProduct.comm R S Ω[A⁄R]) : (a : Ω[A⁄R] ⊗[R] S) → S ⊗[R] Ω[A⁄R])
        (HSMul.hSMul (β := TensorProduct.{u_1, u_3, u_2} R Ω[A⁄R] S) a
          ((TensorProduct.comm R S Ω[A⁄R] : (a : S ⊗[R] Ω[A⁄R]) → Ω[A⁄R] ⊗[R] S) y :
            TensorProduct.{u_1, u_3, u_2} R Ω[A⁄R] S)) :
      TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) =
  a • x + a • y
Tactic: rw [map_add, smul_add, map_add]
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.TensorProduct (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra A B
inst_8 : Algebra S B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
r s : A
x : TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]
⊢ (r + s) • x = r • x + s • x
have zero : HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) (r + s) 0 =
  HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) r 0 +
    HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) s 0
Tactic: induction x
Cleared hypotheses: x