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

Goal state before:
pp: case a
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
⊢ (p + q).totalDegree ≤ p.totalDegree

pp: case a
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
⊢ p.totalDegree ≤ (p + q).totalDegree

Tactic:
·

Goal state after:
case a
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
⊢ (p + q).totalDegree ≤ p.totalDegree
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: case monomial_add.refine_1
R : Type u
σ : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
subS : Type u_3
inst✝² : CommSemiring S
inst✝¹ : SetLike subS S
inst✝ : SubsemiringClass subS S
f✝ : R →+* S
s : subS
v : σ → S
hv : ∀ (i : σ), v i ∈ s
a : σ →₀ ℕ
b : R
f : MvPolynomial σ R
ha : a ∉ f.coeff.support
a✝ : b ≠ 0
ih : (∀ (i : σ →₀ ℕ), f✝ (coeff i f) ∈ s) → eval₂ f✝ v f ∈ s
hs : ∀ (i : σ →₀ ℕ), f✝ (coeff i ((monomial a) b + f)) ∈ s
⊢ f✝ b ∈ s

pp: case monomial_add.refine_2
R : Type u
σ : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
subS : Type u_3
inst✝² : CommSemiring S
inst✝¹ : SetLike subS S
inst✝ : SubsemiringClass subS S
f✝ : R →+* S
s : subS
v : σ → S
hv : ∀ (i : σ), v i ∈ s
a : σ →₀ ℕ
b : R
f : MvPolynomial σ R
ha : a ∉ f.coeff.support
a✝ : b ≠ 0
ih : (∀ (i : σ →₀ ℕ), f✝ (coeff i f) ∈ s) → eval₂ f✝ v f ∈ s
hs : ∀ (i : σ →₀ ℕ), f✝ (coeff i ((monomial a) b + f)) ∈ s
i : σ →₀ ℕ
⊢ f✝ (coeff i f) ∈ s

Tactic:
·

Goal state after:
case monomial_add.refine_1
R : Type u
σ : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
subS : Type u_3
inst✝² : CommSemiring S
inst✝¹ : SetLike subS S
inst✝ : SubsemiringClass subS S
f✝ : R →+* S
s : subS
v : σ → S
hv : ∀ (i : σ), v i ∈ s
a : σ →₀ ℕ
b : R
f : MvPolynomial σ R
ha : a ∉ f.coeff.support
a✝ : b ≠ 0
ih : (∀ (i : σ →₀ ℕ), f✝ (coeff i f) ∈ s) → eval₂ f✝ v f ∈ s
hs : ∀ (i : σ →₀ ℕ), f✝ (coeff i ((monomial a) b + f)) ∈ s
⊢ f✝ b ∈ s
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: case pos
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
hp : p = 0
⊢ p.totalDegree ≤ (p + q).totalDegree

pp: case neg
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
hp : ¬p = 0
⊢ p.totalDegree ≤ (p + q).totalDegree

Tactic:
·

Goal state after:
case pos
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
hp : p = 0
⊢ p.totalDegree ≤ (p + q).totalDegree
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: case pos
R : Type u
σ : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
subS : Type u_3
inst✝² : CommSemiring S
inst✝¹ : SetLike subS S
inst✝ : SubsemiringClass subS S
f✝ : R →+* S
s : subS
v : σ → S
hv : ∀ (i : σ), v i ∈ s
a : σ →₀ ℕ
b : R
f : MvPolynomial σ R
ha : a ∉ f.coeff.support
a✝ : b ≠ 0
ih : (∀ (i : σ →₀ ℕ), f✝ (coeff i f) ∈ s) → eval₂ f✝ v f ∈ s
hs : ∀ (i : σ →₀ ℕ), f✝ (coeff i ((monomial a) b + f)) ∈ s
i : σ →₀ ℕ
h : a = i
this : f✝ (b + coeff i f) ∈ s
⊢ f✝ (coeff i f) ∈ s

pp: case neg
R : Type u
σ : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
subS : Type u_3
inst✝² : CommSemiring S
inst✝¹ : SetLike subS S
inst✝ : SubsemiringClass subS S
f✝ : R →+* S
s : subS
v : σ → S
hv : ∀ (i : σ), v i ∈ s
a : σ →₀ ℕ
b : R
f : MvPolynomial σ R
ha : a ∉ f.coeff.support
a✝ : b ≠ 0
ih : (∀ (i : σ →₀ ℕ), f✝ (coeff i f) ∈ s) → eval₂ f✝ v f ∈ s
hs : ∀ (i : σ →₀ ℕ), f✝ (coeff i ((monomial a) b + f)) ∈ s
i : σ →₀ ℕ
h : ¬a = i
this : f✝ (0 + coeff i f) ∈ s
⊢ f✝ (coeff i f) ∈ s

Tactic:
·

Goal state after:
case pos
R : Type u
σ : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
subS : Type u_3
inst✝² : CommSemiring S
inst✝¹ : SetLike subS S
inst✝ : SubsemiringClass subS S
f✝ : R →+* S
s : subS
v : σ → S
hv : ∀ (i : σ), v i ∈ s
a : σ →₀ ℕ
b : R
f : MvPolynomial σ R
ha : a ∉ f.coeff.support
a✝ : b ≠ 0
ih : (∀ (i : σ →₀ ℕ), f✝ (coeff i f) ∈ s) → eval₂ f✝ v f ∈ s
hs : ∀ (i : σ →₀ ℕ), f✝ (coeff i ((monomial a) b + f)) ∈ s
i : σ →₀ ℕ
h : a = i
this : f✝ (b + coeff i f) ∈ s
⊢ f✝ (coeff i f) ∈ s
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial σ R
i : σ
d : σ →₀ ℕ
hd : d ∈ f.support
⊢ d i = 0 → d i ≤ f.totalDegree

Tactic:
by lia

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial σ R
i : σ
d : σ →₀ ℕ
hd : d ∈ f.support
h : d i ≠ 0
⊢ ∀ i ∈ d.support, 0 ≤ d i

Tactic:
by lia

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

Goal state before:
pp: case neg
R : Type u
σ : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
subS : Type u_3
inst✝² : CommSemiring S
inst✝¹ : SetLike subS S
inst✝ : SubsemiringClass subS S
f✝ : R →+* S
s : subS
v : σ → S
hv : ∀ (i : σ), v i ∈ s
a : σ →₀ ℕ
b : R
f : MvPolynomial σ R
ha : a ∉ f.coeff.support
a✝ : b ≠ 0
ih : (∀ (i : σ →₀ ℕ), f✝ (coeff i f) ∈ s) → eval₂ f✝ v f ∈ s
hs : ∀ (i : σ →₀ ℕ), f✝ (coeff i ((monomial a) b + f)) ∈ s
i : σ →₀ ℕ
h : ¬a = i
this : f✝ (0 + coeff i f) ∈ s
⊢ f✝ (coeff i f) ∈ s

Tactic:
·

Goal state after:
case neg
R : Type u
σ : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
subS : Type u_3
inst✝² : CommSemiring S
inst✝¹ : SetLike subS S
inst✝ : SubsemiringClass subS S
f✝ : R →+* S
s : subS
v : σ → S
hv : ∀ (i : σ), v i ∈ s
a : σ →₀ ℕ
b : R
f : MvPolynomial σ R
ha : a ∉ f.coeff.support
a✝ : b ≠ 0
ih : (∀ (i : σ →₀ ℕ), f✝ (coeff i f) ∈ s) → eval₂ f✝ v f ∈ s
hs : ∀ (i : σ →₀ ℕ), f✝ (coeff i ((monomial a) b + f)) ∈ s
i : σ →₀ ℕ
h : ¬a = i
this : f✝ (0 + coeff i f) ∈ s
⊢ f✝ (coeff i f) ∈ s
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
h : ∀ b ∈ f.support, (b.sum fun x e ↦ e) < ∑ i ∈ d.support, d i
⊢ coeff d f = 0

pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
h : (f.support.sup fun s ↦ s.sum fun x e ↦ e) < ∑ i ∈ d.support, d i
⊢ ⊥ < ∑ i ∈ d.support, d i

Tactic:
·

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
h : ∀ b ∈ f.support, (b.sum fun x e ↦ e) < ∑ i ∈ d.support, d i
⊢ coeff d f = 0
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
h : (f.support.sup fun s ↦ s.sum fun x e ↦ e) < ∑ i ∈ d.support, d i
⊢ ⊥ < ∑ i ∈ d.support, d i

Tactic:
·

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
h : (f.support.sup fun s ↦ s.sum fun x e ↦ e) < ∑ i ∈ d.support, d i
⊢ ⊥ < ∑ i ∈ d.support, d i
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: case mp
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : p.totalDegree = 0
⊢ p = C (coeff 0 p)

pp: case mpr
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : p = C (coeff 0 p)
⊢ p.totalDegree = 0

Tactic:
·

Goal state after:
case mp
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : p.totalDegree = 0
⊢ p = C (coeff 0 p)
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: case pos
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : p.totalDegree = 0
m : σ →₀ ℕ
hm : 0 = m
⊢ coeff m p = coeff 0 p

pp: case neg
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : p.totalDegree = 0
m : σ →₀ ℕ
hm : ¬0 = m
⊢ coeff m p = 0

Tactic:
·

Goal state after:
case pos
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : p.totalDegree = 0
m : σ →₀ ℕ
hm : 0 = m
⊢ coeff m p = coeff 0 p
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: case mpr
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : p = C (coeff 0 p)
⊢ p.totalDegree = 0

Tactic:
·

Goal state after:
case mpr
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : p = C (coeff 0 p)
⊢ p.totalDegree = 0
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: case refine_1
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
f : τ → σ
hfi : Injective f
hf : ↑p.vars ⊆ range f
⊢ ((rename f).comp (aeval fun i ↦ Option.elim' 0 X (partialInv f i)).toRingHom).comp C =
    (RingHom.id (MvPolynomial σ R)).comp C

pp: case refine_2
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
f : τ → σ
hfi : Injective f
hf : ↑p.vars ⊆ range f
⊢ ∀ i ∈ p.vars,
    i ∈ p.vars →
      ((rename f).comp (aeval fun i ↦ Option.elim' 0 X (partialInv f i)).toRingHom) (X i) =
        (RingHom.id (MvPolynomial σ R)) (X i)

pp: case refine_3
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
f : τ → σ
hfi : Injective f
hf : ↑p.vars ⊆ range f
⊢ p = p

Tactic:
·

Goal state after:
case refine_1
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
f : τ → σ
hfi : Injective f
hf : ↑p.vars ⊆ range f
⊢ ((rename f).comp (aeval fun i ↦ Option.elim' 0 X (partialInv f i)).toRingHom).comp C =
    (RingHom.id (MvPolynomial σ R)).comp C
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: case refine_2
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
f : τ → σ
hfi : Injective f
hf : ↑p.vars ⊆ range f
⊢ ∀ i ∈ p.vars,
    i ∈ p.vars →
      ((rename f).comp (aeval fun i ↦ Option.elim' 0 X (partialInv f i)).toRingHom) (X i) =
        (RingHom.id (MvPolynomial σ R)) (X i)

pp: case refine_3
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
f : τ → σ
hfi : Injective f
hf : ↑p.vars ⊆ range f
⊢ p = p

Tactic:
·

Goal state after:
case refine_2
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
f : τ → σ
hfi : Injective f
hf : ↑p.vars ⊆ range f
⊢ ∀ i ∈ p.vars,
    i ∈ p.vars →
      ((rename f).comp (aeval fun i ↦ Option.elim' 0 X (partialInv f i)).toRingHom) (X i) =
        (RingHom.id (MvPolynomial σ R)) (X i)
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: case refine_3
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
f : τ → σ
hfi : Injective f
hf : ↑p.vars ⊆ range f
⊢ p = p

Tactic:
·

Goal state after:
case refine_3
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
f : τ → σ
hfi : Injective f
hf : ↑p.vars ⊆ range f
⊢ p = p
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
x : MvPolynomial σ R
hx : x.degrees = 0
⊢ x ∈ 1

Tactic:
have := (totalDegree_eq_zero_iff_eq_C (p := x)).mp
    (Nat.eq_zero_of_le_zero (x.totalDegree_le_degrees_card.trans (by simp [hx])))

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
x : MvPolynomial σ R
hx : x.degrees = 0
this : x = C (coeff 0 x)
⊢ x ∈ 1
Module: Mathlib.Algebra.Polynomial.Degree.Monomial

Goal state before:
pp: case zero
R : Type u
inst✝ : Semiring R
p : R[X]
hf : p.natDegree ≤ 0
hn : p.coeff 0 = 0
⊢ p.natDegree ≤ 0 - 1

pp: case succ
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
hf : p.natDegree ≤ n + 1
hn : p.coeff (n + 1) = 0
⊢ p.natDegree ≤ n + 1 - 1

Tactic:
·

Goal state after:
case zero
R : Type u
inst✝ : Semiring R
p : R[X]
hf : p.natDegree ≤ 0
hn : p.coeff 0 = 0
⊢ p.natDegree ≤ 0 - 1
Module: Mathlib.Algebra.Polynomial.Degree.Monomial

Goal state before:
pp: case succ
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
hf : p.natDegree ≤ n + 1
hn : p.coeff (n + 1) = 0
⊢ p.natDegree ≤ n + 1 - 1

Tactic:
·

Goal state after:
case succ
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
hf : p.natDegree ≤ n + 1
hn : p.coeff (n + 1) = 0
⊢ p.natDegree ≤ n + 1 - 1
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ^ p.natDegree ≠ 0
hq : q.natDegree = 0
⊢ (p.comp q).natDegree = p.natDegree * q.natDegree

pp: case neg
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ^ p.natDegree ≠ 0
hq : ¬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]
h : p.leadingCoeff * q.leadingCoeff ^ p.natDegree ≠ 0
hq : q.natDegree = 0
⊢ (p.comp q).natDegree = p.natDegree * q.natDegree
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: case mp
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p.coeff p.natTrailingDegree = 0 → p = 0

pp: case mpr
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p = 0 → p.coeff p.natTrailingDegree = 0

Tactic:
·

Goal state after:
case mp
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p.coeff p.natTrailingDegree = 0 → p = 0
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: case mpr
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p = 0 → p.coeff p.natTrailingDegree = 0

Tactic:
·

Goal state after:
case mpr
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p = 0 → p.coeff p.natTrailingDegree = 0
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: case mpr
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p = 0 → p.coeff p.natTrailingDegree = 0

Tactic:
· rintro rfl
    simp

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

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

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

Tactic:
·

Goal state after:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : n < p.natTrailingDegree
hp : p = 0
⊢ ↑n < p.trailingDegree
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : n < p.natTrailingDegree
hp : ¬p = 0
⊢ ↑n < p.trailingDegree

Tactic:
·

Goal state after:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : n < p.natTrailingDegree
hp : ¬p = 0
⊢ ↑n < p.trailingDegree
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
h : p ≠ 0
⊢ ENat.toNat p.support.min = p.support.min' ⋯

Tactic:
← Finset.coe_min' (support_nonempty.mpr h)

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
h : p ≠ 0
⊢ ENat.toNat ↑(p.support.min' ⋯) = p.support.min' ⋯
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p = 0
⊢ p.natTrailingDegree ≤ p.natDegree

pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : ¬p = 0
⊢ p.natTrailingDegree ≤ p.natDegree

Tactic:
·

Goal state after:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p = 0
⊢ p.natTrailingDegree ≤ p.natDegree
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

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

Tactic:
·

Goal state after:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : ¬p = 0
⊢ p.natTrailingDegree ≤ p.natDegree
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: case a
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
n : ℕ
⊢ (p * X ^ n).natTrailingDegree ≤ p.natTrailingDegree + n

pp: case a
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
n : ℕ
⊢ p.natTrailingDegree + n ≤ (p * X ^ n).natTrailingDegree

Tactic:
·

Goal state after:
case a
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
n : ℕ
⊢ (p * X ^ n).natTrailingDegree ≤ p.natTrailingDegree + n
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: case a
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
n : ℕ
⊢ p.natTrailingDegree + n ≤ (p * X ^ n).natTrailingDegree

Tactic:
·

Goal state after:
case a
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
n : ℕ
⊢ p.natTrailingDegree + n ≤ (p * X ^ n).natTrailingDegree
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case inl
R : Type u
m n : ℕ
inst✝ : Semiring R
p : R[X]
pn : p.natDegree ≤ n
mno : m * n ≤ m * n
⊢ (p ^ m).coeff (m * n) = if m * n = m * n then p.coeff n ^ m else 0

pp: case inr
R : Type u
m n : ℕ
inst✝ : Semiring R
p : R[X]
o : ℕ
pn : p.natDegree ≤ n
mno : m * n ≤ o
h : o ≠ m * n
⊢ (p ^ m).coeff o = if o = m * n then p.coeff n ^ m else 0

Tactic:
·

Goal state after:
case inl
R : Type u
m n : ℕ
inst✝ : Semiring R
p : R[X]
pn : p.natDegree ≤ n
mno : m * n ≤ m * n
⊢ (p ^ m).coeff (m * n) = if m * n = m * n then p.coeff n ^ m else 0
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case inr
R : Type u
m n : ℕ
inst✝ : Semiring R
p : R[X]
o : ℕ
pn : p.natDegree ≤ n
mno : m * n ≤ o
h : o ≠ m * n
⊢ (p ^ m).coeff o = if o = m * n then p.coeff n ^ m else 0

Tactic:
·

Goal state after:
case inr
R : Type u
m n : ℕ
inst✝ : Semiring R
p : R[X]
o : ℕ
pn : p.natDegree ≤ n
mno : m * n ≤ o
h : o ≠ m * n
⊢ (p ^ m).coeff o = if o = m * n then p.coeff n ^ m else 0
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case insert.inl
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
IH : (s.sum f).degree = s.sup fun i ↦ (f i).degree
h : {i | i ∈ insert x s ∧ f i ≠ 0}.Pairwise (Ne on degree ∘ f)
H : (f x).degree < (s.sum f).degree
⊢ (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sup fun i ↦ (f i).degree)

pp: case insert.inr.inl
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
IH : (s.sum f).degree = s.sup fun i ↦ (f i).degree
h : {i | i ∈ insert x s ∧ f i ≠ 0}.Pairwise (Ne on degree ∘ f)
H : (f x).degree = (s.sum f).degree
⊢ (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sup fun i ↦ (f i).degree)

pp: case insert.inr.inr
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
IH : (s.sum f).degree = s.sup fun i ↦ (f i).degree
h : {i | i ∈ insert x s ∧ f i ≠ 0}.Pairwise (Ne on degree ∘ f)
H : (s.sum f).degree < (f x).degree
⊢ (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sup fun i ↦ (f i).degree)

Tactic:
·

Goal state after:
case insert.inl
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
IH : (s.sum f).degree = s.sup fun i ↦ (f i).degree
h : {i | i ∈ insert x s ∧ f i ≠ 0}.Pairwise (Ne on degree ∘ f)
H : (f x).degree < (s.sum f).degree
⊢ (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sup fun i ↦ (f i).degree)
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case insert.inr.inl
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
IH : (s.sum f).degree = s.sup fun i ↦ (f i).degree
h : {i | i ∈ insert x s ∧ f i ≠ 0}.Pairwise (Ne on degree ∘ f)
H : (f x).degree = (s.sum f).degree
⊢ (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sup fun i ↦ (f i).degree)

pp: case insert.inr.inr
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
IH : (s.sum f).degree = s.sup fun i ↦ (f i).degree
h : {i | i ∈ insert x s ∧ f i ≠ 0}.Pairwise (Ne on degree ∘ f)
H : (s.sum f).degree < (f x).degree
⊢ (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sup fun i ↦ (f i).degree)

Tactic:
·

Goal state after:
case insert.inr.inl
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
IH : (s.sum f).degree = s.sup fun i ↦ (f i).degree
h : {i | i ∈ insert x s ∧ f i ≠ 0}.Pairwise (Ne on degree ∘ f)
H : (f x).degree = (s.sum f).degree
⊢ (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sup fun i ↦ (f i).degree)
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natTrailingDegree + q.natTrailingDegree
h₂ : (i, j) ≠ (p.natTrailingDegree, q.natTrailingDegree)
hi : i < p.natTrailingDegree
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0

pp: case neg
R : Type u
inst✝ : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natTrailingDegree + q.natTrailingDegree
h₂ : (i, j) ≠ (p.natTrailingDegree, q.natTrailingDegree)
hi : p.natTrailingDegree ≤ i
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0

Tactic:
·

Goal state after:
case pos
R : Type u
inst✝ : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natTrailingDegree + q.natTrailingDegree
h₂ : (i, j) ≠ (p.natTrailingDegree, q.natTrailingDegree)
hi : i < p.natTrailingDegree
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natTrailingDegree + q.natTrailingDegree
h₂ : (i, j) ≠ (p.natTrailingDegree, q.natTrailingDegree)
hi : p.natTrailingDegree ≤ i
hj : j < q.natTrailingDegree
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0

pp: case neg
R : Type u
inst✝ : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natTrailingDegree + q.natTrailingDegree
h₂ : (i, j) ≠ (p.natTrailingDegree, q.natTrailingDegree)
hi : p.natTrailingDegree ≤ i
hj : q.natTrailingDegree ≤ j
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0

Tactic:
·

Goal state after:
case pos
R : Type u
inst✝ : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natTrailingDegree + q.natTrailingDegree
h₂ : (i, j) ≠ (p.natTrailingDegree, q.natTrailingDegree)
hi : p.natTrailingDegree ≤ i
hj : j < q.natTrailingDegree
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case insert.inr.inl.inl
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
x : S
hx : x ∉ ∅
IH : (∅.sum f).degree = ∅.sup fun i ↦ (f i).degree
h : {i | i ∈ insert x ∅ ∧ f i ≠ 0}.Pairwise (Ne on degree ∘ f)
H : (f x).degree = (∅.sum f).degree
⊢ (f x + ∑ x ∈ ∅, f x).degree = max (f x).degree (∅.sup fun i ↦ (f i).degree)

pp: case insert.inr.inl.inr
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
IH : (s.sum f).degree = s.sup fun i ↦ (f i).degree
h : {i | i ∈ insert x s ∧ f i ≠ 0}.Pairwise (Ne on degree ∘ f)
H : (f x).degree = (s.sum f).degree
hs : s.Nonempty
⊢ (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sup fun i ↦ (f i).degree)

Tactic:
·

Goal state after:
case insert.inr.inl.inl
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
x : S
hx : x ∉ ∅
IH : (∅.sum f).degree = ∅.sup fun i ↦ (f i).degree
h : {i | i ∈ insert x ∅ ∧ f i ≠ 0}.Pairwise (Ne on degree ∘ f)
H : (f x).degree = (∅.sum f).degree
⊢ (f x + ∑ x ∈ ∅, f x).degree = max (f x).degree (∅.sup fun i ↦ (f i).degree)
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case pos
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
IH : (s.sum f).degree = s.sup fun i ↦ (f i).degree
h : {i | i ∈ insert x s ∧ f i ≠ 0}.Pairwise (Ne on degree ∘ f)
hs : s.Nonempty
y : S
H : (f x).degree = (f y).degree
hy : y ∈ s
hy' : (s.sup fun i ↦ (f i).degree) = (f y).degree
hx0 : f x = 0
⊢ (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sup fun i ↦ (f i).degree)

pp: case neg
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
IH : (s.sum f).degree = s.sup fun i ↦ (f i).degree
h : {i | i ∈ insert x s ∧ f i ≠ 0}.Pairwise (Ne on degree ∘ f)
hs : s.Nonempty
y : S
H : (f x).degree = (f y).degree
hy : y ∈ s
hy' : (s.sup fun i ↦ (f i).degree) = (f y).degree
hx0 : ¬f x = 0
⊢ (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sup fun i ↦ (f i).degree)

Tactic:
·

Goal state after:
case pos
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
IH : (s.sum f).degree = s.sup fun i ↦ (f i).degree
h : {i | i ∈ insert x s ∧ f i ≠ 0}.Pairwise (Ne on degree ∘ f)
hs : s.Nonempty
y : S
H : (f x).degree = (f y).degree
hy : y ∈ s
hy' : (s.sup fun i ↦ (f i).degree) = (f y).degree
hx0 : f x = 0
⊢ (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sup fun i ↦ (f i).degree)
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: case inl
R : Type u
inst✝ : Semiring R
hp : coeff 0 0 = 0
⊢ nextCoeffUp 0 = coeff 0 (natTrailingDegree 0 + 1)

pp: case inr
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.coeff 0 = 0
hp₀ : p ≠ 0
⊢ p.nextCoeffUp = p.coeff (p.natTrailingDegree + 1)

Tactic:
·

Goal state after:
case inl
R : Type u
inst✝ : Semiring R
hp : coeff 0 0 = 0
⊢ nextCoeffUp 0 = coeff 0 (natTrailingDegree 0 + 1)