-- Mathlib/Algebra/MvPolynomial/Funext.lean
theorem funext_fin {n : ℕ} {p : MvPolynomial (Fin n) R}
    (h : ∀ x : Fin n → R, eval x p = 0) : p = 0

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
n : ℕ
ih : ∀ {p : MvPolynomial (Fin n) R}, (∀ (x : Fin n → R), (eval x) p = 0) → p = 0
p : MvPolynomial (Fin (n + 1)) R
h : ∀ (x : Fin (n + 1) → R), (eval x) p = 0
q : MvPolynomial (Fin n) R
x : Fin n → R
⊢ (eval x) (Polynomial.eval q ((finSuccEquiv R n) p)) = 0

Tactic:
calc _ = _ := eval_polynomial_eval_finSuccEquiv p _
     _ = 0 := h _

Result:
no goals

Proof state:
case succ.a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
n : ℕ
ih : ∀ {p : MvPolynomial (Fin n) R}, (∀ (x : Fin n → R), (eval x) p = 0) → p = 0
p : MvPolynomial (Fin (n + 1)) R
h : ∀ (x : Fin (n + 1) → R), (eval x) p = 0
q : MvPolynomial (Fin n) R
⊢ Polynomial.eval q ((finSuccEquiv R n) p) = 0

Tactic:
apply ih fun x => ?_

Result:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
n : ℕ
ih : ∀ {p : MvPolynomial (Fin n) R}, (∀ (x : Fin n → R), (eval x) p = 0) → p = 0
p : MvPolynomial (Fin (n + 1)) R
h : ∀ (x : Fin (n + 1) → R), (eval x) p = 0
q : MvPolynomial (Fin n) R
x : Fin n → R
⊢ (eval x) (Polynomial.eval q ((finSuccEquiv R n) p)) = 0

Proof state:
case zero.a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
p : MvPolynomial (Fin 0) R
h : ∀ (x : Fin 0 → R), (eval x) p = 0
⊢ (isEmptyRingEquiv R (Fin 0)) p = (isEmptyRingEquiv R (Fin 0)) 0

Tactic:
rw [RingEquiv.map_zero]

Result:
case zero.a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
p : MvPolynomial (Fin 0) R
h : ∀ (x : Fin 0 → R), (eval x) p = 0
⊢ (isEmptyRingEquiv R (Fin 0)) p = 0

Proof state:
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

Tactic:
induction n with
| zero =>
  apply (MvPolynomial.isEmptyRingEquiv R (Fin 0)).injective
  rw [RingEquiv.map_zero]
  convert h finZeroElim
| succ n ih =>
  apply (finSuccEquiv R n).injective
  simp only [map_zero]
  refine Polynomial.funext fun q => ?_
  rw [Polynomial.eval_zero]
  apply ih fun x => ?_
  calc _ = _ := eval_polynomial_eval_finSuccEquiv p _
       _ = 0 := h _

Result:
no goals

Proof state:
case succ.a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
n : ℕ
ih : ∀ {p : MvPolynomial (Fin n) R}, (∀ (x : Fin n → R), (eval x) p = 0) → p = 0
p : MvPolynomial (Fin (n + 1)) R
h : ∀ (x : Fin (n + 1) → R), (eval x) p = 0
q : MvPolynomial (Fin n) R
⊢ Polynomial.eval q ((finSuccEquiv R n) p) = Polynomial.eval q 0

Tactic:
rw [Polynomial.eval_zero]

Result:
case succ.a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
n : ℕ
ih : ∀ {p : MvPolynomial (Fin n) R}, (∀ (x : Fin n → R), (eval x) p = 0) → p = 0
p : MvPolynomial (Fin (n + 1)) R
h : ∀ (x : Fin (n + 1) → R), (eval x) p = 0
q : MvPolynomial (Fin n) R
⊢ Polynomial.eval q ((finSuccEquiv R n) p) = 0

Proof state:
case succ.a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
n : ℕ
ih : ∀ {p : MvPolynomial (Fin n) R}, (∀ (x : Fin n → R), (eval x) p = 0) → p = 0
p : MvPolynomial (Fin (n + 1)) R
h : ∀ (x : Fin (n + 1) → R), (eval x) p = 0
⊢ (finSuccEquiv R n) p = 0

Tactic:
refine Polynomial.funext fun q => ?_

Result:
case succ.a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
n : ℕ
ih : ∀ {p : MvPolynomial (Fin n) R}, (∀ (x : Fin n → R), (eval x) p = 0) → p = 0
p : MvPolynomial (Fin (n + 1)) R
h : ∀ (x : Fin (n + 1) → R), (eval x) p = 0
q : MvPolynomial (Fin n) R
⊢ Polynomial.eval q ((finSuccEquiv R n) p) = Polynomial.eval q 0

Proof state:
case zero.a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
p : MvPolynomial (Fin 0) R
h : ∀ (x : Fin 0 → R), (eval x) p = 0
⊢ (isEmptyRingEquiv R (Fin 0)) p = 0

Tactic:
convert h finZeroElim

Result:
no goals

Proof state:
case zero
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
p : MvPolynomial (Fin 0) R
h : ∀ (x : Fin 0 → R), (eval x) p = 0
⊢ p = 0

Tactic:
apply (MvPolynomial.isEmptyRingEquiv R (Fin 0)).injective

Result:
case zero.a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
p : MvPolynomial (Fin 0) R
h : ∀ (x : Fin 0 → R), (eval x) p = 0
⊢ (isEmptyRingEquiv R (Fin 0)) p = (isEmptyRingEquiv R (Fin 0)) 0

Proof state:
case succ.a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
n : ℕ
ih : ∀ {p : MvPolynomial (Fin n) R}, (∀ (x : Fin n → R), (eval x) p = 0) → p = 0
p : MvPolynomial (Fin (n + 1)) R
h : ∀ (x : Fin (n + 1) → R), (eval x) p = 0
⊢ (finSuccEquiv R n) p = (finSuccEquiv R n) 0

Tactic:
simp only [map_zero]

Result:
case succ.a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
n : ℕ
ih : ∀ {p : MvPolynomial (Fin n) R}, (∀ (x : Fin n → R), (eval x) p = 0) → p = 0
p : MvPolynomial (Fin (n + 1)) R
h : ∀ (x : Fin (n + 1) → R), (eval x) p = 0
⊢ (finSuccEquiv R n) p = 0

Proof state:
case succ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
n : ℕ
ih : ∀ {p : MvPolynomial (Fin n) R}, (∀ (x : Fin n → R), (eval x) p = 0) → p = 0
p : MvPolynomial (Fin (n + 1)) R
h : ∀ (x : Fin (n + 1) → R), (eval x) p = 0
⊢ p = 0

Tactic:
apply (finSuccEquiv R n).injective

Result:
case succ.a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
n : ℕ
ih : ∀ {p : MvPolynomial (Fin n) R}, (∀ (x : Fin n → R), (eval x) p = 0) → p = 0
p : MvPolynomial (Fin (n + 1)) R
h : ∀ (x : Fin (n + 1) → R), (eval x) p = 0
⊢ (finSuccEquiv R n) p = (finSuccEquiv R n) 0