no goals
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q p : MvPolynomial σ R
f : σ → τ
h : Injective f
⊢ degrees (↑(rename f) p) = Multiset.map f (degrees p)
classical
simp only [degrees, Multiset.map_finset_sup p.support Finsupp.toMultiset f h,
  support_rename_of_injective h, Finset.sup_image]
refine' Finset.sup_congr rfl fun x _ => _
exact (Finsupp.toMultiset_map _ _).symm
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q p : MvPolynomial σ R
f : σ → τ
h : Injective f
⊢ Finset.sup (support p) ((fun s => ↑toMultiset s) ∘ Finsupp.mapDomain f) =
    Finset.sup (support p) (Multiset.map f ∘ ↑toMultiset)
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q p : MvPolynomial σ R
f : σ → τ
h : Injective f
⊢ degrees (↑(rename f) p) = Multiset.map f (degrees p)
simp only [degrees, Multiset.map_finset_sup p.support Finsupp.toMultiset f h,
  support_rename_of_injective h, Finset.sup_image]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q p : MvPolynomial σ R
f : σ → τ
h : Injective f
x : σ →₀ ℕ
x✝ : x ∈ support p
⊢ ((fun s => ↑toMultiset s) ∘ Finsupp.mapDomain f) x = (Multiset.map f ∘ ↑toMultiset) x
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q p : MvPolynomial σ R
f : σ → τ
h : Injective f
⊢ Finset.sup (support p) ((fun s => ↑toMultiset s) ∘ Finsupp.mapDomain f) =
    Finset.sup (support p) (Multiset.map f ∘ ↑toMultiset)
refine' Finset.sup_congr rfl fun x _ => _
no goals
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q p : MvPolynomial σ R
f : σ → τ
h : Injective f
x : σ →₀ ℕ
x✝ : x ∈ support p
⊢ ((fun s => ↑toMultiset s) ∘ Finsupp.mapDomain f) x = (Multiset.map f ∘ ↑toMultiset) x
exact (Finsupp.toMultiset_map _ _).symm