awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
i : σ
c : R
⊢ Multiset.count i
      (HMul.hMul (β := MvPolynomial σ R) p ((C : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R)).degrees ≤
    Multiset.count i (p.degrees + degrees.{u, u_1} (R := R) ((C : (a : R) → MvPolynomial σ R) c))

Tactic:
Multiset.count_le_of_le i degrees_mul_le

Premises used: Multiset.count_le_of_le, MvPolynomial.degrees_mul_le
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
i : σ
c : R
h : p.degrees = p.degrees + degrees.{u, u_1} (R := R) ((C : (a : R) → MvPolynomial σ R) c)
⊢ Multiset.count i
      (HMul.hMul (β := MvPolynomial σ R) p ((C : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R)).degrees ≤
    Multiset.count i p.degrees

Tactic:
convert! Multiset.count_le_of_le i degrees_mul_le
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
i : σ
c : R
⊢ p.degrees = p.degrees + degrees.{u, u_1} (R := R) ((C : (a : R) → MvPolynomial σ R) c)

Tactic:
simp only [degrees_C, add_zero]

Premises used: MvPolynomial.degrees_C, add_zero
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
τ : Type u_2
inst : CommSemiring R
p : MvPolynomial σ R
f : σ → τ
h : Injective f
i : σ
⊢ degreeOf.{u, u_2} (R := R) (f i) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p) = degreeOf i p

Tactic:
simp only [degreeOf, degrees_rename_of_injective h, Multiset.count_map_eq_count' f p.degrees h]

Premises used: MvPolynomial.degrees_rename_of_injective, MvPolynomial.degrees, Multiset.count_map_eq_count', MvPolynomial.degreeOf
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
τ : Type u_2
inst : CommSemiring R
p : MvPolynomial σ R
f : σ → τ
h : Injective f
i : σ
⊢ degreeOf.{u, u_2} (R := R) (f i) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p) = degreeOf i p

Tactic:
classical
  simp only [degreeOf, degrees_rename_of_injective h, Multiset.count_map_eq_count' f p.degrees h]

Premises used: MvPolynomial.degrees_rename_of_injective, MvPolynomial.degreeOf
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
e_f :
  Eq.{u_1 + 1} (α := (σ →₀ ℕ) → ℕ) (fun (s : σ →₀ ℕ) ↦ s.sum fun (x : σ) (e : ℕ) ↦ e) fun (m : σ →₀ ℕ) ↦
    Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) m)
⊢ Eq (α := ℕ) (p.support.sup fun (s : σ →₀ ℕ) ↦ s.sum fun (x : σ) (e : ℕ) ↦ e)
    (p.support.sup fun (m : σ →₀ ℕ) ↦ Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) m))

Tactic:
congr
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
e_f :
  ∀ (m : σ →₀ ℕ),
    (m.sum fun (x : σ) (e : ℕ) ↦ e) = Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) m)
⊢ Eq.{u_1 + 1} (α := (σ →₀ ℕ) → ℕ) (fun (s : σ →₀ ℕ) ↦ s.sum fun (x : σ) (e : ℕ) ↦ e) fun (m : σ →₀ ℕ) ↦
    Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) m)

Tactic:
funext m
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
m : σ →₀ ℕ
⊢ (m.sum fun (x : σ) (e : ℕ) ↦ e) = Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) m)

Tactic:
(Finsupp.card_toMultiset _).symm

Premises used: Finsupp.card_toMultiset, Eq.symm
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
m : σ →₀ ℕ
⊢ (m.sum fun (x : σ) (e : ℕ) ↦ e) = Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) m)

Tactic:
exact (Finsupp.card_toMultiset _).symm

Premises used: Finsupp.card_toMultiset, Eq.symm
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
s : σ →₀ ℕ
h : s ∈ p.support
⊢ (s.sum fun (x : σ) (e : ℕ) ↦ e) ≤ p.totalDegree

Tactic:
Finset.le_sup (α := ℕ) (f := fun s => sum s fun _ e => e) h

Premises used: MvPolynomial.totalDegree, Finset.le_sup
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
rw :
  (p.support.sup fun (m : σ →₀ ℕ) ↦ Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) m)) ≤
    p.degrees.card
⊢ p.totalDegree ≤ p.degrees.card

Tactic:
rw [totalDegree_eq]

Premises used: MvPolynomial.totalDegree_eq
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
⊢ (p.support.sup fun (m : σ →₀ ℕ) ↦ Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) m)) ≤
    p.degrees.card

Tactic:
Finset.sup_le fun s hs => Multiset.card_le_card <| Finset.le_sup hs

Premises used: Multiset.card_le_card, Finset.sup_le, Finset.le_sup
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
⊢ (p.support.sup fun (m : σ →₀ ℕ) ↦ Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) m)) ≤
    p.degrees.card

Tactic:
exact Finset.sup_le fun s hs => Multiset.card_le_card <| Finset.le_sup hs

Premises used: Multiset.card_le_card, Finset.sup_le
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
rw rw₁ rw₂ :
  (p.support.sup fun (m : σ →₀ ℕ) ↦ Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) m)) ≤
    p.degrees.card
⊢ p.totalDegree ≤ p.degrees.card

Tactic:
classical
  rw [totalDegree_eq]
  exact Finset.sup_le fun s hs => Multiset.card_le_card <| Finset.le_sup hs

Premises used: MvPolynomial.totalDegree_eq, Multiset.card_le_card, Finset.sup_le
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
h : p.support ⊆ q.support
⊢ p.totalDegree ≤ q.totalDegree

Tactic:
Finset.sup_mono h

Premises used: MvPolynomial.totalDegree, Finset.sup_mono
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
a : R
rw : Eq (α := ℕ) (if a = 0 then ⊥ else 0) 0
rw₁ : Eq (α := ℕ) (if a = 0 then 0 else 0) 0
rw₂ rw₃ : Eq (α := ℕ) 0 0
⊢ Eq (α := ℕ) (if a = 0 then ⊥ else sum 0 fun (x : σ) (e : ℕ) ↦ e) 0

Tactic:
rw [sum_zero_index, bot_eq_zero', ite_self]

Premises used: ite_self, Finsupp.sum_zero_index, bot_eq_zero'
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
rw : totalDegree.{u, u_1} (R := R) (σ := σ) ((C : (a : R) → MvPolynomial σ R) 0) = 0
⊢ totalDegree.{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
⊢ totalDegree.{u, u_1} (R := R) (σ := σ) ((C : (a : R) → MvPolynomial σ R) 0) = 0

Tactic:
totalDegree_C (0 : R)

Premises used: MvPolynomial.totalDegree_C, OfNat.ofNat
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
⊢ totalDegree.{u, u_1} (R := R) (σ := σ) ((C : (a : R) → MvPolynomial σ R) 0) = 0

Tactic:
exact totalDegree_C (0 : R)

Premises used: MvPolynomial.totalDegree_C, OfNat.ofNat
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
⊢ totalDegree.{u, u_1} (R := R) (σ := σ) 1 = 0

Tactic:
totalDegree_C (1 : R)

Premises used: MvPolynomial.totalDegree_C, OfNat.ofNat, Finsupp.single
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
inst_1 : Nontrivial R
s : σ
rw : Eq (α := ℕ) (Finset.sup {Finsupp.single s 1} fun (s : σ →₀ ℕ) ↦ s.sum fun (x : σ) (e : ℕ) ↦ e) 1
⊢ totalDegree.{u_3, u_1} (R := R) (X s) = 1

Tactic:
rw [totalDegree, support_X]

Premises used: MvPolynomial.totalDegree, MvPolynomial.support_X
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
inst_1 : Nontrivial R
s : σ
⊢ Eq (α := ℕ) (Finset.sup {Finsupp.single s 1} fun (s : σ →₀ ℕ) ↦ s.sum fun (x : σ) (e : ℕ) ↦ e) 1

Tactic:
simp only [Finset.sup, Finsupp.sum_single_index, Finset.fold_singleton, sup_bot_eq]

Premises used: Finsupp.sum_single_index, Finset.fold_singleton, sup_bot_eq, Finset.sup
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
a b : MvPolynomial σ R
⊢ (a + b).totalDegree ≤ max a.totalDegree b.totalDegree

Tactic:
sup_support_add_le _ _ _

Premises used: MvPolynomial.support, MvPolynomial.totalDegree, AddMonoidAlgebra.sup_support_add_le
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
a : (p + q).totalDegree ≤ p.totalDegree
a₁ : p.totalDegree ≤ (p + q).totalDegree
⊢ (p + q).totalDegree = p.totalDegree

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
a : (p + q).totalDegree ≤ max p.totalDegree q.totalDegree
⊢ (p + q).totalDegree ≤ p.totalDegree

Tactic:
rw [← max_eq_left_of_lt h]

Premises used: max_eq_left_of_lt
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
⊢ (p + q).totalDegree ≤ max p.totalDegree q.totalDegree

Tactic:
totalDegree_add p q

Premises used: MvPolynomial.totalDegree_add
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
⊢ (p + q).totalDegree ≤ max p.totalDegree q.totalDegree

Tactic:
exact totalDegree_add p q

Premises used: MvPolynomial.totalDegree_add
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
pos : ∀ (hp : p = 0), p.totalDegree ≤ (p + q).totalDegree
neg : ∀ (hp : ¬p = 0), p.totalDegree ≤ (p + q).totalDegree
⊢ p.totalDegree ≤ (p + q).totalDegree

Tactic:
by_cases hp : p = 0
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
hp : p = 0
⊢ p.totalDegree ≤ (p + q).totalDegree

Tactic:
simp [hp]
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
hp : ¬p = 0
neg :
  ∀ (b : σ →₀ ℕ) (hb₁ : b ∈ p.support)
    (hb₂ :
      (p.support.sup fun (m : σ →₀ ℕ) ↦ Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) m)) =
        Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) b)),
    p.totalDegree ≤ (p + q).totalDegree
⊢ p.totalDegree ≤ (p + q).totalDegree

Tactic:
obtain ⟨b, hb₁, hb₂⟩ :=
      p.support.exists_mem_eq_sup (Finsupp.support_nonempty_iff.mpr hp) fun m : σ →₀ ℕ =>
        Multiset.card (toMultiset m)

Premises used: Iff.mpr, Finsupp.toMultiset, MvPolynomial.support, Finsupp.support_nonempty_iff, Finset.exists_mem_eq_sup, Multiset.card, DFunLike.coe
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
hp : ¬p = 0
b : σ →₀ ℕ
hb₁ : b ∈ p.support
hb₂ :
  (p.support.sup fun (m : σ →₀ ℕ) ↦ Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) m)) =
    Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) b)
contrapose! : ∀ (h : b ∈ q.support), p.totalDegree ≤ q.totalDegree
⊢ b ∉ q.support

Tactic:
contrapose! h
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
hp : ¬p = 0
b : σ →₀ ℕ
hb₁ : b ∈ p.support
hb₂ :
  (p.support.sup fun (m : σ →₀ ℕ) ↦ Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) m)) =
    Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) b)
h : b ∈ q.support
rw :
  Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) b) ≤
    q.support.sup fun (m : σ →₀ ℕ) ↦ Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) m)
⊢ p.totalDegree ≤ q.totalDegree

Tactic:
rw [totalDegree_eq p, hb₂, totalDegree_eq]

Premises used: MvPolynomial.totalDegree_eq
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
hp : ¬p = 0
b : σ →₀ ℕ
hb₁ : b ∈ p.support
hb₂ :
  (p.support.sup fun (m : σ →₀ ℕ) ↦ Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) m)) =
    Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) b)
h : b ∈ q.support
⊢ Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) b) ≤
    q.support.sup fun (m : σ →₀ ℕ) ↦ Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) m)

Tactic:
apply Finset.le_sup h

Premises used: Finset.le_sup
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
hp : ¬p = 0
b : σ →₀ ℕ
hb₁ : b ∈ p.support
hb₂ :
  (p.support.sup fun (m : σ →₀ ℕ) ↦ Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) m)) =
    Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) b)
⊢ b ∉ q.support

Tactic:
have hb : b ∉ q.support := by
      contrapose! h
      rw [totalDegree_eq p, hb₂, totalDegree_eq]
      apply Finset.le_sup h
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
hp : ¬p = 0
b : σ →₀ ℕ
hb₁ : b ∈ p.support
hb₂ :
  (p.support.sup fun (m : σ →₀ ℕ) ↦ Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) m)) =
    Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) b)
hb : b ∉ q.support
a : b ∈ p.support \ q.support
⊢ b ∈ (p + q).support

Tactic:
apply support_sdiff_support_subset_support_add

Premises used: MvPolynomial.support_sdiff_support_subset_support_add
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
hp : ¬p = 0
b : σ →₀ ℕ
hb₁ : b ∈ p.support
hb₂ :
  (p.support.sup fun (m : σ →₀ ℕ) ↦ Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) m)) =
    Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) b)
hb : b ∉ q.support
a : b ∈ p.support ∧ b ∉ q.support
⊢ b ∈ p.support \ q.support

Tactic:
rw [Finset.mem_sdiff]

Premises used: Finset.mem_sdiff
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
hp : ¬p = 0
b : σ →₀ ℕ
hb₁ : b ∈ p.support
hb₂ :
  (p.support.sup fun (m : σ →₀ ℕ) ↦ Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) m)) =
    Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) b)
hb : b ∉ q.support
⊢ b ∈ p.support ∧ b ∉ q.support

Tactic:
⟨hb₁, hb⟩

Premises used: And.intro
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
hp : ¬p = 0
b : σ →₀ ℕ
hb₁ : b ∈ p.support
hb₂ :
  (p.support.sup fun (m : σ →₀ ℕ) ↦ Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) m)) =
    Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) b)
hb : b ∉ q.support
⊢ b ∈ p.support ∧ b ∉ q.support

Tactic:
exact ⟨hb₁, hb⟩
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
hp : ¬p = 0
b : σ →₀ ℕ
hb₁ : b ∈ p.support
hb₂ :
  (p.support.sup fun (m : σ →₀ ℕ) ↦ Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) m)) =
    Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) b)
hb : b ∉ q.support
⊢ b ∈ (p + q).support

Tactic:
have hbb : b ∈ (p + q).support := by
      apply support_sdiff_support_subset_support_add
      rw [Finset.mem_sdiff]
      exact ⟨hb₁, hb⟩
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
hp : ¬p = 0
b : σ →₀ ℕ
hb₁ : b ∈ p.support
hb₂ :
  (p.support.sup fun (m : σ →₀ ℕ) ↦ Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) m)) =
    Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) b)
hb : b ∉ q.support
hbb : b ∈ (p + q).support
neg :
  Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) b) ≤
    (p + q).support.sup fun (m : σ →₀ ℕ) ↦ Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) m)
⊢ p.totalDegree ≤ (p + q).totalDegree

Tactic:
rw [totalDegree_eq, hb₂, totalDegree_eq]

Premises used: MvPolynomial.totalDegree_eq
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
hp : ¬p = 0
b : σ →₀ ℕ
hb₁ : b ∈ p.support
hb₂ :
  (p.support.sup fun (m : σ →₀ ℕ) ↦ Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) m)) =
    Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) b)
hb : b ∉ q.support
hbb : b ∈ (p + q).support
⊢ Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) b) ≤
    (p + q).support.sup fun (m : σ →₀ ℕ) ↦ Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) m)

Tactic:
Finset.le_sup (f := fun m => Multiset.card (Finsupp.toMultiset m)) hbb

Premises used: Finset.le_sup
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
hp : ¬p = 0
b : σ →₀ ℕ
hb₁ : b ∈ p.support
hb₂ :
  (p.support.sup fun (m : σ →₀ ℕ) ↦ Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) m)) =
    Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) b)
hb : b ∉ q.support
hbb : b ∈ (p + q).support
⊢ Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) b) ≤
    (p + q).support.sup fun (m : σ →₀ ℕ) ↦ Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) m)

Tactic:
exact Finset.le_sup (f := fun m => Multiset.card (Finsupp.toMultiset m)) hbb

Premises used: Finset.le_sup
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
a : (p + q).totalDegree ≤ p.totalDegree
a₁ a₂ : p.totalDegree ≤ (p + q).totalDegree
pos : ∀ (hp : p = 0), p.totalDegree ≤ (p + q).totalDegree
neg neg₁ : ∀ (hp : ¬p = 0), p.totalDegree ≤ (p + q).totalDegree
neg₂ :
  ∀ (hp : ¬p = 0) (b : σ →₀ ℕ) (hb₁ : b ∈ p.support)
    (hb₂ :
      (p.support.sup fun (m : σ →₀ ℕ) ↦ Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) m)) =
        Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) b)),
    p.totalDegree ≤ (p + q).totalDegree
neg₃ :
  ∀ (hp : ¬p = 0) (b : σ →₀ ℕ) (hb₁ : b ∈ p.support)
    (hb₂ :
      (p.support.sup fun (m : σ →₀ ℕ) ↦ Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) m)) =
        Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) b))
    (hb : b ∉ q.support), p.totalDegree ≤ (p + q).totalDegree
neg₄ :
  ∀ (hp : ¬p = 0) (b : σ →₀ ℕ) (hb₁ : b ∈ p.support)
    (hb₂ :
      (p.support.sup fun (m : σ →₀ ℕ) ↦ Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) m)) =
        Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) b))
    (hb : b ∉ q.support) (hbb : b ∈ (p + q).support), p.totalDegree ≤ (p + q).totalDegree
neg₅ :
  ∀ (hp : ¬p = 0) (b : σ →₀ ℕ) (hb₁ : b ∈ p.support)
    (hb₂ :
      (p.support.sup fun (m : σ →₀ ℕ) ↦ Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) m)) =
        Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) b))
    (hb : b ∉ q.support) (hbb : b ∈ (p + q).support),
    Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) b) ≤
      (p + q).support.sup fun (m : σ →₀ ℕ) ↦ Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) m)
⊢ (p + q).totalDegree = p.totalDegree

Tactic:
classical
    apply le_antisymm
    · rw [← max_eq_left_of_lt h]
      exact totalDegree_add p q
    by_cases hp : p = 0
    · simp [hp]
    obtain ⟨b, hb₁, hb₂⟩ :=
      p.support.exists_mem_eq_sup (Finsupp.support_nonempty_iff.mpr hp) fun m : σ →₀ ℕ =>
        Multiset.card (toMultiset m)
    have hb : b ∉ q.support := by
      contrapose! h
      rw [totalDegree_eq p, hb₂, totalDegree_eq]
      apply Finset.le_sup h
    have hbb : b ∈ (p + q).support := by
      apply support_sdiff_support_subset_support_add
      rw [Finset.mem_sdiff]
      exact ⟨hb₁, hb⟩
    rw [totalDegree_eq, hb₂, totalDegree_eq]
    exact Finset.le_sup (f := fun m => Multiset.card (Finsupp.toMultiset m)) hbb

Premises used: MvPolynomial.totalDegree_eq, MvPolynomial.totalDegree_add, le_antisymm, max_eq_left_of_lt
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
rw : (p + q).totalDegree = p.totalDegree
rw₁ rw₂ : p.totalDegree = p.totalDegree
⊢ (q + p).totalDegree = p.totalDegree

Tactic:
rw [add_comm, totalDegree_add_eq_left_of_totalDegree_lt h]

Premises used: add_comm, MvPolynomial.totalDegree_add_eq_left_of_totalDegree_lt
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
a b : MvPolynomial σ R
⊢ (a * b).totalDegree ≤ a.totalDegree + b.totalDegree

Tactic:
sup_support_mul_le (fun _ _ ↦ (Finsupp.sum_add_index' (fun _ => rfl) (fun _ _ _ => rfl)).le) _ _

Premises used: MvPolynomial.support, AddMonoidAlgebra.sup_support_mul_le, MvPolynomial.totalDegree
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
S : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : DistribMulAction R S
a : R
f : MvPolynomial σ S
⊢ (a • f).totalDegree ≤ f.totalDegree

Tactic:
Finset.sup_mono support_smul

Premises used: MvPolynomial.totalDegree, Finset.sup_mono, MvPolynomial.support_smul
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
a : MvPolynomial σ R
n : ℕ
rw : totalDegree.{u, u_1} (R := R) (σ := σ) (∏ _k ∈ Finset.range n, a) ≤ ∑ _k ∈ Finset.range n, a.totalDegree
⊢ (a ^ n).totalDegree ≤ n * a.totalDegree

Tactic:
rw [Finset.pow_eq_prod_const, ← Nat.nsmul_eq_mul, Finset.nsmul_eq_sum_const]

Premises used: Nat.nsmul_eq_mul, Finset.nsmul_eq_sum_const, Finset.pow_eq_prod_const
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
a : MvPolynomial σ R
n : ℕ
⊢ totalDegree.{u, u_1} (R := R) (σ := σ) (∏ _k ∈ Finset.range n, a) ≤ ∑ _k ∈ Finset.range n, a.totalDegree

Tactic:
supDegree_prod_le rfl (fun _ _ => ?_)

Premises used: MvPolynomial.support, MvPolynomial.totalDegree, AddMonoidAlgebra.supDegree_prod_le
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
a : MvPolynomial σ R
n : ℕ
refine :
  ∀ (x x_1 : σ →₀ ℕ),
    ((x + x_1).sum fun (x : σ) (e : ℕ) ↦ e) =
      HAdd.hAdd (α := ℕ) (x.sum fun (x : σ) (e : ℕ) ↦ e) (x_1.sum fun (x : σ) (e : ℕ) ↦ e)
⊢ totalDegree.{u, u_1} (R := R) (σ := σ) (∏ _k ∈ Finset.range n, a) ≤ ∑ _k ∈ Finset.range n, a.totalDegree

Tactic:
refine supDegree_prod_le rfl (fun _ _ => ?_)

Premises used: AddMonoidAlgebra.supDegree_prod_le
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
a : MvPolynomial σ R
n : ℕ
x x_1 : σ →₀ ℕ
⊢ ((x + x_1).sum fun (x : σ) (e : ℕ) ↦ e) =
    HAdd.hAdd (α := ℕ) (x.sum fun (x : σ) (e : ℕ) ↦ e) (x_1.sum fun (x : σ) (e : ℕ) ↦ e)

Tactic:
Finsupp.sum_add_index' (fun _ => rfl) (fun _ _ _ => rfl)

Premises used: Finsupp.sum_add_index', rfl