mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i : σ
h : degreeOf i q < degreeOf i p
⊢ degreeOf i (p + q) = degreeOf i p

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i : σ
h : degreeOf i (p + q) < degreeOf i p
⊢ degreeOf i p = degreeOf i q

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
i : σ
c : R
⊢ degreeOf i (C c * p) ≤ degreeOf i p

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
i : σ
c : R
⊢ degreeOf i (p * C c) ≤ degreeOf i p

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
f : σ → τ
h : Injective f
i : σ
⊢ degreeOf (f i) ((rename f) p) = degreeOf i p

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ p.totalDegree = p.support.sup fun m ↦ (toMultiset m).card

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ p.totalDegree ≤ p.degrees.card

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
a : R
⊢ (if a = 0 then ⊥ else sum 0 fun x e ↦ e) = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
⊢ totalDegree 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
s : σ
⊢ (X s).totalDegree = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : constantCoeff p = 0
d : σ →₀ ℕ
hd : d ∈ p.support
⊢ d.support.Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
hp : ¬p = 0
⊢ p.support.Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: 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 ↦ (toMultiset m).card) = (toMultiset b).card
⊢ b ∉ q.support

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: 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 ↦ (toMultiset m).card) = (toMultiset b).card
hb : b ∉ q.support
⊢ b ∈ (p + q).support

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
⊢ (p + q).totalDegree = p.totalDegree

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
⊢ (q + p).totalDegree = p.totalDegree

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
a b : MvPolynomial σ R
x✝¹ x✝ : σ →₀ ℕ
⊢ ((x✝¹ + x✝).sum fun x e ↦ e) ≤ (x✝¹.sum fun x e ↦ e) + x✝.sum fun x e ↦ e

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
a : MvPolynomial σ R
n : ℕ
⊢ (a ^ n).totalDegree ≤ n * a.totalDegree

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s : σ →₀ ℕ
c : R
hc : c ≠ 0
⊢ ((monomial s) c).totalDegree = s.sum fun x e ↦ e

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s : σ →₀ ℕ
c : R
hc : ¬c = 0
⊢ (s.sum fun x e ↦ e) ≤ s.sum fun x ↦ id

Tactic:
Function.id_def

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s : σ →₀ ℕ
c : R
hc : ¬c = 0
⊢ (s.sum fun x e ↦ e) ≤ s.sum fun x x_1 ↦ x_1
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s : σ →₀ ℕ
c : R
⊢ ((monomial s) c).totalDegree ≤ s.sum fun x ↦ id

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
s : σ
n : ℕ
⊢ (X s ^ n).totalDegree = n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : ¬constantCoeff p = 0
d : σ →₀ ℕ
hd : d ∈ p.support
hd0 : d ≠ 0
⊢ d.support.Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
ι : Type u_3
s : Finset ι
f : ι → MvPolynomial σ R
⊢ (s.sum f).totalDegree ≤ s.sup fun i ↦ (f i).totalDegree

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial σ R
i : σ
d : σ →₀ ℕ
hd : d ∈ f.support
⊢ d i = 0 → d i ≤ f.totalDegree

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial σ R
i : σ
d : σ →₀ ℕ
hd : d ∈ f.support
h : d i ≠ 0
⊢ ∀ i ∈ d.support, 0 ≤ d i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
f : MvPolynomial σ R
n : ℕ
d : σ →₀ ℕ
hd : d ∈ f.support
h : ∀ (i : σ), n ≤ d i
⊢ n * Fintype.card σ = ∑ _s, n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
f : MvPolynomial σ R
n : ℕ
d : σ →₀ ℕ
hd : d ∈ f.support
h : ∀ (i : σ), n ≤ d i
⊢ ∑ s, d s ≤ d.sum fun x e ↦ e

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
f : MvPolynomial σ R
n : ℕ
h : f.totalDegree < n * Fintype.card σ
d : σ →₀ ℕ
hd : d ∈ f.support
⊢ ∃ i, d i < n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
⊢ (eval₂Hom f g) p = f (constantCoeff p)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
subS : Type u_3
inst✝² : CommSemiring S
inst✝¹ : SetLike subS S
inst✝ : SubsemiringClass subS S
f : R →+* S
p : MvPolynomial σ R
s : subS
hs : ∀ i ∈ p.support, f (coeff i p) ∈ s
v : σ → S
hv : ∀ (i : σ), v i ∈ s
⊢ eval₂ f v p ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
h : f.totalDegree < ∑ i ∈ d.support, d i
⊢ coeff d f = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f₁ : R →+* S
g₁ g₂ : σ → S
p₁ : MvPolynomial σ R
h : ∀ i ∈ p₁.vars, i ∈ p₁.vars → g₁ i = g₂ i
d : σ →₀ ℕ
hd : d ∈ p₁.support
i : σ
hi : i ∈ d.support
⊢ i ∈ p₁.vars

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ p.totalDegree = 0 ↔ p = C (coeff 0 p)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f₁ f₂ : R →+* S
g₁ g₂ : σ → S
p₁ p₂ : MvPolynomial σ R
⊢ f₁ = f₂ → (∀ i ∈ p₁.vars, i ∈ p₂.vars → g₁ i = g₂ i) → p₁ = p₂ → (eval₂Hom f₁ g₁) p₁ = (eval₂Hom f₂ g₂) p₂

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
f : σ → τ
p : MvPolynomial σ R
b : τ →₀ ℕ
h : b ∈ ((rename f) p).support
⊢ (b.sum fun x e ↦ e) ≤ p.totalDegree

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R : Type u
inst✝⁶ : CommSemiring R
S : Type u_2
T : Type u_3
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : CommSemiring T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
σ : Type u_4
τ : Type u_5
p : MvPolynomial (σ ⊕ τ) R
f : τ → S
g : σ → T
⊢ (aeval (Sum.elim g (⇑(algebraMap S T) ∘ f))) p = (aeval g) ((aeval (Sum.elim X (⇑C ∘ f))) p)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
f : σ ≃ τ
p : MvPolynomial σ R
⊢ p.totalDegree ≤ ((rename ⇑f.symm) ((rename ⇑f) p)).totalDegree

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s t : Multiset σ
a b : MvPolynomial σ R
ha : a ∈ {p | p.degrees ≤ s}
hb : b ∈ {p | p.degrees ≤ s}
⊢ a + b ∈ {p | p.degrees ≤ s}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R✝ : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ✝ : Type u_1
a a' a₁ a₂ : R✝
e : ℕ
n m : σ✝
s : σ✝ →₀ ℕ
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
⊢ algebraMap R (MvPolynomial σ S) =
    (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)).comp (algebraMap R (MvPolynomial σ R))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s t : Multiset σ
⊢ 0 ∈ {p | p.degrees ≤ s}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f₁ f₂ : MvPolynomial σ R →+* S
p₁ p₂ : MvPolynomial σ R
hC : f₁.comp C = f₂.comp C
hv : ∀ i ∈ p₁.vars, i ∈ p₂.vars → f₁ (X i) = f₂ (X i)
hp : p₁ = p₂
⊢ f₁ = eval₂Hom (f₁.comp C) (⇑f₁ ∘ X)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s t : Multiset σ
c : R
x : MvPolynomial σ R
hx : x ∈ {p | p.degrees ≤ s}
⊢ c • x ∈ {p | p.degrees ≤ s}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f₁ f₂ : MvPolynomial σ R →+* S
p₁ p₂ : MvPolynomial σ R
hC : f₁.comp C = f₂.comp C
hv : ∀ i ∈ p₁.vars, i ∈ p₂.vars → f₁ (X i) = f₂ (X i)
hp : p₁ = p₂
⊢ eval₂Hom (f₂.comp C) (⇑f₂ ∘ X) = f₂

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s t : Multiset σ
x : MvPolynomial σ R
hx : x ∈ degreesLE R σ (s + t)
i : σ →₀ ℕ
hi : toMultiset i ≤ s + t
a : σ →₀ ℕ := Multiset.toFinsupp (toMultiset i - t)
b : σ →₀ ℕ := Multiset.toFinsupp (toMultiset i ⊓ t)
⊢ Multiset.toFinsupp.symm (a + b) = Multiset.toFinsupp.symm i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s t : Multiset σ
x : MvPolynomial σ R
hx : x ∈ degreesLE R σ (s + t)
i : σ →₀ ℕ
hi : toMultiset i ≤ s + t
a : σ →₀ ℕ := Multiset.toFinsupp (toMultiset i - t)
b : σ →₀ ℕ := Multiset.toFinsupp (toMultiset i ⊓ t)
this : a + b = i
⊢ toMultiset a ≤ s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s t : Multiset σ
x : MvPolynomial σ R
hx : x ∈ degreesLE R σ (s + t)
i : σ →₀ ℕ
hi : toMultiset i ≤ s + t
a : σ →₀ ℕ := Multiset.toFinsupp (toMultiset i - t)
b : σ →₀ ℕ := Multiset.toFinsupp (toMultiset i ⊓ t)
this : a + b = i
ha : toMultiset a ≤ s
⊢ toMultiset b ≤ t

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
f : τ → σ
hfi : Injective f
hf : ↑p.vars ⊆ range f
⊢ (rename f) ((aeval fun i ↦ Option.elim' 0 X (partialInv f i)) p) = p

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: R : Type u
σ : Type u_1
τ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : DecidableEq τ
f : σ → τ
φ : MvPolynomial σ R
⊢ ((rename f) φ).vars ⊆ Finset.image f φ.vars

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
j : τ
h : j ∈ ((rename f) φ).vars
⊢ ∃ i ∈ φ.vars, f i = j

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s t : Multiset σ
⊢ degreesLE R σ (s + t) = degreesLE R σ s * degreesLE R σ t

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
⊢ 1 ≤ degreesLE R σ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
q : MvPolynomial σ R
s : Set σ
hs : ↑q.vars ⊆ s
inst✝ : (i : σ) → Decidable (i ∈ s)
u : σ →₀ ℕ
hu : u ∈ q.support
i : σ
hi : i ∈ u.support
⊢ (if i ∈ s then X i else 0) ^ u i = X i ^ u i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
x : MvPolynomial σ R
hx : x.degrees = 0
⊢ x.degrees.card ≤ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
q : MvPolynomial σ R
s : Set σ
hs : ↑q.vars ⊆ s
inst✝ : (i : σ) → Decidable (i ∈ s)
⊢ (aeval fun i ↦ if i ∈ s then X i else 0) q = q

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
x : MvPolynomial σ R
hx : x.degrees = 0
this : x = C (coeff 0 x)
⊢ (LinearMap.toSpanSingleton R (MvPolynomial σ R) 1) (coeff 0 x) = x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
⊢ degreesLE R σ 0 = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s : Multiset σ
⊢ degreesLE R σ (0 • s) = degreesLE R σ s ^ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s : Multiset σ
k : ℕ
⊢ degreesLE R σ ((k + 1) • s) = degreesLE R σ s ^ (k + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
p : MvPolynomial σ R
inst✝ : LinearOrder σ
⊢ leadingCoeff (⇑toLex) p = coeff (ofLex (supDegree (⇑toLex) p)) p

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : LinearOrder σ
r : R
⊢ supDegree (⇑toLex) (C r) = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.Monomial

Goal state before:
pp: R : Type u
n : ℕ
inst✝ : Semiring R
p : R[X]
hf : p.natDegree ≤ n
hn : p.coeff n = 0
⊢ p.natDegree ≤ n - 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.Monomial

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
h : #p.support ≤ 1
⊢ (monomial p.natDegree) p.leadingCoeff = p

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.Monomial

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
h : #p.support ≤ 1
⊢ C p.leadingCoeff * X ^ p.natDegree = p

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
h0 : p.comp q = 0
⊢ (p.comp q).natDegree ≤ p.natDegree * q.natDegree

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
h0 : ¬p.comp q = 0
n : ℕ
hn : n ∈ p.support
⊢ ↑(C (p.coeff n)).natDegree + n • q.degree ≤ ↑(C (p.coeff n)).natDegree + n • ↑q.natDegree

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
h0 : ¬p.comp q = 0
n : ℕ
hn : n ∈ p.support
⊢ ↑(C (p.coeff n)).natDegree + n • ↑q.natDegree = ↑(n * q.natDegree)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
h0 : ¬p.comp q = 0
n : ℕ
hn : n ∈ p.support
⊢ ↑(n * q.natDegree) ≤ ↑(p.natDegree * q.natDegree)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
h : p = 0
⊢ p.trailingDegree = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
hp : p ≠ 0
⊢ p.trailingDegree = ↑n ↔ p.natTrailingDegree = n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ≠ 0
⊢ p.trailingDegree = ↑n ↔ p.natTrailingDegree = n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.trailingDegree = ↑n
⊢ p.natTrailingDegree = n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
q : S[X]
h : p.trailingDegree = q.trailingDegree
⊢ p.natTrailingDegree = q.natTrailingDegree

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ^ p.natDegree ≠ 0
hq : q.natDegree = 0
⊢ p.natDegree * q.natDegree ≤ (p.comp q).natDegree

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
h : p.coeff p.natTrailingDegree = 0
hp : ¬p = 0
⊢ ?m.25

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p.coeff p.natTrailingDegree = 0 ↔ p = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p.natTrailingDegree = 0 ↔ p = 0 ∨ p.coeff 0 ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ ¬(p = 0 ∨ p.coeff 0 ≠ 0) ↔ p ≠ 0 ∧ p.coeff 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
h : p.coeff 0 ≠ 0
⊢ p.trailingCoeff = p.coeff 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ^ p.natDegree ≠ 0
⊢ (p.comp q).natDegree = p.natDegree * q.natDegree

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
hp : p ≠ 0
H : ↑n ≤ p.trailingDegree
⊢ n ≤ p.natTrailingDegree

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hq : q ≠ 0
hpq : p.trailingDegree ≤ q.trailingDegree
⊢ q.trailingDegree ≠ ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: R : Type u
a : R
n : ℕ
inst✝ : Semiring R
ha : a ≠ 0
⊢ ((monomial n) a).trailingDegree = ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: R : Type u
a : R
n : ℕ
inst✝ : Semiring R
ha : a ≠ 0
⊢ ((monomial n) a).natTrailingDegree = n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: R : Type u
a : R
n : ℕ
inst✝ : Semiring R
this : DecidableEq R := Classical.decEq R
ha : a = 0
⊢ ((monomial n) a).natTrailingDegree ≤ n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: R : Type u
a : R
n : ℕ
inst✝ : Semiring R
this : DecidableEq R := Classical.decEq R
ha : a = 0
⊢ ↑n ≤ ((monomial n) a).trailingDegree

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: R : Type u
inst✝ : Semiring R
⊢ 0 ≤ trailingDegree 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
h : p.IsRoot a
hlt : p.degree ≤ 0
⊢ False

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
⊢ (↑n).natTrailingDegree = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
n : ℕ
ha : a ≠ 0
⊢ (C a * X ^ n).trailingDegree = ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
n : ℕ
inst✝ : Semiring R
p : R[X]
⊢ p.natDegree ≤ n ↔ ∀ (N : ℕ), n < N → p.coeff N = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
a : R
⊢ ↑n ≤ (C a * X ^ n).trailingDegree

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
p q : R[X]
qn : q.natDegree ≤ n
⊢ (p + q).natDegree ≤ n ↔ p.natDegree ≤ n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
p q : R[X]
pn : p.natDegree ≤ n
⊢ (p + q).natDegree ≤ n ↔ q.natDegree ≤ n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : n < p.natTrailingDegree
⊢ p.coeff n = 0

Tactic:
by

Goal state after: