no goals
R : Type u
S : Type v
σ : Type u_2
τ : Type u_1
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝² : CommSemiring R
p q : MvPolynomial σ R
inst✝¹ : CommSemiring S
inst✝ : DecidableEq τ
f : σ → τ
φ : MvPolynomial σ R
⊢ vars (↑(rename f) φ) ⊆ Finset.image f (vars φ)
classical
intro i hi
simp only [vars_def, exists_prop, Multiset.mem_toFinset, Finset.mem_image] at hi⊢
simpa only [Multiset.mem_map] using degrees_rename _ _ hi
R : Type u
S : Type v
σ : Type u_2
τ : Type u_1
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝² : CommSemiring R
p q : MvPolynomial σ R
inst✝¹ : CommSemiring S
inst✝ : DecidableEq τ
f : σ → τ
φ : MvPolynomial σ R
i : τ
hi : i ∈ vars (↑(rename f) φ)
⊢ i ∈ Finset.image f (vars φ)
R : Type u
S : Type v
σ : Type u_2
τ : Type u_1
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝² : CommSemiring R
p q : MvPolynomial σ R
inst✝¹ : CommSemiring S
inst✝ : DecidableEq τ
f : σ → τ
φ : MvPolynomial σ R
⊢ vars (↑(rename f) φ) ⊆ Finset.image f (vars φ)
intro i hi
R : Type u
S : Type v
σ : Type u_2
τ : Type u_1
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝² : CommSemiring R
p q : MvPolynomial σ R
inst✝¹ : CommSemiring S
inst✝ : DecidableEq τ
f : σ → τ
φ : MvPolynomial σ R
i : τ
hi : i ∈ degrees (↑(rename f) φ)
⊢ ∃ a, a ∈ degrees φ ∧ f a = i
R : Type u
S : Type v
σ : Type u_2
τ : Type u_1
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝² : CommSemiring R
p q : MvPolynomial σ R
inst✝¹ : CommSemiring S
inst✝ : DecidableEq τ
f : σ → τ
φ : MvPolynomial σ R
i : τ
hi : i ∈ vars (↑(rename f) φ)
⊢ i ∈ Finset.image f (vars φ)
simp only [vars_def, exists_prop, Multiset.mem_toFinset, Finset.mem_image] at hi⊢
no goals
R : Type u
S : Type v
σ : Type u_2
τ : Type u_1
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝² : CommSemiring R
p q : MvPolynomial σ R
inst✝¹ : CommSemiring S
inst✝ : DecidableEq τ
f : σ → τ
φ : MvPolynomial σ R
i : τ
hi : i ∈ degrees (↑(rename f) φ)
⊢ ∃ a, a ∈ degrees φ ∧ f a = i
simpa only [Multiset.mem_map] using degrees_rename _ _ hi