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

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
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
induction' n with n ih
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
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
apply (MvPolynomial.isEmptyRingEquiv R (Fin 0)).injective
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
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
rw [RingEquiv.map_zero]
no goals
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
convert h finZeroElim
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
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
apply (finSuccEquiv R n).injective
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
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
simp only [AlgEquiv.map_zero]
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
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
refine Polynomial.funext fun q => ?_
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
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
rw [Polynomial.eval_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
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
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
apply ih fun x => ?_
no goals
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
calc _ = _ := eval_polynomial_eval_finSuccEquiv p _
     _ = 0 := h _