-- Mathlib/Algebra/MvPolynomial/Funext.lean
theorem funext {σ : Type*} {p q : MvPolynomial σ R} (h : ∀ x : σ → R, eval x p = eval x q) :
    p = q

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

Tactic:
intro p h

Result:
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

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

Tactic:
suffices p = 0 by rw [this, map_zero]

Result:
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

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

Tactic:
rw [← sub_eq_zero, this (p - q)]

Result:
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

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

Tactic:
apply funext_fin

Result:
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

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

Tactic:
simp only [eval, eval₂Hom_rename, Function.extend_comp hf]

Result:
no goals

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

Tactic:
rw [this, map_zero]

Result:
no goals

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

Tactic:
simp only [h, RingHom.map_sub, forall_const, sub_self]

Result:
no goals

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

Tactic:
intro x

Result:
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

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

Tactic:
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]

Result:
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

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

Tactic:
classical
  convert h (Function.extend f x 0)
  simp only [eval, eval₂Hom_rename, Function.extend_comp hf]

Result:
no goals

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

Tactic:
clear h p q

Result:
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

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

Tactic:
obtain ⟨n, f, hf, p, rfl⟩ := exists_fin_rename p

Result:
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

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

Tactic:
convert h (Function.extend f x 0)

Result:
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)