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

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
ha : IsUnit a
p : R[X]
hp : p ≠ 0
a✝ : Nontrivial R
⊢ 0 + p.degree = p.degree

pp: R : Type u
a : R
inst✝ : Semiring R
ha : IsUnit a
p : R[X]
hp : p ≠ 0
a✝ : Nontrivial R
⊢ (C a).leadingCoeff * p.leadingCoeff ≠ 0

Tactic:
]

Goal state after:
R : Type u
a : R
inst✝ : Semiring R
ha : IsUnit a
p : R[X]
hp : p ≠ 0
a✝ : Nontrivial R
⊢ 0 + p.degree = p.degree

R : Type u
a : R
inst✝ : Semiring R
ha : IsUnit a
p : R[X]
hp : p ≠ 0
a✝ : Nontrivial R
⊢ (C a).leadingCoeff * p.leadingCoeff ≠ 0
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
ha : IsUnit a
p : R[X]
hp : p ≠ 0
a✝ : Nontrivial R
⊢ p.degree + 0 = p.degree

pp: R : Type u
a : R
inst✝ : Semiring R
ha : IsUnit a
p : R[X]
hp : p ≠ 0
a✝ : Nontrivial R
⊢ p.leadingCoeff * (C a).leadingCoeff ≠ 0

Tactic:
]

Goal state after:
R : Type u
a : R
inst✝ : Semiring R
ha : IsUnit a
p : R[X]
hp : p ≠ 0
a✝ : Nontrivial R
⊢ p.degree + 0 = p.degree

R : Type u
a : R
inst✝ : Semiring R
ha : IsUnit a
p : R[X]
hp : p ≠ 0
a✝ : Nontrivial R
⊢ p.leadingCoeff * (C a).leadingCoeff ≠ 0
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case neg.refine_1
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
i : ι
f : ι → R[A]
inst✝ : AddZeroClass A
hi : i ∈ s
hmax : ∀ j ∈ s, j ≠ i → supDegree D (f j) < supDegree D (f i)
hs : (s.erase i).Nonempty
⊢ (s.erase i).Nonempty

Tactic:
exact hs

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

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

Tactic:
]

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
h : p.degree = ↑1
⊢ C (p.coeff 1) * X + C (p.coeff 0) = C p.leadingCoeff * X + C (p.coeff 0)
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case neg.refine_2
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
i : ι
f : ι → R[A]
inst✝ : AddZeroClass A
hi : i ∈ s
hmax : ∀ j ∈ s, j ≠ i → supDegree D (f j) < supDegree D (f i)
hs : (s.erase i).Nonempty
j : ι
hj : j ≠ i ∧ j ∈ s
⊢ supDegree D (f j) < supDegree D (f i)

Tactic:
]

Goal state after:
case neg.refine_2
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
i : ι
f : ι → R[A]
inst✝ : AddZeroClass A
hi : i ∈ s
hmax : ∀ j ∈ s, j ≠ i → supDegree D (f j) < supDegree D (f i)
hs : (s.erase i).Nonempty
j : ι
hj : j ≠ i ∧ j ∈ s
⊢ supDegree D (f j) < supDegree D (f i)
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
ha : IsUnit a
p : R[X]
⊢ a * p.coeff p.natDegree = a * p.coeff p.natDegree

pp: case ha
R : Type u
a : R
inst✝ : Semiring R
ha : IsUnit a
p : R[X]
⊢ IsUnit a

Tactic:
]

Goal state after:
case ha
R : Type u
a : R
inst✝ : Semiring R
ha : IsUnit a
p : R[X]
⊢ IsUnit a
Module: Mathlib.Algebra.Polynomial.Degree.SmallDegree

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

Tactic:
]

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

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
ha : IsUnit a
p : R[X]
⊢ p.coeff p.natDegree * a = p.coeff p.natDegree * a

pp: case ha
R : Type u
a : R
inst✝ : Semiring R
ha : IsUnit a
p : R[X]
⊢ IsUnit a

Tactic:
]

Goal state after:
case ha
R : Type u
a : R
inst✝ : Semiring R
ha : IsUnit a
p : R[X]
⊢ IsUnit a
Module: Mathlib.Algebra.Polynomial.Degree.SmallDegree

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hm : p.Monic
hnd : p.natDegree = 1
⊢ p = p

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

Goal state after:
R : Type u
n : ℕ
inst✝ : Semiring R
p : R[X]
hdeg : ↑n ≤ ↑p.natDegree
⊢ ↑n ≤ ↑p.natDegree
Module: Mathlib.Algebra.Polynomial.Degree.SmallDegree

Goal state before:
pp: R : Type u
a b : R
inst✝ : Semiring R
ha : a ≠ 0
⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p : R[X]
h : IsUnit p
a✝ : Nontrivial R
q : R[X]
hq : p * q = 1
this : p.natDegree = 0 ∧ q.natDegree = 0
⊢ p.natDegree = 0

Tactic:
]

Goal state after:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p : R[X]
h : IsUnit p
a✝ : Nontrivial R
q : R[X]
hq : p * q = 1
this : p.natDegree = 0 ∧ q.natDegree = 0
⊢ p.natDegree = 0
Module: Mathlib.Algebra.Polynomial.Degree.SmallDegree

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

Tactic:
]

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

Goal state before:
pp: case succ
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
⊢ (p ^ i * p).coeff (i * p.natDegree + p.natDegree) = p.leadingCoeff ^ i * p.leadingCoeff

Tactic:
]

Goal state after:
case succ
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
⊢ (p ^ i * p).coeff (i * p.natDegree + p.natDegree) = p.leadingCoeff ^ i * p.leadingCoeff
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case pos
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
f : ι → R[A]
inst✝ : AddZeroClass A
hd : Set.InjOn (supDegree D ∘ f) ↑s
j : ι
hj : j ∈ s
hne✝ : f j ≠ 0
i : ι
hi : i ∈ s
he : s.sup (supDegree D ∘ f) = (supDegree D ∘ f) i
h : ∀ k ∈ s, k = i
k : ι
hk : k ∈ s
hne : i ≠ i
⊢ f k = 0

Tactic:
]

Goal state after:
case pos
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
f : ι → R[A]
inst✝ : AddZeroClass A
hd : Set.InjOn (supDegree D ∘ f) ↑s
j : ι
hj : j ∈ s
hne✝ : f j ≠ 0
i : ι
hi : i ∈ s
he : s.sup (supDegree D ∘ f) = (supDegree D ∘ f) i
h : ∀ k ∈ s, k = i
k : ι
hk : k ∈ s
hne : i ≠ i
⊢ f k = 0
Module: Mathlib.Algebra.Polynomial.Degree.SmallDegree

Goal state before:
pp: R : Type u
a b c : R
inst✝ : Semiring R
ha : a ≠ 0
⊢ ↑2 = 2

Tactic:
]

Goal state after:
R : Type u
a b c : R
inst✝ : Semiring R
ha : a ≠ 0
⊢ ↑2 = 2
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
hp1 : p.leadingCoeff ^ i = 0
⊢ (p ^ i * p).coeff (i * p.natDegree + p.natDegree) = 0

Tactic:
]

Goal state after:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
hp1 : p.leadingCoeff ^ i = 0
⊢ (p ^ i * p).coeff (i * p.natDegree + p.natDegree) = 0
Module: Mathlib.Algebra.Polynomial.Degree.Units

Goal state before:
pp: R : Type u
inst✝² : Semiring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
u : R[X]ˣ
⊢ ¬↑u = 0

Tactic:
]

Goal state after:
R : Type u
inst✝² : Semiring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
u : R[X]ˣ
⊢ ¬↑u = 0
Module: Mathlib.Algebra.Polynomial.Degree.SmallDegree

Goal state before:
pp: R : Type u
a b c : R
inst✝ : Semiring R
ha : a ≠ 0
⊢ a = a

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
a p : R[X]
hp : p.Monic
hap : C (a.coeff 0) ∣ p
h : a.degree ≤ 0
⊢ IsUnit (C (a.coeff 0))

Tactic:
]

Goal state after:
R : Type u
inst✝ : CommSemiring R
a p : R[X]
hp : p.Monic
hap : C (a.coeff 0) ∣ p
h : a.degree ≤ 0
⊢ IsUnit (C (a.coeff 0))
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case neg
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
f : ι → R[A]
inst✝ : AddZeroClass A
hd : Set.InjOn (supDegree D ∘ f) ↑s
j✝ : ι
hj✝ : j✝ ∈ s
hne✝ : f j✝ ≠ 0
i : ι
hi : i ∈ s
he : s.sup (supDegree D ∘ f) = (supDegree D ∘ f) i
j : ι
hj : j ∈ s
hne : j ≠ i
this : ∀ k ∈ s, k ≠ i → supDegree D (f k) < supDegree D (f i)
⊢ supDegree D (f i) ≠ ⊥

Tactic:
]

Goal state after:
case neg
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
f : ι → R[A]
inst✝ : AddZeroClass A
hd : Set.InjOn (supDegree D ∘ f) ↑s
j✝ : ι
hj✝ : j✝ ∈ s
hne✝ : f j✝ ≠ 0
i : ι
hi : i ∈ s
he : s.sup (supDegree D ∘ f) = (supDegree D ∘ f) i
j : ι
hj : j ∈ s
hne : j ≠ i
this : ∀ k ∈ s, k ≠ i → supDegree D (f k) < supDegree D (f i)
⊢ supDegree D (f i) ≠ ⊥
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
hp1 : p.leadingCoeff ^ i = 0
hp2 : p ^ i = 0
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: R : Type u
a b c d : R
inst✝ : Semiring R
ha : a ≠ 0
⊢ ↑3 = 3

Tactic:
]

Goal state after:
R : Type u
a b c d : R
inst✝ : Semiring R
ha : a ≠ 0
⊢ ↑3 = 3
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (p ^ i).natDegree = 0
hp1 : p.leadingCoeff ^ i = 0
hp2 : ¬p ^ i = 0
h : (p ^ i).natDegree = i * p.natDegree
⊢ p ^ i = 0

Tactic:
]

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (p ^ i).natDegree = 0
hp1 : p.leadingCoeff ^ i = 0
hp2 : ¬p ^ i = 0
h : (p ^ i).natDegree = i * p.natDegree
⊢ p ^ i = 0
Module: Mathlib.Algebra.Polynomial.Degree.SmallDegree

Goal state before:
pp: R : Type u
a b c d : R
inst✝ : Semiring R
ha : a ≠ 0
⊢ a = a

Tactic:
]

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

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
hp1 : ¬p.leadingCoeff ^ i = 0
⊢ (p ^ i * p).coeff ((p ^ i).natDegree + p.natDegree) = (p ^ i).leadingCoeff * p.leadingCoeff

Tactic:
]

Goal state after:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
hp1 : ¬p.leadingCoeff ^ i = 0
⊢ (p ^ i * p).coeff ((p ^ i).natDegree + p.natDegree) = (p ^ i).leadingCoeff * p.leadingCoeff
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝ : Semiring R
df dg : ℕ
f g : R[X]
hdf : f.natDegree ≤ df
hdg : g.natDegree ≤ dg
⊢ f.coeff (df, dg).1 * g.coeff (df, dg).2 = f.coeff df * g.coeff dg

pp: case h
R : Type u
inst✝ : Semiring R
df dg : ℕ
f g : R[X]
hdf : f.natDegree ≤ df
hdg : g.natDegree ≤ dg
⊢ (df, dg) ∈ antidiagonal (df + dg)

pp: case h₀
R : Type u
inst✝ : Semiring R
df dg : ℕ
f g : R[X]
hdf : f.natDegree ≤ df
hdg : g.natDegree ≤ dg
⊢ ∀ b ∈ antidiagonal (df + dg), b ≠ (df, dg) → f.coeff b.1 * g.coeff b.2 = 0

Tactic:
]

Goal state after:
case h
R : Type u
inst✝ : Semiring R
df dg : ℕ
f g : R[X]
hdf : f.natDegree ≤ df
hdg : g.natDegree ≤ dg
⊢ (df, dg) ∈ antidiagonal (df + dg)

case h₀
R : Type u
inst✝ : Semiring R
df dg : ℕ
f g : R[X]
hdf : f.natDegree ≤ df
hdg : g.natDegree ≤ dg
⊢ ∀ b ∈ antidiagonal (df + dg), b ≠ (df, dg) → f.coeff b.1 * g.coeff b.2 = 0
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: case h
R : Type u
inst✝ : Semiring R
df dg : ℕ
f g : R[X]
hdf : f.natDegree ≤ df
hdg : g.natDegree ≤ dg
⊢ (df, dg).1 + (df, dg).2 = df + dg

Tactic:
]

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

Goal state before:
pp: case h₀.inl
R : Type u
inst✝ : Semiring R
df dg : ℕ
f g : R[X]
hdf : f.natDegree ≤ df
hdg : g.natDegree ≤ dg
df' dg' : ℕ
hmem : (df', dg') ∈ antidiagonal (df + dg)
hne : (df', dg') ≠ (df, dg)
h : df < df'
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case h₀.inr.inl
R : Type u
inst✝ : Semiring R
df dg : ℕ
f g : R[X]
hdf : f.natDegree ≤ df
hdg : g.natDegree ≤ dg
df' dg' : ℕ
hmem : (df', dg') ∈ antidiagonal (df + dg)
hne : (df', dg') ≠ (df, dg)
hdf' : df' ≤ df
h : dg < dg'
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case hb
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder B
inst✝⁴ : OrderBot B
p q : R[A]
D : A → B
inst✝³ : AddZeroClass A
inst✝² : Add B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hpq : leadingCoeff D p * leadingCoeff D q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ supDegree D p + supDegree D q ∈ { toFun := D, map_add' := hadd }.srange

pp: case hb
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder B
inst✝⁴ : OrderBot B
p q : R[A]
D : A → B
inst✝³ : AddZeroClass A
inst✝² : Add B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hpq : leadingCoeff D p * leadingCoeff D q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ ∀ {a b : B}, a ∈ Set.range D → b ∈ Set.range D → a + b ∈ Set.range D

Tactic:
]

Goal state after:
case hb
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder B
inst✝⁴ : OrderBot B
p q : R[A]
D : A → B
inst✝³ : AddZeroClass A
inst✝² : Add B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hpq : leadingCoeff D p * leadingCoeff D q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ supDegree D p + supDegree D q ∈ { toFun := D, map_add' := hadd }.srange

case hb
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder B
inst✝⁴ : OrderBot B
p q : R[A]
D : A → B
inst✝³ : AddZeroClass A
inst✝² : Add B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hpq : leadingCoeff D p * leadingCoeff D q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ ∀ {a b : B}, a ∈ Set.range D → b ∈ Set.range D → a + b ∈ Set.range D
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
S : Type u_2
inst✝ : SMulZeroClass S R
a : S
p : R[X]
m : ℕ
hm : ∀ (m_1 : ℕ), m ≤ m_1 → p.coeff m_1 = 0
⊢ (a • p).coeff m = 0

Tactic:
]

Goal state after:
R : Type u
inst✝¹ : Semiring R
S : Type u_2
inst✝ : SMulZeroClass S R
a : S
p : R[X]
m : ℕ
hm : ∀ (m_1 : ℕ), m ≤ m_1 → p.coeff m_1 = 0
⊢ (a • p).coeff m = 0
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
p : R[X]
ha : a ≠ 0
hp : IsRightRegular p.leadingCoeff
⊢ ¬a * p.leadingCoeff = 0

Tactic:
]

Goal state after:
R : Type u
a : R
inst✝ : Semiring R
p : R[X]
ha : a ≠ 0
hp : IsRightRegular p.leadingCoeff
⊢ ¬a * p.leadingCoeff = 0
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
this✝ : Nontrivial R
this : p.leadingCoeff * X.leadingCoeff ≠ 0
⊢ ↑p.natDegree < ↑(p.natDegree + 1)

Tactic:
]

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
this✝ : Nontrivial R
this : p.leadingCoeff * X.leadingCoeff ≠ 0
⊢ ↑p.natDegree < ↑(p.natDegree + 1)
Module: Mathlib.Algebra.Polynomial.Degree.Operations

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

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hf : p.coeff 0 = 1
hfd : p.natDegree = 0
⊢ p = 1

Tactic:
]

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
hf : p.coeff 0 = 1
hfd : p.natDegree = 0
⊢ p = 1
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hf : p.coeff 0 = 1
hfd : p.natDegree = 0
⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
p : R[X]
hp : p ≠ 0
⊢ p.natDegree + 1 = p.natDegree + 1

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
p : R[X]
n : ℕ
hp : p ≠ 0
⊢ p.natDegree + n = p.natDegree + n

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
a✝ : Nontrivial R
⊢ n ≤ n

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
x✝ : IsUnit X
g : R[X]
_hfg : (monomial 1) 1 * g = 1
hgf : g * (monomial 1) 1 = 1
⊢ 0 = (g * (monomial 1) 1).coeff 0

Tactic:
]

Goal state after:
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
x✝ : IsUnit X
g : R[X]
_hfg : (monomial 1) 1 * g = 1
hgf : g * (monomial 1) 1 = 1
⊢ 0 = (g * (monomial 1) 1).coeff 0
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
a : R
inst✝ : Ring R
p : R[X]
hp : 0 < p.degree
⊢ p.degree = p.degree

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
a : R
⊢ p.natDegree = p.natDegree

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
h : (-q).degree < p.degree
⊢ (p - q).leadingCoeff = p.leadingCoeff

Tactic:
]

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
h : (-q).degree < p.degree
⊢ (p - q).leadingCoeff = p.leadingCoeff
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
h : (-q).degree < p.degree
⊢ p.leadingCoeff = p.leadingCoeff

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
h : p.degree < (-q).degree
⊢ (p - q).leadingCoeff = -q.leadingCoeff

Tactic:
]

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
h : p.degree < (-q).degree
⊢ (p - q).leadingCoeff = -q.leadingCoeff
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
h : p.degree < (-q).degree
⊢ -q.leadingCoeff = -q.leadingCoeff

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
h : p.degree = q.degree
hlc : p.leadingCoeff ≠ q.leadingCoeff
⊢ p.degree = q.degree

Tactic:
]

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
h : p.degree = q.degree
hlc : p.leadingCoeff ≠ q.leadingCoeff
⊢ p.degree = q.degree
Module: Mathlib.Algebra.Polynomial.Eval.Coeff

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
x : R
⊢ x • X ^ n = x • X ^ n

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hlc : p.leadingCoeff + (-q).leadingCoeff ≠ 0
h : p.degree = (-q).degree
⊢ p.leadingCoeff + (-q).leadingCoeff ≠ 0

Tactic:
]

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
hlc : p.leadingCoeff + (-q).leadingCoeff ≠ 0
h : p.degree = (-q).degree
⊢ p.leadingCoeff + (-q).leadingCoeff ≠ 0
Module: Mathlib.Algebra.Polynomial.Eval.Coeff

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ (p.sum fun e a ↦ a * 0 ^ e) = p.coeff 0 * 0 ^ 0

Tactic:
]

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ (p.sum fun e a ↦ a * 0 ^ e) = p.coeff 0 * 0 ^ 0
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
h : p.degree = (-q).degree
hlc : p.leadingCoeff + (-q).leadingCoeff ≠ 0
⊢ p.leadingCoeff + -q.leadingCoeff = p.leadingCoeff + -q.leadingCoeff

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Eval.Coeff

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

Tactic:
]

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

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

Tactic:
]

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
h : (-q).degree < p.degree
⊢ (p - q).degree = p.degree
Module: Mathlib.Algebra.Polynomial.Degree.Operations

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

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Eval.Coeff

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
n : ℕ
⊢ ∑ n_1 ∈ p.support, ((C.comp f) (p.coeff n_1) * X ^ n_1).coeff n = f (p.coeff n)

Tactic:
]

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
n : ℕ
⊢ ∑ n_1 ∈ p.support, ((C.comp f) (p.coeff n_1) * X ^ n_1).coeff n = f (p.coeff n)
Module: Mathlib.Algebra.Polynomial.Degree.Operations

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

Tactic:
]

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
h : p.degree < (-q).degree
⊢ (p - q).degree = q.degree
Module: Mathlib.Algebra.Polynomial.Degree.Operations

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

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝¹ : Nontrivial R
inst✝ : Semiring R
a : R
this : (C a).degree < X.degree
⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝¹ : Nontrivial R
inst✝ : Semiring R
n : ℕ
hn : 0 < n
a : R
⊢ 0 < n

Tactic:
]

Goal state after:
R : Type u
inst✝¹ : Nontrivial R
inst✝ : Semiring R
n : ℕ
hn : 0 < n
a : R
⊢ 0 < n
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Nontrivial R
inst✝ : Semiring R
n : ℕ
hn : 0 < n
a : R
this : (C a).degree < (X ^ n).degree
⊢ ↑n = ↑n

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder B
inst✝⁴ : OrderBot B
p q : R[A]
D : A → B
inst✝³ : AddZeroClass A
inst✝² : Add B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hp : Monic D p
hq : q ≠ 0
⊢ supDegree D (p * q) = supDegree D p + supDegree D q

Tactic:
by
  cases subsingleton_or_nontrivial R; · exact (hq (Subsingleton.elim _ _)).elim
  apply supDegree_mul hD hadd ?_ hp.ne_zero hq
  simp_rw [hp, one_mul, Ne, leadingCoeff_eq_zero hD, hq, not_false_eq_true]

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

Goal state before:
pp: R : Type u
inst✝¹ : Nontrivial R
inst✝ : Semiring R
n : ℕ
hn : 0 < n
a : R
⊢ ↑n ≠ ⊥

Tactic:
]

Goal state after:
R : Type u
inst✝¹ : Nontrivial R
inst✝ : Semiring R
n : ℕ
hn : 0 < n
a : R
⊢ ↑n ≠ ⊥
Module: Mathlib.Algebra.Polynomial.Eval.Coeff

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Function.Injective ⇑f
p q : R[X]
h : map f p = map f q
m : ℕ
⊢ (map f q).coeff m = (map f q).coeff m

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
hn : 0 < n
r : R
a✝ : Nontrivial R
⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: S : Type v
inst✝ : Semiring S
r : S
⊢ 1 = 1

Tactic:
]

Goal state after: