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⁄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
have 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])
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
σ : Type u_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])
      ((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)
have 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
Tactic: rw [map_zero, map_zero, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Polynomial (goal)
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
⊢ 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)
have 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
Tactic: rw [map_zero, map_zero, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Polynomial (goal)
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
⊢ 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)
have zero₂ : Eq (α := Ω[MvPolynomial σ R⁄R]) 0 0
Tactic: rw [map_zero, map_zero, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Polynomial (goal)
Goal:
R : Type u
inst : CommRing R
σ : Type u_1
a b : 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])
            (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])
have 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])
Tactic: simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, Finsupp.linearCombination_single,
        map_smul, Derivation.liftKaehlerDifferential_comp_D]
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Polynomial (goal)
Goal:
R : Type u
inst : CommRing R
σ : Type u_1
a b : MvPolynomial σ 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])
have 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])
Tactic: congr 1
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Polynomial (goal)
Goal:
R : Type u
inst : CommRing R
σ : Type u_1
a b : 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])
        ((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])
have single : ∀ (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: induction a using MvPolynomial.induction_on
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Polynomial (goal)
Goal:
R : Type u
inst : CommRing R
σ : Type u_1
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])
have 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])
    (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])
        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: induction x using Finsupp.induction_linear with
    | zero =>
      simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom]
      rw [map_zero, map_zero, map_zero]
    | add => simp only [map_add, AddHom.toFun_eq_coe, LinearMap.coe_toAddHom] at *; simp only [*]
    | single a b =>
      simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, Finsupp.linearCombination_single,
        map_smul, Derivation.liftKaehlerDifferential_comp_D]
      congr 1
      induction a using MvPolynomial.induction_on
      · simp only [MvPolynomial.derivation_C, map_zero]
      · simp only [map_add, *]
      · simp [*]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Polynomial (goal)
Goal:
R : Type u
inst : CommRing R
σ : Type u_1
⊢ 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
have zero : Eq (α := σ →₀ MvPolynomial σ R)
  ((Derivation.liftKaehlerDifferential (MvPolynomial.mkDerivation R fun (x : σ) ↦ Finsupp.single x 1) :
      (a : Ω[MvPolynomial σ R⁄R]) → σ →₀ MvPolynomial σ R)
    0)
  0
Tactic: rw [map_zero, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Polynomial (goal)
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
⊢ 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
have zero₁ : Eq (α := σ →₀ MvPolynomial σ R) 0 0
Tactic: rw [map_zero, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Polynomial (goal)
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
⊢ 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
have 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
Tactic: simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, map_add] at *
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Polynomial (goal)
Goal:
R : Type u
inst : CommRing R
σ : Type u_1
x : σ →₀ 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])
        x) =
    x
have zero : 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])
      0))
  0
Tactic: induction x using Finsupp.induction_linear with
    | zero => simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom]; rw [map_zero, map_zero]
    | add => simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, map_add] at *; simp only [*]
    | single a b => simp [-map_smul]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Polynomial (goal)
Goal:
R : Type u
inst : CommRing R
σ : Type u_1
x : σ →₀ MvPolynomial σ R
zero :
  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])
        0))
    0
⊢ 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])
        x) =
    x
have add : ∀ (f g : σ →₀ 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])
          f) =
      f →
    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 →
      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: induction x using Finsupp.induction_linear with
    | zero => simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom]; rw [map_zero, map_zero]
    | add => simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, map_add] at *; simp only [*]
    | single a b => simp [-map_smul]
Cleared hypotheses: x