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
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))
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
⊢ ((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_add : ∀ (a : σ) (b₁ b₂ : ℕ),
  HSMul.hSMul (α := MvPolynomial σ R)
      ((monomial (s + Finsupp.single i 1 - Finsupp.single a 1) : (a : R) → MvPolynomial σ R) (↑(b₁ + b₂) : R)) (f a) =
    HSMul.hSMul (α := MvPolynomial σ R)
        ((monomial (s + Finsupp.single i 1 - Finsupp.single a 1) : (a : R) → MvPolynomial σ R) (↑b₁ : R)) (f a) +
      HSMul.hSMul (α := MvPolynomial σ R)
        ((monomial (s + Finsupp.single i 1 - Finsupp.single a 1) : (a : R) → MvPolynomial σ R) (↑b₂ : R)) (f a)
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 : σ
⊢ ((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'] <;>
        [skip; simp; (intros; simp only [Nat.cast_add, (monomial _).map_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
f : σ → A
s : σ →₀ ℕ
i : σ
⊢ 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))
have rw : (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)) +
    HSMul.hSMul (α := MvPolynomial σ R)
      ((monomial (s + Finsupp.single i 1 - Finsupp.single i 1) : (a : R) → MvPolynomial σ R) (↑1 : R)) (f i) =
  HSMul.hSMul (α := MvPolynomial σ R) ((monomial s : (a : R) → MvPolynomial σ R) 1)
      (HSMul.hSMul (α := MvPolynomial σ R)
        ((monomial (HSub.hSub (α := σ →₀ ℕ) (Finsupp.single i 1) (Finsupp.single i 1)) : (a : R) → MvPolynomial σ R)
          (↑1 : R))
        (f i)) +
    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_single_index, Finsupp.sum_single_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 :
  (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)) +
      HSMul.hSMul (α := MvPolynomial σ R)
        ((monomial (s + Finsupp.single i 1 - Finsupp.single i 1) : (a : R) → MvPolynomial σ R) (↑1 : R)) (f i) =
    HSMul.hSMul (α := MvPolynomial σ R) ((monomial s : (a : R) → MvPolynomial σ R) 1)
        (HSMul.hSMul (α := MvPolynomial σ R)
          ((monomial (HSub.hSub (α := σ →₀ ℕ) (Finsupp.single i 1) (Finsupp.single i 1)) : (a : R) → MvPolynomial σ R)
            (↑1 : R))
          (f i)) +
      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))
⊢ 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))
have rw₁ : HSMul.hSMul (α := MvPolynomial σ R)
    ((monomial (HSub.hSub (α := σ →₀ ℕ) (Finsupp.single i 1) (Finsupp.single i 1)) : (a : R) → MvPolynomial σ R)
      (↑0 : R))
    (f i) =
  0
Tactic: rw [Finsupp.sum_single_index, Finsupp.sum_single_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 :
  (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)) +
      HSMul.hSMul (α := MvPolynomial σ R)
        ((monomial (s + Finsupp.single i 1 - Finsupp.single i 1) : (a : R) → MvPolynomial σ R) (↑1 : R)) (f i) =
    HSMul.hSMul (α := MvPolynomial σ R) ((monomial s : (a : R) → MvPolynomial σ R) 1)
        (HSMul.hSMul (α := MvPolynomial σ R)
          ((monomial (HSub.hSub (α := σ →₀ ℕ) (Finsupp.single i 1) (Finsupp.single i 1)) : (a : R) → MvPolynomial σ R)
            (↑1 : R))
          (f i)) +
      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))
rw₁ :
  HSMul.hSMul (α := MvPolynomial σ R)
      ((monomial (HSub.hSub (α := σ →₀ ℕ) (Finsupp.single i 1) (Finsupp.single i 1)) : (a : R) → MvPolynomial σ R)
        (↑0 : R))
      (f i) =
    0
⊢ 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))
have rw₂ : HSMul.hSMul (α := MvPolynomial σ R)
    ((monomial (s + Finsupp.single i 1 - Finsupp.single i 1) : (a : R) → MvPolynomial σ R) (↑0 : R)) (f i) =
  0
Tactic: rw [Finsupp.sum_single_index, Finsupp.sum_single_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 : σ
⊢ 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))
have rw : (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)) +
    HSMul.hSMul (α := MvPolynomial σ R)
      ((monomial (s + Finsupp.single i 1 - Finsupp.single i 1) : (a : R) → MvPolynomial σ R) (↑1 : R)) (f i) =
  HSMul.hSMul (α := MvPolynomial σ R) ((monomial s : (a : R) → MvPolynomial σ R) 1)
      (HSMul.hSMul (α := MvPolynomial σ R)
        ((monomial (HSub.hSub (α := σ →₀ ℕ) (Finsupp.single i 1) (Finsupp.single i 1)) : (a : R) → MvPolynomial σ R)
          (↑1 : R))
        (f i)) +
    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_single_index, Finsupp.sum_single_index] <;> [skip; simp; simp]
-- 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.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)
        ((monomial (s + Finsupp.single i 1 - Finsupp.single i 1) : (a : R) → MvPolynomial σ R) (↑1 : R)) (f i) =
    HSMul.hSMul (α := MvPolynomial σ R) ((monomial s : (a : R) → MvPolynomial σ R) 1)
        (HSMul.hSMul (α := MvPolynomial σ R)
          ((monomial (HSub.hSub (α := σ →₀ ℕ) (Finsupp.single i 1) (Finsupp.single i 1)) : (a : R) → MvPolynomial σ R)
            (↑1 : R))
          (f i)) +
      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 : (HSMul.hSMul (α := MvPolynomial σ R) ((monomial s : (a : R) → MvPolynomial σ R) 1) (f i) +
    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)) =
  HSMul.hSMul (α := MvPolynomial σ R) ((monomial s : (a : R) → MvPolynomial σ R) 1) (f i) +
    s.sum fun (a : σ) (b : ℕ) ↦
      HSMul.hSMul (α := MvPolynomial σ R) ((monomial (Finsupp.single i 1) : (a : R) → MvPolynomial σ R) 1)
        (HSMul.hSMul (α := MvPolynomial σ R) ((monomial (s - Finsupp.single a 1) : (a : R) → MvPolynomial σ R) (↑b : R))
          (f a))
Tactic: rw [tsub_self, add_tsub_cancel_right, Nat.cast_one, ← C_apply, C_1, one_smul, add_comm,
        Finsupp.smul_sum]
-- 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 : σ
⊢ (HSMul.hSMul (α := MvPolynomial σ R) ((monomial s : (a : R) → MvPolynomial σ R) 1) (f i) +
      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)) =
    HSMul.hSMul (α := MvPolynomial σ R) ((monomial s : (a : R) → MvPolynomial σ R) 1) (f i) +
      s.sum fun (a : σ) (b : ℕ) ↦
        HSMul.hSMul (α := MvPolynomial σ R) ((monomial (Finsupp.single i 1) : (a : R) → MvPolynomial σ R) 1)
          (HSMul.hSMul (α := MvPolynomial σ R)
            ((monomial (s - Finsupp.single a 1) : (a : R) → MvPolynomial σ R) (↑b : R)) (f a))
have refine : ∀ (j : σ) (hj : j ∈ s.support),
  Eq.{u_3 + 1} (α := A)
    ((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))
      j ((s : (a : σ) → ℕ) j))
    ((fun (a : σ) (b : ℕ) ↦
        HSMul.hSMul (α := MvPolynomial σ R) ((monomial (Finsupp.single i 1) : (a : R) → MvPolynomial σ R) 1)
          (HSMul.hSMul (α := MvPolynomial σ R)
            ((monomial (s - Finsupp.single a 1) : (a : R) → MvPolynomial σ R) (↑b : R)) (f a)))
      j ((s : (a : σ) → ℕ) j))
Tactic: refine congr_arg₂ (· + ·) rfl (Finset.sum_congr rfl fun j hj => ?_)
-- 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 j : σ
hj : j ∈ s.support
⊢ HSMul.hSMul (α := MvPolynomial σ R)
      ((monomial (s + Finsupp.single i 1 - Finsupp.single j 1) : (a : R) → MvPolynomial σ R)
        (↑((s : (a : σ) → ℕ) j) : R))
      (f j) =
    HSMul.hSMul (α := MvPolynomial σ R) ((monomial (Finsupp.single i 1) : (a : R) → MvPolynomial σ R) 1)
      (HSMul.hSMul (α := MvPolynomial σ R)
        ((monomial (s - Finsupp.single j 1) : (a : R) → MvPolynomial σ R) (↑((s : (a : σ) → ℕ) j) : R)) (f j))
have h : Finsupp.single j 1 ≤ s
Tactic: rw [smul_smul, monomial_mul, one_mul, add_comm s, add_tsub_assoc_of_le]
-- 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 j : σ
hj : j ∈ s.support
⊢ Finsupp.single j 1 ≤ s
have h : LE.le (α := ℕ) (1 : ℕ) ((s : (a : σ) → ℕ) j : ℕ)
Tactic: rwa [Finsupp.single_le_iff, Nat.succ_le_iff, pos_iff_ne_zero, ← Finsupp.mem_support_iff]
-- 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 j : σ
hj : j ∈ s.support
h : LE.le (α := ℕ) (1 : ℕ) ((s : (a : σ) → ℕ) j : ℕ)
⊢ Finsupp.single j 1 ≤ s
have h₁ : LT.lt (α := ℕ) (0 : ℕ) ((s : (a : σ) → ℕ) j : ℕ)
Tactic: rwa [Finsupp.single_le_iff, Nat.succ_le_iff, pos_iff_ne_zero, ← Finsupp.mem_support_iff]
-- 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 j : σ
hj : j ∈ s.support
h : LE.le (α := ℕ) (1 : ℕ) ((s : (a : σ) → ℕ) j : ℕ)
h₁ : LT.lt (α := ℕ) (0 : ℕ) ((s : (a : σ) → ℕ) j : ℕ)
⊢ Finsupp.single j 1 ≤ s
have h₂ : Ne (α := ℕ) ((s : (a : σ) → ℕ) j : ℕ) (0 : ℕ)
Tactic: rwa [Finsupp.single_le_iff, Nat.succ_le_iff, pos_iff_ne_zero, ← Finsupp.mem_support_iff]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
r s : R
i j : σ →₀ ℕ
⊢ Dvd.dvd (α := MvPolynomial σ R) ((monomial i : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
      ((monomial j : (a : R) → MvPolynomial σ R) s : MvPolynomial σ R) ↔
    (s = 0 ∨ i ≤ j) ∧ r ∣ s
have mp : Dvd.dvd (α := MvPolynomial σ R) ((monomial i : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
    ((monomial j : (a : R) → MvPolynomial σ R) s : MvPolynomial σ R) →
  (s = 0 ∨ i ≤ j) ∧ r ∣ s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
r s : R
i j : σ →₀ ℕ
mp :
  Dvd.dvd (α := MvPolynomial σ R) ((monomial i : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
      ((monomial j : (a : R) → MvPolynomial σ R) s : MvPolynomial σ R) →
    (s = 0 ∨ i ≤ j) ∧ r ∣ s
⊢ Dvd.dvd (α := MvPolynomial σ R) ((monomial i : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
      ((monomial j : (a : R) → MvPolynomial σ R) s : MvPolynomial σ R) ↔
    (s = 0 ∨ i ≤ j) ∧ r ∣ s
have mpr : (s = 0 ∨ i ≤ j) ∧ r ∣ s →
  Dvd.dvd (α := MvPolynomial σ R) ((monomial i : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
    ((monomial j : (a : R) → MvPolynomial σ R) s : MvPolynomial σ R)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (hypothesis)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
r s : R
i j : σ →₀ ℕ
x : MvPolynomial σ R
hx :
  (monomial j : (a : R) → MvPolynomial σ R) s =
    HMul.hMul (α := MvPolynomial σ R) ((monomial i : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) x
⊢ (s = 0 ∨ i ≤ j) ∧ r ∣ s
have hx₁ : ∀ (m : σ →₀ ℕ),
  coeff m ((monomial j : (a : R) → MvPolynomial σ R) s) =
    coeff m (HMul.hMul (α := MvPolynomial σ R) ((monomial i : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) x)
Tactic: rw [MvPolynomial.ext_iff] at hx
Cleared hypotheses: hx