σ : Type u_2
τ : Type ?u.131145
R✝ : Type u
S : Type v
r : R✝
e : ℕ
n m : σ
inst✝¹ : CommSemiring R✝
p q : MvPolynomial σ R✝
s t : Set σ
R : Type u_1
inst✝ : CommRing R
F : MvPolynomial σ ℤ
hF : ∃ x, ↑(rename Subtype.val) x = F
⊢ ∃ f, ∀ (x : σ → R), f (x ∘ Subtype.val) = ↑(aeval x) F
σ : Type u_2
τ : Type ?u.131145
R✝ : Type u
S : Type v
r : R✝
e : ℕ
n m : σ
inst✝¹ : CommSemiring R✝
p q : MvPolynomial σ R✝
s t : Set σ
R : Type u_1
inst✝ : CommRing R
F : MvPolynomial σ ℤ
hF : ↑(vars F) ⊆ s
⊢ ∃ f, ∀ (x : σ → R), f (x ∘ Subtype.val) = ↑(aeval x) F
rw [← mem_supported, supported_eq_range_rename, AlgHom.mem_range] at hF
case intro
σ : Type u_2
τ : Type ?u.131145
R✝ : Type u
S : Type v
r : R✝
e : ℕ
n m : σ
inst✝¹ : CommSemiring R✝
p q : MvPolynomial σ R✝
s t : Set σ
R : Type u_1
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
σ : Type u_2
τ : Type ?u.131145
R✝ : Type u
S : Type v
r : R✝
e : ℕ
n m : σ
inst✝¹ : CommSemiring R✝
p q : MvPolynomial σ R✝
s t : Set σ
R : Type u_1
inst✝ : CommRing R
F : MvPolynomial σ ℤ
hF : ∃ x, ↑(rename Subtype.val) x = F
⊢ ∃ f, ∀ (x : σ → R), f (x ∘ Subtype.val) = ↑(aeval x) F
cases' hF with F' hF'
case intro
σ : Type u_2
τ : Type ?u.131145
R✝ : Type u
S : Type v
r : R✝
e : ℕ
n m : σ
inst✝¹ : CommSemiring R✝
p q : MvPolynomial σ R✝
s t : Set σ
R : Type u_1
inst✝ : CommRing R
F : MvPolynomial σ ℤ
F' : MvPolynomial { x // x ∈ s } ℤ
hF' : ↑(rename Subtype.val) F' = F
⊢ ∀ (x : σ → R), (fun z => ↑(aeval z) F') (x ∘ Subtype.val) = ↑(aeval x) F
case intro
σ : Type u_2
τ : Type ?u.131145
R✝ : Type u
S : Type v
r : R✝
e : ℕ
n m : σ
inst✝¹ : CommSemiring R✝
p q : MvPolynomial σ R✝
s t : Set σ
R : Type u_1
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
use fun z ↦ aeval z F'
case intro
σ : Type u_2
τ : Type ?u.131145
R✝ : Type u
S : Type v
r : R✝
e : ℕ
n m : σ
inst✝¹ : CommSemiring R✝
p q : MvPolynomial σ R✝
s t : Set σ
R : Type u_1
inst✝ : CommRing R
F : MvPolynomial σ ℤ
F' : MvPolynomial { x // x ∈ s } ℤ
hF' : ↑(rename Subtype.val) F' = F
x : σ → R
⊢ (fun z => ↑(aeval z) F') (x ∘ Subtype.val) = ↑(aeval x) F
case intro
σ : Type u_2
τ : Type ?u.131145
R✝ : Type u
S : Type v
r : R✝
e : ℕ
n m : σ
inst✝¹ : CommSemiring R✝
p q : MvPolynomial σ R✝
s t : Set σ
R : Type u_1
inst✝ : CommRing R
F : MvPolynomial σ ℤ
F' : MvPolynomial { x // x ∈ s } ℤ
hF' : ↑(rename Subtype.val) F' = F
⊢ ∀ (x : σ → R), (fun z => ↑(aeval z) F') (x ∘ Subtype.val) = ↑(aeval x) F
intro x
no goals
case intro
σ : Type u_2
τ : Type ?u.131145
R✝ : Type u
S : Type v
r : R✝
e : ℕ
n m : σ
inst✝¹ : CommSemiring R✝
p q : MvPolynomial σ R✝
s t : Set σ
R : Type u_1
inst✝ : CommRing R
F : MvPolynomial σ ℤ
F' : MvPolynomial { x // x ∈ s } ℤ
hF' : ↑(rename Subtype.val) F' = F
x : σ → R
⊢ (fun z => ↑(aeval z) F') (x ∘ Subtype.val) = ↑(aeval x) F
simp only [← hF', aeval_rename]