awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Derivation (goal)
Goal:
σ : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Module (MvPolynomial σ R) A
inst_4 : IsScalarTower R (MvPolynomial σ R) A
D : MvPolynomial σ R →ₗ[R] A
h₁ : Eq.{u_3 + 1} (α := A) ((D : (a : MvPolynomial σ R) → A) 1 : A) (0 : A)
H :
  ∀ (s : σ →₀ ℕ) (i : σ),
    (D : (a : MvPolynomial σ R) → A)
        (HMul.hMul (α := MvPolynomial σ R) ((monomial s : (a : R) → MvPolynomial σ R) 1) (X i)) =
      HSMul.hSMul (α := MvPolynomial σ R) (β := A) ((monomial s : (a : R) → MvPolynomial σ R) 1)
          ((D : (a : MvPolynomial σ R) → A) (X i) : A) +
        HSMul.hSMul (α := MvPolynomial σ R) (β := A) (X i)
          ((D : (a : MvPolynomial σ R) → A) ((monomial s : (a : R) → MvPolynomial σ R) 1) : A)
hC :
  ∀ (r : R),
    Eq.{u_3 + 1} (α := A)
      ((D : (a : MvPolynomial σ R) → A) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) : A)
      (0 : A)
this :
  ∀ (p : MvPolynomial σ R) (i : σ),
    (D : (a : MvPolynomial σ R) → A) (p * X i) =
      HSMul.hSMul (β := A) p ((D : (a : MvPolynomial σ R) → A) (X i) : A) +
        HSMul.hSMul (α := MvPolynomial σ R) (β := A) (X i) ((D : (a : MvPolynomial σ R) → A) p : A)
p : MvPolynomial σ R
c : R
C :
  (D : (a : MvPolynomial σ R) → A)
      (HMul.hMul (α := MvPolynomial σ R) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R) p) =
    HSMul.hSMul (β := A) p
        ((D : (a : MvPolynomial σ R) → A) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R) : A) +
      HSMul.hSMul (α := MvPolynomial σ R) (β := A) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R)
        ((D : (a : MvPolynomial σ R) → A) p : A)
C₁ :
  (D : (a : MvPolynomial σ R) → A) (c • p) =
    HSMul.hSMul (β := A) p
        ((D : (a : MvPolynomial σ R) → A) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R) : A) +
      HSMul.hSMul (α := MvPolynomial σ R) (β := A) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R)
        ((D : (a : MvPolynomial σ R) → A) p : A)
C₂ :
  (D : (a : MvPolynomial σ R) → A) (c • p) =
    HSMul.hSMul (β := A) p 0 +
      HSMul.hSMul (α := MvPolynomial σ R) (β := A) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R)
        ((D : (a : MvPolynomial σ R) → A) p : A)
⊢ (D : (a : MvPolynomial σ R) → A)
      (HMul.hMul (β := MvPolynomial σ R) p ((MvPolynomial.C : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R)) =
    HSMul.hSMul (β := A) p
        ((D : (a : MvPolynomial σ R) → A) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R) : A) +
      HSMul.hSMul (α := MvPolynomial σ R) (β := A) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R)
        ((D : (a : MvPolynomial σ R) → A) p : A)
have C₃ : (D : (a : MvPolynomial σ R) → A) (c • p) =
  0 +
    HSMul.hSMul (α := MvPolynomial σ R) (β := A) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R)
      ((D : (a : MvPolynomial σ R) → A) p : A)
Tactic: rw [mul_comm, C_mul', hC, smul_zero, zero_add, D.map_smul, C_eq_smul_one, smul_one_smul]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Derivation (goal)
Goal:
σ : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Module (MvPolynomial σ R) A
inst_4 : IsScalarTower R (MvPolynomial σ R) A
D : MvPolynomial σ R →ₗ[R] A
h₁_1 : Eq.{u_3 + 1} (α := A) ((D : (a : MvPolynomial σ R) → A) 1 : A) (0 : A)
H :
  ∀ (s : σ →₀ ℕ) (i : σ),
    (D : (a : MvPolynomial σ R) → A)
        (HMul.hMul (α := MvPolynomial σ R) ((monomial s : (a : R) → MvPolynomial σ R) 1) (X i)) =
      HSMul.hSMul (α := MvPolynomial σ R) (β := A) ((monomial s : (a : R) → MvPolynomial σ R) 1)
          ((D : (a : MvPolynomial σ R) → A) (X i) : A) +
        HSMul.hSMul (α := MvPolynomial σ R) (β := A) (X i)
          ((D : (a : MvPolynomial σ R) → A) ((monomial s : (a : R) → MvPolynomial σ R) 1) : A)
hC :
  ∀ (r : R),
    Eq.{u_3 + 1} (α := A) ((D : (a : MvPolynomial σ R) → A) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) : A)
      (0 : A)
this :
  ∀ (p : MvPolynomial σ R) (i : σ),
    (D : (a : MvPolynomial σ R) → A) (p * X i) =
      HSMul.hSMul (β := A) p ((D : (a : MvPolynomial σ R) → A) (X i) : A) +
        HSMul.hSMul (α := MvPolynomial σ R) (β := A) (X i) ((D : (a : MvPolynomial σ R) → A) p : A)
p q₁ q₂ : MvPolynomial σ R
h₁ :
  (D : (a : MvPolynomial σ R) → A) (p * q₁) =
    HSMul.hSMul (β := A) p ((D : (a : MvPolynomial σ R) → A) q₁ : A) +
      HSMul.hSMul (β := A) q₁ ((D : (a : MvPolynomial σ R) → A) p : A)
h₂ :
  (D : (a : MvPolynomial σ R) → A) (p * q₂) =
    HSMul.hSMul (β := A) p ((D : (a : MvPolynomial σ R) → A) q₂ : A) +
      HSMul.hSMul (β := A) q₂ ((D : (a : MvPolynomial σ R) → A) p : A)
⊢ (D : (a : MvPolynomial σ R) → A) (p * (q₁ + q₂)) =
    HSMul.hSMul (β := A) p ((D : (a : MvPolynomial σ R) → A) (q₁ + q₂) : A) +
      HSMul.hSMul (β := A) (q₁ + q₂) ((D : (a : MvPolynomial σ R) → A) p : A)
have add : HSMul.hSMul (β := A) p ((D : (a : MvPolynomial σ R) → A) q₁ : A) +
      HSMul.hSMul (β := A) q₁ ((D : (a : MvPolynomial σ R) → A) p : A) +
    (HSMul.hSMul (β := A) p ((D : (a : MvPolynomial σ R) → A) q₂ : A) +
      HSMul.hSMul (β := A) q₂ ((D : (a : MvPolynomial σ R) → A) p : A)) =
  HSMul.hSMul (β := A) p ((D : (a : MvPolynomial σ R) → A) q₁ : A) +
      HSMul.hSMul (β := A) p ((D : (a : MvPolynomial σ R) → A) q₂ : A) +
    (HSMul.hSMul (β := A) q₁ ((D : (a : MvPolynomial σ R) → A) p : A) +
      HSMul.hSMul (β := A) q₂ ((D : (a : MvPolynomial σ R) → A) p : A))
Tactic: simp only [mul_add, map_add, h₁, h₂, smul_add, add_smul]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Derivation (goal)
Goal:
σ : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Module (MvPolynomial σ R) A
inst_4 : IsScalarTower R (MvPolynomial σ R) A
D : MvPolynomial σ R →ₗ[R] A
h₁ : Eq.{u_3 + 1} (α := A) ((D : (a : MvPolynomial σ R) → A) 1 : A) (0 : A)
H :
  ∀ (s : σ →₀ ℕ) (i : σ),
    (D : (a : MvPolynomial σ R) → A)
        (HMul.hMul (α := MvPolynomial σ R) ((monomial s : (a : R) → MvPolynomial σ R) 1) (X i)) =
      HSMul.hSMul (α := MvPolynomial σ R) (β := A) ((monomial s : (a : R) → MvPolynomial σ R) 1)
          ((D : (a : MvPolynomial σ R) → A) (X i) : A) +
        HSMul.hSMul (α := MvPolynomial σ R) (β := A) (X i)
          ((D : (a : MvPolynomial σ R) → A) ((monomial s : (a : R) → MvPolynomial σ R) 1) : A)
hC :
  ∀ (r : R),
    Eq.{u_3 + 1} (α := A) ((D : (a : MvPolynomial σ R) → A) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) : A)
      (0 : A)
this :
  ∀ (p : MvPolynomial σ R) (i : σ),
    (D : (a : MvPolynomial σ R) → A) (p * X i) =
      HSMul.hSMul (β := A) p ((D : (a : MvPolynomial σ R) → A) (X i) : A) +
        HSMul.hSMul (α := MvPolynomial σ R) (β := A) (X i) ((D : (a : MvPolynomial σ R) → A) p : A)
p q : MvPolynomial σ R
i : σ
hq :
  (D : (a : MvPolynomial σ R) → A) (p * q) =
    HSMul.hSMul (β := A) p ((D : (a : MvPolynomial σ R) → A) q : A) +
      HSMul.hSMul (β := A) q ((D : (a : MvPolynomial σ R) → A) p : A)
⊢ (D : (a : MvPolynomial σ R) → A) (p * (q * X i)) =
    HSMul.hSMul (β := A) p ((D : (a : MvPolynomial σ R) → A) (q * X i) : A) +
      HSMul.hSMul (β := A) (q * X i) ((D : (a : MvPolynomial σ R) → A) p : A)
have mul_X : p • HSMul.hSMul (β := A) q ((D : (a : MvPolynomial σ R) → A) (X i) : A) +
    (HSMul.hSMul (α := MvPolynomial σ R) (X i) (HSMul.hSMul (β := A) p ((D : (a : MvPolynomial σ R) → A) q : A)) +
      HSMul.hSMul (α := MvPolynomial σ R) (X i) (HSMul.hSMul (β := A) q ((D : (a : MvPolynomial σ R) → A) p : A))) =
  p • HSMul.hSMul (β := A) q ((D : (a : MvPolynomial σ R) → A) (X i) : A) +
    (p • HSMul.hSMul (α := MvPolynomial σ R) (β := A) (X i) ((D : (a : MvPolynomial σ R) → A) q : A) +
      q • HSMul.hSMul (α := MvPolynomial σ R) (β := A) (X i) ((D : (a : MvPolynomial σ R) → A) p : A))
Tactic: simp only [this, ← mul_assoc, hq, mul_smul, smul_add, add_assoc]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Derivation (goal)
Goal:
σ : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Module (MvPolynomial σ R) A
inst_4 : IsScalarTower R (MvPolynomial σ R) A
D : MvPolynomial σ R →ₗ[R] A
h₁ : Eq.{u_3 + 1} (α := A) ((D : (a : MvPolynomial σ R) → A) 1 : A) (0 : A)
H :
  ∀ (s : σ →₀ ℕ) (i : σ),
    (D : (a : MvPolynomial σ R) → A)
        (HMul.hMul (α := MvPolynomial σ R) ((monomial s : (a : R) → MvPolynomial σ R) 1) (X i)) =
      HSMul.hSMul (α := MvPolynomial σ R) (β := A) ((monomial s : (a : R) → MvPolynomial σ R) 1)
          ((D : (a : MvPolynomial σ R) → A) (X i) : A) +
        HSMul.hSMul (α := MvPolynomial σ R) (β := A) (X i)
          ((D : (a : MvPolynomial σ R) → A) ((monomial s : (a : R) → MvPolynomial σ R) 1) : A)
hC :
  ∀ (r : R),
    Eq.{u_3 + 1} (α := A) ((D : (a : MvPolynomial σ R) → A) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) : A)
      (0 : A)
this :
  ∀ (p : MvPolynomial σ R) (i : σ),
    (D : (a : MvPolynomial σ R) → A) (p * X i) =
      HSMul.hSMul (β := A) p ((D : (a : MvPolynomial σ R) → A) (X i) : A) +
        HSMul.hSMul (α := MvPolynomial σ R) (β := A) (X i) ((D : (a : MvPolynomial σ R) → A) p : A)
p q : MvPolynomial σ R
i : σ
hq :
  (D : (a : MvPolynomial σ R) → A) (p * q) =
    HSMul.hSMul (β := A) p ((D : (a : MvPolynomial σ R) → A) q : A) +
      HSMul.hSMul (β := A) q ((D : (a : MvPolynomial σ R) → A) p : A)
⊢ p • HSMul.hSMul (β := A) q ((D : (a : MvPolynomial σ R) → A) (X i) : A) +
      (HSMul.hSMul (α := MvPolynomial σ R) (X i) (HSMul.hSMul (β := A) p ((D : (a : MvPolynomial σ R) → A) q : A)) +
        HSMul.hSMul (α := MvPolynomial σ R) (X i) (HSMul.hSMul (β := A) q ((D : (a : MvPolynomial σ R) → A) p : A))) =
    p • HSMul.hSMul (β := A) q ((D : (a : MvPolynomial σ R) → A) (X i) : A) +
      (p • HSMul.hSMul (α := MvPolynomial σ R) (β := A) (X i) ((D : (a : MvPolynomial σ R) → A) q : A) +
        q • HSMul.hSMul (α := MvPolynomial σ R) (β := A) (X i) ((D : (a : MvPolynomial σ R) → A) p : A))
have mul_X : p • HSMul.hSMul (β := A) q ((D : (a : MvPolynomial σ R) → A) (X i) : A) +
    (p • HSMul.hSMul (α := MvPolynomial σ R) (β := A) (X i) ((D : (a : MvPolynomial σ R) → A) q : A) +
      HSMul.hSMul (α := MvPolynomial σ R) (X i) (HSMul.hSMul (β := A) q ((D : (a : MvPolynomial σ R) → A) p : A))) =
  p • HSMul.hSMul (β := A) q ((D : (a : MvPolynomial σ R) → A) (X i) : A) +
    (p • HSMul.hSMul (α := MvPolynomial σ R) (β := A) (X i) ((D : (a : MvPolynomial σ R) → A) q : A) +
      q • HSMul.hSMul (α := MvPolynomial σ R) (β := A) (X i) ((D : (a : MvPolynomial σ R) → A) p : A))
Tactic: rw [smul_comm (X i), smul_comm (X i)]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Derivation (goal)
Goal:
σ : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Module (MvPolynomial σ R) A
inst_4 : IsScalarTower R (MvPolynomial σ R) A
D : MvPolynomial σ R →ₗ[R] A
h₁ : Eq.{u_3 + 1} (α := A) ((D : (a : MvPolynomial σ R) → A) 1 : A) (0 : A)
H :
  ∀ (s : σ →₀ ℕ) (i : σ),
    (D : (a : MvPolynomial σ R) → A)
        (HMul.hMul (α := MvPolynomial σ R) ((monomial s : (a : R) → MvPolynomial σ R) 1) (X i)) =
      HSMul.hSMul (α := MvPolynomial σ R) (β := A) ((monomial s : (a : R) → MvPolynomial σ R) 1)
          ((D : (a : MvPolynomial σ R) → A) (X i) : A) +
        HSMul.hSMul (α := MvPolynomial σ R) (β := A) (X i)
          ((D : (a : MvPolynomial σ R) → A) ((monomial s : (a : R) → MvPolynomial σ R) 1) : A)
hC :
  ∀ (r : R),
    Eq.{u_3 + 1} (α := A) ((D : (a : MvPolynomial σ R) → A) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) : A)
      (0 : A)
this :
  ∀ (p : MvPolynomial σ R) (i : σ),
    (D : (a : MvPolynomial σ R) → A) (p * X i) =
      HSMul.hSMul (β := A) p ((D : (a : MvPolynomial σ R) → A) (X i) : A) +
        HSMul.hSMul (α := MvPolynomial σ R) (β := A) (X i) ((D : (a : MvPolynomial σ R) → A) p : A)
p q : MvPolynomial σ R
⊢ (D : (a : MvPolynomial σ R) → A) (p * q) =
    HSMul.hSMul (β := A) p ((D : (a : MvPolynomial σ R) → A) q : A) +
      HSMul.hSMul (β := A) q ((D : (a : MvPolynomial σ R) → A) p : A)
have C : ∀ (c : R),
  (D : (a : MvPolynomial σ R) → A)
      (HMul.hMul (β := MvPolynomial σ R) p ((C : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R)) =
    HSMul.hSMul (β := A) p
        ((D : (a : MvPolynomial σ R) → A) ((C : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R) : A) +
      HSMul.hSMul (α := MvPolynomial σ R) (β := A) ((C : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R)
        ((D : (a : MvPolynomial σ R) → A) p : A)
Tactic: induction q using MvPolynomial.induction_on with
  | C c =>
    rw [mul_comm, C_mul', hC, smul_zero, zero_add, D.map_smul, C_eq_smul_one, smul_one_smul]
  | add q₁ q₂ h₁ h₂ => simp only [mul_add, map_add, h₁, h₂, smul_add, add_smul]; abel
  | mul_X q i hq =>
    simp only [this, ← mul_assoc, hq, mul_smul, smul_add, add_assoc]
    rw [smul_comm (X i), smul_comm (X i)]
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Derivation (goal)
Goal:
σ : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Module (MvPolynomial σ R) A
inst_4 : IsScalarTower R (MvPolynomial σ R) A
D : MvPolynomial σ R →ₗ[R] A
h₁ : Eq.{u_3 + 1} (α := A) ((D : (a : MvPolynomial σ R) → A) 1 : A) (0 : A)
H :
  ∀ (s : σ →₀ ℕ) (i : σ),
    (D : (a : MvPolynomial σ R) → A)
        (HMul.hMul (α := MvPolynomial σ R) ((monomial s : (a : R) → MvPolynomial σ R) 1) (X i)) =
      HSMul.hSMul (α := MvPolynomial σ R) (β := A) ((monomial s : (a : R) → MvPolynomial σ R) 1)
          ((D : (a : MvPolynomial σ R) → A) (X i) : A) +
        HSMul.hSMul (α := MvPolynomial σ R) (β := A) (X i)
          ((D : (a : MvPolynomial σ R) → A) ((monomial s : (a : R) → MvPolynomial σ R) 1) : A)
hC :
  ∀ (r : R),
    Eq.{u_3 + 1} (α := A)
      ((D : (a : MvPolynomial σ R) → A) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) : A)
      (0 : A)
this :
  ∀ (p : MvPolynomial σ R) (i : σ),
    (D : (a : MvPolynomial σ R) → A) (p * X i) =
      HSMul.hSMul (β := A) p ((D : (a : MvPolynomial σ R) → A) (X i) : A) +
        HSMul.hSMul (α := MvPolynomial σ R) (β := A) (X i) ((D : (a : MvPolynomial σ R) → A) p : A)
p q : MvPolynomial σ R
C :
  ∀ (c : R),
    (D : (a : MvPolynomial σ R) → A)
        (HMul.hMul (β := MvPolynomial σ R) p ((MvPolynomial.C : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R)) =
      HSMul.hSMul (β := A) p
          ((D : (a : MvPolynomial σ R) → A) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R) : A) +
        HSMul.hSMul (α := MvPolynomial σ R) (β := A)
          ((MvPolynomial.C : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R) ((D : (a : MvPolynomial σ R) → A) p : A)
⊢ (D : (a : MvPolynomial σ R) → A) (p * q) =
    HSMul.hSMul (β := A) p ((D : (a : MvPolynomial σ R) → A) q : A) +
      HSMul.hSMul (β := A) q ((D : (a : MvPolynomial σ R) → A) p : A)
have add : ∀ (q₁ q₂ : MvPolynomial σ R)
  (h₁ :
    (D : (a : MvPolynomial σ R) → A) (p * q₁) =
      HSMul.hSMul (β := A) p ((D : (a : MvPolynomial σ R) → A) q₁ : A) +
        HSMul.hSMul (β := A) q₁ ((D : (a : MvPolynomial σ R) → A) p : A))
  (h₂ :
    (D : (a : MvPolynomial σ R) → A) (p * q₂) =
      HSMul.hSMul (β := A) p ((D : (a : MvPolynomial σ R) → A) q₂ : A) +
        HSMul.hSMul (β := A) q₂ ((D : (a : MvPolynomial σ R) → A) p : A)),
  (D : (a : MvPolynomial σ R) → A) (p * (q₁ + q₂)) =
    HSMul.hSMul (β := A) p ((D : (a : MvPolynomial σ R) → A) (q₁ + q₂) : A) +
      HSMul.hSMul (β := A) (q₁ + q₂) ((D : (a : MvPolynomial σ R) → A) p : A)
Tactic: induction q using MvPolynomial.induction_on with
  | C c =>
    rw [mul_comm, C_mul', hC, smul_zero, zero_add, D.map_smul, C_eq_smul_one, smul_one_smul]
  | add q₁ q₂ h₁ h₂ => simp only [mul_add, map_add, h₁, h₂, smul_add, add_smul]; abel
  | mul_X q i hq =>
    simp only [this, ← mul_assoc, hq, mul_smul, smul_add, add_assoc]
    rw [smul_comm (X i), smul_comm (X i)]
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Derivation (goal)
Goal:
σ : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Module (MvPolynomial σ R) A
inst_4 : IsScalarTower R (MvPolynomial σ R) A
f : σ → A
s : σ →₀ ℕ
i : σ
⊢ (mkDerivationₗ R f : (a : MvPolynomial σ R) → A)
      (HMul.hMul (α := MvPolynomial σ R) ((monomial s : (a : R) → MvPolynomial σ R) 1) (X i)) =
    HSMul.hSMul (α := MvPolynomial σ R) (β := A) ((monomial s : (a : R) → MvPolynomial σ R) 1)
        ((mkDerivationₗ R f : (a : MvPolynomial σ R) → A) (X i) : A) +
      HSMul.hSMul (α := MvPolynomial σ R) (β := A) (X i)
        ((mkDerivationₗ R f : (a : MvPolynomial σ R) → A) ((monomial s : (a : R) → MvPolynomial σ R) 1) : A)
have simp : ((s + Finsupp.single i 1).sum fun (i_1 : σ) (k : ℕ) ↦
    HSMul.hSMul (α := MvPolynomial σ R)
      ((monomial (s + Finsupp.single i 1 - Finsupp.single i_1 1) : (a : R) → MvPolynomial σ R) (↑k : R)) (f i_1)) =
  HSMul.hSMul (α := MvPolynomial σ R) (β := A) ((monomial s : (a : R) → MvPolynomial σ R) 1)
      (Finsupp.sum (Finsupp.single i 1) fun (i_1 : σ) (k : ℕ) ↦
        HSMul.hSMul (α := MvPolynomial σ R)
          ((monomial (HSub.hSub (α := σ →₀ ℕ) (Finsupp.single i 1) (Finsupp.single i_1 1)) : (a : R) → MvPolynomial σ R)
            (↑k : R))
          (f i_1)) +
    HSMul.hSMul (α := MvPolynomial σ R) (β := A) ((monomial (Finsupp.single i 1) : (a : R) → MvPolynomial σ R) 1)
      (s.sum fun (i : σ) (k : ℕ) ↦
        HSMul.hSMul (α := MvPolynomial σ R) ((monomial (s - Finsupp.single i 1) : (a : R) → MvPolynomial σ R) (↑k : R))
          (f i))
Tactic: simp only [mkDerivationₗ_monomial, X, monomial_mul, one_smul, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Derivation (goal)
Goal:
σ : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Module (MvPolynomial σ R) A
inst_4 : IsScalarTower R (MvPolynomial σ R) A
f : σ → A
s : σ →₀ ℕ
i : σ
⊢ ((s + Finsupp.single i 1).sum fun (i_1 : σ) (k : ℕ) ↦
      HSMul.hSMul (α := MvPolynomial σ R)
        ((monomial (s + Finsupp.single i 1 - Finsupp.single i_1 1) : (a : R) → MvPolynomial σ R) (↑k : R)) (f i_1)) =
    HSMul.hSMul (α := MvPolynomial σ R) (β := A) ((monomial s : (a : R) → MvPolynomial σ R) 1)
        (Finsupp.sum (Finsupp.single i 1) fun (i_1 : σ) (k : ℕ) ↦
          HSMul.hSMul (α := MvPolynomial σ R)
            ((monomial (HSub.hSub (α := σ →₀ ℕ) (Finsupp.single i 1) (Finsupp.single i_1 1)) :
                (a : R) → MvPolynomial σ R)
              (↑k : R))
            (f i_1)) +
      HSMul.hSMul (α := MvPolynomial σ R) (β := A) ((monomial (Finsupp.single i 1) : (a : R) → MvPolynomial σ R) 1)
        (s.sum fun (i : σ) (k : ℕ) ↦
          HSMul.hSMul (α := MvPolynomial σ R)
            ((monomial (s - Finsupp.single i 1) : (a : R) → MvPolynomial σ R) (↑k : R)) (f i))
have rw : HAdd.hAdd (α := A)
    (s.sum fun (i_1 : σ) (k : ℕ) ↦
      HSMul.hSMul (α := MvPolynomial σ R)
        ((monomial (s + Finsupp.single i 1 - Finsupp.single i_1 1) : (a : R) → MvPolynomial σ R) (↑k : R)) (f i_1))
    (Finsupp.sum (Finsupp.single i 1) fun (i_1 : σ) (k : ℕ) ↦
      HSMul.hSMul (α := MvPolynomial σ R)
        ((monomial (s + Finsupp.single i 1 - Finsupp.single i_1 1) : (a : R) → MvPolynomial σ R) (↑k : R)) (f i_1)) =
  HSMul.hSMul (α := MvPolynomial σ R) (β := A) ((monomial s : (a : R) → MvPolynomial σ R) 1)
      (Finsupp.sum (Finsupp.single i 1) fun (i_1 : σ) (k : ℕ) ↦
        HSMul.hSMul (α := MvPolynomial σ R)
          ((monomial (HSub.hSub (α := σ →₀ ℕ) (Finsupp.single i 1) (Finsupp.single i_1 1)) : (a : R) → MvPolynomial σ R)
            (↑k : R))
          (f i_1)) +
    HSMul.hSMul (α := MvPolynomial σ R) (β := A) ((monomial (Finsupp.single i 1) : (a : R) → MvPolynomial σ R) 1)
      (s.sum fun (i : σ) (k : ℕ) ↦
        HSMul.hSMul (α := MvPolynomial σ R) ((monomial (s - Finsupp.single i 1) : (a : R) → MvPolynomial σ R) (↑k : R))
          (f i))
Tactic: rw [Finsupp.sum_add_index']
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Derivation (goal)
Goal:
σ : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Module (MvPolynomial σ R) A
inst_4 : IsScalarTower R (MvPolynomial σ R) A
f : σ → A
s : σ →₀ ℕ
i : σ
rw :
  HAdd.hAdd (α := A)
      (s.sum fun (i_1 : σ) (k : ℕ) ↦
        HSMul.hSMul (α := MvPolynomial σ R)
          ((monomial (s + Finsupp.single i 1 - Finsupp.single i_1 1) : (a : R) → MvPolynomial σ R) (↑k : R)) (f i_1))
      (Finsupp.sum (Finsupp.single i 1) fun (i_1 : σ) (k : ℕ) ↦
        HSMul.hSMul (α := MvPolynomial σ R)
          ((monomial (s + Finsupp.single i 1 - Finsupp.single i_1 1) : (a : R) → MvPolynomial σ R) (↑k : R)) (f i_1)) =
    HSMul.hSMul (α := MvPolynomial σ R) (β := A) ((monomial s : (a : R) → MvPolynomial σ R) 1)
        (Finsupp.sum (Finsupp.single i 1) fun (i_1 : σ) (k : ℕ) ↦
          HSMul.hSMul (α := MvPolynomial σ R)
            ((monomial (HSub.hSub (α := σ →₀ ℕ) (Finsupp.single i 1) (Finsupp.single i_1 1)) :
                (a : R) → MvPolynomial σ R)
              (↑k : R))
            (f i_1)) +
      HSMul.hSMul (α := MvPolynomial σ R) (β := A) ((monomial (Finsupp.single i 1) : (a : R) → MvPolynomial σ R) 1)
        (s.sum fun (i : σ) (k : ℕ) ↦
          HSMul.hSMul (α := MvPolynomial σ R)
            ((monomial (s - Finsupp.single i 1) : (a : R) → MvPolynomial σ R) (↑k : R)) (f i))
⊢ ((s + Finsupp.single i 1).sum fun (i_1 : σ) (k : ℕ) ↦
      HSMul.hSMul (α := MvPolynomial σ R)
        ((monomial (s + Finsupp.single i 1 - Finsupp.single i_1 1) : (a : R) → MvPolynomial σ R) (↑k : R)) (f i_1)) =
    HSMul.hSMul (α := MvPolynomial σ R) (β := A) ((monomial s : (a : R) → MvPolynomial σ R) 1)
        (Finsupp.sum (Finsupp.single i 1) fun (i_1 : σ) (k : ℕ) ↦
          HSMul.hSMul (α := MvPolynomial σ R)
            ((monomial (HSub.hSub (α := σ →₀ ℕ) (Finsupp.single i 1) (Finsupp.single i_1 1)) :
                (a : R) → MvPolynomial σ R)
              (↑k : R))
            (f i_1)) +
      HSMul.hSMul (α := MvPolynomial σ R) (β := A) ((monomial (Finsupp.single i 1) : (a : R) → MvPolynomial σ R) 1)
        (s.sum fun (i : σ) (k : ℕ) ↦
          HSMul.hSMul (α := MvPolynomial σ R)
            ((monomial (s - Finsupp.single i 1) : (a : R) → MvPolynomial σ R) (↑k : R)) (f i))
have h_zero : ∀ (a : σ),
  HSMul.hSMul (α := MvPolynomial σ R)
      ((monomial (s + Finsupp.single i 1 - Finsupp.single a 1) : (a : R) → MvPolynomial σ R) (↑0 : R)) (f a) =
    0
Tactic: rw [Finsupp.sum_add_index']