no goals
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.3088
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s : σ →₀ ℕ
a : R
⊢ degrees (↑(monomial s) a) ≤ ↑toMultiset s
classical
  refine' Finset.sup_le fun t h => _
  have := Finsupp.support_single_subset h
  rw [Finset.mem_singleton] at this
  rw [this]
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.3088
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s : σ →₀ ℕ
a : R
t : σ →₀ ℕ
h : t ∈ support (↑(monomial s) a)
⊢ ↑toMultiset t ≤ ↑toMultiset s
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.3088
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s : σ →₀ ℕ
a : R
⊢ degrees (↑(monomial s) a) ≤ ↑toMultiset s
refine' Finset.sup_le fun t h => _
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.3088
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s : σ →₀ ℕ
a : R
t : σ →₀ ℕ
h : t ∈ support (↑(monomial s) a)
this : t ∈ {s}
⊢ ↑toMultiset t ≤ ↑toMultiset s
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.3088
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s : σ →₀ ℕ
a : R
t : σ →₀ ℕ
h : t ∈ support (↑(monomial s) a)
⊢ ↑toMultiset t ≤ ↑toMultiset s
have := Finsupp.support_single_subset h
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.3088
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s : σ →₀ ℕ
a : R
t : σ →₀ ℕ
h : t ∈ support (↑(monomial s) a)
this : t = s
⊢ ↑toMultiset t ≤ ↑toMultiset s
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.3088
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s : σ →₀ ℕ
a : R
t : σ →₀ ℕ
h : t ∈ support (↑(monomial s) a)
this : t ∈ {s}
⊢ ↑toMultiset t ≤ ↑toMultiset s
rw [Finset.mem_singleton] at this
no goals
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.3088
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s : σ →₀ ℕ
a : R
t : σ →₀ ℕ
h : t ∈ support (↑(monomial s) a)
this : t = s
⊢ ↑toMultiset t ≤ ↑toMultiset s
rw [this]