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

Goal state before:
pp: case pos
R : Type u_2
inst✝² : Ring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x : R
P : R[X]
hx : x ≠ 0
h : P.nextCoeff = 0
hp : ¬P = 0
he : P.eraseLead = 0
⊢ ((X - C x) * P).eraseLead.eraseLead = (X - C x) * P.eraseLead

pp: case neg
R : Type u_2
inst✝² : Ring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x : R
P : R[X]
hx : x ≠ 0
h : P.nextCoeff = 0
hp : ¬P = 0
he : ¬P.eraseLead = 0
⊢ ((X - C x) * P).eraseLead.eraseLead = (X - C x) * P.eraseLead

Tactic:
·

Goal state after:
case pos
R : Type u_2
inst✝² : Ring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x : R
P : R[X]
hx : x ≠ 0
h : P.nextCoeff = 0
hp : ¬P = 0
he : P.eraseLead = 0
⊢ ((X - C x) * P).eraseLead.eraseLead = (X - C x) * P.eraseLead
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case neg
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
s : Finset S
h : {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Ne on natDegree ∘ f)
H : ∀ x ∈ s, f x = 0
⊢ (s.sum f).natDegree = s.sup fun i ↦ (f i).natDegree

Tactic:
·

Goal state after:
case neg
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
s : Finset S
h : {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Ne on natDegree ∘ f)
H : ∀ x ∈ s, f x = 0
⊢ (s.sum f).natDegree = s.sup fun i ↦ (f i).natDegree
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case pos
R : Type u_2
inst✝² : Ring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x : R
P : R[X]
hx : x ≠ 0
h : P.nextCoeff = 0
hp : ¬P = 0
he : P.eraseLead = 0
he₂ : ((X - C x) * P).eraseLead = 0
⊢ ((X - C x) * P).eraseLead.eraseLead = 0

pp: case neg
R : Type u_2
inst✝² : Ring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x : R
P : R[X]
hx : x ≠ 0
h : P.nextCoeff = 0
hp : ¬P = 0
he : P.eraseLead = 0
he₂ : ¬((X - C x) * P).eraseLead = 0
⊢ ((X - C x) * P).eraseLead.eraseLead = 0

Tactic:
·

Goal state after:
case pos
R : Type u_2
inst✝² : Ring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x : R
P : R[X]
hx : x ≠ 0
h : P.nextCoeff = 0
hp : ¬P = 0
he : P.eraseLead = 0
he₂ : ((X - C x) * P).eraseLead = 0
⊢ ((X - C x) * P).eraseLead.eraseLead = 0
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p = 0
⊢ ↑n < p.degree ↔ n < p.natDegree

pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : ¬p = 0
⊢ ↑n < p.degree ↔ n < p.natDegree

Tactic:
·

Goal state after:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p = 0
⊢ ↑n < p.degree ↔ n < p.natDegree
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case inl
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
h : p = 0
⊢ (map f p).degree = p.degree ↔ f p.leadingCoeff ≠ 0 ∨ p = 0

pp: case inr
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
h : p ≠ 0
⊢ (map f p).degree = p.degree ↔ f p.leadingCoeff ≠ 0 ∨ p = 0

Tactic:
·

Goal state after:
case inl
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
h : p = 0
⊢ (map f p).degree = p.degree ↔ f p.leadingCoeff ≠ 0 ∨ p = 0
Module: Mathlib.Algebra.Polynomial.Reverse

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

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

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

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

Tactic:
·

Goal state after:
case neg.Cg
R : Type u_1
inst✝ : Semiring R
N O : ℕ
f : R[X]
Cf : #f.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
cg : ℕ
hcg : ∀ (g : R[X]), #g.support ≤ cg.succ → g.natDegree ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
g : R[X]
Cg : #g.support ≤ (cg + 1).succ
Og : g.natDegree ≤ O
g0 : ¬g = 0
⊢ #(C g.leadingCoeff * X ^ g.natDegree).support ≤ cg.succ
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
⊢ ((X - C x) * P).eraseLead.eraseLead.coeff n = ((X - C x) * P.eraseLead).coeff n

pp: case neg.inr
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.coeff n = ((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
⊢ ((X - C x) * P).eraseLead.eraseLead.coeff n = ((X - C x) * P.eraseLead).coeff n
Module: Mathlib.Algebra.Polynomial.Reverse

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

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

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

Tactic:
·

Goal state after:
case neg.Og
R : Type u_1
inst✝ : Semiring R
N O : ℕ
f : R[X]
Cf : #f.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
cg : ℕ
hcg : ∀ (g : R[X]), #g.support ≤ cg.succ → g.natDegree ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
g : R[X]
Cg : #g.support ≤ (cg + 1).succ
Og : g.natDegree ≤ O
g0 : ¬g = 0
⊢ (C g.leadingCoeff * X ^ g.natDegree).natDegree ≤ O
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
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
⊢ 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
⊢ a default ^ 0 = 1
Module: Mathlib.Algebra.Polynomial.Reverse

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

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

Tactic:
·

Goal state after:
case neg.Cg
R : Type u_1
inst✝ : Semiring R
N O : ℕ
f : R[X]
Cf : #f.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
cg : ℕ
hcg : ∀ (g : R[X]), #g.support ≤ cg.succ → g.natDegree ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
g : R[X]
Cg : #g.support ≤ (cg + 1).succ
Og : g.natDegree ≤ O
g0 : ¬g = 0
⊢ #g.eraseLead.support ≤ cg.succ
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case inl
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
h : p.natDegree = 0
⊢ (map f p).natDegree = p.natDegree ↔ f p.leadingCoeff ≠ 0 ∨ p.natDegree = 0

pp: case inr
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
h : p.natDegree ≠ 0
⊢ (map f p).natDegree = p.natDegree ↔ f p.leadingCoeff ≠ 0 ∨ p.natDegree = 0

Tactic:
·

Goal state after:
case inl
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
h : p.natDegree = 0
⊢ (map f p).natDegree = p.natDegree ↔ f p.leadingCoeff ≠ 0 ∨ p.natDegree = 0
Module: Mathlib.Algebra.Polynomial.Reverse

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

Tactic:
·

Goal state after:
case neg.Og
R : Type u_1
inst✝ : Semiring R
N O : ℕ
f : R[X]
Cf : #f.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
cg : ℕ
hcg : ∀ (g : R[X]), #g.support ≤ cg.succ → g.natDegree ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
g : R[X]
Cg : #g.support ≤ (cg + 1).succ
Og : g.natDegree ≤ O
g0 : ¬g = 0
⊢ g.eraseLead.natDegree ≤ O
Module: Mathlib.Algebra.Polynomial.Reverse

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

Tactic:
| succ cg hcg =>

Goal state after:
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
⊢ reflect (N + O) (f * g) = reflect N f * reflect O g

pp: case neg
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
⊢ reflect (N + O) (f * g) = reflect N f * reflect O g

Tactic:
·

Goal state after:
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
⊢ reflect (N + O) (f * g) = reflect N f * reflect O g
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
hd₁ : n < ((X - C x) * P).eraseLead.natDegree
⊢ ¬((X - C x) * P).natDegree = n

Tactic:
by lia

Goal state after:
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.coeff 1 = 0
⊢ False

pp: case refine_2
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree = 1
⊢ C (p.coeff 1) * X + C (p.coeff 0) = p

pp: case refine_3
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ (∃ a, a ≠ 0 ∧ ∃ b, C a * X + C b = p) → p.natDegree = 1

Tactic:
·

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

Goal state before:
pp: case neg.inl.zero
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
hn₂ : n = 0
⊢ ((X - C x) * (monomial P.natDegree) P.leadingCoeff).coeff 0 = 0

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
⊢ ((X - C x) * (monomial P.natDegree) P.leadingCoeff).coeff (n✝ + 1) = 0

Tactic:
·

Goal state after:
case neg.inl.zero
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
hn₂ : n = 0
⊢ ((X - C x) * (monomial P.natDegree) P.leadingCoeff).coeff 0 = 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
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
hn₂ : n = 0
x✝ : P.natDegree = 0
⊢ x = 0

Tactic:
by lia

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

Goal state before:
pp: case refine_2
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree = 1
⊢ C (p.coeff 1) * X + C (p.coeff 0) = p

pp: case refine_3
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ (∃ a, a ≠ 0 ∧ ∃ b, C a * X + C b = p) → p.natDegree = 1

Tactic:
·

Goal state after:
case refine_2
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree = 1
⊢ C (p.coeff 1) * X + C (p.coeff 0) = p
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case refine_2.zero
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree = 1
⊢ (C (p.coeff 1) * X + C (p.coeff 0)).coeff 0 = p.coeff 0

pp: case refine_2.succ.zero
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree = 1
⊢ (C (p.coeff 1) * X + C (p.coeff 0)).coeff (0 + 1) = p.coeff (0 + 1)

pp: case refine_2.succ.succ
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree = 1
n : ℕ
⊢ (C (p.coeff 1) * X + C (p.coeff 0)).coeff (n + 1 + 1) = p.coeff (n + 1 + 1)

Tactic:
·

Goal state after:
case refine_2.zero
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree = 1
⊢ (C (p.coeff 1) * X + C (p.coeff 0)).coeff 0 = p.coeff 0
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case refine_2.succ.zero
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree = 1
⊢ (C (p.coeff 1) * X + C (p.coeff 0)).coeff (0 + 1) = p.coeff (0 + 1)

pp: case refine_2.succ.succ
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree = 1
n : ℕ
⊢ (C (p.coeff 1) * X + C (p.coeff 0)).coeff (n + 1 + 1) = p.coeff (n + 1 + 1)

Tactic:
·

Goal state after:
case refine_2.succ.zero
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree = 1
⊢ (C (p.coeff 1) * X + C (p.coeff 0)).coeff (0 + 1) = p.coeff (0 + 1)
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
⊢ ((X - C x) * (monomial P.natDegree) P.leadingCoeff).coeff (n✝ + 1) = 0

Tactic:
·

Goal state after:
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
⊢ ((X - C x) * (monomial P.natDegree) P.leadingCoeff).coeff (n✝ + 1) = 0
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 : ℕ
⊢ (C (p.coeff 1) * X + C (p.coeff 0)).coeff (n + 1 + 1) = p.coeff (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 : ℕ
⊢ (C (p.coeff 1) * X + C (p.coeff 0)).coeff (n + 1 + 1) = p.coeff (n + 1 + 1)
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case refine_3
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ (∃ a, a ≠ 0 ∧ ∃ b, C a * X + C b = p) → p.natDegree = 1

Tactic:
·

Goal state after:
case refine_3
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ (∃ a, a ≠ 0 ∧ ∃ b, C a * X + C b = p) → p.natDegree = 1
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
hd₁ : n < ((X - C x) * P).eraseLead.natDegree
n✝ : ℕ
hn₂ : n = n✝ + 1
⊢ ¬P.natDegree = n✝

Tactic:
by lia

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
hd₁ : n < ((X - C x) * P).eraseLead.natDegree
n✝ : ℕ
hn₂ : n = n✝ + 1
⊢ ¬P.natDegree = n✝ + 1

Tactic:
by lia

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
⊢ (p.comp q).natDegree = p.natDegree * q.natDegree

pp: case neg
R : Type u
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
q0 : ¬q.natDegree = 0
⊢ (p.comp q).natDegree = p.natDegree * q.natDegree

Tactic:
·

Goal state after:
case pos
R : Type u
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
q0 : q.natDegree = 0
⊢ (p.comp q).natDegree = p.natDegree * q.natDegree
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case neg
R : Type u
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
q0 : ¬q.natDegree = 0
⊢ (p.comp q).natDegree = p.natDegree * q.natDegree

Tactic:
·

Goal state after:
case neg
R : Type u
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
q0 : ¬q.natDegree = 0
⊢ (p.comp q).natDegree = p.natDegree * q.natDegree
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
p0 : p = 0
⊢ (p.comp q).natDegree = p.natDegree * q.natDegree

pp: case neg
R : Type u
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
q0 : ¬q.natDegree = 0
p0 : ¬p = 0
⊢ (p.comp q).natDegree = p.natDegree * q.natDegree

Tactic:
·

Goal state after:
case pos
R : Type u
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
q0 : ¬q.natDegree = 0
p0 : p = 0
⊢ (p.comp q).natDegree = p.natDegree * q.natDegree
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case neg.inr
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.coeff n = ((X - C x) * P.eraseLead).coeff n

Tactic:
·

Goal state after:
case neg.inr
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.coeff n = ((X - C x) * P.eraseLead).coeff n
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case neg
R : Type u
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
q0 : ¬q.natDegree = 0
p0 : ¬p = 0
⊢ (p.comp q).natDegree = p.natDegree * q.natDegree

Tactic:
·

Goal state after:
case neg
R : Type u
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
q0 : ¬q.natDegree = 0
p0 : ¬p = 0
⊢ (p.comp q).natDegree = p.natDegree * q.natDegree