awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.MvPolynomial.Derivation
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
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)
⊢ ((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:
rw [Finsupp.sum_add_index']

Premises used: Finsupp.sum_add_index'
-- Module: Mathlib.Algebra.MvPolynomial.Derivation
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 : σ
⊢ ∀ (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:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Derivation
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 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:
simp only [Nat.cast_add, (monomial _).map_add, add_smul]

Premises used: LinearMap.map_add, MvPolynomial.monomial, Nat.cast_add, add_smul
-- Module: Mathlib.Algebra.MvPolynomial.Derivation
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))

Tactic:
rw [Finsupp.sum_add_index'] <;>
        [skip; simp; (intros; simp only [Nat.cast_add, (monomial _).map_add, add_smul])]

Premises used: LinearMap.map_add, MvPolynomial.monomial, Finsupp.sum_add_index', Nat.cast_add, add_smul
-- Module: Mathlib.Algebra.MvPolynomial.Derivation
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
rw₂ :
  HSMul.hSMul (α := MvPolynomial σ R)
      ((monomial (s + 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))

Tactic:
rw [Finsupp.sum_single_index, Finsupp.sum_single_index]

Premises used: Finsupp.sum_single_index
-- Module: Mathlib.Algebra.MvPolynomial.Derivation
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 (HSub.hSub (α := σ →₀ ℕ) (Finsupp.single i 1) (Finsupp.single i 1)) : (a : R) → MvPolynomial σ R)
        (↑0 : R))
      (f i) =
    0

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Derivation
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 + Finsupp.single i 1 - Finsupp.single i 1) : (a : R) → MvPolynomial σ R) (↑0 : R)) (f i) =
    0

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Derivation
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))

Tactic:
rw [Finsupp.sum_single_index, Finsupp.sum_single_index] <;> [skip; simp; simp]

Premises used: Finsupp.sum_single_index
-- Module: Mathlib.Algebra.MvPolynomial.Derivation
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 :
  (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))
⊢ (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 [tsub_self, add_tsub_cancel_right, Nat.cast_one, ← C_apply, C_1, one_smul, add_comm,
        Finsupp.smul_sum]

Premises used: tsub_self, MvPolynomial.C_apply, MvPolynomial.C_1, add_comm, one_smul, Finsupp.smul_sum, add_tsub_cancel_right, Nat.cast_one
-- Module: Mathlib.Algebra.MvPolynomial.Derivation
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))

Tactic:
congr_arg₂ (· + ·) rfl (Finset.sum_congr rfl fun j hj => ?_)

Premises used: HAdd.hAdd, Finset.sum_congr, rfl, congr_arg₂
-- Module: Mathlib.Algebra.MvPolynomial.Derivation
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 : σ
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))
⊢ (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:
refine congr_arg₂ (· + ·) rfl (Finset.sum_congr rfl fun j hj => ?_)

Premises used: HAdd.hAdd, Finset.sum_congr, rfl, congr_arg₂
-- Module: Mathlib.Algebra.MvPolynomial.Derivation
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 : Finsupp.single j 1 ≤ s
⊢ 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))

Tactic:
rw [smul_smul, monomial_mul, one_mul, add_comm s, add_tsub_assoc_of_le]

Premises used: add_tsub_assoc_of_le, smul_smul, add_comm, MvPolynomial.monomial_mul, one_mul
-- Module: Mathlib.Algebra.MvPolynomial.Derivation
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 : ℕ)
h₂ : Ne (α := ℕ) ((s : (a : σ) → ℕ) j : ℕ) (0 : ℕ)
h₃ h₄ h₅ h₆ : j ∈ s.support
⊢ Finsupp.single j 1 ≤ s

Tactic:
rwa [Finsupp.single_le_iff, Nat.succ_le_iff, pos_iff_ne_zero, ← Finsupp.mem_support_iff]

Premises used: Finsupp.mem_support_iff, Finsupp.single_le_iff, Nat.succ_le_iff, pos_iff_ne_zero
-- Module: Mathlib.Algebra.MvPolynomial.Derivation
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
i : σ
⊢ (mkDerivation R f : (a : MvPolynomial σ R) → A) (X i) = f i

Tactic:
mkDerivationₗ_X f i

Premises used: MvPolynomial.mkDerivationₗ_X
-- Module: Mathlib.Algebra.MvPolynomial.Derivation
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 : σ →₀ ℕ
r : R
⊢ (mkDerivation R f : (a : MvPolynomial σ R) → A) ((monomial s : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) =
    HSMul.hSMul (β := A) r
      (s.sum fun (i : σ) (k : ℕ) ↦
        HSMul.hSMul (α := MvPolynomial σ R) ((monomial (s - Finsupp.single i 1) : (a : R) → MvPolynomial σ R) (↑k : R))
          (f i))

Tactic:
mkDerivationₗ_monomial f s r

Premises used: MvPolynomial.mkDerivationₗ_monomial
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
s : σ →₀ ℕ
x : MvPolynomial σ R
s' : σ →₀ ℕ
⊢ coeff s' (x /ᵐᵒⁿᵒᵐⁱᵃˡ s) = coeff (s + s') x

Tactic:
rfl

Premises used: MvPolynomial.coeff, Finsupp.onFinset, Finsupp.zipWith, rfl
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
s : σ →₀ ℕ
x : MvPolynomial σ R
⊢ (x /ᵐᵒⁿᵒᵐⁱᵃˡ s).support = x.support.preimage (fun (x : σ →₀ ℕ) ↦ s + x) ⋯

Tactic:
rfl

Premises used: Set.Mem, setOf, Finset.map, Set.toFinset, Set.Finite.toFinset, Finset.preimage, rfl
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
s : σ →₀ ℕ
⊢ Eq (α := MvPolynomial σ R) (0 /ᵐᵒⁿᵒᵐⁱᵃˡ s) 0

Tactic:
AddMonoidAlgebra.zero_divOf _

Premises used: AddMonoidAlgebra.zero_divOf, MvPolynomial.divMonomial
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
x : MvPolynomial σ R
⊢ x /ᵐᵒⁿᵒᵐⁱᵃˡ 0 = x

Tactic:
x.divOf_zero

Premises used: AddMonoidAlgebra.divOf_zero, MvPolynomial.divMonomial
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
x y : MvPolynomial σ R
s : σ →₀ ℕ
⊢ (x + y) /ᵐᵒⁿᵒᵐⁱᵃˡ s = x /ᵐᵒⁿᵒᵐⁱᵃˡ s + y /ᵐᵒⁿᵒᵐⁱᵃˡ s

Tactic:
map_add (N := _ →₀ _) _ _ _

Premises used: AddMonoidAlgebra.divOf, map_add, MvPolynomial.divMonomial, AddMonoidAlgebra
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
a b : σ →₀ ℕ
x : MvPolynomial σ R
⊢ x /ᵐᵒⁿᵒᵐⁱᵃˡ (a + b) = x /ᵐᵒⁿᵒᵐⁱᵃˡ a /ᵐᵒⁿᵒᵐⁱᵃˡ b

Tactic:
x.divOf_add _ _

Premises used: AddMonoidAlgebra.divOf_add, MvPolynomial.divMonomial
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
a : σ →₀ ℕ
x : MvPolynomial σ R
⊢ (monomial a : (a : R) → MvPolynomial σ R) 1 * x /ᵐᵒⁿᵒᵐⁱᵃˡ a = x

Tactic:
x.of'_mul_divOf _

Premises used: AddMonoidAlgebra.of'_mul_divOf, MvPolynomial.divMonomial, AddMonoidAlgebra.of', Finsupp.single
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
a : σ →₀ ℕ
x : MvPolynomial σ R
⊢ x * (monomial a : (a : R) → MvPolynomial σ R) 1 /ᵐᵒⁿᵒᵐⁱᵃˡ a = x

Tactic:
x.mul_of'_divOf _

Premises used: MvPolynomial.divMonomial, AddMonoidAlgebra.of', Finsupp.single, AddMonoidAlgebra.mul_of'_divOf
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
a : σ →₀ ℕ
⊢ Eq (α := MvPolynomial σ R) ((monomial a : (a : R) → MvPolynomial σ R) 1 /ᵐᵒⁿᵒᵐⁱᵃˡ a) 1

Tactic:
AddMonoidAlgebra.of'_divOf _

Premises used: AddMonoidAlgebra.of'_divOf, MvPolynomial.divMonomial, AddMonoidAlgebra.of', Finsupp.single
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
s : σ →₀ ℕ
x : MvPolynomial σ R
d : σ →₀ ℕ
h : ¬s ≤ s + d
⊢ False

Tactic:
h le_self_add

Premises used: le_self_add
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
s : σ →₀ ℕ
x : MvPolynomial σ R
d : σ →₀ ℕ
h : ¬s ≤ s + d
⊢ False

Tactic:
exact h le_self_add

Premises used: le_self_add
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
s' s : σ →₀ ℕ
x : MvPolynomial σ R
h : s ≤ s'
⊢ coeff s' (x %ᵐᵒⁿᵒᵐⁱᵃˡ s) = 0

Tactic:
x.modOf_apply_of_exists_add _ _ <| exists_add_of_le h

Premises used: AddMonoidAlgebra.modOf_apply_of_exists_add, ExistsAddOfLE.exists_add_of_le, MvPolynomial.coeff