awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.MvPolynomial.CommRing
Goal:
S : Type v
inst : CommRing S
R : Type u
c : ℤ →+* S
f : RingHom.{u, v} (MvPolynomial R ℤ) S
x p : MvPolynomial R ℤ
n : R
hp : eval₂ c (comp (β := MvPolynomial R ℤ) (⇑f : (a : MvPolynomial R ℤ) → S) X) p = (f : (a : MvPolynomial R ℤ) → S) p
⊢ HMul.hMul (α := S) (β := S) ((f : (a : MvPolynomial R ℤ) → S) p : S)
      (comp (β := MvPolynomial R ℤ) (⇑f : (a : MvPolynomial R ℤ) → S) X n : S) =
    (f : (a : MvPolynomial R ℤ) → S) (p * X n)

Tactic:
exact (f.map_mul _ _).symm

Premises used: RingHom.map_mul, Eq.symm
-- Module: Mathlib.Algebra.MvPolynomial.CommRing
Goal:
S : Type v
inst : CommRing S
R : Type u
c : ℤ →+* S
f : RingHom.{u, v} (MvPolynomial R ℤ) S
x : MvPolynomial R ℤ
⊢ eval₂ c (comp (β := MvPolynomial R ℤ) (⇑f : (a : MvPolynomial R ℤ) → S) X) x = (f : (a : MvPolynomial R ℤ) → S) x

Tactic:
apply MvPolynomial.induction_on x
    (fun n => by
      rw [hom_C f, eval₂_C]
      exact eq_intCast c n)
    (fun p q hp hq => by
      rw [eval₂_add, hp, hq]
      exact (f.map_add _ _).symm)
    (fun p n hp => by
      rw [eval₂_mul, eval₂_X, hp]
      exact (f.map_mul _ _).symm)

Premises used: MvPolynomial.induction_on
-- Module: Mathlib.Algebra.MvPolynomial.CommRing
Goal:
R : Type u
S : Type v
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst : CommRing R
p q : MvPolynomial σ R
inst_1 : CommRing S
f_1 : R →+* S
g f : σ → S
x : σ
⊢ (fun (f : RingHom.{u_1, v} (MvPolynomial σ ℤ) S) ↦
        (comp (β := MvPolynomial σ ℤ) (⇑f : (a : MvPolynomial σ ℤ) → S) X : σ → S))
      ((fun (f : σ → S) ↦ (eval₂Hom (Int.castRingHom S) f : RingHom.{u_1, v} (MvPolynomial σ ℤ) S)) f) x =
    f x

Tactic:
simp only [coe_eval₂Hom, Function.comp_apply, eval₂_X]

Premises used: MvPolynomial.eval₂_X, MvPolynomial.coe_eval₂Hom, Function.comp_apply
-- Module: Mathlib.Algebra.MvPolynomial.CommRing
Goal:
R : Type u
σ : Type u_1
inst : CommRing R
x : σ
f g : MvPolynomial σ R
k : ℕ
h : 0 < k
hf : ∀ m ∈ f.support, k ≤ (m : (a : σ) → ℕ) x → coeff m f = coeff m g
hg : ∀ m ∈ g.support, k ≤ (m : (a : σ) → ℕ) x → coeff m f = coeff m g
rw : ∀ m ∈ (f - g).support, (m : (a : σ) → ℕ) x < k
⊢ degreeOf x (f - g) < k

Tactic:
rw [degreeOf_lt_iff h]

Premises used: MvPolynomial.degreeOf_lt_iff
-- Module: Mathlib.Algebra.MvPolynomial.CommRing
Goal:
R : Type u
σ : Type u_1
inst : CommRing R
x : σ
f g : MvPolynomial σ R
k : ℕ
h : 0 < k
hf : ∀ m ∈ f.support, k ≤ (m : (a : σ) → ℕ) x → coeff m f = coeff m g
hg : ∀ m ∈ g.support, k ≤ (m : (a : σ) → ℕ) x → coeff m f = coeff m g
⊢ ∀ m ∈ (f - g).support, (m : (a : σ) → ℕ) x < k

Tactic:
grind [degreeOf_lt_iff]

Premises used: MvPolynomial.degreeOf_lt_iff
-- Module: Mathlib.Algebra.MvPolynomial.CommRing
Goal:
R : Type u
σ : Type u_1
inst : CommRing R
a : MvPolynomial σ R
⊢ (-a).totalDegree = a.totalDegree

Tactic:
simp only [totalDegree, support_neg]

Premises used: MvPolynomial.support_neg, MvPolynomial.totalDegree
-- Module: Mathlib.Algebra.MvPolynomial.CommRing
Goal:
R : Type u
σ : Type u_1
inst : CommRing R
a b : MvPolynomial σ R
rw rw₁ : (a + -b).totalDegree = (a + -b).totalDegree
⊢ (a - b).totalDegree = (a + -b).totalDegree

Tactic:
rw [sub_eq_add_neg]

Premises used: sub_eq_add_neg
-- Module: Mathlib.Algebra.MvPolynomial.CommRing
Goal:
R : Type u
σ : Type u_1
inst : CommRing R
a b : MvPolynomial σ R
rw rw₁ : max a.totalDegree b.totalDegree = max a.totalDegree b.totalDegree
⊢ max a.totalDegree (-b).totalDegree = max a.totalDegree b.totalDegree

Tactic:
rw [totalDegree_neg]

Premises used: MvPolynomial.totalDegree_neg
-- Module: Mathlib.Algebra.MvPolynomial.CommRing
Goal:
R : Type u
σ : Type u_1
inst : CommRing R
p : MvPolynomial σ R
r : R
rw : max p.totalDegree 0 = p.totalDegree
rw₁ rw₂ : p.totalDegree = p.totalDegree
⊢ max p.totalDegree (totalDegree.{u, u_1} (R := R) (σ := σ) ((C : (a : R) → MvPolynomial σ R) r)) = p.totalDegree

Tactic:
rw [totalDegree_C, Nat.max_zero]

Premises used: MvPolynomial.totalDegree_C, Nat.max_zero
-- Module: Mathlib.Algebra.MvPolynomial.Counit
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
inst_1 : CommSemiring B
inst_2 : Algebra A B
b : B
⊢ (ACounit A B : (a : MvPolynomial B A) → B) (X b) = b

Tactic:
aeval_X _ b

Premises used: MvPolynomial.aeval_X
-- Module: Mathlib.Algebra.MvPolynomial.Counit
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
inst_1 : CommSemiring B
inst_2 : Algebra A B
a : A
⊢ Eq.{u_2 + 1} (α := B)
    ((ACounit A B : (a : MvPolynomial B A) → B) ((C : (a : A) → MvPolynomial B A) a : MvPolynomial B A) : B)
    ((algebraMap A B : (a : A) → B) a : B)

Tactic:
aeval_C _ a

Premises used: MvPolynomial.aeval_C
-- Module: Mathlib.Algebra.MvPolynomial.Counit
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
inst_1 : CommSemiring B
inst_2 : Algebra A B
⊢ Surjective (α := MvPolynomial B A) (β := B) (⇑(ACounit A B) : (a : MvPolynomial B A) → B)

Tactic:
fun b => ⟨X b, ACounit_X A b⟩

Premises used: MvPolynomial.ACounit_X, MvPolynomial.X, Exists.intro, Function.Surjective
-- Module: Mathlib.Algebra.MvPolynomial.Counit
Goal:
R : Type u_3
inst : CommRing R
⊢ Surjective (α := MvPolynomial R ℤ) (β := R) (⇑(counit R) : (a : MvPolynomial R ℤ) → R)

Tactic:
ACounit_surjective ℤ R

Premises used: MvPolynomial.ACounit_surjective, Int
-- Module: Mathlib.Algebra.MvPolynomial.Counit
Goal:
A : Type u_1
inst : CommSemiring A
⊢ Surjective (α := MvPolynomial A ℕ) (β := A) (⇑(counitNat A) : (a : MvPolynomial A ℕ) → A)

Tactic:
ACounit_surjective ℕ A

Premises used: Multiset.sum, Multiset.foldr, MvPolynomial.ACounit_surjective, Finsupp.sum, MvPolynomial.eval₂, Nat, Finset.sum
-- Module: Mathlib.Algebra.MvPolynomial.Counit
Goal:
R : Type u_3
inst : CommRing R
n : ℤ
⊢ Eq (α := R) ((counit R : (a : MvPolynomial R ℤ) → R) ((C : (a : ℤ) → MvPolynomial R ℤ) n : MvPolynomial R ℤ) : R)
    ((↑n : R) : R)

Tactic:
ACounit_C _ _

Premises used: MvPolynomial.ACounit_C
-- Module: Mathlib.Algebra.MvPolynomial.Counit
Goal:
A : Type u_1
inst : CommSemiring A
n : ℕ
⊢ Eq (α := A) ((counitNat A : (a : MvPolynomial A ℕ) → A) ((C : (a : ℕ) → MvPolynomial A ℕ) n : MvPolynomial A ℕ) : A)
    ((↑n : A) : A)

Tactic:
ACounit_C _ _

Premises used: Multiset.sum, Multiset.foldr, MvPolynomial.ACounit_C, Finsupp.sum, MvPolynomial.eval₂, Finset.sum
-- Module: Mathlib.Algebra.MvPolynomial.Counit
Goal:
R : Type u_3
inst : CommRing R
r : R
⊢ (counit R : (a : MvPolynomial R ℤ) → R) (X r) = r

Tactic:
ACounit_X _ _

Premises used: MvPolynomial.ACounit_X
-- Module: Mathlib.Algebra.MvPolynomial.Counit
Goal:
A : Type u_1
inst : CommSemiring A
a : A
⊢ (counitNat A : (a : MvPolynomial A ℕ) → A) (X a) = a

Tactic:
ACounit_X _ _

Premises used: Multiset.sum, Multiset.foldr, MvPolynomial.ACounit_X, Finsupp.sum, MvPolynomial.eval₂, Finset.sum
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
p : MvPolynomial σ R
⊢ Eq (α := Multiset σ) (p.support.sup fun (s : σ →₀ ℕ) ↦ (toMultiset : (a : σ →₀ ℕ) → Multiset σ) s)
    (p.support.sup fun (s : σ →₀ ℕ) ↦ (toMultiset : (a : σ →₀ ℕ) → Multiset σ) s)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
p : MvPolynomial σ R
⊢ Eq (α := Multiset σ) (p.support.sup fun (s : σ →₀ ℕ) ↦ (toMultiset : (a : σ →₀ ℕ) → Multiset σ) s)
    (p.support.sup fun (s : σ →₀ ℕ) ↦ (toMultiset : (a : σ →₀ ℕ) → Multiset σ) s)

Tactic:
convert!
      rfl

Premises used: rfl
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
s : σ →₀ ℕ
a : R
⊢ LE.le.{u_1} (α := Multiset σ) (degrees.{u, u_1} (R := R) ((monomial s : (a : R) → MvPolynomial σ R) a))
    ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) s)

Tactic:
(supDegree_single s a).trans_le ?_

Premises used: AddMonoidAlgebra.supDegree_single, Eq.trans_le, MvPolynomial.support, MvPolynomial.degrees
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
s : σ →₀ ℕ
a : R
refine :
  LE.le (α := Multiset σ) (if a = 0 then ⊥ else (toMultiset : (a : σ →₀ ℕ) → Multiset σ) s : Multiset σ)
    ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) s : Multiset σ)
⊢ LE.le.{u_1} (α := Multiset σ) (degrees.{u, u_1} (R := R) ((monomial s : (a : R) → MvPolynomial σ R) a))
    ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) s)

Tactic:
refine (supDegree_single s a).trans_le ?_

Premises used: AddMonoidAlgebra.supDegree_single, Eq.trans_le
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
s : σ →₀ ℕ
a : R
pos : a = 0 → LE.le (α := Multiset σ) (⊥ : Multiset σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) s : Multiset σ)
neg :
  ¬a = 0 →
    LE.le (α := Multiset σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) s : Multiset σ)
      ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) s : Multiset σ)
⊢ LE.le (α := Multiset σ) (if a = 0 then ⊥ else (toMultiset : (a : σ →₀ ℕ) → Multiset σ) s : Multiset σ)
    ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) s : Multiset σ)

Tactic:
split_ifs
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
s : σ →₀ ℕ
a : R
h : a = 0
⊢ LE.le (α := Multiset σ) (⊥ : Multiset σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) s : Multiset σ)

Tactic:
bot_le

Premises used: bot_le
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
s : σ →₀ ℕ
a : R
h : ¬a = 0
⊢ LE.le (α := Multiset σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) s : Multiset σ)
    ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) s : Multiset σ)

Tactic:
le_rfl

Premises used: le_rfl
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
s : σ →₀ ℕ
a : R
h : a = 0
⊢ LE.le (α := Multiset σ) (⊥ : Multiset σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) s : Multiset σ)

Tactic:
exacts [bot_le, le_rfl]

Premises used: le_rfl, bot_le
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
s : σ →₀ ℕ
a : R
refine :
  LE.le (α := Multiset σ) (if a = 0 then ⊥ else (toMultiset : (a : σ →₀ ℕ) → Multiset σ) s : Multiset σ)
    ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) s : Multiset σ)
pos : a = 0 → LE.le (α := Multiset σ) (⊥ : Multiset σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) s : Multiset σ)
neg :
  ¬a = 0 →
    LE.le (α := Multiset σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) s : Multiset σ)
      ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) s : Multiset σ)
⊢ LE.le.{u_1} (α := Multiset σ) (degrees.{u, u_1} (R := R) ((monomial s : (a : R) → MvPolynomial σ R) a))
    ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) s)

Tactic:
classical
    refine (supDegree_single s a).trans_le ?_
    split_ifs
    exacts [bot_le, le_rfl]

Premises used: AddMonoidAlgebra.supDegree_single, le_rfl, Eq.trans_le, bot_le
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
s : σ →₀ ℕ
a : R
ha : a ≠ 0
⊢ Eq.{u_1 + 1} (α := Multiset σ) (degrees.{u, u_1} (R := R) ((monomial s : (a : R) → MvPolynomial σ R) a))
    ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) s)

Tactic:
(supDegree_single s a).trans (if_neg ha)

Premises used: AddMonoidAlgebra.supDegree_single, MvPolynomial.support, if_neg, MvPolynomial.degrees, Eq.trans
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
s : σ →₀ ℕ
a : R
ha : a ≠ 0
⊢ Eq.{u_1 + 1} (α := Multiset σ) (degrees.{u, u_1} (R := R) ((monomial s : (a : R) → MvPolynomial σ R) a))
    ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) s)

Tactic:
exact (supDegree_single s a).trans (if_neg ha)

Premises used: AddMonoidAlgebra.supDegree_single, if_neg, Eq.trans
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
s : σ →₀ ℕ
a : R
ha : a ≠ 0
⊢ Eq.{u_1 + 1} (α := Multiset σ) (degrees.{u, u_1} (R := R) ((monomial s : (a : R) → MvPolynomial σ R) a))
    ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) s)

Tactic:
classical
    exact (supDegree_single s a).trans (if_neg ha)

Premises used: AddMonoidAlgebra.supDegree_single, if_neg, Eq.trans
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
a : R
⊢ Eq.{u_1 + 1} (α := Multiset σ) (degrees.{u, u_1} (R := R) ((C : (a : R) → MvPolynomial σ R) a)) 0

Tactic:
Multiset.le_zero.1 <| degrees_monomial _ _

Premises used: MvPolynomial.degrees_monomial, Iff.mp, Multiset.le_zero
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
n : σ
⊢ degrees.{u, u_1} (R := R) (X n) ≤ {n}

Tactic:
le_trans (degrees_monomial _ _) <| le_of_eq <| toMultiset_single _ _

Premises used: MvPolynomial.degrees_monomial, Finsupp.toMultiset_single, le_of_eq, le_trans
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : Nontrivial R
n : σ
⊢ degrees.{u, u_1} (R := R) (X n) = {n}

Tactic:
(degrees_monomial_eq _ (1 : R) one_ne_zero).trans (toMultiset_single _ _)

Premises used: MvPolynomial.X, MvPolynomial.degrees_monomial_eq, Finsupp.toMultiset_single, one_ne_zero, OfNat.ofNat, Eq.trans
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
rw : Eq.{u_1 + 1} (α := Multiset σ) (degrees.{u, u_1} (R := R) ((C : (a : R) → MvPolynomial σ R) 0)) 0
⊢ Eq.{u_1 + 1} (α := Multiset σ) (degrees.{u, u_1} (R := R) 0) 0

Tactic:
rw [← C_0]

Premises used: MvPolynomial.C_0
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
⊢ Eq.{u_1 + 1} (α := Multiset σ) (degrees.{u, u_1} (R := R) ((C : (a : R) → MvPolynomial σ R) 0)) 0

Tactic:
degrees_C 0

Premises used: MvPolynomial.degrees_C, OfNat.ofNat
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
⊢ Eq.{u_1 + 1} (α := Multiset σ) (degrees.{u, u_1} (R := R) ((C : (a : R) → MvPolynomial σ R) 0)) 0

Tactic:
exact degrees_C 0

Premises used: MvPolynomial.degrees_C, OfNat.ofNat
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
⊢ Eq.{u_1 + 1} (α := Multiset σ) (degrees.{u, u_1} (R := R) 1) 0

Tactic:
degrees_C 1

Premises used: MvPolynomial.degrees_C, OfNat.ofNat, Finsupp.single
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
p q : MvPolynomial σ R
simp_rw :
  LE.le (α := Multiset σ) ((p + q).support.sup fun (s : σ →₀ ℕ) ↦ (toMultiset : (a : σ →₀ ℕ) → Multiset σ) s)
    ((p.support.sup fun (s : σ →₀ ℕ) ↦ (toMultiset : (a : σ →₀ ℕ) → Multiset σ) s) ⊔
      q.support.sup fun (s : σ →₀ ℕ) ↦ (toMultiset : (a : σ →₀ ℕ) → Multiset σ) s)
⊢ (p + q).degrees ≤ p.degrees ⊔ q.degrees

Tactic:
simp_rw [degrees_def]

Premises used: MvPolynomial.degrees_def
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
p q : MvPolynomial σ R
⊢ LE.le (α := Multiset σ) ((p + q).support.sup fun (s : σ →₀ ℕ) ↦ (toMultiset : (a : σ →₀ ℕ) → Multiset σ) s)
    ((p.support.sup fun (s : σ →₀ ℕ) ↦ (toMultiset : (a : σ →₀ ℕ) → Multiset σ) s) ⊔
      q.support.sup fun (s : σ →₀ ℕ) ↦ (toMultiset : (a : σ →₀ ℕ) → Multiset σ) s)

Tactic:
supDegree_add_le

Premises used: AddMonoidAlgebra.supDegree_add_le, MvPolynomial.support
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
p q : MvPolynomial σ R
⊢ LE.le (α := Multiset σ) ((p + q).support.sup fun (s : σ →₀ ℕ) ↦ (toMultiset : (a : σ →₀ ℕ) → Multiset σ) s)
    ((p.support.sup fun (s : σ →₀ ℕ) ↦ (toMultiset : (a : σ →₀ ℕ) → Multiset σ) s) ⊔
      q.support.sup fun (s : σ →₀ ℕ) ↦ (toMultiset : (a : σ →₀ ℕ) → Multiset σ) s)

Tactic:
exact supDegree_add_le

Premises used: AddMonoidAlgebra.supDegree_add_le
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
ι : Type u_3
inst_1 : DecidableEq σ
s : Finset ι
f : ι → MvPolynomial σ R
simp_rw :
  LE.le.{u_1} (α := Multiset σ)
    (Finset.sup (support.{u, u_1} (R := R) (∑ i ∈ s, f i)) fun (s : σ →₀ ℕ) ↦
      (toMultiset : (a : σ →₀ ℕ) → Multiset σ) s)
    (s.sup fun (i : ι) ↦ (f i).support.sup fun (s : σ →₀ ℕ) ↦ (toMultiset : (a : σ →₀ ℕ) → Multiset σ) s)
⊢ LE.le.{u_1} (α := Multiset σ) (degrees.{u, u_1} (R := R) (∑ i ∈ s, f i)) (s.sup fun (i : ι) ↦ (f i).degrees)

Tactic:
simp_rw [degrees_def]

Premises used: MvPolynomial.degrees_def
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
ι : Type u_3
inst_1 : DecidableEq σ
s : Finset ι
f : ι → MvPolynomial σ R
⊢ LE.le.{u_1} (α := Multiset σ)
    (Finset.sup (support.{u, u_1} (R := R) (∑ i ∈ s, f i)) fun (s : σ →₀ ℕ) ↦
      (toMultiset : (a : σ →₀ ℕ) → Multiset σ) s)
    (s.sup fun (i : ι) ↦ (f i).support.sup fun (s : σ →₀ ℕ) ↦ (toMultiset : (a : σ →₀ ℕ) → Multiset σ) s)

Tactic:
supDegree_sum_le

Premises used: MvPolynomial.support, AddMonoidAlgebra.supDegree_sum_le
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
ι : Type u_3
inst_1 : DecidableEq σ
s : Finset ι
f : ι → MvPolynomial σ R
⊢ LE.le.{u_1} (α := Multiset σ)
    (Finset.sup (support.{u, u_1} (R := R) (∑ i ∈ s, f i)) fun (s : σ →₀ ℕ) ↦
      (toMultiset : (a : σ →₀ ℕ) → Multiset σ) s)
    (s.sup fun (i : ι) ↦ (f i).support.sup fun (s : σ →₀ ℕ) ↦ (toMultiset : (a : σ →₀ ℕ) → Multiset σ) s)

Tactic:
exact supDegree_sum_le

Premises used: AddMonoidAlgebra.supDegree_sum_le
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
⊢ ((p * q).support.sup fun (s : σ →₀ ℕ) ↦ (toMultiset : (a : σ →₀ ℕ) → Multiset σ) s) ≤
    HAdd.hAdd (α := Multiset σ) (p.support.sup fun (s : σ →₀ ℕ) ↦ (toMultiset : (a : σ →₀ ℕ) → Multiset σ) s)
      (q.support.sup fun (s : σ →₀ ℕ) ↦ (toMultiset : (a : σ →₀ ℕ) → Multiset σ) s)

Tactic:
supDegree_mul_le (map_add _)

Premises used: map_add, MvPolynomial.support, AddMonoidAlgebra.supDegree_mul_le
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
⊢ ((p * q).support.sup fun (s : σ →₀ ℕ) ↦ (toMultiset : (a : σ →₀ ℕ) → Multiset σ) s) ≤
    HAdd.hAdd (α := Multiset σ) (p.support.sup fun (s : σ →₀ ℕ) ↦ (toMultiset : (a : σ →₀ ℕ) → Multiset σ) s)
      (q.support.sup fun (s : σ →₀ ℕ) ↦ (toMultiset : (a : σ →₀ ℕ) → Multiset σ) s)

Tactic:
exact supDegree_mul_le (map_add _)

Premises used: map_add, AddMonoidAlgebra.supDegree_mul_le
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
ι : Type u_3
s : Finset ι
f : ι → MvPolynomial σ R
⊢ LE.le.{u_1} (α := Multiset σ) (degrees.{u, u_1} (R := R) (∏ i ∈ s, f i)) (∑ i ∈ s, (f i).degrees)

Tactic:
supDegree_prod_le (map_zero _) (map_add _)

Premises used: map_zero, map_add, MvPolynomial.support, MvPolynomial.degrees, AddMonoidAlgebra.supDegree_prod_le
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
ι : Type u_3
s : Finset ι
f : ι → MvPolynomial σ R
⊢ LE.le.{u_1} (α := Multiset σ) (degrees.{u, u_1} (R := R) (∏ i ∈ s, f i)) (∑ i ∈ s, (f i).degrees)

Tactic:
exact supDegree_prod_le (map_zero _) (map_add _)

Premises used: map_zero, map_add, AddMonoidAlgebra.supDegree_prod_le
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
ι : Type u_3
s : Finset ι
f : ι → MvPolynomial σ R
⊢ LE.le.{u_1} (α := Multiset σ) (degrees.{u, u_1} (R := R) (∏ i ∈ s, f i)) (∑ i ∈ s, (f i).degrees)

Tactic:
classical exact supDegree_prod_le (map_zero _) (map_add _)

Premises used: map_zero, map_add, AddMonoidAlgebra.supDegree_prod_le
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
n : ℕ
⊢ (p ^ n).degrees ≤ n • p.degrees

Tactic:
simpa using degrees_prod_le (s := .range n) (f := fun _ ↦ p)

Premises used: MvPolynomial.degrees_prod_le
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
i : σ
⊢ i ∈ p.degrees ↔ ∃ (d : σ →₀ ℕ), coeff d p ≠ 0 ∧ i ∈ d.support

Tactic:
simp only [degrees_def, Multiset.mem_sup, ← mem_support_iff, Finsupp.mem_toMultiset]

Premises used: MvPolynomial.mem_support_iff, MvPolynomial.degrees_def, Finsupp.mem_toMultiset, Multiset.mem_sup
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
i : σ
⊢ i ∈ p.degrees ↔ ∃ (d : σ →₀ ℕ), coeff d p ≠ 0 ∧ i ∈ d.support

Tactic:
classical
  simp only [degrees_def, Multiset.mem_sup, ← mem_support_iff, Finsupp.mem_toMultiset]

Premises used: MvPolynomial.mem_support_iff, MvPolynomial.degrees_def, Finsupp.mem_toMultiset, Multiset.mem_sup
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
rw : (∀ (a : σ), a ∉ p.degrees) ↔ ∀ b ∈ p.support, b = 0
⊢ p.degrees = 0 ↔ p.support ⊆ {0}

Tactic:
rw [Finset.subset_singleton_iff', Multiset.eq_zero_iff_forall_notMem]

Premises used: Multiset.eq_zero_iff_forall_notMem, Finset.subset_singleton_iff'
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
⊢ (∀ (a : σ), a ∉ p.degrees) ↔ ∀ b ∈ p.support, b = 0

Tactic:
⟨fun h s hs ↦ ?_, fun h i hi ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
refine_1 : ∀ (h : ∀ (a : σ), a ∉ p.degrees) (s : σ →₀ ℕ) (hs : s ∈ p.support), s = 0
refine_2 : ∀ (h : ∀ b ∈ p.support, b = 0) (i : σ) (hi : i ∈ p.degrees), False
⊢ (∀ (a : σ), a ∉ p.degrees) ↔ ∀ b ∈ p.support, b = 0

Tactic:
refine ⟨fun h s hs ↦ ?_, fun h i hi ↦ ?_⟩
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
h : ∀ (a : σ), a ∉ p.degrees
s : σ →₀ ℕ
hs : s ∈ p.support
refine_1 : s.support = ∅
⊢ s = 0

Tactic:
rw [← Finsupp.support_eq_empty]

Premises used: Finsupp.support_eq_empty
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
h : ∀ (a : σ), a ∉ p.degrees
s : σ →₀ ℕ
hs : s ∈ p.support
⊢ ∀ (a : σ), ¬∃ (d : σ →₀ ℕ), coeff d p ≠ 0 ∧ a ∈ d.support

Tactic:
simp only [mem_degrees] at h

Premises used: MvPolynomial.mem_degrees
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
s : σ →₀ ℕ
hs : s ∈ p.support
h : ∀ (a : σ), ¬∃ (d : σ →₀ ℕ), coeff d p ≠ 0 ∧ a ∈ d.support
⊢ s.support = ∅

Tactic:
grind
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
h : ∀ b ∈ p.support, b = 0
i : σ
hi : i ∈ p.degrees
refine_2 : ∀ (s : σ →₀ ℕ) (hs1 : coeff s p ≠ 0) (hs2 : i ∈ s.support), False
⊢ False

Tactic:
rcases mem_degrees.mp hi with ⟨s, hs1, hs2⟩

Premises used: Iff.mp, MvPolynomial.mem_degrees
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
h : ∀ b ∈ p.support, b = 0
i : σ
hi : i ∈ p.degrees
s : σ →₀ ℕ
hs1 : coeff s p ≠ 0
hs2 : i ∈ s.support
⊢ Membership.mem (γ := Finset σ) ∅ i

Tactic:
have := Finsupp.support_eq_empty.mpr (h s <| mem_support_iff.mpr hs1) ▸ hs2
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
h : ∀ b ∈ p.support, b = 0
i : σ
hi : i ∈ p.degrees
s : σ →₀ ℕ
hs1 : coeff s p ≠ 0
hs2 : i ∈ s.support
this : Membership.mem (γ := Finset σ) ∅ i
⊢ False

Tactic:
grind
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
h : Disjoint p.degrees q.degrees
a : ∀ b ∈ p.support, (toMultiset : (a : σ →₀ ℕ) → Multiset σ) b ≤ (p + q).degrees
⊢ p.degrees ≤ (p + q).degrees

Tactic:
apply Finset.sup_le

Premises used: Finset.sup_le