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

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

pp: R : Type u
inst✝ : Semiring R
r : R
i : ℕ
a✝ : Nontrivial R
⊢ (X + C r).leadingCoeff ^ i ≠ 0

Tactic:
]

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

R : Type u
inst✝ : Semiring R
r : R
i : ℕ
a✝ : Nontrivial R
⊢ (X + C r).leadingCoeff ^ i ≠ 0
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]
n : ℕ
s : S
r : R
hr : f r = s
⊢ (monomial n) s = (monomial n) s

Tactic:
]

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
p : R[X]
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Semiring T
g : S →+* T
x : T
⊢ eval x (map (g.comp f) p) = eval x (map (g.comp f) p)

Tactic:
]

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

Goal state before:
pp: case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : ¬p = 0
hq : ¬q = 0
⊢ p.leadingCoeff * q.leadingCoeff = p.leadingCoeff * q.leadingCoeff

pp: case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : ¬p = 0
hq : ¬q = 0
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0

Tactic:
]

Goal state after:
case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : ¬p = 0
hq : ¬q = 0
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case inr.inr
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
inst✝ : NoZeroDivisors R
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hp : p ≠ 0
hq : q ≠ 0
⊢ (p * q).coeff (Function.invFun D (supDegree D (p * q))) = (p * q).coeff (Function.invFun D (supDegree D (p * q)))

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
inst✝ : NoZeroDivisors R
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hp : p ≠ 0
hq : q ≠ 0
⊢ leadingCoeff D p * leadingCoeff D q ≠ 0

Tactic:
]

Goal state after:
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
inst✝ : NoZeroDivisors R
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hp : p ≠ 0
hq : q ≠ 0
⊢ leadingCoeff D p * leadingCoeff D q ≠ 0
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: case inr
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
q p : R[X]
hq : q ≠ 0
hp : p ≠ 0
⊢ ↑p.natDegree ≤ ↑p.natDegree + ↑q.natDegree

Tactic:
]

Goal state after:
case inr
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
q p : R[X]
hq : q ≠ 0
hp : p ≠ 0
⊢ ↑p.natDegree ≤ ↑p.natDegree + ↑q.natDegree
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case ha
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
inst✝ : NoZeroDivisors R
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hp : p ≠ 0
hq : q ≠ 0
⊢ ¬p = 0

Tactic:
]

Goal state after:
case ha
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
inst✝ : NoZeroDivisors R
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hp : p ≠ 0
hq : q ≠ 0
⊢ ¬p = 0
Module: Mathlib.Algebra.Polynomial.Degree.Operations

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

Tactic:
]

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
p : R[X]
inst✝¹ : Semiring S
inst✝ : Semiring T
f : R →+* S
g : S →+* T
x : S
⊢ g (eval₂ f x p) = g (eval₂ f x p)

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : Nontrivial R
a : R
⊢ 1 = 1

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
inst✝ : NoZeroDivisors R
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hp : p ≠ 0
hq : q ≠ 0
⊢ ¬q = 0

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
inst✝ : NoZeroDivisors R
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hp : p ≠ 0
hq : q ≠ 0
⊢ ¬q = 0
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : Nontrivial R
x : R
⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: S : Type v
inst✝ : Ring S
c : S
⊢ -c = -c

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: case inl
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder B
inst✝⁴ : OrderBot B
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
⊢ leadingCoeff D 0 = leadingCoeff D 0

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : Nontrivial R
n : ℕ
hn : 0 < n
a : R
⊢ X ^ n + C (-a) ≠ 0

Tactic:
]

Goal state after:
R : Type u
inst✝¹ : Ring R
inst✝ : Nontrivial R
n : ℕ
hn : 0 < n
a : R
⊢ X ^ n + C (-a) ≠ 0
Module: Mathlib.Algebra.Polynomial.Eval.Coeff

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
x : R
p : R[X]
h : p.IsRoot x
⊢ 0 = 0

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: S : Type v
inst✝¹ : CommSemiring S
R : Type u_1
inst✝ : Ring R
f : R →+* S
x : R
p : R[X]
h : (Polynomial.map f p).IsRoot (f x)
hf : Function.Injective ⇑f
⊢ eval (f x) (Polynomial.map f p) = 0

Tactic:
]

Goal state after:
S : Type v
inst✝¹ : CommSemiring S
R : Type u_1
inst✝ : Ring R
f : R →+* S
x : R
p : R[X]
h : (Polynomial.map f p).IsRoot (f x)
hf : Function.Injective ⇑f
⊢ eval (f x) (Polynomial.map f p) = 0
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case inr
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
⊢ leadingCoeff D p = leadingCoeff D p

Tactic:
]

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

Goal state before:
pp: case inl
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder B
inst✝⁴ : OrderBot B
p : 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
⊢ leadingCoeff D 0 = leadingCoeff D 0

Tactic:
]

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

Goal state before:
pp: case mp
R : Type u
inst✝ : Semiring R
f : R[X]
H : ∃ x, f.support ⊆ {x}
⊢ ∃ n a, f = (monomial n) a

Tactic:
]

Goal state after:
case mp
R : Type u
inst✝ : Semiring R
f : R[X]
H : ∃ x, f.support ⊆ {x}
⊢ ∃ n a, f = (monomial n) a
Module: Mathlib.Algebra.Polynomial.Monomial

Goal state before:
pp: R : Type u
inst✝ : Semiring R
f : R[X]
n : ℕ
hn : f.support ⊆ {n}
i : ℕ
hi : ¬i = n
⊢ i ∉ f.support

Tactic:
]

Goal state after:
R : Type u
inst✝ : Semiring R
f : R[X]
n : ℕ
hn : f.support ⊆ {n}
i : ℕ
hi : ¬i = n
⊢ i ∉ f.support
Module: Mathlib.Algebra.Polynomial.Monomial

Goal state before:
pp: case mpr
R : Type u
inst✝ : Semiring R
n : ℕ
a : R
⊢ ((monomial n) a).support.card ≤ {n}.card

Tactic:
]

Goal state after:
case mpr
R : Type u
inst✝ : Semiring R
n : ℕ
a : R
⊢ ((monomial n) a).support.card ≤ {n}.card
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case inr
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
⊢ leadingCoeff D q = leadingCoeff D q

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 : Monic D q
⊢ leadingCoeff D p = 1

Tactic:
]

Goal state after:
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 : Monic D q
⊢ leadingCoeff D p = 1
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case zero
R : Type u_1
inst✝⁶ : Semiring R
A : Type u_8
B : Type u_9
inst✝⁵ : AddMonoid A
inst✝⁴ : AddMonoid B
inst✝³ : LinearOrder B
inst✝² : OrderBot B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
D : A → B
p : R[A]
n : ℕ
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hD : Function.Injective D
hp : Monic D p
⊢ Monic D 1

Tactic:
]

Goal state after:
case zero
R : Type u_1
inst✝⁶ : Semiring R
A : Type u_8
B : Type u_9
inst✝⁵ : AddMonoid A
inst✝⁴ : AddMonoid B
inst✝³ : LinearOrder B
inst✝² : OrderBot B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
D : A → B
p : R[A]
n : ℕ
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hD : Function.Injective D
hp : Monic D p
⊢ Monic D 1
Module: Mathlib.Algebra.Polynomial.Eval.Degree

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
n : ℕ
hn : p.natDegree < n
x : S
⊢ ∑ a ∈ range n, f (p.coeff a) * x ^ a = ∑ i ∈ range n, f (p.coeff i) * x ^ i

pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
n : ℕ
hn : p.natDegree < n
x : S
⊢ ∀ (n : ℕ), f 0 * x ^ n = 0

Tactic:
]

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
n : ℕ
hn : p.natDegree < n
x : S
⊢ ∀ (n : ℕ), f 0 * x ^ n = 0
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case succ
R : Type u_1
inst✝⁶ : Semiring R
A : Type u_8
B : Type u_9
inst✝⁵ : AddMonoid A
inst✝⁴ : AddMonoid B
inst✝³ : LinearOrder B
inst✝² : OrderBot B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
D : A → B
p : R[A]
n✝ : ℕ
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hD : Function.Injective D
hp : Monic D p
n : ℕ
ih : Monic D (p ^ n)
⊢ Monic D (p * p ^ n)

Tactic:
]

Goal state after:
case succ
R : Type u_1
inst✝⁶ : Semiring R
A : Type u_8
B : Type u_9
inst✝⁵ : AddMonoid A
inst✝⁴ : AddMonoid B
inst✝³ : LinearOrder B
inst✝² : OrderBot B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
D : A → B
p : R[A]
n✝ : ℕ
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hD : Function.Injective D
hp : Monic D p
n : ℕ
ih : Monic D (p ^ n)
⊢ Monic D (p * p ^ n)
Module: Mathlib.Algebra.Polynomial.Eval.Degree

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
n : ℕ
hn : p.natDegree < n
x : S
i : ℕ
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
x : R
⊢ ∑ a ∈ range (p.natDegree + 1), p.coeff a * x ^ a = ∑ i ∈ range (p.natDegree + 1), p.coeff i * x ^ i

pp: case h
R : Type u
inst✝ : Semiring R
p : R[X]
x : R
⊢ ∀ (n : ℕ), 0 * x ^ n = 0

Tactic:
]

Goal state after:
case h
R : Type u
inst✝ : Semiring R
p : R[X]
x : R
⊢ ∀ (n : ℕ), 0 * x ^ n = 0
Module: Mathlib.Algebra.Polynomial.Monomial

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : Semiring S
f g : R[X] →+* S
h₁ : ∀ (a : R), f (C a) = g (C a)
h₂ : f X = g X
f' : AddMonoidAlgebra R ℕ →+* S := f.comp (toFinsuppIso R).symm.toRingHom
hf' : f' = f.comp (toFinsuppIso R).symm.toRingHom
g' : AddMonoidAlgebra R ℕ →+* S := g.comp (toFinsuppIso R).symm.toRingHom
hg' : g' = g.comp (toFinsuppIso R).symm.toRingHom
A : f' = g'
⊢ f = f.comp ((toFinsuppIso R).symm.toRingHom.comp ↑(toFinsuppIso R))

Tactic:
]

Goal state after:
R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : Semiring S
f g : R[X] →+* S
h₁ : ∀ (a : R), f (C a) = g (C a)
h₂ : f X = g X
f' : AddMonoidAlgebra R ℕ →+* S := f.comp (toFinsuppIso R).symm.toRingHom
hf' : f' = f.comp (toFinsuppIso R).symm.toRingHom
g' : AddMonoidAlgebra R ℕ →+* S := g.comp (toFinsuppIso R).symm.toRingHom
hg' : g' = g.comp (toFinsuppIso R).symm.toRingHom
A : f' = g'
⊢ f = f.comp ((toFinsuppIso R).symm.toRingHom.comp ↑(toFinsuppIso R))
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case zero
R : Type u_1
inst✝⁷ : Semiring R
A : Type u_8
B : Type u_9
inst✝⁶ : AddMonoid A
inst✝⁵ : AddMonoid B
inst✝⁴ : LinearOrder B
inst✝³ : OrderBot B
inst✝² : AddLeftStrictMono B
inst✝¹ : AddRightStrictMono B
D : A → B
p : R[A]
n : ℕ
hzero : D 0 = 0
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hD : Function.Injective D
inst✝ : Nontrivial R
hp : Monic D p
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : p.natDegree < n
x : R
⊢ ∑ a ∈ range n, p.coeff a * x ^ a = ∑ i ∈ range n, p.coeff i * x ^ i

pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : p.natDegree < n
x : R
⊢ ∀ (n : ℕ), 0 * x ^ n = 0

Tactic:
]

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : p.natDegree < n
x : R
⊢ ∀ (n : ℕ), 0 * x ^ n = 0
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case succ
R : Type u_1
inst✝⁷ : Semiring R
A : Type u_8
B : Type u_9
inst✝⁶ : AddMonoid A
inst✝⁵ : AddMonoid B
inst✝⁴ : LinearOrder B
inst✝³ : OrderBot B
inst✝² : AddLeftStrictMono B
inst✝¹ : AddRightStrictMono B
D : A → B
p : R[A]
n✝ : ℕ
hzero : D 0 = 0
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hD : Function.Injective D
inst✝ : Nontrivial R
hp : Monic D p
n : ℕ
ih : supDegree D (p ^ n) = n • supDegree D p
⊢ supDegree D p + n • supDegree D p = supDegree D p + n • supDegree D p

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : Semiring S
f g : R[X] →+* S
h₁ : ∀ (a : R), f (C a) = g (C a)
h₂ : f X = g X
f' : AddMonoidAlgebra R ℕ →+* S := f.comp (toFinsuppIso R).symm.toRingHom
hf' : f' = f.comp (toFinsuppIso R).symm.toRingHom
g' : AddMonoidAlgebra R ℕ →+* S := g.comp (toFinsuppIso R).symm.toRingHom
hg' : g' = g.comp (toFinsuppIso R).symm.toRingHom
A : f' = g'
B : f = f'.comp ↑(toFinsuppIso R)
⊢ g = g.comp ((toFinsuppIso R).symm.toRingHom.comp ↑(toFinsuppIso R))

Tactic:
]

Goal state after:
R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : Semiring S
f g : R[X] →+* S
h₁ : ∀ (a : R), f (C a) = g (C a)
h₂ : f X = g X
f' : AddMonoidAlgebra R ℕ →+* S := f.comp (toFinsuppIso R).symm.toRingHom
hf' : f' = f.comp (toFinsuppIso R).symm.toRingHom
g' : AddMonoidAlgebra R ℕ →+* S := g.comp (toFinsuppIso R).symm.toRingHom
hg' : g' = g.comp (toFinsuppIso R).symm.toRingHom
A : f' = g'
B : f = f'.comp ↑(toFinsuppIso R)
⊢ g = g.comp ((toFinsuppIso R).symm.toRingHom.comp ↑(toFinsuppIso R))
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: R : Type u_1
A : Type u_3
T : Type u_4
inst✝² : Semiring R
inst✝¹ : SemilatticeInf T
inst✝ : OrderTop T
D : A → T
s : R[A]
hs : s.coeff.support.Nonempty
⊢ ↑(s.coeff.support.inf D) = ↑(s.coeff.support.inf D)

Tactic:
]

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

Goal state before:
pp: S : Type v
inst✝ : CommRing S
d : ℕ
y : S
cast_succ : ↑d + 1 = ↑d.succ
⊢ ↑d.succ * ∑ m ∈ range (d + 1), y ^ m * 1 ^ (d - m) * ↑(d.choose m) - ↑d.succ * y ^ d =
    ∑ x_1 ∈ range (d + 1), ↑((d + 1).choose x_1) * (↑x_1 * y ^ (x_1 - 1))

Tactic:
]

Goal state after:
S : Type v
inst✝ : CommRing S
d : ℕ
y : S
cast_succ : ↑d + 1 = ↑d.succ
⊢ ↑d.succ * ∑ m ∈ range (d + 1), y ^ m * 1 ^ (d - m) * ↑(d.choose m) - ↑d.succ * y ^ d =
    ∑ x_1 ∈ range (d + 1), ↑((d + 1).choose x_1) * (↑x_1 * y ^ (x_1 - 1))
Module: Mathlib.Algebra.Polynomial.Monomial

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : Semiring S
f g : R[X] →+* S
h₁ : ∀ (a : R), f (C a) = g (C a)
h₂ : f X = g X
f' : AddMonoidAlgebra R ℕ →+* S := f.comp (toFinsuppIso R).symm.toRingHom
hf' : f' = f.comp (toFinsuppIso R).symm.toRingHom
g' : AddMonoidAlgebra R ℕ →+* S := g.comp (toFinsuppIso R).symm.toRingHom
hg' : g' = g.comp (toFinsuppIso R).symm.toRingHom
A : f' = g'
B : f = f'.comp ↑(toFinsuppIso R)
C' : g = g'.comp ↑(toFinsuppIso R)
⊢ g'.comp ↑(toFinsuppIso R) = g'.comp ↑(toFinsuppIso R)

Tactic:
]

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

Goal state before:
pp: S : Type v
inst✝ : CommRing S
d : ℕ
y : S
cast_succ : ↑d + 1 = ↑d.succ
⊢ ∑ i ∈ range d, ↑d.succ * (↑(d.choose i) * y ^ i) =
    ∑ k ∈ range d, ↑((d + 1).choose (k + 1)) * (↑(k + 1) * y ^ (k + 1 - 1))

Tactic:
]

Goal state after:
S : Type v
inst✝ : CommRing S
d : ℕ
y : S
cast_succ : ↑d + 1 = ↑d.succ
⊢ ∑ i ∈ range d, ↑d.succ * (↑(d.choose i) * y ^ i) =
    ∑ k ∈ range d, ↑((d + 1).choose (k + 1)) * (↑(k + 1) * y ^ (k + 1 - 1))
Module: Mathlib.Algebra.Polynomial.Eval.Degree

Goal state before:
pp: S : Type v
inst✝ : CommRing S
d : ℕ
y✝ : S
cast_succ : ↑d + 1 = ↑d.succ
y : ℕ
_hy : y ∈ range d
⊢ ↑((d + 1).choose (y + 1)) * ↑(y + 1) * y✝ ^ y = ↑((d + 1).choose (y + 1)) * ↑(y + 1) * y✝ ^ y

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hqd0 : q.natDegree ≠ 0
⊢ (p.sum fun a b ↦ (C b * q ^ a).coeff (p.natDegree * q.natDegree)) = p.leadingCoeff * q.leadingCoeff ^ p.natDegree

Tactic:
]

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
hqd0 : q.natDegree ≠ 0
⊢ (p.sum fun a b ↦ (C b * q ^ a).coeff (p.natDegree * q.natDegree)) = p.leadingCoeff * q.leadingCoeff ^ p.natDegree
Module: Mathlib.RingTheory.Adjoin.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : R[X]
_hp : p ∈ ⊤
S : Subalgebra R R[X] := R[ X]
⊢ (p.sum fun n a ↦ (monomial n) a) ∈ S

Tactic:
]

Goal state after:
R : Type u
inst✝ : CommSemiring R
p : R[X]
_hp : p ∈ ⊤
S : Subalgebra R R[X] := R[ X]
⊢ (p.sum fun n a ↦ (monomial n) a) ∈ S
Module: Mathlib.RingTheory.Adjoin.Polynomial.Basic

Goal state before:
pp: R : Type u
A : Type z
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A
⊢ R[x] = R[x]

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Adjoin.Polynomial.Basic

Goal state before:
pp: R : Type u
A : Type z
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x a : A
h : a ∈ (aeval x).range
⊢ ∃ p, (aeval x) p = a

Tactic:
]

Goal state after:
R : Type u
A : Type z
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x a : A
h : a ∈ (aeval x).range
⊢ ∃ p, (aeval x) p = a
Module: Mathlib.RingTheory.Adjoin.Polynomial.Basic

Goal state before:
pp: R : Type u
A : Type z
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A
a : ↥R[x]
y : A := ↑a
this : y ∈ (aeval x).range
h : y = ↑a
⊢ ∃ p, (aeval x) p = y

Tactic:
]

Goal state after:
R : Type u
A : Type z
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A
a : ↥R[x]
y : A := ↑a
this : y ∈ (aeval x).range
h : y = ↑a
⊢ ∃ p, (aeval x) p = y
Module: Mathlib.Algebra.Polynomial.Eval.Degree

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hqd0 : q.natDegree ≠ 0
b : ℕ
hbs : b ∈ p.support
hbp : b ≠ p.natDegree
⊢ (q ^ b).natDegree < p.natDegree * q.natDegree

Tactic:
]

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
hqd0 : q.natDegree ≠ 0
b : ℕ
hbs : b ∈ p.support
hbp : b ≠ p.natDegree
⊢ (q ^ b).natDegree < p.natDegree * q.natDegree
Module: Mathlib.Algebra.Polynomial.Eval.Degree

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

pp: R : Type u
inst✝ : Semiring R
p : R[X]
r : R
n : ℕ
⊢ ∀ b ∈ range (p.natDegree + 1), b ≠ n → p.coeff b * (r ^ b * if n = b then 1 else 0) = 0

pp: R : Type u
inst✝ : Semiring R
p : R[X]
r : R
n : ℕ
h : n ∉ range (p.natDegree + 1)
⊢ p.coeff n * (r ^ n * if n = n then 1 else 0) = 0

Tactic:
]

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
r : R
n : ℕ
⊢ ∀ b ∈ range (p.natDegree + 1), b ≠ n → p.coeff b * (r ^ b * if n = b then 1 else 0) = 0

R : Type u
inst✝ : Semiring R
p : R[X]
r : R
n : ℕ
h : n ∉ range (p.natDegree + 1)
⊢ p.coeff n * (r ^ n * if n = n then 1 else 0) = 0
Module: Mathlib.Algebra.Polynomial.Eval.Degree

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
r : R
n : ℕ
h : n ∉ range (p.natDegree + 1)
⊢ 0 = 0

pp: R : Type u
inst✝ : Semiring R
p : R[X]
r : R
n : ℕ
h : n ∉ range (p.natDegree + 1)
⊢ p.natDegree < n

Tactic:
]

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
r : R
n : ℕ
h : n ∉ range (p.natDegree + 1)
⊢ p.natDegree < n
Module: Mathlib.Algebra.Polynomial.Eval.Degree

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

Tactic:
]

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
r : R
n : ℕ
h : p.natDegree < n
⊢ p.natDegree < n
Module: Mathlib.Algebra.Polynomial.Eval.Degree

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
r : R
hr : r ∈ nonZeroDivisors R
n : ℕ
⊢ p.coeff n = 0 ↔ p.coeff n = 0

Tactic:
]

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
m : ℕ
hm : ∀ (m_1 : ℕ), m ≤ m_1 → p.coeff m_1 = 0
⊢ (map f p).coeff m = 0

Tactic:
]

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
m : ℕ
hm : ∀ (m_1 : ℕ), m ≤ m_1 → p.coeff m_1 = 0
⊢ (map f p).coeff m = 0
Module: Mathlib.Algebra.Polynomial.Eval.Degree

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

Tactic:
]

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
hp : map f p = 0
hp₀ : p ≠ 0
hpq : (map f p).degree = p.degree
⊢ p = 0