mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.MvPolynomial.Equiv

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

Tactic:
]

Goal state after:
case monomial
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Unique σ
n : ℕ
d : σ →₀ ℕ
r : R
⊢ ((Polynomial.monomial ((Finsupp.single default (d default)) default)) r).coeff n =
    coeff (Finsupp.single default n) ((monomial (Finsupp.single default (d default))) r)
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

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

Tactic:
]

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
h : p ≠ 0
h2 : (map f p).degree = p.degree
h3 : (map f p).natDegree = p.natDegree
⊢ ¬p = 0
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
hp : ¬P = 0
he : ¬P.eraseLead = 0
h₁ : ((X - C x) * P).natDegree = P.natDegree + 1
dP : ℕ
hdP : P.natDegree = dP + 2
h : P.coeff (dP + 1) = 0
⊢ (if dP + 2 + 1 = 0 then 0 else P.coeff (dP + 1) - x * P.coeff (dP + 1 + 1)) ≠ 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
hp : ¬P = 0
he : ¬P.eraseLead = 0
h₁ : ((X - C x) * P).natDegree = P.natDegree + 1
dP : ℕ
hdP : P.natDegree = dP + 2
h : P.coeff (dP + 1) = 0
⊢ (if dP + 2 + 1 = 0 then 0 else P.coeff (dP + 1) - x * P.coeff (dP + 1 + 1)) ≠ 0
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Unique σ
P : R[X]
d : σ →₀ ℕ
⊢ P.coeff (d default) = P.coeff (d default)

Tactic:
]

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

Goal state before:
pp: case monomial
σ : Type u_1
R : Type u_2
S : Type u_3
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Unique σ
φ : R →+* S
a : σ → S
d : σ →₀ ℕ
r : R
⊢ Polynomial.eval₂ φ (a default) ((Polynomial.monomial (d default)) r) = eval₂ φ a ((monomial d) r)

Tactic:
]

Goal state after:
case monomial
σ : Type u_1
R : Type u_2
S : Type u_3
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Unique σ
φ : R →+* S
a : σ → S
d : σ →₀ ℕ
r : R
⊢ Polynomial.eval₂ φ (a default) ((Polynomial.monomial (d default)) r) = eval₂ φ a ((monomial d) r)
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case monomial
σ : Type u_1
R : Type u_2
S : Type u_3
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Unique σ
φ : R →+* S
a : σ → S
d : σ →₀ ℕ
r : R
⊢ φ r * a default ^ (Finsupp.single default (d default)) default = φ r * a default ^ d default

pp: case monomial
σ : Type u_1
R : Type u_2
S : Type u_3
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Unique σ
φ : R →+* S
a : σ → S
d : σ →₀ ℕ
r : R
⊢ a default ^ 0 = 1

Tactic:
]

Goal state after:
case monomial
σ : Type u_1
R : Type u_2
S : Type u_3
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Unique σ
φ : R →+* S
a : σ → S
d : σ →₀ ℕ
r : R
⊢ φ r * a default ^ (Finsupp.single default (d default)) default = φ r * a default ^ d default

case monomial
σ : Type u_1
R : Type u_2
S : Type u_3
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Unique σ
φ : R →+* S
a : σ → S
d : σ →₀ ℕ
r : R
⊢ a default ^ 0 = 1
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

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

Tactic:
]

Goal state after:
case inr
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
h : p ≠ 0
h2 : (map f p).degree = p.degree
h3 : (map f p).natDegree = p.natDegree
h4 : map f p ≠ 0
⊢ ¬map f p = 0
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: σ : Type u_1
R : Type u_2
S : Type u_3
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Unique σ
f : R[X]
φ : R →+* S
a : σ → S
⊢ Polynomial.eval₂ φ (a default) ((uniqueAlgEquiv R σ) ((uniqueAlgEquiv R σ).symm f)) = Polynomial.eval₂ φ (a default) f

Tactic:
]

Goal state after:
σ : Type u_1
R : Type u_2
S : Type u_3
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Unique σ
f : R[X]
φ : R →+* S
a : σ → S
⊢ Polynomial.eval₂ φ (a default) ((uniqueAlgEquiv R σ) ((uniqueAlgEquiv R σ).symm f)) = Polynomial.eval₂ φ (a default) f
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: σ : Type u_1
R : Type u_2
S : Type u_3
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Unique σ
f : R[X]
φ : R →+* S
a : σ → S
⊢ Polynomial.eval₂ φ (a default) f = Polynomial.eval₂ φ (a default) f

Tactic:
]

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

Goal state before:
pp: case neg.inl
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
h₁ : ((X - C x) * P).natDegree = P.natDegree + 1
dP : ℕ
hdP : P.natDegree = dP + 2
h₂ : ((X - C x) * P).nextCoeff ≠ 0
n : ℕ
hn : n < P.natDegree
hd₁ : n < ((X - C x) * P).eraseLead.natDegree
⊢ ((X - C x) * P).eraseLead.coeff n - 0 = ((X - C x) * P.eraseLead).coeff n

Tactic:
]

Goal state after:
case neg.inl
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
h₁ : ((X - C x) * P).natDegree = P.natDegree + 1
dP : ℕ
hdP : P.natDegree = dP + 2
h₂ : ((X - C x) * P).nextCoeff ≠ 0
n : ℕ
hn : n < P.natDegree
hd₁ : n < ((X - C x) * P).eraseLead.natDegree
⊢ ((X - C x) * P).eraseLead.coeff n - 0 = ((X - C x) * P.eraseLead).coeff n
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: σ : Type u_1
R : Type u_2
S : Type u_3
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Unique σ
f : R[X]
φ : R →+* S
a : S
⊢ Polynomial.eval₂ φ a f = Polynomial.eval₂ φ a f

Tactic:
]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
S : Type u_3
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Unique σ
f : MvPolynomial σ R
φ : R →+* S
a : S
⊢ Polynomial.eval₂ φ a ((uniqueAlgEquiv R σ) f) = Polynomial.eval₂ φ a ((uniqueAlgEquiv R σ) f)

Tactic:
]

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

Goal state before:
pp: R : Type u
S₁ : Type v
σ : Type u_1
inst✝³ : CommSemiring R
inst✝² : IsEmpty σ
inst✝¹ : CommSemiring S₁
inst✝ : Algebra R S₁
f : σ → S₁
this : aeval f = (Algebra.ofId R S₁).comp ↑(isEmptyAlgEquiv R σ)
⊢ Injective ⇑((Algebra.ofId R S₁).comp ↑(isEmptyAlgEquiv R σ)) ↔ Injective (⇑(algebraMap R S₁) ∘ ⇑(isEmptyAlgEquiv R σ))

Tactic:
]

Goal state after:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝³ : CommSemiring R
inst✝² : IsEmpty σ
inst✝¹ : CommSemiring S₁
inst✝ : Algebra R S₁
f : σ → S₁
this : aeval f = (Algebra.ofId R S₁).comp ↑(isEmptyAlgEquiv R σ)
⊢ Injective ⇑((Algebra.ofId R S₁).comp ↑(isEmptyAlgEquiv R σ)) ↔ Injective (⇑(algebraMap R S₁) ∘ ⇑(isEmptyAlgEquiv R σ))
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case neg.inl
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
h₁ : ((X - C x) * P).natDegree = P.natDegree + 1
dP : ℕ
hdP : P.natDegree = dP + 2
h₂ : ((X - C x) * P).nextCoeff ≠ 0
n : ℕ
hn : n < P.natDegree
hd₁ : n < ((X - C x) * P).eraseLead.natDegree
⊢ ((X - C x) * P).coeff n - 0 - 0 = ((X - C x) * P.eraseLead).coeff n

Tactic:
]

Goal state after:
case neg.inl
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
h₁ : ((X - C x) * P).natDegree = P.natDegree + 1
dP : ℕ
hdP : P.natDegree = dP + 2
h₂ : ((X - C x) * P).nextCoeff ≠ 0
n : ℕ
hn : n < P.natDegree
hd₁ : n < ((X - C x) * P).eraseLead.natDegree
⊢ ((X - C x) * P).coeff n - 0 - 0 = ((X - C x) * P.eraseLead).coeff n
Module: Mathlib.Algebra.Polynomial.Reverse

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

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: R : Type u
n : ℕ
inst✝ : Ring R
p q : R[X]
qn : (-q).natDegree ≤ n
⊢ (p - q).natDegree ≤ n ↔ p.natDegree ≤ n

Tactic:
]

Goal state after:
R : Type u
n : ℕ
inst✝ : Ring R
p q : R[X]
qn : (-q).natDegree ≤ n
⊢ (p - q).natDegree ≤ n ↔ p.natDegree ≤ n
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
n : ℕ
inst✝ : Ring R
p q : R[X]
qn : (-q).natDegree ≤ n
⊢ p.natDegree ≤ n ↔ p.natDegree ≤ n

Tactic:
]

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

Goal state before:
pp: R : Type u
n : ℕ
inst✝ : Ring R
p q : R[X]
pn : p.natDegree ≤ n
⊢ q.natDegree ≤ n ↔ q.natDegree ≤ n

pp: R : Type u
n : ℕ
inst✝ : Ring R
p q : R[X]
pn : p.natDegree ≤ n
⊢ p.natDegree ≤ n

Tactic:
]

Goal state after:
R : Type u
n : ℕ
inst✝ : Ring R
p q : R[X]
pn : p.natDegree ≤ n
⊢ p.natDegree ≤ n
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
n : ℕ
inst✝ : Ring R
p q : R[X]
dg : (-q).natDegree < n
⊢ (p - q).coeff n = p.coeff n

Tactic:
]

Goal state after:
R : Type u
n : ℕ
inst✝ : Ring R
p q : R[X]
dg : (-q).natDegree < n
⊢ (p - q).coeff n = p.coeff n
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
n : ℕ
inst✝ : Ring R
p q : R[X]
dg : (-q).natDegree < n
⊢ p.coeff n = p.coeff n

Tactic:
]

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

Goal state before:
pp: case neg.inl
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
h₁ : ((X - C x) * P).natDegree = P.natDegree + 1
dP : ℕ
hdP : P.natDegree = dP + 2
h₂ : ((X - C x) * P).nextCoeff ≠ 0
n : ℕ
hn : n < P.natDegree
hd₁ : n < ((X - C x) * P).eraseLead.natDegree
⊢ ((X - C x) * (monomial P.natDegree) P.leadingCoeff).coeff n = 0

Tactic:
]

Goal state after:
case neg.inl
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
h₁ : ((X - C x) * P).natDegree = P.natDegree + 1
dP : ℕ
hdP : P.natDegree = dP + 2
h₂ : ((X - C x) * P).nextCoeff ≠ 0
n : ℕ
hn : n < P.natDegree
hd₁ : n < ((X - C x) * P).eraseLead.natDegree
⊢ ((X - C x) * (monomial P.natDegree) P.leadingCoeff).coeff n = 0
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
n : ℕ
inst✝ : Ring R
p q : R[X]
df : p.natDegree < n
⊢ -q.coeff n = -q.coeff n

pp: R : Type u
n : ℕ
inst✝ : Ring R
p q : R[X]
df : p.natDegree < n
⊢ p.natDegree < n

Tactic:
]

Goal state after:
R : Type u
n : ℕ
inst✝ : Ring R
p q : R[X]
df : p.natDegree < n
⊢ p.natDegree < n
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

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

pp: R : Type u
inst✝ : Semiring R
a : R
ha : a ≠ 0
c : R
⊢ 0 < (C a * X + C c).natDegree

Tactic:
]

Goal state after:
R : Type u
inst✝ : Semiring R
a : R
ha : a ≠ 0
c : R
⊢ (C a * X + C c).coeff ((C a * X + C c).natDegree - 1) = c

R : Type u
inst✝ : Semiring R
a : R
ha : a ≠ 0
c : R
⊢ 0 < (C a * X + C c).natDegree
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case refine_1
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree = 1
h : p = 0
⊢ False

Tactic:
]

Goal state after:
case refine_1
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree = 1
h : p = 0
⊢ False
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case refine_2.succ.succ
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree = 1
n : ℕ
⊢ 0 = 0

pp: case refine_2.succ.succ
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree = 1
n : ℕ
⊢ p.natDegree < n + 1 + 1

Tactic:
]

Goal state after:
case refine_2.succ.succ
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree = 1
n : ℕ
⊢ p.natDegree < n + 1 + 1
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
p : R[X]
inst✝ : IsLeftCancelMulZero R
h : ∃ a, a ≠ 0 ∧ ∃ b, C a * X + C b = p
r₁ : R
⊢ ∃ a, a ≠ 0 ∧ ∃ b, C a * X + C b = p

Tactic:
]

Goal state after:
R : Type u
inst✝¹ : Semiring R
p : R[X]
inst✝ : IsLeftCancelMulZero R
h : ∃ a, a ≠ 0 ∧ ∃ b, C a * X + C b = p
r₁ : R
⊢ ∃ a, a ≠ 0 ∧ ∃ b, C a * X + C b = p
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
p : R[X]
a : R
inst✝ : NoZeroDivisors R
a0 : a ≠ 0
⊢ p.degree = p.degree

Tactic:
]

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

Goal state before:
pp: case neg.inl.succ
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
h₁ : ((X - C x) * P).natDegree = P.natDegree + 1
dP : ℕ
hdP : P.natDegree = dP + 2
h₂ : ((X - C x) * P).nextCoeff ≠ 0
n : ℕ
hn : n < P.natDegree
hd₁ : n < ((X - C x) * P).eraseLead.natDegree
n✝ : ℕ
hn₂ : n = n✝ + 1
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case pos
R : Type u
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
q0 : q.natDegree = 0
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: R : Type u
S₁ : Type v
inst✝ : CommSemiring R
m : Option S₁ →₀ ℕ
r : R
⊢ (algebraMap R (MvPolynomial S₁ R)[X]) r *
      ((none.elim Polynomial.X fun s ↦ Polynomial.C (X s)) ^ m none *
        m.some.prod fun a k ↦ ((Option.some a).elim Polynomial.X fun s ↦ Polynomial.C (X s)) ^ k) =
    (Polynomial.monomial (m none)) ((monomial m.some) r)

pp: case h_zero
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
m : Option S₁ →₀ ℕ
r : R
⊢ ∀ (o : Option S₁), (o.elim Polynomial.X fun s ↦ Polynomial.C (X s)) ^ 0 = 1

pp: case h_add
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
m : Option S₁ →₀ ℕ
r : R
⊢ ∀ (o : Option S₁) (m₁ m₂ : ℕ),
    (o.elim Polynomial.X fun s ↦ Polynomial.C (X s)) ^ (m₁ + m₂) =
      (o.elim Polynomial.X fun s ↦ Polynomial.C (X s)) ^ m₁ * (o.elim Polynomial.X fun s ↦ Polynomial.C (X s)) ^ m₂

Tactic:
]

Goal state after:
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
m : Option S₁ →₀ ℕ
r : R
⊢ (algebraMap R (MvPolynomial S₁ R)[X]) r *
      ((none.elim Polynomial.X fun s ↦ Polynomial.C (X s)) ^ m none *
        m.some.prod fun a k ↦ ((Option.some a).elim Polynomial.X fun s ↦ Polynomial.C (X s)) ^ k) =
    (Polynomial.monomial (m none)) ((monomial m.some) r)

case h_zero
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
m : Option S₁ →₀ ℕ
r : R
⊢ ∀ (o : Option S₁), (o.elim Polynomial.X fun s ↦ Polynomial.C (X s)) ^ 0 = 1

case h_add
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
m : Option S₁ →₀ ℕ
r : R
⊢ ∀ (o : Option S₁) (m₁ m₂ : ℕ),
    (o.elim Polynomial.X fun s ↦ Polynomial.C (X s)) ^ (m₁ + m₂) =
      (o.elim Polynomial.X fun s ↦ Polynomial.C (X s)) ^ m₁ * (o.elim Polynomial.X fun s ↦ Polynomial.C (X s)) ^ m₂
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case succ
R : Type u
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
k : ℕ
IH : (p.comp^[k] q).natDegree = p.natDegree ^ k * q.natDegree
⊢ p.natDegree * (p.natDegree ^ k * q.natDegree) = p.natDegree * (p.natDegree ^ k * q.natDegree)

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
h₁ : ((X - C x) * P).natDegree = P.natDegree + 1
dP : ℕ
hdP : P.natDegree = dP + 2
h₂ : ((X - C x) * P).nextCoeff ≠ 0
n : ℕ
hn : n ≥ P.natDegree
⊢ 0 = 0

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
h₁ : ((X - C x) * P).natDegree = P.natDegree + 1
dP : ℕ
hdP : P.natDegree = dP + 2
h₂ : ((X - C x) * P).nextCoeff ≠ 0
n : ℕ
hn : n ≥ P.natDegree
⊢ ((X - C x) * P).eraseLead.eraseLead.natDegree < n

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
h₁ : ((X - C x) * P).natDegree = P.natDegree + 1
dP : ℕ
hdP : P.natDegree = dP + 2
h₂ : ((X - C x) * P).nextCoeff ≠ 0
n : ℕ
hn : n ≥ P.natDegree
⊢ ((X - C x) * P).eraseLead.eraseLead.natDegree < n
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
hq : q.natDegree ≠ 0
⊢ (p.comp q).leadingCoeff = (p.comp q).leadingCoeff

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
h₁ : ((X - C x) * P).natDegree = P.natDegree + 1
dP : ℕ
hdP : P.natDegree = dP + 2
h₂ : ((X - C x) * P).nextCoeff ≠ 0
n : ℕ
hn : n ≥ P.natDegree
⊢ 0 = 0

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
h₁ : ((X - C x) * P).natDegree = P.natDegree + 1
dP : ℕ
hdP : P.natDegree = dP + 2
h₂ : ((X - C x) * P).nextCoeff ≠ 0
n : ℕ
hn : n ≥ P.natDegree
⊢ ((X - C x) * P.eraseLead).natDegree < n

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
h₁ : ((X - C x) * P).natDegree = P.natDegree + 1
dP : ℕ
hdP : P.natDegree = dP + 2
h₂ : ((X - C x) * P).nextCoeff ≠ 0
n : ℕ
hn : n ≥ P.natDegree
⊢ ((X - C x) * P.eraseLead).natDegree < n
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
S₁ : Type v
inst✝ : CommSemiring R
m : Option S₁ →₀ ℕ
r : R
⊢ (algebraMap R (MvPolynomial S₁ R)[X]) r *
      ((none.elim Polynomial.X fun s ↦ Polynomial.C (X s)) ^ m none *
        m.some.prod fun a k ↦ ((Option.some a).elim Polynomial.X fun s ↦ Polynomial.C (X s)) ^ k) =
    Polynomial.C (C r * m.some.prod fun n e ↦ X n ^ e) * Polynomial.X ^ m none

Tactic:
]

Goal state after:
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
m : Option S₁ →₀ ℕ
r : R
⊢ (algebraMap R (MvPolynomial S₁ R)[X]) r *
      ((none.elim Polynomial.X fun s ↦ Polynomial.C (X s)) ^ m none *
        m.some.prod fun a k ↦ ((Option.some a).elim Polynomial.X fun s ↦ Polynomial.C (X s)) ^ k) =
    Polynomial.C (C r * m.some.prod fun n e ↦ X n ^ e) * Polynomial.X ^ m none
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
h₁ : ((X - C x) * P).natDegree = P.natDegree + 1
dP : ℕ
hdP : P.natDegree = dP + 2
h₂ : ((X - C x) * P).nextCoeff ≠ 0
n : ℕ
hn : n ≥ P.natDegree
⊢ ((X - C x) * P).natDegree - 1 - 1 < n

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
h₁ : ((X - C x) * P).natDegree = P.natDegree + 1
dP : ℕ
hdP : P.natDegree = dP + 2
h₂ : ((X - C x) * P).nextCoeff ≠ 0
n : ℕ
hn : n ≥ P.natDegree
⊢ ((X - C x) * P).natDegree - 1 - 1 < n
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case neg
R : Type u
inst✝ : Ring R
p : R[X]
a✝ : Nontrivial R
h : ¬p = 0
⊢ p.leadingCoeff * (-X).leadingCoeff ^ p.natDegree = (-1) ^ p.natDegree * p.leadingCoeff

pp: case neg
R : Type u
inst✝ : Ring R
p : R[X]
a✝ : Nontrivial R
h : ¬p = 0
⊢ (-X).natDegree ≠ 0

pp: case neg
R : Type u
inst✝ : Ring R
p : R[X]
a✝ : Nontrivial R
h : ¬p = 0
⊢ p.leadingCoeff * (-X).leadingCoeff ^ p.natDegree ≠ 0

Tactic:
]

Goal state after:
case neg
R : Type u
inst✝ : Ring R
p : R[X]
a✝ : Nontrivial R
h : ¬p = 0
⊢ p.leadingCoeff * (-X).leadingCoeff ^ p.natDegree = (-1) ^ p.natDegree * p.leadingCoeff

case neg
R : Type u
inst✝ : Ring R
p : R[X]
a✝ : Nontrivial R
h : ¬p = 0
⊢ (-X).natDegree ≠ 0

case neg
R : Type u
inst✝ : Ring R
p : R[X]
a✝ : Nontrivial R
h : ¬p = 0
⊢ p.leadingCoeff * (-X).leadingCoeff ^ p.natDegree ≠ 0
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case h_add
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
m : Option S₁ →₀ ℕ
r : R
o✝ : Option S₁
m₁✝ m₂✝ : ℕ
⊢ (o✝.elim Polynomial.X fun s ↦ Polynomial.C (X s)) ^ m₁✝ * (o✝.elim Polynomial.X fun s ↦ Polynomial.C (X s)) ^ m₂✝ =
    (o✝.elim Polynomial.X fun s ↦ Polynomial.C (X s)) ^ m₁✝ * (o✝.elim Polynomial.X fun s ↦ Polynomial.C (X s)) ^ m₂✝

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
h₁ : ((X - C x) * P).natDegree = P.natDegree + 1
dP : ℕ
hdP : P.natDegree = dP + 2
h₂ : ((X - C x) * P).nextCoeff ≠ 0
n : ℕ
hn : n ≥ P.natDegree
⊢ (X - C x).natDegree + (P.natDegree - 2) < n

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
h₁ : ((X - C x) * P).natDegree = P.natDegree + 1
dP : ℕ
hdP : P.natDegree = dP + 2
h₂ : ((X - C x) * P).nextCoeff ≠ 0
n : ℕ
hn : n ≥ P.natDegree
⊢ (X - C x).natDegree + (P.natDegree - 2) < n
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case monomial
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
j : Option S₁ →₀ ℕ
r : R
n : Option S₁ →₀ ℕ
⊢ coeff n.some (((Polynomial.monomial (j none)) ((monomial j.some) r)).coeff (n none)) = coeff n ((monomial j) r)

Tactic:
]

Goal state after:
case monomial
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
j : Option S₁ →₀ ℕ
r : R
n : Option S₁ →₀ ℕ
⊢ coeff n.some (((Polynomial.monomial (j none)) ((monomial j.some) r)).coeff (n none)) = coeff n ((monomial j) r)
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

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

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h : p.comp q = 0
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case neg
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
j : Option S₁ →₀ ℕ
r : R
n : Option S₁ →₀ ℕ
hj : ¬j = n
⊢ (if j none = n none then if j.some = n.some then r else 0 else 0) = 0

Tactic:
]

Goal state after:
case neg
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
j : Option S₁ →₀ ℕ
r : R
n : Option S₁ →₀ ℕ
hj : ¬j = n
⊢ (if j none = n none then if j.some = n.some then r else 0 else 0) = 0