case ofFinsupp
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type ?u.559926
n : ℕ
p : AddMonoidAlgebra R ℕ
⊢ degree (erase n { toFinsupp := p }) ≤ degree { toFinsupp := p }
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type ?u.559926
p : R[X]
n : ℕ
⊢ degree (erase n p) ≤ degree p
rcases p with ⟨p⟩
case ofFinsupp
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type ?u.559926
n : ℕ
p : AddMonoidAlgebra R ℕ
⊢ Finset.max (Finsupp.erase n p).support ≤ Finset.max p.support
case ofFinsupp
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type ?u.559926
n : ℕ
p : AddMonoidAlgebra R ℕ
⊢ degree (erase n { toFinsupp := p }) ≤ degree { toFinsupp := p }
simp only [erase_def, degree, coeff, support]
case ofFinsupp.h
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type ?u.559926
n : ℕ
p : AddMonoidAlgebra R ℕ
⊢ (Finsupp.erase n p).support ⊆ p.support
case ofFinsupp
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type ?u.559926
n : ℕ
p : AddMonoidAlgebra R ℕ
⊢ Finset.max (Finsupp.erase n p).support ≤ Finset.max p.support
apply sup_mono
case ofFinsupp.h
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type ?u.559926
n : ℕ
p : AddMonoidAlgebra R ℕ
⊢ Finset.erase p.support n ⊆ p.support
case ofFinsupp.h
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type ?u.559926
n : ℕ
p : AddMonoidAlgebra R ℕ
⊢ (Finsupp.erase n p).support ⊆ p.support
rw [Finsupp.support_erase]
no goals
case ofFinsupp.h
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type ?u.559926
n : ℕ
p : AddMonoidAlgebra R ℕ
⊢ Finset.erase p.support n ⊆ p.support
apply Finset.erase_subset