[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u
S : Type v
r : R
e : ℕ
n m : σ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s : Set σ
⊢ supported R s = AlgHom.range (rename Subtype.val)
[PROOFSTEP]
rw [supported, Set.image_eq_range, adjoin_range_eq_range_aeval, rename]
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u
S : Type v
r : R
e : ℕ
n m : σ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s : Set σ
⊢ AlgHom.range (aeval fun x => X ↑x) = AlgHom.range (aeval (X ∘ Subtype.val))
[PROOFSTEP]
congr
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u
S : Type v
r : R
e : ℕ
n m : σ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s : Set σ
x : R
⊢ ↑(AlgEquiv.symm (supportedEquivMvPolynomial s)) (↑C x) = ↑(algebraMap R { x // x ∈ supported R s }) x
[PROOFSTEP]
ext1
[GOAL]
case a
σ : Type u_1
τ : Type u_2
R : Type u
S : Type v
r : R
e : ℕ
n m : σ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s : Set σ
x : R
⊢ ↑(↑(AlgEquiv.symm (supportedEquivMvPolynomial s)) (↑C x)) = ↑(↑(algebraMap R { x // x ∈ supported R s }) x)
[PROOFSTEP]
simp [supportedEquivMvPolynomial, MvPolynomial.algebraMap_eq]
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u
S : Type v
r : R
e : ℕ
n m : σ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s : Set σ
i : ↑s
⊢ ↑(↑(AlgEquiv.symm (supportedEquivMvPolynomial s)) (X i)) = X ↑i
[PROOFSTEP]
simp [supportedEquivMvPolynomial]
[GOAL]
σ : Type u_1
τ : Type u_2
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
[PROOFSTEP]
classical
rw [supported_eq_range_rename, AlgHom.mem_range]
constructor
· rintro ⟨p, rfl⟩
  refine' _root_.trans (Finset.coe_subset.2 (vars_rename _ _)) _
  simp
· intro hs
  exact exists_rename_eq_of_vars_subset_range p ((↑) : s → σ) Subtype.val_injective (by simpa)
[GOAL]
σ : Type u_1
τ : Type u_2
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
[PROOFSTEP]
rw [supported_eq_range_rename, AlgHom.mem_range]
[GOAL]
σ : Type u_1
τ : Type u_2
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
[PROOFSTEP]
constructor
[GOAL]
case mp
σ : Type u_1
τ : Type u_2
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
[PROOFSTEP]
rintro ⟨p, rfl⟩
[GOAL]
case mp.intro
σ : Type u_1
τ : Type u_2
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
[PROOFSTEP]
refine' _root_.trans (Finset.coe_subset.2 (vars_rename _ _)) _
[GOAL]
case mp.intro
σ : Type u_1
τ : Type u_2
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
[PROOFSTEP]
simp
[GOAL]
case mpr
σ : Type u_1
τ : Type u_2
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
[PROOFSTEP]
intro hs
[GOAL]
case mpr
σ : Type u_1
τ : Type u_2
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
[PROOFSTEP]
exact exists_rename_eq_of_vars_subset_range p ((↑) : s → σ) Subtype.val_injective (by simpa)
[GOAL]
σ : Type u_1
τ : Type u_2
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
[PROOFSTEP]
simpa
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u
S : Type v
r : R
e : ℕ
n m : σ
inst✝ : CommSemiring R
p✝ q : MvPolynomial σ R
s t : Set σ
p : MvPolynomial σ R
⊢ p ∈ supported R ↑(vars p)
[PROOFSTEP]
rw [mem_supported]
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u
S : Type v
r : R
e : ℕ
n m : σ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s t : Set σ
⊢ supported R Set.univ = ⊤
[PROOFSTEP]
simp [Algebra.eq_top_iff, mem_supported]
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u
S : Type v
r : R
e : ℕ
n m : σ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s t : Set σ
⊢ supported R ∅ = ⊥
[PROOFSTEP]
simp [supported_eq_adjoin_X]
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u
S : Type v
r : R
e : ℕ
n m : σ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
s t : Set σ
inst✝ : Nontrivial R
i : σ
⊢ X i ∈ supported R s ↔ i ∈ s
[PROOFSTEP]
simp [mem_supported]
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u
S : Type v
r : R
e : ℕ
n m : σ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
s t : Set σ
inst✝ : Nontrivial R
⊢ supported R s ≤ supported R t ↔ s ⊆ t
[PROOFSTEP]
constructor
[GOAL]
case mp
σ : Type u_1
τ : Type u_2
R : Type u
S : Type v
r : R
e : ℕ
n m : σ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
s t : Set σ
inst✝ : Nontrivial R
⊢ supported R s ≤ supported R t → s ⊆ t
[PROOFSTEP]
intro h i
[GOAL]
case mp
σ : Type u_1
τ : Type u_2
R : Type u
S : Type v
r : R
e : ℕ
n m : σ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
s t : Set σ
inst✝ : Nontrivial R
h : supported R s ≤ supported R t
i : σ
⊢ i ∈ s → i ∈ t
[PROOFSTEP]
simpa using @h (X i)
[GOAL]
case mpr
σ : Type u_1
τ : Type u_2
R : Type u
S : Type v
r : R
e : ℕ
n m : σ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
s t : Set σ
inst✝ : Nontrivial R
⊢ s ⊆ t → supported R s ≤ supported R t
[PROOFSTEP]
exact supported_mono
[GOAL]
σ : Type u_1
τ : Type u_2
R✝ : Type u
S : Type v
r : R✝
e : ℕ
n m : σ
inst✝¹ : CommSemiring R✝
p q : MvPolynomial σ R✝
s t : Set σ
R : Type u_3
inst✝ : CommRing R
F : MvPolynomial σ ℤ
hF : ↑(vars F) ⊆ s
⊢ ∃ f, ∀ (x : σ → R), f (x ∘ Subtype.val) = ↑(aeval x) F
[PROOFSTEP]
rw [← mem_supported, supported_eq_range_rename, AlgHom.mem_range] at hF 
[GOAL]
σ : Type u_1
τ : Type u_2
R✝ : Type u
S : Type v
r : R✝
e : ℕ
n m : σ
inst✝¹ : CommSemiring R✝
p q : MvPolynomial σ R✝
s t : Set σ
R : Type u_3
inst✝ : CommRing R
F : MvPolynomial σ ℤ
hF : ∃ x, ↑(rename Subtype.val) x = F
⊢ ∃ f, ∀ (x : σ → R), f (x ∘ Subtype.val) = ↑(aeval x) F
[PROOFSTEP]
cases' hF with F' hF'
[GOAL]
case intro
σ : Type u_1
τ : Type u_2
R✝ : Type u
S : Type v
r : R✝
e : ℕ
n m : σ
inst✝¹ : CommSemiring R✝
p q : MvPolynomial σ R✝
s t : Set σ
R : Type u_3
inst✝ : CommRing R
F : MvPolynomial σ ℤ
F' : MvPolynomial { x // x ∈ s } ℤ
hF' : ↑(rename Subtype.val) F' = F
⊢ ∃ f, ∀ (x : σ → R), f (x ∘ Subtype.val) = ↑(aeval x) F
[PROOFSTEP]
use fun z ↦ aeval z F'
[GOAL]
case h
σ : Type u_1
τ : Type u_2
R✝ : Type u
S : Type v
r : R✝
e : ℕ
n m : σ
inst✝¹ : CommSemiring R✝
p q : MvPolynomial σ R✝
s t : Set σ
R : Type u_3
inst✝ : CommRing R
F : MvPolynomial σ ℤ
F' : MvPolynomial { x // x ∈ s } ℤ
hF' : ↑(rename Subtype.val) F' = F
⊢ ∀ (x : σ → R), ↑(aeval (x ∘ Subtype.val)) F' = ↑(aeval x) F
[PROOFSTEP]
intro x
[GOAL]
case h
σ : Type u_1
τ : Type u_2
R✝ : Type u
S : Type v
r : R✝
e : ℕ
n m : σ
inst✝¹ : CommSemiring R✝
p q : MvPolynomial σ R✝
s t : Set σ
R : Type u_3
inst✝ : CommRing R
F : MvPolynomial σ ℤ
F' : MvPolynomial { x // x ∈ s } ℤ
hF' : ↑(rename Subtype.val) F' = F
x : σ → R
⊢ ↑(aeval (x ∘ Subtype.val)) F' = ↑(aeval x) F
[PROOFSTEP]
simp only [← hF', aeval_rename]
