mathlib-initiative/mathlib-tactics huggingface dataset:
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
h' : ∃ a ∈ p.coeff.support, (mapDomain.addMonoidHom f) a = b
⊢ (b.sum fun x e ↦ e) ≤ p.totalDegree

Tactic:
]

Goal state after:
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
f : σ → τ
p : MvPolynomial σ R
b : τ →₀ ℕ
h : b ∈ ((rename f) p).support
h' : ∃ a ∈ p.coeff.support, (mapDomain.addMonoidHom f) a = b
⊢ (b.sum fun x e ↦ e) ≤ p.totalDegree
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}
⊢ ((algebraMap R (MvPolynomial σ R)) c * x).degrees ≤ s

Tactic:
]

Goal state after:
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}
⊢ ((algebraMap R (MvPolynomial σ R)) c * x).degrees ≤ s
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 ∧
    ∀ m ∈ degreesLE R σ s, ∀ n ∈ degreesLE R σ t, m * n ∈ degreesLE R σ (s + t)

Tactic:
]

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s t : Multiset σ
⊢ degreesLE R σ (s + t) ≤ degreesLE R σ s * degreesLE R σ t ∧
    ∀ m ∈ degreesLE R σ s, ∀ n ∈ degreesLE R σ t, m * n ∈ degreesLE R σ (s + t)
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
hb : toMultiset b ≤ t
⊢ (monomial a) (coeff i x) * (monomial b) 1 ∈ degreesLE R σ s * degreesLE R σ t

Tactic:
]

Goal state after:
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
hb : toMultiset b ≤ t
⊢ (monomial a) (coeff i x) * (monomial b) 1 ∈ degreesLE R σ s * degreesLE R σ t
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)
⊢ ∑ i ∈ q.support, (aeval fun i ↦ if i ∈ s then X i else 0) ((monomial i) (coeff i q)) =
    ∑ v ∈ q.support, (monomial v) (coeff v q)

Tactic:
]

Goal state after:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
q : MvPolynomial σ R
s : Set σ
hs : ↑q.vars ⊆ s
inst✝ : (i : σ) → Decidable (i ∈ s)
⊢ ∑ i ∈ q.support, (aeval fun i ↦ if i ∈ s then X i else 0) ((monomial i) (coeff i q)) =
    ∑ v ∈ q.support, (monomial v) (coeff v q)
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
⊢ ((algebraMap R (MvPolynomial σ R)) (coeff u q) * u.prod fun i k ↦ (if i ∈ s then X i else 0) ^ k) =
    C (coeff u q) * u.prod fun n e ↦ X n ^ e

Tactic:
]

Goal state after:
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
⊢ ((algebraMap R (MvPolynomial σ R)) (coeff u q) * u.prod fun i k ↦ (if i ∈ s then X i else 0) ^ k) =
    C (coeff u q) * u.prod fun n e ↦ X n ^ e
Module: Mathlib.Algebra.MvPolynomial.Variables

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

Tactic:
]

Goal state after:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
p : MvPolynomial σ R
inst✝ : LinearOrder σ
⊢ p.coeff (invFun (⇑toLex) (supDegree (⇑toLex) p)) = coeff (ofLex (supDegree (⇑toLex) p)) p
Module: Mathlib.Algebra.MvPolynomial.Variables

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

Tactic:
]

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

Goal state before:
pp: case succ
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
hf : p.natDegree ≤ n + 1
hn : p = 0
h : p.natDegree = n.succ
⊢ False

Tactic:
]

Goal state after:
case succ
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
hf : p.natDegree ≤ n + 1
hn : p = 0
h : p.natDegree = n.succ
⊢ False
Module: Mathlib.Algebra.Polynomial.Degree.Monomial

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

Tactic:
]

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
⊢ 0 ≤ p.natDegree * q.natDegree

Tactic:
]

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
h0 : p.comp q = 0
⊢ 0 ≤ p.natDegree * q.natDegree
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 ≤ ↑(C (p.coeff n)).natDegree + n • ↑q.natDegree

Tactic:
]

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 = ↑(n * q.natDegree)

Tactic:
]

Goal state after:
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 = ↑(n * q.natDegree)
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

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

Tactic:
]

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.trailingDegree = ↑n

Tactic:
]

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
⊢ q.trailingDegree.toNat = q.trailingDegree.toNat

Tactic:
]

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 simp [hq]

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:
]

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

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ^ p.natDegree ≠ 0
hq : ¬q.natDegree = 0
⊢ p.leadingCoeff * q.leadingCoeff ^ p.natDegree ≠ 0

Tactic:
]

Goal state after:
case neg
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ^ p.natDegree ≠ 0
hq : ¬q.natDegree = 0
⊢ p.leadingCoeff * q.leadingCoeff ^ p.natDegree ≠ 0
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.coeff 0 = p.coeff 0

Tactic:
]

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
⊢ n = n

Tactic:
]

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.natTrailingDegree
⊢ n ≤ p.natTrailingDegree

Tactic:
]

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
hp : p ≠ 0
H : n ≤ p.natTrailingDegree
⊢ n ≤ p.natTrailingDegree
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

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

Tactic:
]

Goal state after:
R : Type u
a : R
n : ℕ
inst✝ : Semiring R
ha : a ≠ 0
⊢ ↑n = ↑n
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

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

Tactic:
]

Goal state after:
R : Type u
a : R
n : ℕ
inst✝ : Semiring R
ha : a ≠ 0
⊢ (↑n).toNat = n
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.coeff 0 = 0
hlt : p.degree ≤ 0
this : p = C (p.coeff 0)
⊢ False

Tactic:
]

Goal state after:
R : Type u
a : R
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
h : p.coeff 0 = 0
hlt : p.degree ≤ 0
this : p = C (p.coeff 0)
⊢ False
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

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

Tactic:
]

Goal state after:
R : Type u
inst✝ : Semiring R
⊢ 0 ≤ (C 1).trailingDegree
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

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

Tactic:
]

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

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

Tactic:
]

Goal state after:
R : Type u
inst✝ : Semiring R
n : ℕ
a : R
⊢ ↑n ≤ ((monomial n) a).trailingDegree
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:
apply coeff_eq_zero_of_lt_trailingDegree

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : n < p.natTrailingDegree
⊢ ↑n < p.trailingDegree
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

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

Tactic:
]

Goal state after:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : n < p.natTrailingDegree
hp : p = 0
⊢ ↑n < ⊤
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
h : (p + q).natDegree ≤ n
m : ℕ
hm : n < m
⊢ p.coeff m = p.coeff m

Tactic:
]

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

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

Tactic:
]

Goal state after:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : n < p.natTrailingDegree
hp : ¬p = 0
⊢ ↑n < ↑p.natTrailingDegree
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
⊢ (q + p).natDegree ≤ n ↔ q.natDegree ≤ n

Tactic:
]

Goal state after:
R : Type u
inst✝ : Semiring R
n : ℕ
p q : R[X]
pn : p.natDegree ≤ n
⊢ (q + p).natDegree ≤ n ↔ q.natDegree ≤ n
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
h : p ≠ 0
⊢ ENat.toNat ↑(p.support.min' ⋯) = p.support.min' ⋯

Tactic:
]

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
h : p ≠ 0
⊢ ENat.toNat ↑(p.support.min' ⋯) = p.support.min' ⋯
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
p : R[X]
ai : R
au : ai * a = 1
⊢ (1 * p).natDegree = (1 * p).natDegree

Tactic:
]

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

Goal state before:
pp: R : Type u
n : ℕ
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
hn : ∀ m < n, p.coeff m = 0
⊢ n ≤ p.support.min' ⋯

Tactic:
]

Goal state after:
R : Type u
n : ℕ
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
hn : ∀ m < n, p.coeff m = 0
⊢ n ≤ p.support.min' ⋯
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
p : R[X]
ai : R
au : ai * a = 1
⊢ (C ai * C a * p).natDegree = (C ai * C a * p).natDegree

Tactic:
]

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

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
p : R[X]
ai : R
au : a * ai = 1
⊢ (p * 1).natDegree = (p * 1).natDegree

Tactic:
]

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

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p = 0
⊢ 0 ≤ 0

Tactic:
]

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

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
p : R[X]
ai : R
au : a * ai = 1
⊢ (p * C a * C ai).natDegree = (p * C a * C ai).natDegree

Tactic:
]

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

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
p : R[X]
h : p.leadingCoeff * a ≠ 0
⊢ p.coeff p.natDegree * a ≠ 0

Tactic:
]

Goal state after:
R : Type u
a : R
inst✝ : Semiring R
p : R[X]
h : p.leadingCoeff * a ≠ 0
⊢ p.coeff p.natDegree * a ≠ 0
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: case a
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
n : ℕ
h : (p * X ^ n).coeff (p.natTrailingDegree + n) = 0
⊢ (p * X ^ ?a.n✝).coeff (p.natTrailingDegree + ?a.n✝) = 0

pp: case a.n
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
n : ℕ
h : (p * X ^ n).coeff (p.natTrailingDegree + n) = 0
⊢ ℕ

Tactic:
]

Goal state after:
case a
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
n : ℕ
h : (p * X ^ n).coeff (p.natTrailingDegree + n) = 0
⊢ (p * X ^ ?a.n✝).coeff (p.natTrailingDegree + ?a.n✝) = 0

case a.n
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
n : ℕ
h : (p * X ^ n).coeff (p.natTrailingDegree + n) = 0
⊢ ℕ
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: case a
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
n : ℕ
⊢ ∀ y ∈ (p * X ^ n).support, p.natTrailingDegree + n ≤ y

Tactic:
]

Goal state after:
case a
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
n : ℕ
⊢ ∀ y ∈ (p * X ^ n).support, p.natTrailingDegree + n ≤ y
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
p : R[X]
h : a * p.leadingCoeff ≠ 0
⊢ a * p.coeff p.natDegree ≠ 0

Tactic:
]

Goal state after:
R : Type u
a : R
inst✝ : Semiring R
p : R[X]
h : a * p.leadingCoeff ≠ 0
⊢ a * p.coeff p.natDegree ≠ 0
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
p : R[X]
h : a * p.leadingCoeff ≠ 0
⊢ (C a * p).coeff p.natDegree ≠ 0

Tactic:
rwa [coeff_C_mul]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
n y : ℕ
hy : (if n ≤ y then p.coeff (y - n) else 0) ≠ 0
⊢ n ≤ y

Tactic:
]

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
n y : ℕ
hy : (if n ≤ y then p.coeff (y - n) else 0) ≠ 0
⊢ n ≤ y
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
p : R[X]
h : a * p.leadingCoeff ≠ 0
⊢ (C a).degree + p.degree = p.degree

Tactic:
]

Goal state after:
R : Type u
a : R
inst✝ : Semiring R
p : R[X]
h : a * p.leadingCoeff ≠ 0
⊢ (C a).degree + p.degree = p.degree
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: case a
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
n y : ℕ
hy : p.coeff (y - n) ≠ 0
key : n ≤ y
⊢ p.natTrailingDegree + n ≤ y

Tactic:
]

Goal state after:
case a
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
n y : ℕ
hy : p.coeff (y - n) ≠ 0
key : n ≤ y
⊢ p.natTrailingDegree + n ≤ y
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
hn : ∑ x ∈ antidiagonal n, p.coeff x.1 * q.coeff x.2 ≠ 0
⊢ p.trailingDegree + q.trailingDegree ≤ ↑n

Tactic:
]

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
hn : ∑ x ∈ antidiagonal n, p.coeff x.1 * q.coeff x.2 ≠ 0
⊢ p.trailingDegree + q.trailingDegree ≤ ↑n
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case succ
R : Type u
m✝ n : ℕ
inst✝ : Semiring R
p : R[X]
pn : p.natDegree ≤ n
m : ℕ
hm : (p ^ m).coeff (m * n) = p.coeff n ^ m
⊢ (p ^ m).coeff (m * n) * p.coeff n = (p ^ m).coeff (m * n) * p.coeff n

pp: R : Type u
m✝ n : ℕ
inst✝ : Semiring R
p : R[X]
pn : p.natDegree ≤ n
m : ℕ
hm : (p ^ m).coeff (m * n) = p.coeff n ^ m
⊢ (p ^ m).natDegree ≤ m * n

Tactic:
]

Goal state after:
R : Type u
m✝ n : ℕ
inst✝ : Semiring R
p : R[X]
pn : p.natDegree ≤ n
m : ℕ
hm : (p ^ m).coeff (m * n) = p.coeff n ^ m
⊢ (p ^ m).natDegree ≤ m * n
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
hn : ∑ x ∈ antidiagonal n, p.coeff x.1 * q.coeff x.2 ≠ 0
i j : ℕ
hij : (i, j) ∈ antidiagonal n
hpq : p.coeff (i, j).1 * q.coeff (i, j).2 ≠ 0
⊢ (i, j) ∈ antidiagonal n

Tactic:
]

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
hn : ∑ x ∈ antidiagonal n, p.coeff x.1 * q.coeff x.2 ≠ 0
i j : ℕ
hij : (i, j) ∈ antidiagonal n
hpq : p.coeff (i, j).1 * q.coeff (i, j).2 ≠ 0
⊢ (i, j) ∈ antidiagonal n
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

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

Tactic:
]

Goal state after:
R : Type u
n : ℕ
inst✝ : Semiring R
p q : R[X]
pn : p.natDegree < n
⊢ (q + p).coeff n = q.coeff n
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
h : p * q ≠ 0
hp : p = 0
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
h : p * q ≠ 0
hp : p ≠ 0
hq : q = 0
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
h : p * q ≠ 0
hp : p ≠ 0
hq : q = 0
⊢ p * q = 0

Tactic:
by rw [hq, mul_zero]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
h : p * q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ p.trailingDegree + q.trailingDegree ≤ (p * q).trailingDegree

Tactic:
]

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p * q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ p.trailingDegree + q.trailingDegree ≤ (p * q).trailingDegree
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case insert.inl
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
IH : (s.sum f).degree = s.sup fun i ↦ (f i).degree
h : {i | i ∈ insert x s ∧ f i ≠ 0}.Pairwise (Ne on degree ∘ f)
H : (f x).degree < (s.sum f).degree
⊢ (s.sum f).degree = (s.sum f).degree

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ ∑ x ∈ antidiagonal (p.natTrailingDegree + q.natTrailingDegree), p.coeff x.1 * q.coeff x.2 =
    p.trailingCoeff * q.trailingCoeff

Tactic:
]

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ ∑ x ∈ antidiagonal (p.natTrailingDegree + q.natTrailingDegree), p.coeff x.1 * q.coeff x.2 =
    p.trailingCoeff * q.trailingCoeff
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natTrailingDegree + q.natTrailingDegree
h₂ : (i, j) ≠ (p.natTrailingDegree, q.natTrailingDegree)
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0

Tactic:
]

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natTrailingDegree + q.natTrailingDegree
h₂ : (i, j) ≠ (p.natTrailingDegree, q.natTrailingDegree)
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natTrailingDegree + q.natTrailingDegree
h₂ : (i, j) ≠ (p.natTrailingDegree, q.natTrailingDegree)
hi : i < p.natTrailingDegree
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natTrailingDegree + q.natTrailingDegree
h₂ : (i, j) ≠ (p.natTrailingDegree, q.natTrailingDegree)
hi : p.natTrailingDegree ≤ i
hj : j < q.natTrailingDegree
⊢ 0 = 0

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.trailingCoeff * q.trailingCoeff ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ (p * q).trailingDegree ≤ ↑(p.natTrailingDegree + q.natTrailingDegree)

Tactic:
]

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.trailingCoeff * q.trailingCoeff ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ (p * q).trailingDegree ≤ ↑(p.natTrailingDegree + q.natTrailingDegree)
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case insert.inr.inl.inr
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
IH : (s.sum f).degree = s.sup fun i ↦ (f i).degree
h : {i | i ∈ insert x s ∧ f i ≠ 0}.Pairwise (Ne on degree ∘ f)
hs : s.Nonempty
y : S
H : (f x).degree = (f y).degree
hy : y ∈ s
hy' : (s.sup fun i ↦ (f i).degree) = (f y).degree
⊢ (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sup fun i ↦ (f i).degree)

Tactic:
]

Goal state after:
case insert.inr.inl.inr
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
IH : (s.sum f).degree = s.sup fun i ↦ (f i).degree
h : {i | i ∈ insert x s ∧ f i ≠ 0}.Pairwise (Ne on degree ∘ f)
hs : s.Nonempty
y : S
H : (f x).degree = (f y).degree
hy : y ∈ s
hy' : (s.sup fun i ↦ (f i).degree) = (f y).degree
⊢ (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sup fun i ↦ (f i).degree)
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.trailingCoeff * q.trailingCoeff ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ p.trailingCoeff * q.trailingCoeff ≠ 0

Tactic:
]

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.trailingCoeff * q.trailingCoeff ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ p.trailingCoeff * q.trailingCoeff ≠ 0
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.trailingCoeff * q.trailingCoeff ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ p.trailingDegree + q.trailingDegree = p.trailingDegree + q.trailingDegree

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℕ
⊢ ↑n = ↑n

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℕ
⊢ n = n

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
⊢ (-p).support.min = p.support.min

Tactic:
support_neg

Goal state after:
R : Type u
inst✝ : Ring R
p : R[X]
⊢ p.support.min = p.support.min