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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
h0 : p.comp q = 0
⊢ (p.comp q).natDegree ≤ p.natDegree * q.natDegree

Tactic:
h0,

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
h0 : p.comp q = 0
⊢ natDegree 0 ≤ p.natDegree * q.natDegree
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

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

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

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.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
⊢ eval₂ φ (fun x ↦ a) ((uniqueAlgEquiv R σ).symm f) = Polynomial.eval₂ φ a f

Tactic:
by
  rw [eval₂_uniqueAlgEquiv_symm]

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

Goal state before:
pp: case pos
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Function.Injective ⇑f
p : R[X]
h✝ : p.natDegree = 0
⊢ 0 = f 0

pp: case neg
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Function.Injective ⇑f
p : R[X]
h✝ : ¬p.natDegree = 0
⊢ (map f p).coeff (p.natDegree - 1) = f (p.coeff (p.natDegree - 1))

Tactic:
<;>

Goal state after:
case pos
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Function.Injective ⇑f
p : R[X]
h✝ : p.natDegree = 0
⊢ 0 = f 0

case neg
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Function.Injective ⇑f
p : R[X]
h✝ : ¬p.natDegree = 0
⊢ (map f p).coeff (p.natDegree - 1) = f (p.coeff (p.natDegree - 1))
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.MvPolynomial.Equiv

Goal state before:
pp: case hC
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
i✝ : S₁
⊢ (((aeval fun o ↦ o.elim Polynomial.X fun s ↦ Polynomial.C (X s)).comp
            (Polynomial.aevalTower (rename Option.some) (X none))).comp
        CAlgHom)
      (X i✝) =
    ((AlgHom.id R (MvPolynomial S₁ R)[X]).comp CAlgHom) (X i✝)

pp: case hX
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n✝ : ℕ
⊢ (((aeval fun o ↦ o.elim Polynomial.X fun s ↦ Polynomial.C (X s)).comp
            (Polynomial.aevalTower (rename Option.some) (X none)))
          Polynomial.X).coeff
      n✝ =
    ((AlgHom.id R (MvPolynomial S₁ R)[X]) Polynomial.X).coeff n✝

Tactic:
<;>

Goal state after:
case hC
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
i✝ : S₁
⊢ (((aeval fun o ↦ o.elim Polynomial.X fun s ↦ Polynomial.C (X s)).comp
            (Polynomial.aevalTower (rename Option.some) (X none))).comp
        CAlgHom)
      (X i✝) =
    ((AlgHom.id R (MvPolynomial S₁ R)[X]).comp CAlgHom) (X i✝)

case hX
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n✝ : ℕ
⊢ (((aeval fun o ↦ o.elim Polynomial.X fun s ↦ Polynomial.C (X s)).comp
            (Polynomial.aevalTower (rename Option.some) (X none)))
          Polynomial.X).coeff
      n✝ =
    ((AlgHom.id R (MvPolynomial S₁ R)[X]) Polynomial.X).coeff n✝
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case none
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
m✝ : Option S₁ →₀ ℕ
⊢ coeff m✝
      (((Polynomial.aevalTower (rename Option.some) (X none)).comp
          (aeval fun o ↦ o.elim Polynomial.X fun s ↦ Polynomial.C (X s)))
        (X none)) =
    coeff m✝ ((AlgHom.id R (MvPolynomial (Option S₁) R)) (X none))

pp: case some
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
m✝ : Option S₁ →₀ ℕ
val✝ : S₁
⊢ coeff m✝
      (((Polynomial.aevalTower (rename Option.some) (X none)).comp
          (aeval fun o ↦ o.elim Polynomial.X fun s ↦ Polynomial.C (X s)))
        (X (Option.some val✝))) =
    coeff m✝ ((AlgHom.id R (MvPolynomial (Option S₁) R)) (X (Option.some val✝)))

Tactic:
<;>

Goal state after:
case none
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
m✝ : Option S₁ →₀ ℕ
⊢ coeff m✝
      (((Polynomial.aevalTower (rename Option.some) (X none)).comp
          (aeval fun o ↦ o.elim Polynomial.X fun s ↦ Polynomial.C (X s)))
        (X none)) =
    coeff m✝ ((AlgHom.id R (MvPolynomial (Option S₁) R)) (X none))

case some
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
m✝ : Option S₁ →₀ ℕ
val✝ : S₁
⊢ coeff m✝
      (((Polynomial.aevalTower (rename Option.some) (X none)).comp
          (aeval fun o ↦ o.elim Polynomial.X fun s ↦ Polynomial.C (X s)))
        (X (Option.some val✝))) =
    coeff m✝ ((AlgHom.id R (MvPolynomial (Option S₁) R)) (X (Option.some val✝)))
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: case neg.Cf
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
⊢ #(C f.leadingCoeff * X ^ f.natDegree).support ≤ cf.succ

pp: case neg.Nf
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
⊢ (C f.leadingCoeff * X ^ f.natDegree).natDegree ≤ N

pp: case neg.Cf
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
⊢ #f.eraseLead.support ≤ cf.succ

pp: case neg.Nf
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
⊢ f.eraseLead.natDegree ≤ N

Tactic:
<;>

Goal state after:
case neg.Cf
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
⊢ #(C f.leadingCoeff * X ^ f.natDegree).support ≤ cf.succ

case neg.Nf
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
⊢ (C f.leadingCoeff * X ^ f.natDegree).natDegree ≤ N

case neg.Cf
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
⊢ #f.eraseLead.support ≤ cf.succ

case neg.Nf
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
⊢ f.eraseLead.natDegree ≤ N
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).eraseLead.eraseLead.coeff n = 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
⊢ 0 = ((X - C x) * P.eraseLead).coeff 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.coeff n = 0

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

Goal state before:
pp: case pos
R : Type u
inst✝¹ : Semiring R
p : R[X]
a : R
inst✝ : NoZeroDivisors R
h₀ : a = 0
⊢ (C a * p).nextCoeff = a * p.nextCoeff

pp: case neg
R : Type u
inst✝¹ : Semiring R
p : R[X]
a : R
inst✝ : NoZeroDivisors R
h₀ : ¬a = 0
⊢ (C a * p).nextCoeff = a * p.nextCoeff

Tactic:
<;>

Goal state after:
case pos
R : Type u
inst✝¹ : Semiring R
p : R[X]
a : R
inst✝ : NoZeroDivisors R
h₀ : a = 0
⊢ (C a * p).nextCoeff = a * p.nextCoeff

case neg
R : Type u
inst✝¹ : Semiring R
p : R[X]
a : R
inst✝ : NoZeroDivisors R
h₀ : ¬a = 0
⊢ (C a * p).nextCoeff = a * p.nextCoeff
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case pos
R : Type u
inst✝¹ : Semiring R
p : R[X]
a : R
inst✝ : NoZeroDivisors R
h₀ : a = 0
⊢ (p * C a).nextCoeff = p.nextCoeff * a

pp: case neg
R : Type u
inst✝¹ : Semiring R
p : R[X]
a : R
inst✝ : NoZeroDivisors R
h₀ : ¬a = 0
⊢ (p * C a).nextCoeff = p.nextCoeff * a

Tactic:
<;>

Goal state after:
case pos
R : Type u
inst✝¹ : Semiring R
p : R[X]
a : R
inst✝ : NoZeroDivisors R
h₀ : a = 0
⊢ (p * C a).nextCoeff = p.nextCoeff * a

case neg
R : Type u
inst✝¹ : Semiring R
p : R[X]
a : R
inst✝ : NoZeroDivisors R
h₀ : ¬a = 0
⊢ (p * C a).nextCoeff = p.nextCoeff * a
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:
· rw [MvPolynomial.monomial_eq, ← Polynomial.C_mul_X_pow_eq_monomial]
    simp only [Polynomial.algebraMap_apply, algebraMap_eq, Option.elim_none, Option.elim_some,
      map_mul, mul_assoc]
    simp only [mul_comm, map_finsuppProd, map_pow]

Goal state after:
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 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.Polynomial.EraseLead

Goal state before:
pp: case succ.zero
R : Type u_1
inst✝ : Semiring R
motive : R[X] → Prop
N : ℕ
zero : motive 0
C_mul_pow : ∀ (n : ℕ) (r : R), r ≠ 0 → n ≤ N → motive (C r * X ^ n)
add : ∀ (f g : R[X]), f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)
f : R[X]
df : f.natDegree ≤ N
hc : ∀ (f : R[X]), f.natDegree ≤ N → #f.support = 0 → motive f
hf : #f.support = 0 + 1
⊢ f.leadingCoeff ≠ 0

Tactic:
rw [leadingCoeff_ne_zero, Ne, ← card_support_eq_zero, hf]

Goal state after:
case succ.zero
R : Type u_1
inst✝ : Semiring R
motive : R[X] → Prop
N : ℕ
zero : motive 0
C_mul_pow : ∀ (n : ℕ) (r : R), r ≠ 0 → n ≤ N → motive (C r * X ^ n)
add : ∀ (f g : R[X]), f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)
f : R[X]
df : f.natDegree ≤ N
hc : ∀ (f : R[X]), f.natDegree ≤ N → #f.support = 0 → motive f
hf : #f.support = 0 + 1
⊢ ¬0 + 1 = 0
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case pos
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
p : MvPolynomial (Option S₁) R
i : ℕ
hi : i ≤ p.totalDegree
hpi : ((optionEquivLeft R S₁) p).coeff i = 0
⊢ (((optionEquivLeft R S₁) p).coeff i).totalDegree + i ≤ p.totalDegree

Tactic:
rw [hpi]

Goal state after:
case pos
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
p : MvPolynomial (Option S₁) R
i : ℕ
hi : i ≤ p.totalDegree
hpi : ((optionEquivLeft R S₁) p).coeff i = 0
⊢ totalDegree 0 + i ≤ p.totalDegree
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
b : R
hp : b * p.leadingCoeff = 1
a✝ : Nontrivial R
⊢ (C b).leadingCoeff * p.leadingCoeff = 1

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

Tactic:
<;>

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
b : R
hp : b * p.leadingCoeff = 1
a✝ : Nontrivial R
⊢ (C b).leadingCoeff * p.leadingCoeff = 1

R : Type u
inst✝ : Semiring R
p : R[X]
b : R
hp : b * p.leadingCoeff = 1
a✝ : Nontrivial R
⊢ (C b).leadingCoeff * p.leadingCoeff ≠ 0
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
b : R
hp : p.leadingCoeff * b = 1
a✝ : Nontrivial R
⊢ p.leadingCoeff * (C b).leadingCoeff = 1

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

Tactic:
<;>

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
b : R
hp : p.leadingCoeff * b = 1
a✝ : Nontrivial R
⊢ p.leadingCoeff * (C b).leadingCoeff = 1

R : Type u
inst✝ : Semiring R
p : R[X]
b : R
hp : p.leadingCoeff * b = 1
a✝ : Nontrivial R
⊢ p.leadingCoeff * (C b).leadingCoeff ≠ 0
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case pos
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
p : MvPolynomial (Option S₁) R
i : ℕ
hpi : ((optionEquivLeft R S₁) p).coeff i = 0
⊢ (((optionEquivLeft R S₁) p).coeff i).totalDegree ≤ p.totalDegree

Tactic:
rw [hpi]

Goal state after:
case pos
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
p : MvPolynomial (Option S₁) R
i : ℕ
hpi : ((optionEquivLeft R S₁) p).coeff i = 0
⊢ totalDegree 0 ≤ p.totalDegree
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case e_m
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial (Option σ) R
m : ℕ
d : σ →₀ ℕ
⊢ d = (optionElim m d).some

pp: case e_a
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial (Option σ) R
m : ℕ
d : σ →₀ ℕ
⊢ m = (optionElim m d) none

Tactic:
<;>

Goal state after:
case e_m
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial (Option σ) R
m : ℕ
d : σ →₀ ℕ
⊢ d = (optionElim m d).some

case e_a
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial (Option σ) R
m : ℕ
d : σ →₀ ℕ
⊢ m = (optionElim m d) none
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case h₁
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
⊢ (((aeval fun o ↦ o.elim (C Polynomial.X) X).comp
            (aevalTower (Polynomial.aeval (X none)) fun i ↦ X (Option.some i))).comp
        (IsScalarTower.toAlgHom R R[X] (MvPolynomial S₁ R[X])))
      Polynomial.X =
    ((AlgHom.id R (MvPolynomial S₁ R[X])).comp (IsScalarTower.toAlgHom R R[X] (MvPolynomial S₁ R[X]))) Polynomial.X

pp: case h₂
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
i✝ : S₁
m✝ : S₁ →₀ ℕ
⊢ coeff m✝
      (((aeval fun o ↦ o.elim (C Polynomial.X) X).comp
          (aevalTower (Polynomial.aeval (X none)) fun i ↦ X (Option.some i)))
        (X i✝)) =
    coeff m✝ ((AlgHom.id R (MvPolynomial S₁ R[X])) (X i✝))

Tactic:
<;>

Goal state after:
case h₁
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
⊢ (((aeval fun o ↦ o.elim (C Polynomial.X) X).comp
            (aevalTower (Polynomial.aeval (X none)) fun i ↦ X (Option.some i))).comp
        (IsScalarTower.toAlgHom R R[X] (MvPolynomial S₁ R[X])))
      Polynomial.X =
    ((AlgHom.id R (MvPolynomial S₁ R[X])).comp (IsScalarTower.toAlgHom R R[X] (MvPolynomial S₁ R[X]))) Polynomial.X

case h₂
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
i✝ : S₁
m✝ : S₁ →₀ ℕ
⊢ coeff m✝
      (((aeval fun o ↦ o.elim (C Polynomial.X) X).comp
          (aevalTower (Polynomial.aeval (X none)) fun i ↦ X (Option.some i)))
        (X i✝)) =
    coeff m✝ ((AlgHom.id R (MvPolynomial S₁ R[X])) (X i✝))
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case none
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
m✝ : Option S₁ →₀ ℕ
⊢ coeff m✝
      (((aevalTower (Polynomial.aeval (X none)) fun i ↦ X (Option.some i)).comp
          (aeval fun o ↦ o.elim (C Polynomial.X) X))
        (X none)) =
    coeff m✝ ((AlgHom.id R (MvPolynomial (Option S₁) R)) (X none))

pp: case some
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
val✝ : S₁
m✝ : Option S₁ →₀ ℕ
⊢ coeff m✝
      (((aevalTower (Polynomial.aeval (X none)) fun i ↦ X (Option.some i)).comp
          (aeval fun o ↦ o.elim (C Polynomial.X) X))
        (X (Option.some val✝))) =
    coeff m✝ ((AlgHom.id R (MvPolynomial (Option S₁) R)) (X (Option.some val✝)))

Tactic:
<;>

Goal state after:
case none
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
m✝ : Option S₁ →₀ ℕ
⊢ coeff m✝
      (((aevalTower (Polynomial.aeval (X none)) fun i ↦ X (Option.some i)).comp
          (aeval fun o ↦ o.elim (C Polynomial.X) X))
        (X none)) =
    coeff m✝ ((AlgHom.id R (MvPolynomial (Option S₁) R)) (X none))

case some
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
val✝ : S₁
m✝ : Option S₁ →₀ ℕ
⊢ coeff m✝
      (((aevalTower (Polynomial.aeval (X none)) fun i ↦ X (Option.some i)).comp
          (aeval fun o ↦ o.elim (C Polynomial.X) X))
        (X (Option.some val✝))) =
    coeff m✝ ((AlgHom.id R (MvPolynomial (Option S₁) R)) (X (Option.some val✝)))