R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
σ : Type u_1
p q : MvPolynomial σ R
h : ∀ (x : σ → R), ↑(eval x) p = ↑(eval x) q
⊢ ∀ (p : MvPolynomial σ R), (∀ (x : σ → R), ↑(eval x) p = 0) → p = 0
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
σ : Type u_1
p q : MvPolynomial σ R
h : ∀ (x : σ → R), ↑(eval x) p = ↑(eval x) q
⊢ p = q
suffices ∀ p, (∀ x : σ → R, eval x p = 0) → p = 0 by
  rw [← sub_eq_zero, this (p - q)]
  simp only [h, RingHom.map_sub, forall_const, sub_self]
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
σ : Type u_1
⊢ ∀ (p : MvPolynomial σ R), (∀ (x : σ → R), ↑(eval x) p = 0) → p = 0
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
σ : Type u_1
p q : MvPolynomial σ R
h : ∀ (x : σ → R), ↑(eval x) p = ↑(eval x) q
⊢ ∀ (p : MvPolynomial σ R), (∀ (x : σ → R), ↑(eval x) p = 0) → p = 0
clear h p q
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
σ : Type u_1
p : MvPolynomial σ R
h : ∀ (x : σ → R), ↑(eval x) p = 0
⊢ p = 0
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
σ : Type u_1
⊢ ∀ (p : MvPolynomial σ R), (∀ (x : σ → R), ↑(eval x) p = 0) → p = 0
intro p h
case intro.intro.intro.intro
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
σ : Type u_1
n : ℕ
f : Fin n → σ
hf : Function.Injective f
p : MvPolynomial (Fin n) R
h : ∀ (x : σ → R), ↑(eval x) (↑(rename f) p) = 0
⊢ ↑(rename f) p = 0
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
σ : Type u_1
p : MvPolynomial σ R
h : ∀ (x : σ → R), ↑(eval x) p = 0
⊢ p = 0
obtain ⟨n, f, hf, p, rfl⟩ := exists_fin_rename p
case intro.intro.intro.intro
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
σ : Type u_1
n : ℕ
f : Fin n → σ
hf : Function.Injective f
p : MvPolynomial (Fin n) R
h : ∀ (x : σ → R), ↑(eval x) (↑(rename f) p) = 0
⊢ p = 0
case intro.intro.intro.intro
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
σ : Type u_1
n : ℕ
f : Fin n → σ
hf : Function.Injective f
p : MvPolynomial (Fin n) R
h : ∀ (x : σ → R), ↑(eval x) (↑(rename f) p) = 0
⊢ ↑(rename f) p = 0
suffices p = 0 by rw [this, AlgHom.map_zero]
case intro.intro.intro.intro.h
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
σ : Type u_1
n : ℕ
f : Fin n → σ
hf : Function.Injective f
p : MvPolynomial (Fin n) R
h : ∀ (x : σ → R), ↑(eval x) (↑(rename f) p) = 0
⊢ ∀ (x : Fin n → R), ↑(eval x) p = 0
case intro.intro.intro.intro
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
σ : Type u_1
n : ℕ
f : Fin n → σ
hf : Function.Injective f
p : MvPolynomial (Fin n) R
h : ∀ (x : σ → R), ↑(eval x) (↑(rename f) p) = 0
⊢ p = 0
apply funext_fin
case intro.intro.intro.intro.h
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
σ : Type u_1
n : ℕ
f : Fin n → σ
hf : Function.Injective f
p : MvPolynomial (Fin n) R
h : ∀ (x : σ → R), ↑(eval x) (↑(rename f) p) = 0
x : Fin n → R
⊢ ↑(eval x) p = 0
case intro.intro.intro.intro.h
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
σ : Type u_1
n : ℕ
f : Fin n → σ
hf : Function.Injective f
p : MvPolynomial (Fin n) R
h : ∀ (x : σ → R), ↑(eval x) (↑(rename f) p) = 0
⊢ ∀ (x : Fin n → R), ↑(eval x) p = 0
intro x
no goals
case intro.intro.intro.intro.h
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
σ : Type u_1
n : ℕ
f : Fin n → σ
hf : Function.Injective f
p : MvPolynomial (Fin n) R
h : ∀ (x : σ → R), ↑(eval x) (↑(rename f) p) = 0
x : Fin n → R
⊢ ↑(eval x) p = 0
classical
  convert h (Function.extend f x 0)
  simp only [eval, eval₂Hom_rename, Function.extend_comp hf]
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
σ : Type u_1
p q : MvPolynomial σ R
h : ∀ (x : σ → R), ↑(eval x) p = ↑(eval x) q
this : ∀ (p : MvPolynomial σ R), (∀ (x : σ → R), ↑(eval x) p = 0) → p = 0
⊢ ∀ (x : σ → R), ↑(eval x) (p - q) = 0
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
σ : Type u_1
p q : MvPolynomial σ R
h : ∀ (x : σ → R), ↑(eval x) p = ↑(eval x) q
this : ∀ (p : MvPolynomial σ R), (∀ (x : σ → R), ↑(eval x) p = 0) → p = 0
⊢ p = q
rw [← sub_eq_zero, this (p - q)]
no goals
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
σ : Type u_1
p q : MvPolynomial σ R
h : ∀ (x : σ → R), ↑(eval x) p = ↑(eval x) q
this : ∀ (p : MvPolynomial σ R), (∀ (x : σ → R), ↑(eval x) p = 0) → p = 0
⊢ ∀ (x : σ → R), ↑(eval x) (p - q) = 0
simp only [h, RingHom.map_sub, forall_const, sub_self]
no goals
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
σ : Type u_1
n : ℕ
f : Fin n → σ
hf : Function.Injective f
p : MvPolynomial (Fin n) R
h : ∀ (x : σ → R), ↑(eval x) (↑(rename f) p) = 0
this : p = 0
⊢ ↑(rename f) p = 0
rw [this, AlgHom.map_zero]
case h.e'_2
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
σ : Type u_1
n : ℕ
f : Fin n → σ
hf : Function.Injective f
p : MvPolynomial (Fin n) R
h : ∀ (x : σ → R), ↑(eval x) (↑(rename f) p) = 0
x : Fin n → R
⊢ ↑(eval x) p = ↑(eval (Function.extend f x 0)) (↑(rename f) p)
case intro.intro.intro.intro.h
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
σ : Type u_1
n : ℕ
f : Fin n → σ
hf : Function.Injective f
p : MvPolynomial (Fin n) R
h : ∀ (x : σ → R), ↑(eval x) (↑(rename f) p) = 0
x : Fin n → R
⊢ ↑(eval x) p = 0
convert h (Function.extend f x 0)
no goals
case h.e'_2
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
σ : Type u_1
n : ℕ
f : Fin n → σ
hf : Function.Injective f
p : MvPolynomial (Fin n) R
h : ∀ (x : σ → R), ↑(eval x) (↑(rename f) p) = 0
x : Fin n → R
⊢ ↑(eval x) p = ↑(eval (Function.extend f x 0)) (↑(rename f) p)
simp only [eval, eval₂Hom_rename, Function.extend_comp hf]