mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

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

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a : R
f : R[X]
⊢ (C a * f).natDegree ≤ f.natDegree

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
f : R[X]
a : R
⊢ (f * C a).natDegree ≤ f.natDegree

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]
ai : R
au : ai * a = 1
⊢ p.natDegree = (1 * p).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.natTrailingDegree = p.support.min' ⋯

Tactic:
by

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.natTrailingDegree

Tactic:
rw [natTrailingDegree_eq_support_min' hp]
  exact Finset.le_min' _ _ _ fun m hm => not_lt.1 fun hmn => mem_support_iff.1 hm <| hn _ hmn

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 : ai * a = 1
⊢ (1 * p).natDegree = (C ai * (C a * p)).natDegree

Tactic:
by

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.natTrailingDegree

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]
ai : R
au : a * ai = 1
⊢ p.natDegree = (p * 1).natDegree

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]
ai : R
au : a * ai = 1
⊢ (p * 1).natDegree = (p * C a * C ai).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]
⊢ p.natTrailingDegree ≤ p.natDegree

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]
h : p.leadingCoeff * a ≠ 0
⊢ (p * C a).natDegree = p.natDegree

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]
h : a * p.leadingCoeff ≠ 0
⊢ (C a * p).natDegree = p.natDegree

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]
h : a * p.leadingCoeff ≠ 0
⊢ (C a).leadingCoeff * p.leadingCoeff ≠ 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]
hp : p ≠ 0
n y : ℕ
hy : y ∈ (p * X ^ n).support
⊢ n ≤ y

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]
h : a * p.leadingCoeff ≠ 0
⊢ (C a * p).degree = p.degree

Tactic:
by

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 : ℕ
⊢ (p * X ^ n).natTrailingDegree = p.natTrailingDegree + n

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
f g : R[X]
⊢ (f * g).coeff (f.natDegree + g.natDegree) = f.coeff f.natDegree * g.coeff g.natDegree

Tactic:
by

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

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

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]
⊢ p.trailingDegree + q.trailingDegree ≤ (p * q).trailingDegree

Tactic:
by

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

Goal state before:
pp: R : Type u
m n : ℕ
inst✝ : Semiring R
p : R[X]
o : ℕ
pn : p.natDegree ≤ n
mno : m * n ≤ o
⊢ (p ^ m).coeff o = if o = m * n then p.coeff n ^ m else 0

Tactic:
by

Goal state after:
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
⊢ (p + q).coeff n = q.coeff n

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]
h : p * q ≠ 0
hp : p = 0
⊢ p * q = 0

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
IH : {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Ne on degree ∘ f) → (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)
x✝ : S
⊢ x✝ ∈ {i | i ∈ s ∧ f i ≠ 0} → x✝ ∈ {i | i ∈ insert x s ∧ f i ≠ 0}

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]
h : p * q ≠ 0
hp : p ≠ 0
hq : q = 0
⊢ p * q = 0

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]
h : p * q ≠ 0
⊢ p.natTrailingDegree + q.natTrailingDegree ≤ (p * q).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]
⊢ (p * q).coeff (p.natTrailingDegree + q.natTrailingDegree) = p.trailingCoeff * q.trailingCoeff

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]
h : p.trailingCoeff * q.trailingCoeff ≠ 0
hp : p = 0
⊢ p.trailingCoeff * q.trailingCoeff = 0

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]
h : p.trailingCoeff * q.trailingCoeff ≠ 0
hp : p ≠ 0
hq : q = 0
⊢ p.trailingCoeff * q.trailingCoeff = 0

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]
h : p.trailingCoeff * q.trailingCoeff ≠ 0
⊢ (p * q).trailingDegree = p.trailingDegree + q.trailingDegree

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]
h : p.trailingCoeff * q.trailingCoeff ≠ 0
⊢ (p * q).natTrailingDegree = p.natTrailingDegree + q.natTrailingDegree

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℕ
⊢ (X ^ n).trailingDegree = ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ f.eraseLead.support = f.support.erase f.natDegree

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℕ
⊢ (X ^ n).natTrailingDegree = n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
i : ℕ
⊢ f.eraseLead.coeff i = if i = f.natDegree then 0 else f.coeff i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ f.eraseLead.coeff f.natDegree = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
i : ℕ
hi : i ≠ f.natDegree
⊢ f.eraseLead.coeff i = f.coeff i

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
⊢ eraseLead 0 = 0

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
⊢ nextCoeffUp 0 = 0

Tactic:
by

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

Goal state before:
pp: 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
hx0 : ¬f x = 0
⊢ f y ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ f.eraseLead + C f.leadingCoeff * X ^ f.natDegree = f

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
c : R
⊢ (C c).nextCoeffUp = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_2
inst✝ : Ring R
f : R[X]
⊢ f - C f.leadingCoeff * X ^ f.natDegree = f.eraseLead

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
f0 : 2 ≤ #f.support
⊢ f.eraseLead ≠ 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]
hp : p.coeff 0 = 0
⊢ p.nextCoeffUp = p.coeff (p.natTrailingDegree + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
a : ℕ
h : a ∈ f.eraseLead.support
⊢ a < f.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 : ℕ∞
h : p.trailingDegree < n
h₀ : p = 0
⊢ n ≤ p.trailingDegree

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f ≠ 0
⊢ #f.eraseLead.support < #f.support

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f ≠ 0
⊢ #f.eraseLead.support + 1 = #f.support

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ #f.eraseLead.support = #f.support - 1

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.Monic
⊢ p = X ^ p.natDegree ↔ p.natDegree ≤ p.natTrailingDegree

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
c : ℕ
fc : #f.support = c + 1
⊢ #f.eraseLead.support = c

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.eraseLead = 0
⊢ #f.support ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: N i : ℕ
⊢ revAtFun N (revAtFun N i) = i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: N a b : ℕ
hab : revAtFun N a = revAtFun N b
⊢ revAtFun N (revAtFun N b) = b

Tactic:
revAtFun_invol

Goal state after:
N a b : ℕ
hab : revAtFun N a = revAtFun N b
⊢ b = b
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: N : ℕ
⊢ Function.Injective (revAtFun N)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: N i : ℕ
h : N < i
⊢ (revAt N) i = i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: N O n o : ℕ
hn : n ≤ N
ho : o ≤ O
⊢ (revAt (N + O)) (n + o) = (revAt N) n + (revAt O) o

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: N : ℕ
⊢ (revAt N) 0 = N

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
i : ℕ
r : R
⊢ ((monomial i) r).eraseLead = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
N : ℕ
f : R[X]
⊢ (reflect N f).support = image (⇑(revAt N)) f.support

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
⊢ (X ^ n).eraseLead = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
N i : ℕ
f : AddMonoidAlgebra R ℕ
⊢ (embDomain (revAt N) f.coeff) i = (embDomain (revAt N) f.coeff) ((revAt N) ((revAt N) i))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
r : R
n : ℕ
⊢ (C r * X ^ n).eraseLead = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
N : ℕ
f : R[X]
i : ℕ
⊢ (reflect N f).coeff i = f.coeff ((revAt N) i)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
r : R
⊢ (C r * X).eraseLead = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
N : ℕ
p : R[X]
⊢ reflect N (reflect N p) = p

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
N : ℕ
f : R[X]
⊢ reflect N f = 0 ↔ f = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f g : R[X]
N : ℕ
⊢ reflect N (f + g) = reflect N f + reflect N g

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
r : R
N : ℕ
⊢ reflect N (C r * f) = C r * reflect N f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
N n : ℕ
c : R
⊢ reflect N (C c * X ^ n) = C c * X ^ (revAt N) n

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
r : R
N : ℕ
⊢ reflect N (C r) = C r * X ^ N

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
N n : ℕ
⊢ reflect N (X ^ n) = X ^ (revAt N) n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
⊢ reflect 1 X = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
S : Type u_2
inst✝ : Semiring S
f : R →+* S
p : R[X]
n : ℕ
⊢ reflect n (map f p) = map f (reflect n p)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : q.degree < p.degree
⊢ (p + q).eraseLead = p.eraseLead + q

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
⊢ reflect n 1 = X ^ n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : p.degree < q.degree
⊢ (p + q).eraseLead = p + q.eraseLead

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.eraseLead ≠ 0
⊢ 0 < f.natDegree

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ f.eraseLead.natDegree < f.natDegree ∨ f.eraseLead = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ f.eraseLead.natDegree ≤ f.natDegree - 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
⊢ f.eraseLead.natDegree = f.natDegree - 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
⊢ f.eraseLead.natDegree + 1 = f.natDegree

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff = 0
⊢ f.eraseLead.natDegree ≤ f.natDegree - 2

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
hlead : f.eraseLead ≠ 0
hnext : f.nextCoeff = 0
⊢ 2 ≤ f.natDegree

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
⊢ f.eraseLead.leadingCoeff = f.nextCoeff

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.eraseLead = 0
⊢ f.nextCoeff = 0

Tactic:
by

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

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

Tactic:
obtain ⟨x, hx, hx'⟩ := H
    have hs : s.Nonempty := ⟨x, hx⟩
    refine natDegree_eq_of_degree_eq_some ?_
    rw [degree_sum_eq_of_disjoint]
    · rw [← Finset.sup'_eq_sup hs, ← Finset.sup'_eq_sup hs,
        Nat.cast_withBot, Finset.coe_sup' hs, ←
        Finset.sup'_eq_sup hs]
      refine le_antisymm ?_ ?_
      · rw [Finset.sup'_le_iff]
        intro b hb
        by_cases hb' : f b = 0
        · simpa [hb'] using! hs
        rw [degree_eq_natDegree hb', Nat.cast_withBot]
        exact Finset.le_sup' (fun i : S => (natDegree (f i) : WithBot ℕ)) hb
      · rw [Finset.sup'_le_iff]
        intro b hb
        simp only [Finset.le_sup'_iff, Function.comp_apply]
        by_cases hb' : f b = 0
        · refine ⟨x, hx, ?_⟩
          contrapose! hx'
          simpa [← Nat.cast_withBot, hb', degree_eq_bot] using! hx'
        exact ⟨b, hb, (degree_eq_natDegree hb').ge⟩
    · exact h.imp fun x y hxy hxy' => hxy (natDegree_eq_of_degree_eq hxy')

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

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 : ℕ
s : σ✝ →₀ ℕ
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : Unique σ
⊢ LeftInverse (Polynomial.eval₂ C (X default)) (eval₂ Polynomial.C fun x ↦ Polynomial.X)

Tactic:
by

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

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 : ℕ
s : σ✝ →₀ ℕ
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : Unique σ
p : R[X]
a : R
⊢ eval₂ Polynomial.C (fun x ↦ Polynomial.X) (Polynomial.eval₂ C (X default) (Polynomial.C a)) = Polynomial.C a

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
s : Finset S
h : {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Ne on natDegree ∘ f)
⊢ (s.sum f).natDegree = s.sup fun i ↦ (f i).natDegree

Tactic:
by

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

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 : ℕ
s : σ✝ →₀ ℕ
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : Unique σ
p✝ p q : R[X]
hp : eval₂ Polynomial.C (fun x ↦ Polynomial.X) (Polynomial.eval₂ C (X default) p) = p
hq : eval₂ Polynomial.C (fun x ↦ Polynomial.X) (Polynomial.eval₂ C (X default) q) = q
⊢ eval₂ Polynomial.C (fun x ↦ Polynomial.X) (Polynomial.eval₂ C (X default) (p + q)) = p + q

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_2
inst✝² : Ring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x : R
P : R[X]
hx : x ≠ 0
h : P.nextCoeff = 0
hp : ¬P = 0
he : P.eraseLead = 0
he₂ : ¬((X - C x) * P).eraseLead = 0
this : #((X - C x) * P).support ≤ 2
⊢ ((X - C x) * P).eraseLead.eraseLead = 0

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
hp : p ≠ 0
f : R →+* S
z : S
hz : eval₂ f z p = 0
inj : ∀ (x : R), f x = 0 → x = 0
hlt : p.natDegree ≤ 0
⊢ False

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_2
inst✝² : Ring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x : R
P : R[X]
hx : x ≠ 0
h : P.nextCoeff = 0
hp : ¬P = 0
he : P.eraseLead = 0
he₂ : ¬((X - C x) * P).eraseLead = 0
⊢ #(X - C x).support = 2

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ ↑n < p.degree ↔ n < p.natDegree

Tactic:
by

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

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 : ℕ
s : σ✝ →₀ ℕ
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : Unique σ
p✝ : R[X]
p : ℕ
n : R
x✝ :
  eval₂ Polynomial.C (fun x ↦ Polynomial.X) (Polynomial.eval₂ C (X default) (Polynomial.C n * Polynomial.X ^ p)) =
    Polynomial.C n * Polynomial.X ^ p
⊢ eval₂ Polynomial.C (fun x ↦ Polynomial.X) (Polynomial.eval₂ C (X default) (Polynomial.C n * Polynomial.X ^ (p + 1))) =
    Polynomial.C n * Polynomial.X ^ (p + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_2
inst✝² : Ring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x : R
P : R[X]
hx : x ≠ 0
h : P.nextCoeff = 0
hp : ¬P = 0
he : ¬P.eraseLead = 0
⊢ ((X - C x) * P).natDegree = P.natDegree + 1

Tactic:
by

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Unique σ
d : σ →₀ ℕ
r : R
⊢ (uniqueAlgEquiv R σ) ((monomial d) r) = (Polynomial.monomial (d default)) r

Tactic:
by

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Unique σ
d : σ →₀ ℕ
r : R
⊢ (uniqueAlgEquiv R σ).symm ((Polynomial.monomial (d default)) r) = (monomial d) r

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
h : p ≠ 0
h2 : (map f p).degree = p.degree
⊢ (map f p).natDegree = p.natDegree

Tactic:
by

Goal state after: