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 : MvPolynomial σ R
inst✝ : CommSemiring S
f : σ → τ
φ : MvPolynomial σ R
j : τ
h : j ∈ vars (↑(rename f) φ)
⊢ ∃ i, i ∈ vars φ ∧ f i = j
classical
simpa only [exists_prop, Finset.mem_image] using vars_rename f φ h
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 : MvPolynomial σ R
inst✝ : CommSemiring S
f : σ → τ
φ : MvPolynomial σ R
j : τ
h : j ∈ vars (↑(rename f) φ)
⊢ ∃ i, i ∈ vars φ ∧ f i = j
simpa only [exists_prop, Finset.mem_image] using vars_rename f φ h