σ : Type u_1
τ : Type ?u.120933
R : Type u
S : Type v
r : R
e : ℕ
n m : σ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s t : Set σ
⊢ (∃ x, ↑(rename Subtype.val) x = p) ↔ ↑(vars p) ⊆ s
σ : Type u_1
τ : Type ?u.120933
R : Type u
S : Type v
r : R
e : ℕ
n m : σ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s t : Set σ
⊢ p ∈ supported R s ↔ ↑(vars p) ⊆ s
rw [supported_eq_range_rename, AlgHom.mem_range]
case mp
σ : Type u_1
τ : Type ?u.120933
R : Type u
S : Type v
r : R
e : ℕ
n m : σ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s t : Set σ
⊢ (∃ x, ↑(rename Subtype.val) x = p) → ↑(vars p) ⊆ s

case mpr
σ : Type u_1
τ : Type ?u.120933
R : Type u
S : Type v
r : R
e : ℕ
n m : σ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s t : Set σ
⊢ ↑(vars p) ⊆ s → ∃ x, ↑(rename Subtype.val) x = p
σ : Type u_1
τ : Type ?u.120933
R : Type u
S : Type v
r : R
e : ℕ
n m : σ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s t : Set σ
⊢ (∃ x, ↑(rename Subtype.val) x = p) ↔ ↑(vars p) ⊆ s
constructor
case mp.intro
σ : Type u_1
τ : Type ?u.120933
R : Type u
S : Type v
r : R
e : ℕ
n m : σ
inst✝ : CommSemiring R
q : MvPolynomial σ R
s t : Set σ
p : MvPolynomial { x // x ∈ s } R
⊢ ↑(vars (↑(rename Subtype.val) p)) ⊆ s
case mp
σ : Type u_1
τ : Type ?u.120933
R : Type u
S : Type v
r : R
e : ℕ
n m : σ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s t : Set σ
⊢ (∃ x, ↑(rename Subtype.val) x = p) → ↑(vars p) ⊆ s
rintro ⟨p, rfl⟩
case mp.intro
σ : Type u_1
τ : Type ?u.120933
R : Type u
S : Type v
r : R
e : ℕ
n m : σ
inst✝ : CommSemiring R
q : MvPolynomial σ R
s t : Set σ
p : MvPolynomial { x // x ∈ s } R
⊢ ↑(Finset.image Subtype.val (vars p)) ⊆ s
case mp.intro
σ : Type u_1
τ : Type ?u.120933
R : Type u
S : Type v
r : R
e : ℕ
n m : σ
inst✝ : CommSemiring R
q : MvPolynomial σ R
s t : Set σ
p : MvPolynomial { x // x ∈ s } R
⊢ ↑(vars (↑(rename Subtype.val) p)) ⊆ s
refine' _root_.trans (Finset.coe_subset.2 (vars_rename _ _)) _
no goals
case mp.intro
σ : Type u_1
τ : Type ?u.120933
R : Type u
S : Type v
r : R
e : ℕ
n m : σ
inst✝ : CommSemiring R
q : MvPolynomial σ R
s t : Set σ
p : MvPolynomial { x // x ∈ s } R
⊢ ↑(Finset.image Subtype.val (vars p)) ⊆ s
simp
case mpr
σ : Type u_1
τ : Type ?u.120933
R : Type u
S : Type v
r : R
e : ℕ
n m : σ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s t : Set σ
hs : ↑(vars p) ⊆ s
⊢ ∃ x, ↑(rename Subtype.val) x = p
case mpr
σ : Type u_1
τ : Type ?u.120933
R : Type u
S : Type v
r : R
e : ℕ
n m : σ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s t : Set σ
⊢ ↑(vars p) ⊆ s → ∃ x, ↑(rename Subtype.val) x = p
intro hs
no goals
case mpr
σ : Type u_1
τ : Type ?u.120933
R : Type u
S : Type v
r : R
e : ℕ
n m : σ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s t : Set σ
hs : ↑(vars p) ⊆ s
⊢ ∃ x, ↑(rename Subtype.val) x = p
exact exists_rename_eq_of_vars_subset_range p ((↑) : s → σ) Subtype.val_injective (by simpa)
no goals
σ : Type u_1
τ : Type ?u.120933
R : Type u
S : Type v
r : R
e : ℕ
n m : σ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s t : Set σ
hs : ↑(vars p) ⊆ s
⊢ ↑(vars p) ⊆ Set.range Subtype.val
simpa