awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
τ : Type u_2
inst : CommSemiring R
f : σ → τ
p : MvPolynomial σ R
b : τ →₀ ℕ
intro :
  ∀
    (h :
      Membership.mem (γ := Finset (τ →₀ ℕ))
        (support.{u, u_2} (R := R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p)) b),
    (b.sum fun (x : τ) (e : ℕ) ↦ e) ≤ p.totalDegree
intro₁ :
  ∀ (h : b ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) p)), (b.sum fun (x : τ) (e : ℕ) ↦ e) ≤ p.totalDegree
intro₂ :
  ∀ (h : b ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) p))
    (h' : b ∈ Finset.image (Finsupp.mapDomain f) p.support), (b.sum fun (x : τ) (e : ℕ) ↦ e) ≤ p.totalDegree
intro₃ :
  ∀ (h : b ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) p)) (h' : ∃ a ∈ p.support, Finsupp.mapDomain f a = b),
    (b.sum fun (x : τ) (e : ℕ) ↦ e) ≤ p.totalDegree
intro₄ :
  ∀ (s : σ →₀ ℕ) (hs : s ∈ p.support) (h : Finsupp.mapDomain f s ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) p)),
    ((Finsupp.mapDomain f s).sum fun (x : τ) (e : ℕ) ↦ e) ≤ p.totalDegree
⊢ Membership.mem (γ := Finset (τ →₀ ℕ))
      (support.{u, u_2} (R := R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p)) b →
    (b.sum fun (x : τ) (e : ℕ) ↦ e) ≤ p.totalDegree

Tactic:
classical
    intro h
    rw [rename_eq] at h
    have h' := Finsupp.mapDomain_support h
    rw [Finset.mem_image] at h'
    rcases h' with ⟨s, hs, rfl⟩
    exact (sum_mapDomain_index (fun _ => rfl) (fun _ _ _ => rfl)).trans_le (le_totalDegree hs)

Premises used: Finset.mem_image, rfl, MvPolynomial.rename_eq
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
τ : Type u_2
inst : CommSemiring R
f : σ ≃ τ
p : MvPolynomial σ R
⊢ p.totalDegree ≤
    totalDegree.{u, u_1} (R := R) (σ := σ)
      ((rename (⇑f.symm : (a : τ) → σ) : (a : MvPolynomial τ R) → MvPolynomial σ R)
        ((rename (⇑f : (a : σ) → τ) : (a : MvPolynomial σ R) → MvPolynomial τ R) p))

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s_1 : σ →₀ ℕ
inst : CommSemiring R
p q : MvPolynomial σ R
s t : Multiset σ
a b : MvPolynomial σ R
ha : Membership.mem (γ := Set (MvPolynomial σ R)) {p : MvPolynomial σ R | p.degrees ≤ s} a
hb : Membership.mem (γ := Set (MvPolynomial σ R)) {p : MvPolynomial σ R | p.degrees ≤ s} b
⊢ Membership.mem (γ := Set (MvPolynomial σ R)) {p : MvPolynomial σ R | p.degrees ≤ s} (a + b)

Tactic:
degrees_add_le.trans (sup_le ha hb)

Premises used: Multiset.Le, Set.Mem, setOf, MvPolynomial.degrees_add_le, sup_le, LE.le.trans
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s_1 : σ →₀ ℕ
inst : CommSemiring R
p q : MvPolynomial σ R
s t : Multiset σ
a b : MvPolynomial σ R
ha : Membership.mem (γ := Set (MvPolynomial σ R)) {p : MvPolynomial σ R | p.degrees ≤ s} a
hb : Membership.mem (γ := Set (MvPolynomial σ R)) {p : MvPolynomial σ R | p.degrees ≤ s} b
⊢ Membership.mem (γ := Set (MvPolynomial σ R)) {p : MvPolynomial σ R | p.degrees ≤ s} (a + b)

Tactic:
exact degrees_add_le.trans (sup_le ha hb)

Premises used: MvPolynomial.degrees_add_le, sup_le, LE.le.trans
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s_1 : σ →₀ ℕ
inst : CommSemiring R
p q : MvPolynomial σ R
s t : Multiset σ
a b : MvPolynomial σ R
ha : Membership.mem (γ := Set (MvPolynomial σ R)) {p : MvPolynomial σ R | p.degrees ≤ s} a
hb : Membership.mem (γ := Set (MvPolynomial σ R)) {p : MvPolynomial σ R | p.degrees ≤ s} b
⊢ Membership.mem (γ := Set (MvPolynomial σ R)) {p : MvPolynomial σ R | p.degrees ≤ s} (a + b)

Tactic:
classical exact degrees_add_le.trans (sup_le ha hb)
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s_1 : σ →₀ ℕ
inst : CommSemiring R
p q : MvPolynomial σ R
s t : Multiset σ
⊢ Membership.mem (γ := Set (MvPolynomial σ R)) {p : MvPolynomial σ R | p.degrees ≤ s} 0

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s_1 : σ →₀ ℕ
inst : CommSemiring R
p q : MvPolynomial σ R
s t : Multiset σ
c : R
x : MvPolynomial σ R
hx : Membership.mem (γ := Set (MvPolynomial σ R)) {p : MvPolynomial σ R | p.degrees ≤ s} x
rw :
  (HMul.hMul (α := MvPolynomial σ R)
        ((algebraMap R (MvPolynomial σ R) : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R) x).degrees ≤
    s
⊢ (c • x).degrees ≤ s

Tactic:
rw [Algebra.smul_def]

Premises used: Algebra.smul_def
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s_1 : σ →₀ ℕ
inst : CommSemiring R
p q : MvPolynomial σ R
s t : Multiset σ
c : R
x : MvPolynomial σ R
hx : Membership.mem (γ := Set (MvPolynomial σ R)) {p : MvPolynomial σ R | p.degrees ≤ s} x
⊢ (HMul.hMul (α := MvPolynomial σ R)
        ((algebraMap R (MvPolynomial σ R) : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R) x).degrees ≤
    s

Tactic:
degrees_mul_le.trans ?_

Premises used: MvPolynomial.degrees_mul_le, LE.le.trans
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s_1 : σ →₀ ℕ
inst : CommSemiring R
p q : MvPolynomial σ R
s t : Multiset σ
c : R
x : MvPolynomial σ R
hx : Membership.mem (γ := Set (MvPolynomial σ R)) {p : MvPolynomial σ R | p.degrees ≤ s} x
refine : degrees.{u, u_1} (R := R) ((algebraMap R (MvPolynomial σ R) : (a : R) → MvPolynomial σ R) c) + x.degrees ≤ s
⊢ (HMul.hMul (α := MvPolynomial σ R)
        ((algebraMap R (MvPolynomial σ R) : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R) x).degrees ≤
    s

Tactic:
refine degrees_mul_le.trans ?_

Premises used: MvPolynomial.degrees_mul_le, LE.le.trans
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s_1 : σ →₀ ℕ
inst : CommSemiring R
p q : MvPolynomial σ R
s t : Multiset σ
c : R
x : MvPolynomial σ R
hx : Membership.mem (γ := Set (MvPolynomial σ R)) {p : MvPolynomial σ R | p.degrees ≤ s} x
⊢ degrees.{u, u_1} (R := R) ((algebraMap R (MvPolynomial σ R) : (a : R) → MvPolynomial σ R) c) + x.degrees ≤ s

Tactic:
simpa [degrees_C] using hx

Premises used: MvPolynomial.degrees_C
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
s : Multiset σ
⊢ Membership.mem (γ := Submodule R (MvPolynomial σ R)) (degreesLE R σ s) p ↔ p.degrees ≤ s

Tactic:
Iff.rfl

Premises used: Multiset.Le, Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
s t : Multiset σ
rw :
  degreesLE R σ (s + t) ≤ HMul.hMul (α := Submodule R (MvPolynomial σ R)) (degreesLE R σ s) (degreesLE R σ t) ∧
    ∀ (m : MvPolynomial σ R),
      Membership.mem (γ := Submodule R (MvPolynomial σ R)) (degreesLE R σ s) m →
        ∀ (n : MvPolynomial σ R),
          Membership.mem (γ := Submodule R (MvPolynomial σ R)) (degreesLE R σ t) n →
            Membership.mem (γ := Submodule R (MvPolynomial σ R)) (degreesLE R σ (s + t)) (m * n)
⊢ degreesLE R σ (s + t) = HMul.hMul (α := Submodule R (MvPolynomial σ R)) (degreesLE R σ s) (degreesLE R σ t)

Tactic:
rw [le_antisymm_iff, Submodule.mul_le]

Premises used: le_antisymm_iff, Submodule.mul_le
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
s t : Multiset σ
⊢ degreesLE R σ (s + t) ≤ HMul.hMul (α := Submodule R (MvPolynomial σ R)) (degreesLE R σ s) (degreesLE R σ t) ∧
    ∀ (m : MvPolynomial σ R),
      Membership.mem (γ := Submodule R (MvPolynomial σ R)) (degreesLE R σ s) m →
        ∀ (n : MvPolynomial σ R),
          Membership.mem (γ := Submodule R (MvPolynomial σ R)) (degreesLE R σ t) n →
            Membership.mem (γ := Submodule R (MvPolynomial σ R)) (degreesLE R σ (s + t)) (m * n)

Tactic:
⟨fun x hx ↦ x.as_sum ▸ sum_mem fun i hi ↦ ?_,
    fun x hx y hy ↦ degrees_mul_le.trans (add_le_add hx hy)⟩

Premises used: add_le_add, Eq.rec, MvPolynomial.as_sum, MvPolynomial.degrees_mul_le, And.intro, LE.le.trans, Eq.symm, sum_mem
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
s t : Multiset σ
refine :
  ∀ (x : MvPolynomial σ R) (hx : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (degreesLE R σ (s + t)) x)
    (i : σ →₀ ℕ) (hi : i ∈ x.support),
    Membership.mem (α := MvPolynomial σ R)
      (HMul.hMul (α := Submodule R (MvPolynomial σ R)) (degreesLE R σ s) (degreesLE R σ t))
      ((monomial i : (a : R) → MvPolynomial σ R) (coeff i x) : MvPolynomial σ R)
⊢ degreesLE R σ (s + t) ≤ HMul.hMul (α := Submodule R (MvPolynomial σ R)) (degreesLE R σ s) (degreesLE R σ t) ∧
    ∀ (m : MvPolynomial σ R),
      Membership.mem (γ := Submodule R (MvPolynomial σ R)) (degreesLE R σ s) m →
        ∀ (n : MvPolynomial σ R),
          Membership.mem (γ := Submodule R (MvPolynomial σ R)) (degreesLE R σ t) n →
            Membership.mem (γ := Submodule R (MvPolynomial σ R)) (degreesLE R σ (s + t)) (m * n)

Tactic:
refine ⟨fun x hx ↦ x.as_sum ▸ sum_mem fun i hi ↦ ?_,
    fun x hx y hy ↦ degrees_mul_le.trans (add_le_add hx hy)⟩
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
s t : Multiset σ
x : MvPolynomial σ R
hx : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (degreesLE R σ (s + t)) x
i : σ →₀ ℕ
hi : i ∈ x.support
⊢ (toMultiset : (a : σ →₀ ℕ) → Multiset σ) i ≤ s + t

Tactic:
replace hi : i.toMultiset ≤ s + t := (Finset.le_sup hi).trans hx
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
s t : Multiset σ
x : MvPolynomial σ R
hx : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (degreesLE R σ (s + t)) x
i : σ →₀ ℕ
hi : (toMultiset : (a : σ →₀ ℕ) → Multiset σ) i ≤ s + t
a : σ →₀ ℕ :=
  (Multiset.toFinsupp : (a : Multiset σ) → σ →₀ ℕ)
    (HSub.hSub (α := Multiset σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) i : Multiset σ) t)
b : σ →₀ ℕ :=
  (Multiset.toFinsupp : (a : Multiset σ) → σ →₀ ℕ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) i ⊓ t : Multiset σ)
⊢ Eq (α := Multiset σ) ((AddEquiv.symm Multiset.toFinsupp : (a : σ →₀ ℕ) → Multiset σ) (a + b) : Multiset σ)
    ((AddEquiv.symm Multiset.toFinsupp : (a : σ →₀ ℕ) → Multiset σ) i : Multiset σ)

Tactic:
simp [a, b, Multiset.sub_add_inter]

Premises used: Multiset.sub_add_inter
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
s t : Multiset σ
x : MvPolynomial σ R
hx : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (degreesLE R σ (s + t)) x
i : σ →₀ ℕ
hi : (toMultiset : (a : σ →₀ ℕ) → Multiset σ) i ≤ s + t
a : σ →₀ ℕ :=
  (Multiset.toFinsupp : (a : Multiset σ) → σ →₀ ℕ)
    (HSub.hSub (α := Multiset σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) i : Multiset σ) t)
b : σ →₀ ℕ :=
  (Multiset.toFinsupp : (a : Multiset σ) → σ →₀ ℕ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) i ⊓ t : Multiset σ)
⊢ a + b = i

Tactic:
have : a + b = i := Multiset.toFinsupp.symm.injective (by simp [a, b, Multiset.sub_add_inter])
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
s t : Multiset σ
x : MvPolynomial σ R
hx : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (degreesLE R σ (s + t)) x
i : σ →₀ ℕ
hi : (toMultiset : (a : σ →₀ ℕ) → Multiset σ) i ≤ s + t
a : σ →₀ ℕ :=
  (Multiset.toFinsupp : (a : Multiset σ) → σ →₀ ℕ)
    (HSub.hSub (α := Multiset σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) i : Multiset σ) t)
b : σ →₀ ℕ :=
  (Multiset.toFinsupp : (a : Multiset σ) → σ →₀ ℕ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) i ⊓ t : Multiset σ)
this : a + b = i
⊢ (toMultiset : (a : σ →₀ ℕ) → Multiset σ) a ≤ s

Tactic:
simpa [a, add_comm (a := t)] using hi

Premises used: add_comm
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
s t : Multiset σ
x : MvPolynomial σ R
hx : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (degreesLE R σ (s + t)) x
i : σ →₀ ℕ
hi : (toMultiset : (a : σ →₀ ℕ) → Multiset σ) i ≤ s + t
a : σ →₀ ℕ :=
  (Multiset.toFinsupp : (a : Multiset σ) → σ →₀ ℕ)
    (HSub.hSub (α := Multiset σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) i : Multiset σ) t)
b : σ →₀ ℕ :=
  (Multiset.toFinsupp : (a : Multiset σ) → σ →₀ ℕ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) i ⊓ t : Multiset σ)
this : a + b = i
⊢ (toMultiset : (a : σ →₀ ℕ) → Multiset σ) a ≤ s

Tactic:
have ha : a.toMultiset ≤ s := by simpa [a, add_comm (a := t)] using hi
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
s t : Multiset σ
x : MvPolynomial σ R
hx : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (degreesLE R σ (s + t)) x
i : σ →₀ ℕ
hi : (toMultiset : (a : σ →₀ ℕ) → Multiset σ) i ≤ s + t
a : σ →₀ ℕ :=
  (Multiset.toFinsupp : (a : Multiset σ) → σ →₀ ℕ)
    (HSub.hSub (α := Multiset σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) i : Multiset σ) t)
b : σ →₀ ℕ :=
  (Multiset.toFinsupp : (a : Multiset σ) → σ →₀ ℕ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) i ⊓ t : Multiset σ)
this : a + b = i
ha : (toMultiset : (a : σ →₀ ℕ) → Multiset σ) a ≤ s
⊢ (toMultiset : (a : σ →₀ ℕ) → Multiset σ) b ≤ t

Tactic:
simp [b, Multiset.inter_le_right]

Premises used: Multiset.inter_le_right
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
s t : Multiset σ
x : MvPolynomial σ R
hx : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (degreesLE R σ (s + t)) x
i : σ →₀ ℕ
hi : (toMultiset : (a : σ →₀ ℕ) → Multiset σ) i ≤ s + t
a : σ →₀ ℕ :=
  (Multiset.toFinsupp : (a : Multiset σ) → σ →₀ ℕ)
    (HSub.hSub (α := Multiset σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) i : Multiset σ) t)
b : σ →₀ ℕ :=
  (Multiset.toFinsupp : (a : Multiset σ) → σ →₀ ℕ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) i ⊓ t : Multiset σ)
this : a + b = i
ha : (toMultiset : (a : σ →₀ ℕ) → Multiset σ) a ≤ s
⊢ (toMultiset : (a : σ →₀ ℕ) → Multiset σ) b ≤ t

Tactic:
have hb : b.toMultiset ≤ t := by simp [b, Multiset.inter_le_right]
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
s t : Multiset σ
x : MvPolynomial σ R
hx : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (degreesLE R σ (s + t)) x
i : σ →₀ ℕ
hi : (toMultiset : (a : σ →₀ ℕ) → Multiset σ) i ≤ s + t
a : σ →₀ ℕ :=
  (Multiset.toFinsupp : (a : Multiset σ) → σ →₀ ℕ)
    (HSub.hSub (α := Multiset σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) i : Multiset σ) t)
b : σ →₀ ℕ :=
  (Multiset.toFinsupp : (a : Multiset σ) → σ →₀ ℕ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) i ⊓ t : Multiset σ)
this : a + b = i
ha : (toMultiset : (a : σ →₀ ℕ) → Multiset σ) a ≤ s
hb : (toMultiset : (a : σ →₀ ℕ) → Multiset σ) b ≤ t
⊢ (monomial i : (a : R) → MvPolynomial σ R) (coeff i x) =
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
      ((monomial a : (a : R) → MvPolynomial σ R) (coeff i x) : MvPolynomial σ R)
      ((monomial b : (a : R) → MvPolynomial σ R) 1 : MvPolynomial σ R)

Tactic:
simp [this]
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
s t : Multiset σ
x : MvPolynomial σ R
hx : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (degreesLE R σ (s + t)) x
i : σ →₀ ℕ
hi : (toMultiset : (a : σ →₀ ℕ) → Multiset σ) i ≤ s + t
a : σ →₀ ℕ :=
  (Multiset.toFinsupp : (a : Multiset σ) → σ →₀ ℕ)
    (HSub.hSub (α := Multiset σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) i : Multiset σ) t)
b : σ →₀ ℕ :=
  (Multiset.toFinsupp : (a : Multiset σ) → σ →₀ ℕ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) i ⊓ t : Multiset σ)
this : a + b = i
ha : (toMultiset : (a : σ →₀ ℕ) → Multiset σ) a ≤ s
hb : (toMultiset : (a : σ →₀ ℕ) → Multiset σ) b ≤ t
rw :
  HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
      ((monomial a : (a : R) → MvPolynomial σ R) (coeff i x) : MvPolynomial σ R)
      ((monomial b : (a : R) → MvPolynomial σ R) 1 : MvPolynomial σ R) ∈
    HMul.hMul (α := Submodule R (MvPolynomial σ R)) (degreesLE R σ s) (degreesLE R σ t)
⊢ Membership.mem (α := MvPolynomial σ R)
    (HMul.hMul (α := Submodule R (MvPolynomial σ R)) (degreesLE R σ s) (degreesLE R σ t))
    ((monomial i : (a : R) → MvPolynomial σ R) (coeff i x) : MvPolynomial σ R)

Tactic:
rw [show monomial i (x.coeff i) = monomial a (x.coeff i) * monomial b 1 by simp [this]]
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
s t : Multiset σ
x : MvPolynomial σ R
hx : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (degreesLE R σ (s + t)) x
i : σ →₀ ℕ
hi : (toMultiset : (a : σ →₀ ℕ) → Multiset σ) i ≤ s + t
a : σ →₀ ℕ :=
  (Multiset.toFinsupp : (a : Multiset σ) → σ →₀ ℕ)
    (HSub.hSub (α := Multiset σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) i : Multiset σ) t)
b : σ →₀ ℕ :=
  (Multiset.toFinsupp : (a : Multiset σ) → σ →₀ ℕ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) i ⊓ t : Multiset σ)
this : a + b = i
ha : (toMultiset : (a : σ →₀ ℕ) → Multiset σ) a ≤ s
hb : (toMultiset : (a : σ →₀ ℕ) → Multiset σ) b ≤ t
⊢ HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
      ((monomial a : (a : R) → MvPolynomial σ R) (coeff i x) : MvPolynomial σ R)
      ((monomial b : (a : R) → MvPolynomial σ R) 1 : MvPolynomial σ R) ∈
    HMul.hMul (α := Submodule R (MvPolynomial σ R)) (degreesLE R σ s) (degreesLE R σ t)

Tactic:
Submodule.mul_mem_mul ((degrees_monomial _ _).trans ha) ((degrees_monomial _ _).trans hb)

Premises used: MvPolynomial.degrees_monomial, Submodule.mul_mem_mul, Set.Mem, LE.le.trans
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
s t : Multiset σ
x : MvPolynomial σ R
hx : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (degreesLE R σ (s + t)) x
i : σ →₀ ℕ
hi : (toMultiset : (a : σ →₀ ℕ) → Multiset σ) i ≤ s + t
a : σ →₀ ℕ :=
  (Multiset.toFinsupp : (a : Multiset σ) → σ →₀ ℕ)
    (HSub.hSub (α := Multiset σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) i : Multiset σ) t)
b : σ →₀ ℕ :=
  (Multiset.toFinsupp : (a : Multiset σ) → σ →₀ ℕ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) i ⊓ t : Multiset σ)
this : a + b = i
ha : (toMultiset : (a : σ →₀ ℕ) → Multiset σ) a ≤ s
hb : (toMultiset : (a : σ →₀ ℕ) → Multiset σ) b ≤ t
⊢ HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
      ((monomial a : (a : R) → MvPolynomial σ R) (coeff i x) : MvPolynomial σ R)
      ((monomial b : (a : R) → MvPolynomial σ R) 1 : MvPolynomial σ R) ∈
    HMul.hMul (α := Submodule R (MvPolynomial σ R)) (degreesLE R σ s) (degreesLE R σ t)

Tactic:
exact Submodule.mul_mem_mul ((degrees_monomial _ _).trans ha) ((degrees_monomial _ _).trans hb)

Premises used: Submodule.mul_mem_mul
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
⊢ LE.le (α := Submodule R (MvPolynomial σ R)) 1 (degreesLE R σ 0)

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
refine :
  ∀ (x : MvPolynomial σ R) (hx : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (degreesLE R σ 0) x),
    Membership.mem (γ := Submodule R (MvPolynomial σ R)) 1 x
⊢ Eq (α := Submodule R (MvPolynomial σ R)) (degreesLE R σ 0) 1

Tactic:
refine le_antisymm (fun x hx ↦ ?_) (by simp)

Premises used: le_antisymm
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
x : MvPolynomial σ R
hx : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (degreesLE R σ 0) x
⊢ x.degrees = 0

Tactic:
simp only [mem_degreesLE, nonpos_iff_eq_zero] at hx

Premises used: MvPolynomial.mem_degreesLE, nonpos_iff_eq_zero
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
x : MvPolynomial σ R
hx : x.degrees = 0
⊢ x.degrees.card ≤ 0

Tactic:
simp [hx]
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
x : MvPolynomial σ R
hx : x.degrees = 0
⊢ x = (C : (a : R) → MvPolynomial σ R) (coeff 0 x)

Tactic:
have := (totalDegree_eq_zero_iff_eq_C (p := x)).mp
    (Nat.eq_zero_of_le_zero (x.totalDegree_le_degrees_card.trans (by simp [hx])))
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
x : MvPolynomial σ R
hx : x.degrees = 0
this : x = (C : (a : R) → MvPolynomial σ R) (coeff 0 x)
⊢ (LinearMap.toSpanSingleton R (MvPolynomial σ R) 1 : (a : R) → MvPolynomial σ R) (coeff 0 x) = x

Tactic:
simp [Algebra.smul_def, ← this]

Premises used: Algebra.smul_def
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
x : MvPolynomial σ R
hx : x.degrees = 0
this : x = (C : (a : R) → MvPolynomial σ R) (coeff 0 x)
⊢ Membership.mem (γ := Submodule R (MvPolynomial σ R)) 1 x

Tactic:
exact ⟨x.coeff 0, by simp [Algebra.smul_def, ← this]⟩
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
s : Multiset σ
⊢ degreesLE R σ (HSMul.hSMul (α := ℕ) 0 s) =
    HPow.hPow (α := Submodule R (MvPolynomial σ R)) (β := ℕ) (degreesLE R σ s) 0

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
s : Multiset σ
k : ℕ
⊢ degreesLE R σ ((k + 1) • s) = HPow.hPow (α := Submodule R (MvPolynomial σ R)) (degreesLE R σ s) (k + 1)

Tactic:
simp only [pow_succ, degreesLE_nsmul, degreesLE_add, add_smul, one_smul]

Premises used: pow_succ, MvPolynomial.degreesLE_add, one_smul, 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
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:
sum_monomial_eq <| map_zero _

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, map_zero, MvPolynomial.sum_monomial_eq, Finset.sum
-- 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
f : σ → A
r : R
⊢ Eq.{u_3 + 1} (α := A)
    ((mkDerivationₗ R f : (a : MvPolynomial σ R) → A) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) : A)
    (0 : A)

Tactic:
(mkDerivationₗ_monomial f _ _).trans (smul_zero _)

Premises used: smul_zero, MvPolynomial.mkDerivationₗ_monomial, Eq.trans, Finsupp.single
-- 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
f : σ → A
i : σ
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := A) 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)) =
    f i

Tactic:
simp [tsub_self]

Premises used: tsub_self
-- 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
D : Derivation R (MvPolynomial σ R) A
a : R
⊢ Eq.{u_3 + 1} (α := A) ((D : (a : MvPolynomial σ R) → A) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) : A)
    (0 : A)

Tactic:
D.map_algebraMap a

Premises used: Derivation.map_algebraMap
-- 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
D : Derivation R (MvPolynomial σ R) A
a : R
f : MvPolynomial σ R
⊢ HSMul.hSMul (α := MvPolynomial σ R) (β := A) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      ((D : (a : MvPolynomial σ R) → A) f : A) =
    (D : (a : MvPolynomial σ R) → A)
      (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) f)

Tactic:
simp