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

Goal state before:
pp: case succ
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)
c : ℕ
hc : ∀ (f : R[X]), f.natDegree ≤ N → #f.support = c → motive f
f : R[X]
df : f.natDegree ≤ N
hf : #f.support = c + 1
⊢ motive (f.eraseLead + C f.leadingCoeff * X ^ f.natDegree)

Tactic:
]

Goal state after:
case succ
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)
c : ℕ
hc : ∀ (f : R[X]), f.natDegree ≤ N → #f.support = c → motive f
f : R[X]
df : f.natDegree ≤ N
hf : #f.support = c + 1
⊢ motive (f.eraseLead + C f.leadingCoeff * X ^ f.natDegree)
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

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

Tactic:
]

Goal state after:
case inl
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h : C (p.coeff 0) = 0
key✝ : p.natDegree = 0 ∨ q.natDegree = 0
key : p = C (p.coeff 0)
⊢ p = 0 ∨ eval (q.coeff 0) p = 0 ∧ q = C (q.coeff 0)
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

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

Tactic:
]

Goal state after:
case inr
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h : eval (q.coeff 0) p = 0
key✝ : p.natDegree = 0 ∨ q.natDegree = 0
key : q = C (q.coeff 0)
⊢ p = 0 ∨ eval (q.coeff 0) p = 0 ∧ q = C (q.coeff 0)
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: 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 = 0

Tactic:
]

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

Goal state before:
pp: case inl
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
q : R[X]
hq : 0 < q.degree
⊢ ⊥ = if q.degree = 0 then 0 else ⊥

Tactic:
]

Goal state after:
case inl
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
q : R[X]
hq : 0 < q.degree
⊢ ⊥ = if q.degree = 0 then 0 else ⊥
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
S₁ : Type v
inst✝ : CommSemiring R
s : S₁ → R
y : R
f : MvPolynomial (Option S₁) R
φ : (MvPolynomial S₁ R)[X] →ₐ[R] R[X] :=
  let __src := Polynomial.mapRingHom (eval s);
  { toRingHom := __src, commutes' := ⋯ }
⊢ (aeval fun x ↦ x.elim y s) (X none) = ((Polynomial.aeval y).comp (φ.comp ↑(optionEquivLeft R S₁))) (X none) ∧
    ∀ (x : S₁),
      (aeval fun x ↦ x.elim y s) (X (Option.some x)) =
        ((Polynomial.aeval y).comp (φ.comp ↑(optionEquivLeft R S₁))) (X (Option.some x))

Tactic:
]

Goal state after:
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
s : S₁ → R
y : R
f : MvPolynomial (Option S₁) R
φ : (MvPolynomial S₁ R)[X] →ₐ[R] R[X] :=
  let __src := Polynomial.mapRingHom (eval s);
  { toRingHom := __src, commutes' := ⋯ }
⊢ (aeval fun x ↦ x.elim y s) (X none) = ((Polynomial.aeval y).comp (φ.comp ↑(optionEquivLeft R S₁))) (X none) ∧
    ∀ (x : S₁),
      (aeval fun x ↦ x.elim y s) (X (Option.some x)) =
        ((Polynomial.aeval y).comp (φ.comp ↑(optionEquivLeft R S₁))) (X (Option.some x))
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
⊢ ¬0 + 1 = 0

Tactic:
]

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.Polynomial.Degree.Lemmas

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

Tactic:
]

Goal state after:
case inr
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hq : 0 < q.degree
hp : p ≠ 0
⊢ (p.comp q).degree = ↑(p.comp q).natDegree
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: case refine_2
R : Type u_1
inst✝² : Semiring R
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
n : ℕ
r : R
a✝ : r ≠ 0
hnN : n ≤ N
⊢ i r * x ^ n = i r * x ^ n

Tactic:
]

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

Goal state before:
pp: case inl
R : Type u
inst✝ : Ring R
a✝ : Nontrivial R
⊢ degree 0 = degree 0

Tactic:
]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial (Option σ) R
h : f ≠ 0
⊢ f ≠ 0

Tactic:
]

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial (Option σ) R
h : f ≠ 0
⊢ f ≠ 0
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial (Option σ) R
h : f ≠ 0
⊢ (f.support.sup fun x ↦ x none) = f.support.sup fun m ↦ m none

Tactic:
]

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

Goal state before:
pp: case inr
R : Type u
inst✝ : Ring R
p : R[X]
a✝ : Nontrivial R
hp : p ≠ 0
⊢ p.natDegree = p.natDegree

Tactic:
]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial (Option σ) R
h : f ≠ 0
h' : (((optionEquivLeft R σ) f).support.sup fun x ↦ x) = degreeOf none f
⊢ ((optionEquivLeft R σ) f).support.sup WithBot.some = ((optionEquivLeft R σ) f).support.sup fun x ↦ ↑x

Tactic:
]

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

Goal state before:
pp: case succ.succ.refine_1.refine_2
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
n✝ : ℕ
hc : ∀ (f : R[X]), f.natDegree ≤ N → #f.support = n✝ + 1 → motive f
hf : #f.support = n✝ + 1 + 1
⊢ f.natDegree = f.natDegree

pp: 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
n✝ : ℕ
hc : ∀ (f : R[X]), f.natDegree ≤ N → #f.support = n✝ + 1 → motive f
hf : #f.support = n✝ + 1 + 1
⊢ f ≠ 0

Tactic:
]

Goal state after:
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
n✝ : ℕ
hc : ∀ (f : R[X]), f.natDegree ≤ N → #f.support = n✝ + 1 → motive f
hf : #f.support = n✝ + 1 + 1
⊢ f ≠ 0
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case pos
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial (Option σ) R
c : p = 0
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: K : Type u_1
inst✝ : DivisionRing K
p : K[X]
h : p ≠ 0
⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: case neg
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial (Option σ) R
c : ¬p = 0
⊢ degreeOf none p = degreeOf none p

Tactic:
]

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

Goal state before:
pp: K : Type u_1
inst✝ : DivisionRing K
p q : K[X]
h : q ≠ 0
h₁ : q.leadingCoeff⁻¹ ≠ 0
⊢ p.degree = p.degree

Tactic:
]

Goal state after:
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
⊢ totalDegree 0 + i ≤ p.totalDegree

Tactic:
]

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.Degree.Lemmas

Goal state before:
pp: K : Type u_1
inst✝ : DivisionRing K
p : K[X]
⊢ p.degree = p.degree

Tactic:
]

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

Goal state before:
pp: case neg
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
⊢ ∀ b ∈ (((optionEquivLeft R S₁) p).coeff i).support, (i + b.sum fun x e ↦ e) ≤ p.totalDegree

Tactic:
]

Goal state after:
case neg
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
⊢ ∀ b ∈ (((optionEquivLeft R S₁) p).coeff i).support, (i + b.sum fun x e ↦ e) ≤ p.totalDegree
Module: Mathlib.Algebra.Polynomial.Monic

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

Tactic:
]

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

Goal state before:
pp: case mp
R : Type u_1
inst✝² : Semiring R
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
h : eval₂ i (⅟x) (reflect N f) = 0
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
H : p.degree < ↑n
⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: case succ.succ.refine_4
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
n✝ : ℕ
hc : ∀ (f : R[X]), f.natDegree ≤ N → #f.support = n✝ + 1 → motive f
hf : #f.support = n✝ + 1 + 1
⊢ ¬n✝ + 1 + 1 = 0

Tactic:
]

Goal state after:
case succ.succ.refine_4
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
n✝ : ℕ
hc : ∀ (f : R[X]), f.natDegree ≤ N → #f.support = n✝ + 1 → motive f
hf : #f.support = n✝ + 1 + 1
⊢ ¬n✝ + 1 + 1 = 0
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
this : DecidableEq R := Classical.decEq R
h0 : ¬0 = 1
⊢ (p * q).Monic

Tactic:
have : p.leadingCoeff * q.leadingCoeff ≠ 0 := by
      simp [Monic.def.1 hp, Monic.def.1 hq, Ne.symm h0]

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
this✝ : DecidableEq R := Classical.decEq R
h0 : ¬0 = 1
this : p.leadingCoeff * q.leadingCoeff ≠ 0
⊢ (p * q).Monic
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
this✝ : DecidableEq R := Classical.decEq R
h0 : ¬0 = 1
this : p.leadingCoeff * q.leadingCoeff ≠ 0
⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
n : ℕ
⊢ (p ^ n * p).Monic

Tactic:
]

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
n : ℕ
⊢ (p ^ n * p).Monic
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hpq : q.degree < p.degree
⊢ p.leadingCoeff = 1

Tactic:
]

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hpq : q.degree < p.degree
⊢ p.leadingCoeff = 1
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hq : q.Monic
hpq : p.degree < q.degree
⊢ q.leadingCoeff = 1

Tactic:
]

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
hq : q.Monic
hpq : p.degree < q.degree
⊢ q.leadingCoeff = 1
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hpq : ¬q.leadingCoeff = 1
⊢ ¬(p * q).leadingCoeff = 1

Tactic:
]

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hpq : ¬q.leadingCoeff = 1
⊢ ¬(p * q).leadingCoeff = 1
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hpq : ¬q.leadingCoeff = 1
⊢ ¬q.leadingCoeff = 1

Tactic:
]

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hpq : ¬q.leadingCoeff = 1
⊢ ¬q.leadingCoeff = 1
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hq : q.Monic
hpq : ¬p.leadingCoeff = 1
⊢ ¬(p * q).leadingCoeff = 1

Tactic:
]

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
hq : q.Monic
hpq : ¬p.leadingCoeff = 1
⊢ ¬(p * q).leadingCoeff = 1
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hq : q.Monic
hpq : ¬p.leadingCoeff = 1
⊢ ¬p.leadingCoeff = 1

Tactic:
]

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
hq : q.Monic
hpq : ¬p.leadingCoeff = 1
⊢ ¬p.leadingCoeff = 1
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: case mpr
R : Type u_1
inst✝² : Semiring R
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
h : eval₂ i (⅟x) (reflect N f) * x ^ N = 0
⊢ 0 = 0

Tactic:
]

Goal state after:
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
⊢ totalDegree 0 ≤ p.totalDegree

Tactic:
]

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.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
h : q.natDegree ≠ 0
a✝ : Nontrivial R
this : (p.comp q).natDegree = p.natDegree * q.natDegree
⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
r : R
a✝ : Nontrivial R
ha : 1 = 0
⊢ False

Tactic:
]

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
r : R
a✝ : Nontrivial R
ha : 1 = 0
⊢ False
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
⊢ p.degree ≤ 0 ↔ p.degree ≤ 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
p : MvPolynomial (Option S₁) R
i : ℕ
hpi : ¬((optionEquivLeft R S₁) p).coeff i = 0
⊢ ∀ b ∈ (((optionEquivLeft R S₁) p).coeff i).support, (b.sum fun x e ↦ e) ≤ p.totalDegree

Tactic:
]

Goal state after:
case neg
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
p : MvPolynomial (Option S₁) R
i : ℕ
hpi : ¬((optionEquivLeft R S₁) p).coeff i = 0
⊢ ∀ b ∈ (((optionEquivLeft R S₁) p).coeff i).support, (b.sum fun x e ↦ e) ≤ p.totalDegree
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
n : ℕ
⊢ f.coeff ((revAt f.natDegree) n) = f.coeff ((revAt f.natDegree) n)

Tactic:
]

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

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
h : ¬q = 0
⊢ p.degree + q.degree = q.degree + p.degree

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

Tactic:
]

Goal state after:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
h : ¬q = 0
⊢ p.degree + q.degree = q.degree + p.degree

case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
h : ¬q = 0
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
h : ¬q = 0
⊢ q ≠ 0

Tactic:
]

Goal state after:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
h : ¬q = 0
⊢ q ≠ 0
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ f.coeff f.natDegree = f.coeff f.natDegree

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hq : q ≠ 0
⊢ p.natDegree + q.natDegree = p.natDegree + q.natDegree

pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hq : q ≠ 0
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0

Tactic:
]

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hq : q ≠ 0
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ ∀ (m : ℕ), ↑f.natDegree < ↑m → f.reverse.coeff m = 0

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ ∀ (m : ℕ), ↑f.natDegree < ↑m → f.reverse.coeff m = 0
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
n : ℕ
hn : f.natDegree < n
⊢ f.reverse.coeff n = 0

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : R[X]
n : ℕ
hn : f.natDegree < n
⊢ f.reverse.coeff n = 0
Module: Mathlib.Algebra.MvPolynomial.Equiv

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

Tactic:
]

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial (Option σ) R
m : ℕ
d : σ →₀ ℕ
⊢ coeff d (((optionEquivLeft R σ) p).coeff m) =
    coeff (optionElim m d).some (((optionEquivLeft R σ) p).coeff ((optionElim m d) none))
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
n : ℕ
hn : f.natDegree < n
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
h : ¬q = 0
⊢ q.natDegree + p.natDegree = q.natDegree + p.natDegree

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

Tactic:
]

Goal state after:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
h : ¬q = 0
⊢ q.leadingCoeff * p.leadingCoeff ≠ 0
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : f = 0
⊢ 0 = 0 + 0

Tactic:
]

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

Goal state before:
pp: case neg.a
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : ¬f = 0
⊢ f.coeff f.natTrailingDegree ≠ 0

Tactic:
]

Goal state after:
case neg.a
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : ¬f = 0
⊢ f.coeff f.natTrailingDegree ≠ 0
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: case a
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : ¬f = 0
⊢ f.natTrailingDegree ≤ f.natDegree - f.reverse.natDegree

Tactic:
]

Goal state after:
case a
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : ¬f = 0
⊢ f.natTrailingDegree ≤ f.natDegree - f.reverse.natDegree
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case refine_1
R : Type u_1
inst✝³ : Semiring R
S : Type u_2
F : Type u_3
inst✝² : Semiring S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : AddMonoidHomClass F R[X] S[X]
φ : F
p : R[X]
k : ℕ
fu : ℕ → ℕ
fu0 : ∀ {n : ℕ}, n ≤ k → fu n = 0
fc : ∀ {n m : ℕ}, k ≤ n → n < m → fu n < fu m
φ_k : ∀ {f : R[X]}, f.natDegree < k → φ f = 0
φ_mon_nat : ∀ (n : ℕ) (c : R), c ≠ 0 → (φ ((monomial n) c)).natDegree = fu n
n : ℕ
r : R
r0 : r ≠ 0
a✝ : n ≤ p.natDegree
⊢ fu n = fu n

Tactic:
]

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

Goal state before:
pp: case a
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : ¬f = 0
key : ¬f.coeff (f.natDegree - f.reverse.natDegree) = 0
⊢ f.coeff (f.natDegree - f.reverse.natDegree) ≠ 0

Tactic:
]

Goal state after:
case a
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : ¬f = 0
key : ¬f.coeff (f.natDegree - f.reverse.natDegree) = 0
⊢ f.coeff (f.natDegree - f.reverse.natDegree) ≠ 0
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
a : R
g : R[X]
hfg : (X + C a) * g = 1
hgf : g * (X + C a) = 1
h : 0 = 1 + g.natDegree
⊢ False

Tactic:
]

Goal state after:
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
a : R
g : R[X]
hfg : (X + C a) * g = 1
hgf : g * (X + C a) = 1
h : 0 = 1 + g.natDegree
⊢ False
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ f.reverse.natDegree = f.reverse.natDegree

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
⊢ (finSuccEquiv R n) p = (finSuccEquiv R n) p

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n : ℕ
x : R
⊢ ↑(finSuccEquiv R n).symm ((Polynomial.C.comp C) x) = C x

Tactic:
]

Goal state after:
R : Type u
inst✝ : CommSemiring R
n : ℕ
x : R
⊢ ↑(finSuccEquiv R n).symm ((Polynomial.C.comp C) x) = C x