no goals
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.279512
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
n : σ
f : MvPolynomial σ R
⊢ degreeOf n f = Finset.sup (support f) fun m => ↑m n
classical
rw [degreeOf_def, degrees, Multiset.count_finset_sup]
congr
ext
simp
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.279512
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
n : σ
f : MvPolynomial σ R
⊢ (Finset.sup (support f) fun a => Multiset.count n (↑toMultiset a)) = Finset.sup (support f) fun m => ↑m n
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.279512
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
n : σ
f : MvPolynomial σ R
⊢ degreeOf n f = Finset.sup (support f) fun m => ↑m n
rw [degreeOf_def, degrees, Multiset.count_finset_sup]
case e_f
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.279512
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
n : σ
f : MvPolynomial σ R
⊢ (fun a => Multiset.count n (↑toMultiset a)) = fun m => ↑m n
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.279512
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
n : σ
f : MvPolynomial σ R
⊢ (Finset.sup (support f) fun a => Multiset.count n (↑toMultiset a)) = Finset.sup (support f) fun m => ↑m n
congr
case e_f.h
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.279512
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
n : σ
f : MvPolynomial σ R
x✝ : σ →₀ ℕ
⊢ Multiset.count n (↑toMultiset x✝) = ↑x✝ n
case e_f
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.279512
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
n : σ
f : MvPolynomial σ R
⊢ (fun a => Multiset.count n (↑toMultiset a)) = fun m => ↑m n
ext
no goals
case e_f.h
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.279512
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
n : σ
f : MvPolynomial σ R
x✝ : σ →₀ ℕ
⊢ Multiset.count n (↑toMultiset x✝) = ↑x✝ n
simp