[GOAL]
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
n : ℕ
p : MvPolynomial (Fin n) R
h : ∀ (x : Fin n → R), ↑(eval x) p = 0
⊢ p = 0
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
n : ℕ
p✝ : MvPolynomial (Fin n) R
h✝ : ∀ (x : Fin n → R), ↑(eval x) p✝ = 0
p : MvPolynomial (Fin Nat.zero) R
h : ∀ (x : Fin Nat.zero → R), ↑(eval x) p = 0
⊢ p = 0
[PROOFSTEP]
apply (MvPolynomial.isEmptyRingEquiv R (Fin 0)).injective
[GOAL]
case zero.a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
n : ℕ
p✝ : MvPolynomial (Fin n) R
h✝ : ∀ (x : Fin n → R), ↑(eval x) p✝ = 0
p : MvPolynomial (Fin Nat.zero) R
h : ∀ (x : Fin Nat.zero → R), ↑(eval x) p = 0
⊢ ↑(isEmptyRingEquiv R (Fin 0)) p = ↑(isEmptyRingEquiv R (Fin 0)) 0
[PROOFSTEP]
rw [RingEquiv.map_zero]
[GOAL]
case zero.a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
n : ℕ
p✝ : MvPolynomial (Fin n) R
h✝ : ∀ (x : Fin n → R), ↑(eval x) p✝ = 0
p : MvPolynomial (Fin Nat.zero) R
h : ∀ (x : Fin Nat.zero → R), ↑(eval x) p = 0
⊢ ↑(isEmptyRingEquiv R (Fin 0)) p = 0
[PROOFSTEP]
convert h finZeroElim
[GOAL]
case succ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
n✝ : ℕ
p✝ : MvPolynomial (Fin n✝) R
h✝ : ∀ (x : Fin n✝ → R), ↑(eval x) p✝ = 0
n : ℕ
ih : ∀ {p : MvPolynomial (Fin n) R}, (∀ (x : Fin n → R), ↑(eval x) p = 0) → p = 0
p : MvPolynomial (Fin (Nat.succ n)) R
h : ∀ (x : Fin (Nat.succ n) → R), ↑(eval x) p = 0
⊢ p = 0
[PROOFSTEP]
apply (finSuccEquiv R n).injective
[GOAL]
case succ.a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
n✝ : ℕ
p✝ : MvPolynomial (Fin n✝) R
h✝ : ∀ (x : Fin n✝ → R), ↑(eval x) p✝ = 0
n : ℕ
ih : ∀ {p : MvPolynomial (Fin n) R}, (∀ (x : Fin n → R), ↑(eval x) p = 0) → p = 0
p : MvPolynomial (Fin (Nat.succ n)) R
h : ∀ (x : Fin (Nat.succ n) → R), ↑(eval x) p = 0
⊢ ↑(finSuccEquiv R n) p = ↑(finSuccEquiv R n) 0
[PROOFSTEP]
simp only [AlgEquiv.map_zero]
[GOAL]
case succ.a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
n✝ : ℕ
p✝ : MvPolynomial (Fin n✝) R
h✝ : ∀ (x : Fin n✝ → R), ↑(eval x) p✝ = 0
n : ℕ
ih : ∀ {p : MvPolynomial (Fin n) R}, (∀ (x : Fin n → R), ↑(eval x) p = 0) → p = 0
p : MvPolynomial (Fin (Nat.succ n)) R
h : ∀ (x : Fin (Nat.succ n) → R), ↑(eval x) p = 0
⊢ ↑(finSuccEquiv R n) p = 0
[PROOFSTEP]
refine Polynomial.funext fun q => ?_
[GOAL]
case succ.a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
n✝ : ℕ
p✝ : MvPolynomial (Fin n✝) R
h✝ : ∀ (x : Fin n✝ → R), ↑(eval x) p✝ = 0
n : ℕ
ih : ∀ {p : MvPolynomial (Fin n) R}, (∀ (x : Fin n → R), ↑(eval x) p = 0) → p = 0
p : MvPolynomial (Fin (Nat.succ n)) R
h : ∀ (x : Fin (Nat.succ n) → R), ↑(eval x) p = 0
q : MvPolynomial (Fin n) R
⊢ Polynomial.eval q (↑(finSuccEquiv R n) p) = Polynomial.eval q 0
[PROOFSTEP]
rw [Polynomial.eval_zero]
[GOAL]
case succ.a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
n✝ : ℕ
p✝ : MvPolynomial (Fin n✝) R
h✝ : ∀ (x : Fin n✝ → R), ↑(eval x) p✝ = 0
n : ℕ
ih : ∀ {p : MvPolynomial (Fin n) R}, (∀ (x : Fin n → R), ↑(eval x) p = 0) → p = 0
p : MvPolynomial (Fin (Nat.succ n)) R
h : ∀ (x : Fin (Nat.succ n) → R), ↑(eval x) p = 0
q : MvPolynomial (Fin n) R
⊢ Polynomial.eval q (↑(finSuccEquiv R n) p) = 0
[PROOFSTEP]
apply ih fun x => ?_
[GOAL]
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
n✝ : ℕ
p✝ : MvPolynomial (Fin n✝) R
h✝ : ∀ (x : Fin n✝ → R), ↑(eval x) p✝ = 0
n : ℕ
ih : ∀ {p : MvPolynomial (Fin n) R}, (∀ (x : Fin n → R), ↑(eval x) p = 0) → p = 0
p : MvPolynomial (Fin (Nat.succ n)) R
h : ∀ (x : Fin (Nat.succ n) → R), ↑(eval x) p = 0
q : MvPolynomial (Fin n) R
x : Fin n → R
⊢ ↑(eval x) (Polynomial.eval q (↑(finSuccEquiv R n) p)) = 0
[PROOFSTEP]
calc
  _ = _ := eval_polynomial_eval_finSuccEquiv p _
  _ = 0 := h _
[GOAL]
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
σ : Type u_2
p q : MvPolynomial σ R
h : ∀ (x : σ → R), ↑(eval x) p = ↑(eval x) q
⊢ p = q
[PROOFSTEP]
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]
[GOAL]
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
σ : Type u_2
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
[PROOFSTEP]
rw [← sub_eq_zero, this (p - q)]
[GOAL]
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
σ : Type u_2
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
[PROOFSTEP]
simp only [h, RingHom.map_sub, forall_const, sub_self]
[GOAL]
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
σ : Type u_2
p q : MvPolynomial σ R
h : ∀ (x : σ → R), ↑(eval x) p = ↑(eval x) q
⊢ ∀ (p : MvPolynomial σ R), (∀ (x : σ → R), ↑(eval x) p = 0) → p = 0
[PROOFSTEP]
clear h p q
[GOAL]
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
σ : Type u_2
⊢ ∀ (p : MvPolynomial σ R), (∀ (x : σ → R), ↑(eval x) p = 0) → p = 0
[PROOFSTEP]
intro p h
[GOAL]
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
σ : Type u_2
p : MvPolynomial σ R
h : ∀ (x : σ → R), ↑(eval x) p = 0
⊢ p = 0
[PROOFSTEP]
obtain ⟨n, f, hf, p, rfl⟩ := exists_fin_rename p
[GOAL]
case intro.intro.intro.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
σ : Type u_2
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
[PROOFSTEP]
suffices p = 0 by rw [this, AlgHom.map_zero]
[GOAL]
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
σ : Type u_2
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
[PROOFSTEP]
rw [this, AlgHom.map_zero]
[GOAL]
case intro.intro.intro.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
σ : Type u_2
n : ℕ
f : Fin n → σ
hf : Function.Injective f
p : MvPolynomial (Fin n) R
h : ∀ (x : σ → R), ↑(eval x) (↑(rename f) p) = 0
⊢ p = 0
[PROOFSTEP]
apply funext_fin
[GOAL]
case intro.intro.intro.intro.h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
σ : Type u_2
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
[PROOFSTEP]
intro x
[GOAL]
case intro.intro.intro.intro.h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
σ : Type u_2
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
[PROOFSTEP]
classical
convert h (Function.extend f x 0)
simp only [eval, eval₂Hom_rename, Function.extend_comp hf]
[GOAL]
case intro.intro.intro.intro.h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
σ : Type u_2
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
[PROOFSTEP]
convert h (Function.extend f x 0)
[GOAL]
case h.e'_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
σ : Type u_2
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)
[PROOFSTEP]
simp only [eval, eval₂Hom_rename, Function.extend_comp hf]
[GOAL]
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
σ : Type u_2
p q : MvPolynomial σ R
⊢ p = q → ∀ (x : σ → R), ↑(eval x) p = ↑(eval x) q
[PROOFSTEP]
rintro rfl
[GOAL]
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
σ : Type u_2
p : MvPolynomial σ R
⊢ ∀ (x : σ → R), ↑(eval x) p = ↑(eval x) p
[PROOFSTEP]
simp only [forall_const, eq_self_iff_true]
