mathlib-initiative/mathlib-tactics huggingface dataset:
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:
]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ f = f

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
c : R
⊢ (if (C c).natTrailingDegree = 0 then 0 else (C c).coeff ((C c).natTrailingDegree + 1)) = 0

Tactic:
]

Goal state after:
R : Type u
inst✝ : Semiring R
c : R
⊢ (if (C c).natTrailingDegree = 0 then 0 else (C c).coeff ((C c).natTrailingDegree + 1)) = 0
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_2
inst✝ : Ring R
f : R[X]
⊢ f.eraseLead = f.eraseLead

Tactic:
]

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.support.erase f.natDegree) = 0

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : R[X]
f0 : 2 ≤ #f.support
⊢ ¬#(f.support.erase f.natDegree) = 0
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: case inr
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.coeff 0 = 0
hp₀ : p ≠ 0
⊢ p.coeff (p.natTrailingDegree + 1) = p.coeff (p.natTrailingDegree + 1)

Tactic:
]

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.natDegree ∧ a ∈ f.support
⊢ a < f.natDegree

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : R[X]
a : ℕ
h : a ≠ f.natDegree ∧ a ∈ f.support
⊢ a < f.natDegree
Module: Mathlib.Algebra.Polynomial.EraseLead

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

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f ≠ 0
⊢ #(f.support.erase f.natDegree) < #f.support
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
h₁ : p.Monic
h : p = X ^ p.natDegree
a✝ : Nontrivial R
⊢ p.natDegree ≤ p.natDegree

Tactic:
]

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

Goal state before:
pp: case refine_2
R : Type u
inst✝ : Semiring R
p : R[X]
h₁ : p.Monic
h : p.natDegree ≤ p.natTrailingDegree
n : ℕ
⊢ p.coeff n = if n = p.natDegree then 1 else 0

Tactic:
]

Goal state after:
case refine_2
R : Type u
inst✝ : Semiring R
p : R[X]
h₁ : p.Monic
h : p.natDegree ≤ p.natTrailingDegree
n : ℕ
⊢ p.coeff n = if n = p.natDegree then 1 else 0
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f ≠ 0
c : ℕ := #f.support
hc : c = #f.support
n✝ : ℕ
h₁ : c = n✝ + 1
⊢ n✝ + 1 - 1 + 1 = n✝ + 1

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f ≠ 0
c : ℕ := #f.support
hc : c = #f.support
n✝ : ℕ
h₁ : c = n✝ + 1
⊢ n✝ + 1 - 1 + 1 = n✝ + 1
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: case refine_2.inl
R : Type u
inst✝ : Semiring R
p : R[X]
h₁ : p.Monic
h : p.natDegree ≤ p.natTrailingDegree
n : ℕ
hn : n < p.natDegree
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : f = 0
⊢ 0 = 0 - 1

Tactic:
]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : ¬f = 0
⊢ #f.eraseLead.support = #f.eraseLead.support

Tactic:
]

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

Goal state before:
pp: case refine_2.inr.inr
R : Type u
inst✝ : Semiring R
p : R[X]
h₁ : p.Monic
h : p.natDegree ≤ p.natTrailingDegree
n : ℕ
hn : p.natDegree < n
⊢ 0 = 0

Tactic:
]

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

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

Goal state after:
n o n' : ℕ
hn : n ≤ n + n'
o' : ℕ
ho : o ≤ o + o'
⊢ (revAt (n + n' + (o + o'))) (n + o) = n + n' - n + (revAt (o + o')) o
Module: Mathlib.Algebra.Polynomial.Reverse

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

Tactic:
]

Goal state after:
n o n' : ℕ
hn : n ≤ n + n'
o' : ℕ
ho : o ≤ o + o'
⊢ (revAt (n + n' + (o + o'))) (n + o) = n + n' - n + (o + o' - o)
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: n o n' : ℕ
hn : n ≤ n + n'
o' : ℕ
ho : o ≤ o + o'
⊢ n + o + (n' + o') - (n + o) = n + n' - n + (o + o' - o)

Tactic:
]

Goal state after:
n o n' : ℕ
hn : n ≤ n + n'
o' : ℕ
ho : o ≤ o + o'
⊢ n + o + (n' + o') - (n + o) = n + n' - n + (o + o' - o)
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: n o n' : ℕ
hn : n ≤ n + n'
o' : ℕ
ho : o ≤ o + o'
⊢ n' + o' = n + n' - n + (o + o' - o)

Tactic:
]

Goal state after:
n o n' : ℕ
hn : n ≤ n + n'
o' : ℕ
ho : o ≤ o + o'
⊢ n' + o' = n + n' - n + (o + o' - o)
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: n o n' : ℕ
hn : n ≤ n + n'
o' : ℕ
ho : o ≤ o + o'
⊢ n' + o' = n' + (o + o' - o)

Tactic:
]

Goal state after:
n o n' : ℕ
hn : n ≤ n + n'
o' : ℕ
ho : o ≤ o + o'
⊢ n' + o' = n' + (o + o' - o)
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: n o n' : ℕ
hn : n ≤ n + n'
o' : ℕ
ho : o ≤ o + o'
⊢ n' + o' = n' + o'

Tactic:
]

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

Goal state before:
pp: case insert.inr.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)
H : (s.sum f).degree < (f x).degree
⊢ (f x).degree = (f x).degree

Tactic:
]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
i : ℕ
r : R
hr : ¬r = 0
⊢ 0 = 0

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
r : R
n : ℕ
⊢ 0 = 0

Tactic:
]

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) i

Tactic:
]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : q.degree < p.degree
n : ℕ
nd : n = p.natDegree
⊢ 0 = (p.eraseLead + q).coeff p.natDegree

Tactic:
]

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : q.degree < p.degree
n : ℕ
nd : n = p.natDegree
⊢ 0 = (p.eraseLead + q).coeff p.natDegree
Module: Mathlib.Algebra.Polynomial.Reverse

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

Tactic:
]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : q.degree < p.degree
n : ℕ
nd : ¬n = p.natDegree
⊢ p.coeff n + q.coeff n = p.coeff n + q.coeff n

pp: case neg.hnc
R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : q.degree < p.degree
n : ℕ
nd : ¬n = p.natDegree
⊢ ¬n = (p + q).natDegree

Tactic:
]

Goal state after:
case neg.hnc
R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : q.degree < p.degree
n : ℕ
nd : ¬n = p.natDegree
⊢ ¬n = (p + q).natDegree
Module: Mathlib.Algebra.Polynomial.Reverse

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

Tactic:
]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : p.degree < q.degree
n : ℕ
nd : n = q.natDegree
⊢ 0 = (p + q.eraseLead).coeff q.natDegree

Tactic:
]

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : p.degree < q.degree
n : ℕ
nd : n = q.natDegree
⊢ 0 = (p + q.eraseLead).coeff q.natDegree
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)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
⊢ (s.sup fun i ↦ (f i).degree) = ↑(s.sup fun i ↦ (f i).natDegree)

pp: case pos.h
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)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
⊢ {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Ne on degree ∘ f)

Tactic:
]

Goal state after:
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)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
⊢ (s.sup fun i ↦ (f i).degree) = ↑(s.sup fun i ↦ (f i).natDegree)

case pos.h
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)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
⊢ {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Ne on degree ∘ f)
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : p.degree < q.degree
n : ℕ
nd : ¬n = q.natDegree
⊢ p.coeff n + q.coeff n = p.coeff n + q.coeff n

pp: case neg.hnc
R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : p.degree < q.degree
n : ℕ
nd : ¬n = q.natDegree
⊢ ¬n = (p + q).natDegree

Tactic:
]

Goal state after:
case neg.hnc
R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : p.degree < q.degree
n : ℕ
nd : ¬n = q.natDegree
⊢ ¬n = (p + q).natDegree
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
h : (C (f.coeff 0)).eraseLead ≠ 0
h₂ : ¬0 < f.natDegree
⊢ False

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : (C (f.coeff 0)).eraseLead ≠ 0
h₂ : ¬0 < f.natDegree
⊢ False
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : #f.support ≤ 1
⊢ (C f.leadingCoeff * X ^ f.natDegree).eraseLead = 0

Tactic:
]

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : #f.support ≤ 1
⊢ (C f.leadingCoeff * X ^ f.natDegree).eraseLead = 0
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: case zero.zero
R : Type u_1
inst✝ : Semiring R
N O : ℕ
f : R[X]
Cf : #f.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
g : R[X]
Cg : #g.support ≤ Nat.succ 0
Og : g.natDegree ≤ O
⊢ reflect (N + O) (C f.leadingCoeff * X ^ f.natDegree * (C g.leadingCoeff * X ^ g.natDegree)) =
    reflect N (C f.leadingCoeff * X ^ f.natDegree) * reflect O (C g.leadingCoeff * X ^ g.natDegree)

Tactic:
]

Goal state after:
case zero.zero
R : Type u_1
inst✝ : Semiring R
N O : ℕ
f : R[X]
Cf : #f.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
g : R[X]
Cg : #g.support ≤ Nat.succ 0
Og : g.natDegree ≤ O
⊢ reflect (N + O) (C f.leadingCoeff * X ^ f.natDegree * (C g.leadingCoeff * X ^ g.natDegree)) =
    reflect N (C f.leadingCoeff * X ^ f.natDegree) * reflect O (C g.leadingCoeff * X ^ g.natDegree)
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)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
⊢ (s.sup' hs fun i ↦ (f i).degree) = s.sup' hs (WithBot.some ∘ fun i ↦ (f i).natDegree)

Tactic:
]

Goal state after:
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)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
⊢ (s.sup' hs fun i ↦ (f i).degree) = s.sup' hs (WithBot.some ∘ fun i ↦ (f i).natDegree)
Module: Mathlib.Algebra.Polynomial.EraseLead

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

pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
this : 0 < f.natDegree
⊢ 0 < f.natDegree

pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
this : 0 < f.natDegree
⊢ 0 < f.natDegree

pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
this : 0 < f.natDegree
⊢ 0 < 1

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
this : 0 < f.natDegree
⊢ f.nextCoeff ≠ 0

R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
this : 0 < f.natDegree
⊢ 0 < f.natDegree

R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
this : 0 < f.natDegree
⊢ 0 < f.natDegree

R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
this : 0 < f.natDegree
⊢ 0 < 1
Module: Mathlib.Algebra.Polynomial.EraseLead

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

pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
⊢ 1 ≤ f.natDegree

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
⊢ 1 ≤ f.natDegree
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case pos.refine_1
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)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
⊢ ∀ b ∈ s, (f b).degree ≤ s.sup' hs (WithBot.some ∘ fun i ↦ (f i).natDegree)

Tactic:
]

Goal state after:
case pos.refine_1
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)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
⊢ ∀ b ∈ s, (f b).degree ≤ s.sup' hs (WithBot.some ∘ fun i ↦ (f i).natDegree)
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
h : (∃ x, C x = f) ∨ 0 < f.natDegree ∧ f.coeff (f.natDegree - 1) = 0
⊢ f.eraseLead.coeff (f.natDegree - 1) = 0

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : (∃ x, C x = f) ∨ 0 < f.natDegree ∧ f.coeff (f.natDegree - 1) = 0
⊢ f.eraseLead.coeff (f.natDegree - 1) = 0
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case neg
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)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
b : S
hb : b ∈ s
hb' : ¬f b = 0
⊢ ↑(f b).natDegree ≤ s.sup' hs (WithBot.some ∘ fun i ↦ (f i).natDegree)

Tactic:
]

Goal state after:
case neg
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)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
b : S
hb : b ∈ s
hb' : ¬f b = 0
⊢ ↑(f b).natDegree ≤ s.sup' hs (WithBot.some ∘ fun i ↦ (f i).natDegree)
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case inr
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : 0 < f.natDegree
h : f.coeff (f.natDegree - 1) = 0
⊢ f.nextCoeff = 0

Tactic:
]

Goal state after:
case inr
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : 0 < f.natDegree
h : f.coeff (f.natDegree - 1) = 0
⊢ f.nextCoeff = 0
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case pos.refine_2
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)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
⊢ ∀ b ∈ s, (WithBot.some ∘ fun i ↦ (f i).natDegree) b ≤ s.sup' hs fun i ↦ (f i).degree

Tactic:
]

Goal state after:
case pos.refine_2
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)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
⊢ ∀ b ∈ s, (WithBot.some ∘ fun i ↦ (f i).natDegree) b ≤ s.sup' hs fun i ↦ (f i).degree
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
hnext : f.nextCoeff = 0
hlead : (∃ x, C x = f) ∨ ∃ a, a ≠ 0 ∧ ∃ b, C a * X + C b = f
⊢ f.eraseLead = 0

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : R[X]
hnext : f.nextCoeff = 0
hlead : (∃ x, C x = f) ∨ ∃ a, a ≠ 0 ∧ ∃ b, C a * X + C b = f
⊢ f.eraseLead = 0
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
N O : ℕ
f : R[X]
Cf : #f.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
cg : ℕ
hcg : ∀ (g : R[X]), #g.support ≤ cg.succ → g.natDegree ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
g : R[X]
Cg : #g.support ≤ (cg + 1).succ
Og : g.natDegree ≤ O
g0 : g = 0
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case inr
R : Type u_1
inst✝ : Semiring R
a : R
ha : a ≠ 0
b : R
hnext : b = 0
⊢ (C a * X + C b).eraseLead = 0

Tactic:
]

Goal state after:
case inr
R : Type u_1
inst✝ : Semiring R
a : R
ha : a ≠ 0
b : R
hnext : b = 0
⊢ (C a * X + C b).eraseLead = 0
Module: Mathlib.Algebra.Polynomial.EraseLead

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

pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
this : 0 < f.natDegree
⊢ 0 < f.natDegree

pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
this : 0 < f.natDegree
⊢ 0 < 1

pp: case hnc
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
this : 0 < f.natDegree
⊢ ¬f.natDegree = 0

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
this : 0 < f.natDegree
⊢ 0 < f.natDegree

R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
this : 0 < f.natDegree
⊢ 0 < 1

case hnc
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
this : 0 < f.natDegree
⊢ ¬f.natDegree = 0
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case hC
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 σ
f : R[X] →+* MvPolynomial σ R := eval₂RingHom C (X default)
g : MvPolynomial σ R →+* R[X] := eval₂Hom Polynomial.C fun x ↦ Polynomial.X
a : R
m✝ : σ →₀ ℕ
⊢ coeff m✝ (C a) = coeff m✝ (C a)

Tactic:
]

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

Goal state before:
pp: case hX
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 σ
f : R[X] →+* MvPolynomial σ R := eval₂RingHom C (X default)
g : MvPolynomial σ R →+* R[X] := eval₂Hom Polynomial.C fun x ↦ Polynomial.X
i : σ
⊢ X default = X i

Tactic:
]

Goal state after:
case hX
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 σ
f : R[X] →+* MvPolynomial σ R := eval₂RingHom C (X default)
g : MvPolynomial σ R →+* R[X] := eval₂Hom Polynomial.C fun x ↦ Polynomial.X
i : σ
⊢ X default = X i
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case pos
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).eraseLead.eraseLead = 0

Tactic:
]

Goal state after:
case pos
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).eraseLead.eraseLead = 0
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case hX
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 σ
f : R[X] →+* MvPolynomial σ R := eval₂RingHom C (X default)
g : MvPolynomial σ R →+* R[X] := eval₂Hom Polynomial.C fun x ↦ Polynomial.X
i : σ
⊢ X i = X i

Tactic:
]

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

Goal state before:
pp: case neg
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_1 ∈ s, (f s_1).natDegree = ⊥

Tactic:
]

Goal state after:
case neg
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_1 ∈ s, (f s_1).natDegree = ⊥
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
⊢ Polynomial.C a = Polynomial.C a

Tactic:
]

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.support = 0

Tactic:
]

Goal state after:
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.support = 0
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
⊢ p + q = p + q

Tactic:
]

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 : f (p.coeff 0) = 0
inj : ∀ (x : R), f x = 0 → x = 0
hlt : p.natDegree ≤ 0
A : p = C (p.coeff 0)
⊢ False

Tactic:
]

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
hp : p ≠ 0
f : R →+* S
z : S
hz : f (p.coeff 0) = 0
inj : ∀ (x : R), f x = 0 → x = 0
hlt : p.natDegree ≤ 0
A : p = C (p.coeff 0)
⊢ False
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case neg
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
h₂ : #(X - C x).support = 2
hmul : #((X - C x) * P).support ≤ 2 * #P.support
⊢ #((X - C x) * P).support ≤ 2

Tactic:
]

Goal state after:
case neg
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
h₂ : #(X - C x).support = 2
hmul : #((X - C x) * P).support ≤ 2 * #P.support
⊢ #((X - C x) * P).support ≤ 2
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
⊢ Polynomial.C n * Polynomial.X ^ (p + 1) = Polynomial.C n * Polynomial.X ^ (p + 1)

Tactic:
]

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
⊢ P.natDegree + 1 = P.natDegree + 1

Tactic:
]

Goal state after: