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]
⊢ (p * C a).degree = p.degree

Tactic:
by

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

Tactic:
by

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 * C a).natDegree = p.natDegree

Tactic:
by

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:
rw [leadingCoeff, natDegree_eq_of_degree_eq_some h]

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]
⊢ (C a * p).leadingCoeff = a * p.leadingCoeff

Tactic:
by

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

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
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)
⊢ supDegree D (∑ j ∈ s, f j) = supDegree D (f i) ∧ leadingCoeff D (∑ j ∈ s, f j) = leadingCoeff D (f i)

Tactic:
classical
  rw [← s.add_sum_erase _ hi]
  by_cases! hs : s.erase i = ∅
  · rw [hs, Finset.sum_empty, add_zero]; exact ⟨rfl, rfl⟩
  suffices _ from ⟨supDegree_add_eq_left this, leadingCoeff_add_eq_left this⟩
  refine supDegree_sum_lt ?_ (fun j hj => ?_)
  · exact hs
  · rw [Finset.mem_erase] at hj; exact hmax j hj.2 hj.1

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
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)
⊢ supDegree D (∑ j ∈ s, f j) = supDegree D (f i) ∧ leadingCoeff D (∑ j ∈ s, f j) = leadingCoeff D (f i)

Tactic:
by

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 * C a).leadingCoeff = p.leadingCoeff * a

Tactic:
by

Goal state after:
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 = X + C (p.coeff 0)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ 0 ≤ p.degree ↔ p ≠ 0

Tactic:
by

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.degree
⊢ ↑n ≤ ↑p.natDegree

Tactic:
by

Goal state after:
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
⊢ ∑ i ∈ s, f i ≠ 0

Tactic:
refine (sum_eq_single_of_mem j hj (fun k hk hne => ?_)).trans_ne hne

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 : k ≠ j
⊢ f k = 0
Module: Mathlib.Algebra.Polynomial.Degree.SmallDegree

Goal state before:
pp: R : Type u
a b : R
inst✝ : Semiring R
ha : a ≠ 0
⊢ (C a * X + C b).degree = 1

Tactic:
by

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

Goal state before:
pp: R : Type u
a b : R
inst✝ : Semiring R
ha : a ≠ 0
⊢ (C a * X + C b).natDegree = 1

Tactic:
by

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
⊢ p.natDegree = 0

Tactic:
by

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

Goal state before:
pp: R : Type u
a b : R
inst✝ : Semiring R
ha : a ≠ 0
⊢ (C a * X + C b).leadingCoeff = a

Tactic:
by

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

Goal state before:
pp: R : Type u
a b c : R
inst✝ : Semiring R
⊢ (C a * X ^ 2 + C b * X + C c).degree ≤ 2

Tactic:
by

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

Goal state before:
pp: R : Type u
a b c : R
inst✝ : Semiring R
ha : a ≠ 0
⊢ (C b * X + C c).degree < (C a * X ^ 2).degree

Tactic:
by

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]
hpl : 0 < p.degree
⊢ ¬IsUnit p

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
u : R[X]ˣ
⊢ (↑u).natDegree = 0

Tactic:
by

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

Goal state before:
pp: R : Type u
a b c : R
inst✝ : Semiring R
ha : a ≠ 0
⊢ (C a * X ^ 2 + C b * X + C c).degree = 2

Tactic:
by

Goal state after:
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).coeff 0 ≠ 0

Tactic:
by

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

Goal state before:
pp: R : Type u
a b c : R
inst✝ : Semiring R
ha : a ≠ 0
⊢ (C a * X ^ 2 + C b * X + C c).leadingCoeff = a

Tactic:
by

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

Goal state before:
pp: R : Type u
a b c d : R
inst✝ : Semiring R
⊢ (C a * X ^ 3 + C b * X ^ 2 + C c * X + C d).degree ≤ 3

Tactic:
by

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
ha : ¬IsUnit a
hap : a ∣ p
⊢ 0 < a.degree

Tactic:
by

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
⊢ (C b * X ^ 2 + C c * X + C d).degree < (C a * X ^ 3).degree

Tactic:
by

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
D : A → B
ι : Type u_7
s : Finset ι
f : ι → R[A]
inst✝ : AddZeroClass A
hs : ∃ i ∈ s, f i ≠ 0
hd : Set.InjOn (supDegree D ∘ f) ↑s
⊢ ∑ i ∈ s, f i ≠ 0

Tactic:
by

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
⊢ (C a * X ^ 3 + C b * X ^ 2 + C c * X + C d).degree = 3

Tactic:
by

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

Goal state before:
pp: 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
⊢ (p ^ i).natDegree < i * p.natDegree

Tactic:
by

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
⊢ (C a * X ^ 3 + C b * X ^ 2 + C c * X + C d).leadingCoeff = a

Tactic:
by

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

Goal state before:
pp: 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
h1 : (p ^ i).natDegree < i * p.natDegree
⊢ (p ^ i).natDegree + p.natDegree < i * p.natDegree + p.natDegree

Tactic:
by

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

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

Tactic:
by

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
⊢ (p * q).coeff (Function.invFun D (supDegree D p + supDegree D q)) = leadingCoeff D p * leadingCoeff D q

Tactic:
by

Goal state after:
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 * g).coeff (df + dg) = f.coeff df * g.coeff dg

Tactic:
by

Goal state after:
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]
⊢ (a • p).degree ≤ p.degree

Tactic:
by

Goal state after:
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).degree = p.degree

Tactic:
by

Goal state after:
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
⊢ p.leadingCoeff * X.leadingCoeff ≠ 0

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
⊢ p.degree < (p * X).degree

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ (∃ x, C x = p) → p.natDegree = 0

Tactic:
by

Goal state after:
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)
⊢ p.natDegree = 0

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: R : Type u
a b : R
inst✝ : Semiring R
ha : a ≠ 0
⊢ (C b).degree < (C a * X).degree

Tactic:
by

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.leadingCoeff * X.leadingCoeff ≠ 0

Tactic:
by

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 * X).natDegree = p.natDegree + 1

Tactic:
by

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
⊢ (X * p).natDegree = p.natDegree + 1

Tactic:
by

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.leadingCoeff * (X ^ n).leadingCoeff ≠ 0

Tactic:
by

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 * X ^ n).natDegree = p.natDegree + n

Tactic:
by

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

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
⊢ (X ^ n).natDegree ≤ n

Tactic:
by

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 = 1

Tactic:
by

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]
⊢ (p * X).degree = p.degree + 1

Tactic:
by

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

Tactic:
by

Goal state after:
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 - C a).degree = p.degree

Tactic:
by

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 - C a).natDegree = p.natDegree

Tactic:
by

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

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
⊢ eval₂ f 0 p = f (p.coeff 0)

Tactic:
by

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

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p✝ p q : R[X]
hp : eval₂ C X p = p
hq : eval₂ C X q = q
⊢ eval₂ C X (p + q) = p + q

Tactic:
by

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

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
x : R
⊢ eval₂ C X ((monomial n) x) = (monomial n) x

Tactic:
by

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

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

Tactic:
by

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
h : p.degree = (-q).degree
⊢ p.leadingCoeff + (-q).leadingCoeff ≠ 0

Tactic:
by

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
hpq : leadingCoeff D p * leadingCoeff D q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ supDegree D (p * q) = supDegree D p + supDegree D q

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
b : ℕ
x✝ : b ∈ p.support
hb : b ≠ 0
⊢ (fun e a ↦ a * 0 ^ e) b (p.coeff b) = 0

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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 - q).leadingCoeff = p.leadingCoeff - q.leadingCoeff

Tactic:
by

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

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 : ℕ
⊢ (map f p).coeff n = f (p.coeff n)

Tactic:
by

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
hq : Monic D q
hp : p ≠ 0
⊢ supDegree D (p * q) = supDegree D p + supDegree D q

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
⊢ (map f p).coeff = ⇑f ∘ p.coeff

Tactic:
by

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).degree = q.degree

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
T : Type w
inst✝² : Semiring R
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Semiring T
g : S →+* T
p : R[X]
⊢ ∀ (n : ℕ), (map g (map f p)).coeff n = (map (g.comp f) p).coeff n

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ map (RingHom.id R) p = p

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: S : Type v
inst✝ : Semiring S
c : S
⊢ (X + C c).nextCoeff = c

Tactic:
by

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 < (X ^ n).degree

Tactic:
by

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

Goal state before:
pp: R✝ : Type u
S : Type v
T : Type w
ι✝ : Type y
a b : R✝
m n : ℕ
inst✝³ : Semiring R✝
p✝ q✝ r : R✝[X]
inst✝² : Semiring S
f : R✝ →+* S
ι : Type ?u.38
inst✝¹ : Finite ι
R : ι → Type u_1
inst✝ : (i : ι) → Semiring (R i)
p q : ((i : ι) → R i)[X]
h : (RingHom.pi fun i ↦ mapRingHom (Pi.evalRingHom R i)) p = (RingHom.pi fun i ↦ mapRingHom (Pi.evalRingHom R i)) q
⊢ p = q

Tactic:
by

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

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
⊢ (X ^ n + C a).degree = ↑n

Tactic:
by

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

Goal state before:
pp: R✝ : Type u
S : Type v
T : Type w
ι✝ : Type y
a b : R✝
m n✝ : ℕ
inst✝³ : Semiring R✝
p✝ q r : R✝[X]
inst✝² : Semiring S
f : R✝ →+* S
ι : Type ?u.38
inst✝¹ : Finite ι
R : ι → Type u_1
inst✝ : (i : ι) → Semiring (R i)
p : (i : ι) → (R i)[X]
n : ℕ
hn : n ∈ Function.support fun n i ↦ (p i).coeff n
⊢ n ∈ ⋃ i, ↑(p i).support

Tactic:
by

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

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

Tactic:
by

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
h : X ^ n + C a = 1
⊢ n = 0

Tactic:
by

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

Goal state before:
pp: R✝ : Type u
S : Type v
T : Type w
ι✝ : Type y
a b : R✝
m n : ℕ
inst✝³ : Semiring R✝
p✝ q r : R✝[X]
inst✝² : Semiring S
f : R✝ →+* S
ι : Type ?u.38
inst✝¹ : Finite ι
R : ι → Type u_1
inst✝ : (i : ι) → Semiring (R i)
p : (i : ι) → (R i)[X]
⊢ (RingHom.pi fun i ↦ mapRingHom (Pi.evalRingHom R i))
      { toFinsupp := ofCoeff (Finsupp.ofSupportFinite (fun n i ↦ (p i).coeff n) ⋯) } =
    p

Tactic:
by

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
⊢ (X ^ n + C r).leadingCoeff = 1

Tactic:
by

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

Tactic:
by

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
hbot : ⊥ + ⊥ = ⊥
hp : Monic D p
hq : Monic D q
⊢ supDegree D (p * q) = supDegree D p + supDegree D q

Tactic:
by

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

Goal state before:
pp: S : Type v
inst✝ : Semiring S
r : S
⊢ (X + C r).leadingCoeff = 1

Tactic:
by

Goal state after:
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
h : Function.Injective (map f)
r r' : R
eq : f r = f r'
⊢ map f (C r) = map f (C r')

Tactic:
by

Goal state after:
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
h : Function.Injective (map f)
r r' : R
eq : f r = f r'
⊢ r = r'

Tactic:
by

Goal state after:
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.Surjective ⇑f
p : S[X]
⊢ ∀ (p q : S[X]), (∃ a, map f a = p) → (∃ a, map f a = q) → ∃ a, map f a = p + q

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
r : R
i : ℕ
⊢ ((X + C r) ^ i).leadingCoeff = 1

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
this : DecidableEq R := Classical.decEq R
hp0 : p = 0
⊢ (p * q).degree = p.degree + q.degree

Tactic:
by

Goal state after: