awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
n : σ
f : MvPolynomial σ R
d : ℕ
h : 0 < d
rwa : (f.support.sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) n) < d ↔ ∀ m ∈ f.support, (m : (a : σ) → ℕ) n < d
rwa₁ : (∀ b ∈ f.support, (b : (a : σ) → ℕ) n < d) ↔ ∀ m ∈ f.support, (m : (a : σ) → ℕ) n < d
rwa₂ : ⊥ < d
rwa₃ : (∀ b ∈ f.support, (b : (a : σ) → ℕ) n < d) ↔ ∀ m ∈ f.support, (m : (a : σ) → ℕ) n < d
rwa₄ rwa₅ rwa₆ : ⊥ < d
⊢ degreeOf n f < d ↔ ∀ m ∈ f.support, (m : (a : σ) → ℕ) n < d

Tactic:
rwa [degreeOf_eq_sup, Finset.sup_lt_iff]

Premises used: Finset.sup_lt_iff, MvPolynomial.degreeOf_eq_sup
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
n : σ
f : MvPolynomial σ R
d : ℕ
rw : (f.support.sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) n) ≤ d ↔ ∀ m ∈ f.support, (m : (a : σ) → ℕ) n ≤ d
rw₁ rw₂ : (∀ b ∈ f.support, (b : (a : σ) → ℕ) n ≤ d) ↔ ∀ m ∈ f.support, (m : (a : σ) → ℕ) n ≤ d
⊢ degreeOf n f ≤ d ↔ ∀ m ∈ f.support, (m : (a : σ) → ℕ) n ≤ d

Tactic:
rw [degreeOf_eq_sup, Finset.sup_le_iff]

Premises used: MvPolynomial.degreeOf_eq_sup, Finset.sup_le_iff
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
n : σ
⊢ degreeOf.{u, u_1} (R := R) n 0 = 0

Tactic:
simp only [degreeOf_def, degrees_zero, Multiset.count_zero]

Premises used: MvPolynomial.degreeOf_def, Multiset.count_zero, MvPolynomial.degrees_zero
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
n : σ
⊢ degreeOf.{u, u_1} (R := R) n 0 = 0

Tactic:
classical simp only [degreeOf_def, degrees_zero, Multiset.count_zero]

Premises used: MvPolynomial.degreeOf_def, Multiset.count_zero, MvPolynomial.degrees_zero
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
n : σ
⊢ degreeOf.{u, u_1} (R := R) n 1 = 0

Tactic:
simp [degreeOf_def, degrees_one]

Premises used: MvPolynomial.degreeOf_def, MvPolynomial.degrees_one
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
n : σ
⊢ degreeOf.{u, u_1} (R := R) n 1 = 0

Tactic:
classical simp [degreeOf_def, degrees_one]

Premises used: MvPolynomial.degreeOf_def, MvPolynomial.degrees_one
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
a : R
x : σ
⊢ degreeOf.{u, u_1} (R := R) x ((C : (a : R) → MvPolynomial σ R) a) = 0

Tactic:
simp [degreeOf_def, degrees_C]

Premises used: MvPolynomial.degreeOf_def, MvPolynomial.degrees_C
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
a : R
x : σ
⊢ degreeOf.{u, u_1} (R := R) x ((C : (a : R) → MvPolynomial σ R) a) = 0

Tactic:
classical simp [degreeOf_def, degrees_C]

Premises used: MvPolynomial.degreeOf_def, MvPolynomial.degrees_C
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
i j : σ
inst_2 : Nontrivial R
pos : ∀ (c : i = j), degreeOf.{u, u_1} (R := R) i (X j) = if i = j then 1 else 0
neg : ∀ (c : ¬i = j), degreeOf.{u, u_1} (R := R) i (X j) = if i = j then 1 else 0
⊢ degreeOf.{u, u_1} (R := R) i (X j) = if i = j then 1 else 0

Tactic:
by_cases c : i = j
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
i j : σ
inst_2 : Nontrivial R
c : i = j
⊢ degreeOf.{u, u_1} (R := R) i (X j) = if i = j then 1 else 0

Tactic:
simp only [c, if_true, degreeOf_def, degrees_X, Multiset.count_singleton]

Premises used: if_true, MvPolynomial.degreeOf_def, MvPolynomial.degrees_X, Multiset.count_singleton
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
i j : σ
inst_2 : Nontrivial R
c : ¬i = j
⊢ degreeOf.{u, u_1} (R := R) i (X j) = if i = j then 1 else 0

Tactic:
simp [c, degreeOf_def, degrees_X]

Premises used: MvPolynomial.degreeOf_def, MvPolynomial.degrees_X
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
i j : σ
inst_2 : Nontrivial R
pos : ∀ (c : i = j), degreeOf.{u, u_1} (R := R) i (X j) = if i = j then 1 else 0
neg neg₁ : ∀ (c : ¬i = j), degreeOf.{u, u_1} (R := R) i (X j) = if i = j then 1 else 0
⊢ degreeOf.{u, u_1} (R := R) i (X j) = if i = j then 1 else 0

Tactic:
classical
  by_cases c : i = j
  · simp only [c, if_true, degreeOf_def, degrees_X, Multiset.count_singleton]
  simp [c, degreeOf_def, degrees_X]

Premises used: if_true, MvPolynomial.degreeOf_def, MvPolynomial.degrees_X, Multiset.count_singleton
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : Nontrivial R
i : σ
⊢ degreeOf.{u, u_1} (R := R) i (X i) = 1

Tactic:
simp [degreeOf_X]

Premises used: MvPolynomial.degreeOf_X
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : Nontrivial R
i : σ
⊢ degreeOf.{u, u_1} (R := R) i (X i) = 1

Tactic:
classical simp [degreeOf_X]

Premises used: MvPolynomial.degreeOf_X
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
i : σ
⊢ degreeOf i p ≠ 0 → p ≠ 0

Tactic:
aesop
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
n : σ
f g : MvPolynomial σ R
simp_rw :
  LE.le (α := ℕ) ((f + g).support.sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) n)
    (max (f.support.sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) n) (g.support.sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) n))
⊢ degreeOf n (f + g) ≤ max (degreeOf n f) (degreeOf n g)

Tactic:
simp_rw [degreeOf_eq_sup]

Premises used: MvPolynomial.degreeOf_eq_sup
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
n : σ
f g : MvPolynomial σ R
⊢ LE.le (α := ℕ) ((f + g).support.sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) n)
    (max (f.support.sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) n) (g.support.sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) n))

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
n : σ
f g : MvPolynomial σ R
⊢ LE.le (α := ℕ) ((f + g).support.sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) n)
    (max (f.support.sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) n) (g.support.sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) n))

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
i : σ
f : MvPolynomial σ R
m : σ →₀ ℕ
h_m : m ∈ f.support
rw : LE.le (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) (f.support.sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) i : ℕ)
⊢ (m : (a : σ) → ℕ) i ≤ degreeOf i f

Tactic:
rw [degreeOf_eq_sup i]

Premises used: MvPolynomial.degreeOf_eq_sup
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
i : σ
f : MvPolynomial σ R
m : σ →₀ ℕ
h_m : m ∈ f.support
⊢ LE.le (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) (f.support.sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) i : ℕ)

Tactic:
apply Finset.le_sup h_m

Premises used: Finset.le_sup
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
s : σ →₀ ℕ
i : σ
a : R
ha : a ≠ 0
rw : Multiset.count i (degrees.{u, u_1} (R := R) ((monomial s : (a : R) → MvPolynomial σ R) a)) = (s : (a : σ) → ℕ) i
rw₁ : Multiset.count i ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) s) = (s : (a : σ) → ℕ) i
rw₂ rw₃ : Eq (α := ℕ) ((s : (a : σ) → ℕ) i : ℕ) ((s : (a : σ) → ℕ) i : ℕ)
⊢ degreeOf.{u, u_1} (R := R) i ((monomial s : (a : R) → MvPolynomial σ R) a) = (s : (a : σ) → ℕ) i

Tactic:
rw [degreeOf_def, degrees_monomial_eq _ _ ha, Finsupp.count_toMultiset]

Premises used: MvPolynomial.degreeOf_def, Finsupp.count_toMultiset, MvPolynomial.degrees_monomial_eq
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
s : σ →₀ ℕ
i : σ
a : R
ha : a ≠ 0
classical :
  Multiset.count i (degrees.{u, u_1} (R := R) ((monomial s : (a : R) → MvPolynomial σ R) a)) = (s : (a : σ) → ℕ) i
classical₁ : Multiset.count i ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) s) = (s : (a : σ) → ℕ) i
classical₂ classical₃ : Eq (α := ℕ) ((s : (a : σ) → ℕ) i : ℕ) ((s : (a : σ) → ℕ) i : ℕ)
⊢ degreeOf.{u, u_1} (R := R) i ((monomial s : (a : R) → MvPolynomial σ R) a) = (s : (a : σ) → ℕ) i

Tactic:
classical rw [degreeOf_def, degrees_monomial_eq _ _ ha, Finsupp.count_toMultiset]

Premises used: MvPolynomial.degreeOf_def, Finsupp.count_toMultiset, MvPolynomial.degrees_monomial_eq
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : Nontrivial R
i : σ
k : ℕ
rw : degreeOf.{u, u_1} (R := R) i ((monomial (Finsupp.single i k) : (a : R) → MvPolynomial σ R) 1) = k
rw₁ : (Finsupp.single i k : (a : σ) → ℕ) i = k
rw₂ rw₃ : k = k
⊢ degreeOf i (HPow.hPow (α := MvPolynomial σ R) (X i) k) = k

Tactic:
rw [X_pow_eq_monomial, degreeOf_monomial_eq _ _ one_ne_zero, Finsupp.single_eq_same]

Premises used: MvPolynomial.X_pow_eq_monomial, Finsupp.single_eq_same, one_ne_zero, MvPolynomial.degreeOf_monomial_eq
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
i : σ
s : σ →₀ ℕ
h : s ∈ p.support
inl : ∀ (si : Eq (α := ℕ) (0 : ℕ) ((s : (a : σ) → ℕ) i : ℕ)), (s : (a : σ) → ℕ) i ≤ degreeOf i p
inr : ∀ (si : LT.lt (α := ℕ) (0 : ℕ) ((s : (a : σ) → ℕ) i : ℕ)), (s : (a : σ) → ℕ) i ≤ degreeOf i p
⊢ (s : (a : σ) → ℕ) i ≤ degreeOf i p

Tactic:
obtain si | si := eq_or_lt_of_le <| Nat.zero_le (s i)

Premises used: Nat.zero_le, eq_or_lt_of_le, DFunLike.coe
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
i : σ
s : σ →₀ ℕ
h : s ∈ p.support
si : Eq (α := ℕ) (0 : ℕ) ((s : (a : σ) → ℕ) i : ℕ)
⊢ (s : (a : σ) → ℕ) i ≤ degreeOf i p

Tactic:
simp [← si]
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
i : σ
s : σ →₀ ℕ
h : s ∈ p.support
si : LT.lt (α := ℕ) (0 : ℕ) ((s : (a : σ) → ℕ) i : ℕ)
inr : ∃ b ∈ p.support, LE.le (α := ℕ) ((s : (a : σ) → ℕ) i : ℕ) ((b : (a : σ) → ℕ) i : ℕ)
⊢ (s : (a : σ) → ℕ) i ≤ degreeOf i p

Tactic:
rw [degreeOf_eq_sup, Finset.le_sup_iff si]

Premises used: Finset.le_sup_iff, MvPolynomial.degreeOf_eq_sup
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
i : σ
s : σ →₀ ℕ
h : s ∈ p.support
si : LT.lt (α := ℕ) (0 : ℕ) ((s : (a : σ) → ℕ) i : ℕ)
w : σ →₀ ℕ
h₁ : s ∈ p.support ∧ LE.le (α := ℕ) ((s : (a : σ) → ℕ) i : ℕ) ((s : (a : σ) → ℕ) i : ℕ)
⊢ ∃ b ∈ p.support, LE.le (α := ℕ) ((s : (a : σ) → ℕ) i : ℕ) ((b : (a : σ) → ℕ) i : ℕ)

Tactic:
use s
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
i : σ
s : σ →₀ ℕ
h : degreeOf i p < (s : (a : σ) → ℕ) i
contrapose! : ∀ (h : s ∈ p.support), (s : (a : σ) → ℕ) i ≤ degreeOf i p
⊢ s ∉ p.support

Tactic:
contrapose! h
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
i : σ
s : σ →₀ ℕ
h : s ∈ p.support
⊢ (s : (a : σ) → ℕ) i ≤ degreeOf i p

Tactic:
le_degreeOf_of_mem_support i h

Premises used: MvPolynomial.le_degreeOf_of_mem_support
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
i : σ
s : σ →₀ ℕ
h : s ∈ p.support
⊢ (s : (a : σ) → ℕ) i ≤ degreeOf i p

Tactic:
exact le_degreeOf_of_mem_support i h

Premises used: MvPolynomial.le_degreeOf_of_mem_support
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
i : σ
f g : MvPolynomial σ R
⊢ Multiset.count i (f * g).degrees ≤ Multiset.count i (f.degrees + g.degrees)

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
i : σ
f g : MvPolynomial σ R
h : Multiset.count i f.degrees + Multiset.count i g.degrees = Multiset.count i (f.degrees + g.degrees)
⊢ Multiset.count i (f * g).degrees ≤ Multiset.count i f.degrees + Multiset.count i g.degrees

Tactic:
convert! 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
i : σ
f g : MvPolynomial σ R
h h₁ : Multiset.count i f.degrees + Multiset.count i g.degrees = Multiset.count i f.degrees + Multiset.count i g.degrees
⊢ Multiset.count i f.degrees + Multiset.count i g.degrees = Multiset.count i (f.degrees + g.degrees)

Tactic:
rw [Multiset.count_add]

Premises used: Multiset.count_add
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
i : σ
f g : MvPolynomial σ R
simp : Multiset.count i (f * g).degrees ≤ Multiset.count i f.degrees + Multiset.count i g.degrees
h : Multiset.count i f.degrees + Multiset.count i g.degrees = Multiset.count i (f.degrees + g.degrees)
⊢ degreeOf i (f * g) ≤ degreeOf i f + degreeOf i g

Tactic:
classical
  simp only [degreeOf]
  convert! Multiset.count_le_of_le i degrees_mul_le
  rw [Multiset.count_add]

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

Tactic:
simp_rw [degreeOf_eq_sup]

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

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
i : σ
s : Finset ι
f : ι → MvPolynomial σ R
⊢ LE.le (α := ℕ) (Finset.sup (support.{u, u_1} (R := R) (∑ j ∈ s, f j)) fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) i)
    (s.sup fun (j : ι) ↦ (f j).support.sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) i)

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
ι : Type u_3
i : σ
s : Finset ι
f : ι → MvPolynomial σ R
simp_rw :
  LE.le (α := ℕ) (Finset.sup (support.{u, u_1} (R := R) (∏ j ∈ s, f j)) fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) i)
    (∑ x ∈ s, (f x).support.sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) i)
⊢ degreeOf.{u, u_1} (R := R) i (∏ j ∈ s, f j) ≤ ∑ j ∈ s, degreeOf i (f j)

Tactic:
simp_rw [degreeOf_eq_sup]

Premises used: MvPolynomial.degreeOf_eq_sup
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
ι : Type u_3
i : σ
s : Finset ι
f : ι → MvPolynomial σ R
⊢ Eq (α := ℕ) ((0 : (a : σ) → ℕ) i : ℕ) (0 : ℕ)

Tactic:
simp only [coe_zero, Pi.zero_apply]

Premises used: Pi.zero_apply, Finsupp.coe_zero
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
ι : Type u_3
i : σ
s : Finset ι
f : ι → MvPolynomial σ R
⊢ ∀ (a1 a2 : σ →₀ ℕ),
    (a1 + a2 : (a : σ) → ℕ) i = HAdd.hAdd (α := ℕ) (β := ℕ) ((a1 : (a : σ) → ℕ) i : ℕ) ((a2 : (a : σ) → ℕ) i : ℕ)

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
ι : Type u_3
i : σ
s : Finset ι
f : ι → MvPolynomial σ R
⊢ LE.le (α := ℕ) (Finset.sup (support.{u, u_1} (R := R) (∏ j ∈ s, f j)) fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) i)
    (∑ x ∈ s, (f x).support.sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) i)

Tactic:
exact supDegree_prod_le (by simp only [coe_zero, Pi.zero_apply]) (by simp)

Premises used: AddMonoidAlgebra.supDegree_prod_le
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
i : σ
p : MvPolynomial σ R
n : ℕ
⊢ degreeOf i (p ^ n) ≤ n * degreeOf i p

Tactic:
simpa using degreeOf_prod_le i (Finset.range n) (fun _ => p)

Premises used: Finset.range, MvPolynomial.degreeOf_prod_le
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
i j : σ
f : MvPolynomial σ R
h : i ≠ j
simp :
  Eq (α := ℕ)
    (f.support.sup
      ((fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) i) ∘ (⇑(addRightEmbedding (Finsupp.single j 1)) : (a : σ →₀ ℕ) → σ →₀ ℕ)))
    (f.support.sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) i)
⊢ degreeOf i (f * X j) = degreeOf i f

Tactic:
simp only [degreeOf_eq_sup i, support_mul_X, Finset.sup_map]

Premises used: MvPolynomial.support_mul_X, Finset.sup_map, MvPolynomial.degreeOf_eq_sup
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
i j : σ
f : MvPolynomial σ R
h : i ≠ j
e_f :
  Eq (α := (σ →₀ ℕ) → ℕ)
    ((fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) i) ∘ (⇑(addRightEmbedding (Finsupp.single j 1)) : (a : σ →₀ ℕ) → σ →₀ ℕ))
    fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) i
⊢ Eq (α := ℕ)
    (f.support.sup
      ((fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) i) ∘ (⇑(addRightEmbedding (Finsupp.single j 1)) : (a : σ →₀ ℕ) → σ →₀ ℕ)))
    (f.support.sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) i)

Tactic:
congr
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
i j : σ
f : MvPolynomial σ R
h : i ≠ j
e_f :
  ∀ (x : σ →₀ ℕ),
    Eq (α := ℕ)
      (((fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) i) ∘ (⇑(addRightEmbedding (Finsupp.single j 1)) : (a : σ →₀ ℕ) → σ →₀ ℕ))
          x :
        ℕ)
      ((x : (a : σ) → ℕ) i : ℕ)
⊢ Eq (α := (σ →₀ ℕ) → ℕ)
    ((fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) i) ∘ (⇑(addRightEmbedding (Finsupp.single j 1)) : (a : σ →₀ ℕ) → σ →₀ ℕ))
    fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) i

Tactic:
ext
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
i j : σ
f : MvPolynomial σ R
h : i ≠ j
x : σ →₀ ℕ
⊢ Eq (α := ℕ)
    (((fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) i) ∘ (⇑(addRightEmbedding (Finsupp.single j 1)) : (a : σ →₀ ℕ) → σ →₀ ℕ))
        x :
      ℕ)
    ((x : (a : σ) → ℕ) i : ℕ)

Tactic:
simp only [Finsupp.single, addRightEmbedding_apply, coe_mk,
    Pi.add_apply, comp_apply, Finsupp.coe_add, Pi.single_eq_of_ne h, add_zero]

Premises used: addRightEmbedding_apply, Pi.single_eq_of_ne, Pi.add_apply, Finsupp.coe_add, Function.comp_apply, add_zero, Finsupp.coe_mk, Finsupp.single
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
i j : σ
f : MvPolynomial σ R
h : i ≠ j
simp :
  Eq (α := ℕ)
    (f.support.sup
      ((fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) i) ∘ (⇑(addRightEmbedding (Finsupp.single j 1)) : (a : σ →₀ ℕ) → σ →₀ ℕ)))
    (f.support.sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) i)
e_f :
  Eq (α := (σ →₀ ℕ) → ℕ)
    ((fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) i) ∘ (⇑(addRightEmbedding (Finsupp.single j 1)) : (a : σ →₀ ℕ) → σ →₀ ℕ))
    fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) i
e_f₁ :
  ∀ (x : σ →₀ ℕ),
    Eq (α := ℕ)
      (((fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) i) ∘ (⇑(addRightEmbedding (Finsupp.single j 1)) : (a : σ →₀ ℕ) → σ →₀ ℕ))
          x :
        ℕ)
      ((x : (a : σ) → ℕ) i : ℕ)
⊢ degreeOf i (f * X j) = degreeOf i f

Tactic:
classical
  simp only [degreeOf_eq_sup i, support_mul_X, Finset.sup_map]
  congr
  ext
  simp only [Finsupp.single, addRightEmbedding_apply, coe_mk,
    Pi.add_apply, comp_apply, Finsupp.coe_add, Pi.single_eq_of_ne h, add_zero]

Premises used: addRightEmbedding_apply, MvPolynomial.support_mul_X, Pi.add_apply, Finsupp.coe_add, Finset.sup_map, MvPolynomial.degreeOf_eq_sup, Function.comp_apply, add_zero, Finsupp.coe_mk, Finsupp.single
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
j : σ
f : MvPolynomial σ R
apply : Multiset.count j (f.degrees + degrees.{u, u_1} (R := R) (X j)) ≤ Multiset.count j f.degrees + 1
⊢ Multiset.count j (f * X j).degrees ≤ Multiset.count j f.degrees + 1

Tactic:
apply (Multiset.count_le_of_le j degrees_mul_le).trans

Premises used: Multiset.count_le_of_le, MvPolynomial.degrees_mul_le, LE.le.trans
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
j : σ
f : MvPolynomial σ R
simp : Multiset.count j (degrees.{u, u_1} (R := R) (X j)) ≤ 1
⊢ Multiset.count j (f.degrees + degrees.{u, u_1} (R := R) (X j)) ≤ Multiset.count j f.degrees + 1

Tactic:
simp only [Multiset.count_add, add_le_add_iff_left]

Premises used: add_le_add_iff_left, Multiset.count_add
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
j : σ
f : MvPolynomial σ R
⊢ Multiset.count j (degrees.{u, u_1} (R := R) (X j)) ≤ Multiset.count j {j}

Tactic:
Multiset.count_le_of_le j <| degrees_X' j

Premises used: Multiset.count_le_of_le, MvPolynomial.degrees_X'
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
j : σ
f : MvPolynomial σ R
h : 1 = Multiset.count j {j}
⊢ Multiset.count j (degrees.{u, u_1} (R := R) (X j)) ≤ 1

Tactic:
convert! Multiset.count_le_of_le j <| degrees_X' j

Premises used: Multiset.count_le_of_le, MvPolynomial.degrees_X'
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
j : σ
f : MvPolynomial σ R
h h₁ : Eq (α := ℕ) 1 1
⊢ 1 = Multiset.count j {j}

Tactic:
rw [Multiset.count_singleton_self]

Premises used: Multiset.count_singleton_self
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
j : σ
f : MvPolynomial σ R
simp : Multiset.count j (f * X j).degrees ≤ Multiset.count j f.degrees + 1
simp₁ : Multiset.count j (f.degrees + degrees.{u, u_1} (R := R) (X j)) ≤ Multiset.count j f.degrees + 1
simp₂ : Multiset.count j (degrees.{u, u_1} (R := R) (X j)) ≤ 1
h : 1 = Multiset.count j {j}
⊢ degreeOf j (f * X j) ≤ degreeOf j f + 1

Tactic:
classical
  simp only [degreeOf]
  apply (Multiset.count_le_of_le j degrees_mul_le).trans
  simp only [Multiset.count_add, add_le_add_iff_left]
  convert! Multiset.count_le_of_le j <| degrees_X' j
  rw [Multiset.count_singleton_self]

Premises used: add_le_add_iff_left, Multiset.count_singleton_self, Multiset.count_add, MvPolynomial.degrees_X', MvPolynomial.degreeOf
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
i j : σ
h : i ≠ j
zero : degreeOf.{u, u_1} (R := R) i 1 = 0
zero₁ : degreeOf.{u, u_1} (R := R) i ((C : (a : R) → MvPolynomial σ R) 1) = 0
zero₂ zero₃ : Eq (α := ℕ) 0 0
⊢ degreeOf i (HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (X j) 0) = 0

Tactic:
rw [pow_zero, ← C_1, degreeOf_C]

Premises used: MvPolynomial.degreeOf_C, MvPolynomial.C_1, pow_zero
-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
i j : σ
h : i ≠ j
k : ℕ
hk : degreeOf i (HPow.hPow (α := MvPolynomial σ R) (X j) k) = 0
succ : degreeOf i (HPow.hPow (α := MvPolynomial σ R) (X j) k * HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (X j) 1) = 0
succ₁ : degreeOf i (HPow.hPow (α := MvPolynomial σ R) (X j) k * X j) = 0
succ₂ : degreeOf i (HPow.hPow (α := MvPolynomial σ R) (X j) k) = 0
succ₃ succ₄ : Eq (α := ℕ) 0 0
⊢ degreeOf i (HPow.hPow (α := MvPolynomial σ R) (X j) (k + 1)) = 0

Tactic:
rw [pow_add, pow_one, degreeOf_mul_X_of_ne _ h, hk]

Premises used: pow_add, pow_one, MvPolynomial.degreeOf_mul_X_of_ne