awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.MvPolynomial.Funext
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
ih :
  ∀ {p : MvPolynomial (Fin n) R} (s : Fin n → Set R) (hs : ∀ (i : Fin n), (s i).Infinite)
    (h :
      ∀ x ∈ Set.pi (α := fun (i : Fin n) ↦ R) Set.univ s,
        Eq (α := R) ((eval x : (a : MvPolynomial (Fin n) R) → R) p : R) (0 : R)),
    p = 0
p : MvPolynomial (Fin (n + 1)) R
s : Fin (n + 1) → Set R
hs : ∀ (i : Fin (n + 1)), (s i).Infinite
h :
  ∀ x ∈ Set.pi (α := fun (i : Fin (n + 1)) ↦ R) Set.univ s,
    Eq (α := R) ((eval x : (a : MvPolynomial (Fin (n + 1)) R) → R) p : R) (0 : R)
r : R
hr : r ∈ s 0
x : (i : Fin n) → R
hx :
  Membership.mem (γ := Set ((i : Fin n) → R)) (Set.pi (α := fun (i : Fin n) ↦ R) Set.univ fun (x : Fin n) ↦ s x.succ) x
⊢ Eq (α := R)
    ((eval fun (i : Fin (n + 1)) ↦
            Fin.cases (motive := fun (x : Fin (n + 1)) ↦ R)
              ((eval x : (a : MvPolynomial (Fin n) R) → R)
                ((C : (a : R) → MvPolynomial (Fin n) R) r : MvPolynomial (Fin n) R))
              x i :
          (a : MvPolynomial (Fin (n + 1)) R) → R)
        p :
      R)
    (0 : R)

Tactic:
exact h _ fun i _ ↦ i.cases (by simpa using hr) (by simpa using hx)

Premises used: Fin.cases
-- Module: Mathlib.Algebra.MvPolynomial.Funext
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
p : MvPolynomial (Fin n) R
s : Fin n → Set R
hs : ∀ (i : Fin n), (s i).Infinite
h :
  ∀ x ∈ Set.pi (α := fun (i : Fin n) ↦ R) Set.univ s,
    Eq (α := R) ((eval x : (a : MvPolynomial (Fin n) R) → R) p : R) (0 : R)
zero :
  ∀ {p : MvPolynomial (Fin 0) R} (s : Fin 0 → Set R) (hs : ∀ (i : Fin 0), (s i).Infinite)
    (h :
      ∀ x ∈ Set.pi (α := fun (i : Fin 0) ↦ R) Set.univ s,
        Eq (α := R) ((eval x : (a : MvPolynomial (Fin 0) R) → R) p : R) (0 : R)),
    p = 0
succ :
  ∀ (n : ℕ)
    (ih :
      ∀ {p : MvPolynomial (Fin n) R} (s : Fin n → Set R) (hs : ∀ (i : Fin n), (s i).Infinite)
        (h :
          ∀ x ∈ Set.pi (α := fun (i : Fin n) ↦ R) Set.univ s,
            Eq (α := R) ((eval x : (a : MvPolynomial (Fin n) R) → R) p : R) (0 : R)),
        p = 0)
    {p : MvPolynomial (Fin (n + 1)) R} (s : Fin (n + 1) → Set R) (hs : ∀ (i : Fin (n + 1)), (s i).Infinite)
    (h :
      ∀ x ∈ Set.pi (α := fun (i : Fin (n + 1)) ↦ R) Set.univ s,
        Eq (α := R) ((eval x : (a : MvPolynomial (Fin (n + 1)) R) → R) p : R) (0 : R)),
    p = 0
⊢ p = 0

Tactic:
induction n with
  | zero =>
    apply (MvPolynomial.isEmptyRingEquiv R (Fin 0)).injective
    rw [map_zero]
    convert! h _ finZeroElim
  | succ n ih =>
    apply (finSuccEquiv R n).injective
    rw [map_zero]
    apply Polynomial.eq_zero_of_infinite_isRoot
    apply ((hs 0).image (C_injective ..).injOn).mono
    rintro _ ⟨r, hr, rfl⟩
    refine ih (s ·.succ) (fun _ ↦ hs _) fun x hx ↦ ?_
    rw [eval_polynomial_eval_finSuccEquiv]
    exact h _ fun i _ ↦ i.cases (by simpa using hr) (by simpa using hx)

Premises used: RingEquiv.injective, map_zero, MvPolynomial.finSuccEquiv, AlgEquiv.injective, Polynomial.eq_zero_of_infinite_isRoot, OfNat.ofNat, Fin, MvPolynomial.isEmptyRingEquiv, rfl, MvPolynomial.eval_polynomial_eval_finSuccEquiv
-- Module: Mathlib.Algebra.MvPolynomial.Funext
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
σ : Type u_2
p q : MvPolynomial σ R
s : σ → Set R
hs : ∀ (i : σ), (s i).Infinite
h :
  ∀ x ∈ Set.pi (α := fun (i : σ) ↦ R) Set.univ s,
    Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) p : R) ((eval x : (a : MvPolynomial σ R) → R) q : R)
this :
  ∀ (p : MvPolynomial σ R),
    (∀ x ∈ Set.pi (α := fun (i : σ) ↦ R) Set.univ s,
        Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) p : R) (0 : R)) →
      p = 0
rw :
  ∀ x ∈ Set.pi (α := fun (i : σ) ↦ R) Set.univ s,
    Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) (p - q) : R) (0 : R)
⊢ p = q

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

Premises used: sub_eq_zero, HSub.hSub
-- Module: Mathlib.Algebra.MvPolynomial.Funext
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
σ : Type u_2
p q : MvPolynomial σ R
s : σ → Set R
hs : ∀ (i : σ), (s i).Infinite
h :
  ∀ x ∈ Set.pi (α := fun (i : σ) ↦ R) Set.univ s,
    Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) p : R) ((eval x : (a : MvPolynomial σ R) → R) q : R)
this :
  ∀ (p : MvPolynomial σ R),
    (∀ x ∈ Set.pi (α := fun (i : σ) ↦ R) Set.univ s,
        Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) p : R) (0 : R)) →
      p = 0
x : (i : σ) → R
hx : x ∈ Set.pi (α := fun (i : σ) ↦ R) Set.univ s
simp_rw :
  HSub.hSub (α := R) (β := R) ((eval x : (a : MvPolynomial σ R) → R) p : R)
      ((eval x : (a : MvPolynomial σ R) → R) q : R) =
    0
simp_rw₁ :
  HSub.hSub (α := R) (β := R) ((eval x : (a : MvPolynomial σ R) → R) q : R)
      ((eval x : (a : MvPolynomial σ R) → R) q : R) =
    0
⊢ Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) (p - q) : R) (0 : R)

Tactic:
simp_rw [map_sub, h x hx, sub_self]

Premises used: map_sub, sub_self
-- Module: Mathlib.Algebra.MvPolynomial.Funext
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
σ : Type u_2
p q : MvPolynomial σ R
s : σ → Set R
hs : ∀ (i : σ), (s i).Infinite
h :
  ∀ x ∈ Set.pi (α := fun (i : σ) ↦ R) Set.univ s,
    Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) p : R) ((eval x : (a : MvPolynomial σ R) → R) q : R)
suffices :
  ∀ (p : MvPolynomial σ R),
    (∀ x ∈ Set.pi (α := fun (i : σ) ↦ R) Set.univ s,
        Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) p : R) (0 : R)) →
      p = 0
⊢ p = q

Tactic:
suffices ∀ p, (∀ x ∈ Set.pi .univ s, eval x p = 0) → p = 0 by
    rw [← sub_eq_zero, this (p - q)]
    intro x hx
    simp_rw [map_sub, h x hx, sub_self]
-- Module: Mathlib.Algebra.MvPolynomial.Funext
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
σ : Type u_2
p_1 q : MvPolynomial σ R
s : σ → Set R
hs : ∀ (i : σ), (s i).Infinite
h_1 :
  ∀ x ∈ Set.pi (α := fun (i : σ) ↦ R) Set.univ s,
    Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) p_1 : R) ((eval x : (a : MvPolynomial σ R) → R) q : R)
p : MvPolynomial σ R
h :
  ∀ x ∈ Set.pi (α := fun (i : σ) ↦ R) Set.univ s,
    Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) p : R) (0 : R)
obtain :
  ∀ (n : ℕ) (f : Fin n → σ) (hf : Function.Injective f) (p : MvPolynomial (Fin n) R)
    (h :
      ∀ x ∈ Set.pi (α := fun (i : σ) ↦ R) Set.univ s,
        Eq.{u_1 + 1} (α := R)
          ((eval x : (a : MvPolynomial σ R) → R)
              ((rename f : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R) p : MvPolynomial σ R) :
            R)
          (0 : R)),
    Eq (α := MvPolynomial σ R) ((rename f : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R) p : MvPolynomial σ R)
      (0 : MvPolynomial σ R)
⊢ p = 0

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

Premises used: MvPolynomial.exists_fin_rename, rfl
-- Module: Mathlib.Algebra.MvPolynomial.Funext
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
σ : Type u_2
p_1 q : MvPolynomial σ R
s : σ → Set R
hs : ∀ (i : σ), (s i).Infinite
h_1 :
  ∀ x ∈ Set.pi (α := fun (i : σ) ↦ R) Set.univ s,
    Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) p_1 : R) ((eval x : (a : MvPolynomial σ R) → R) q : R)
n : ℕ
f : Fin n → σ
hf : Function.Injective f
p : MvPolynomial (Fin n) R
h :
  ∀ x ∈ Set.pi (α := fun (i : σ) ↦ R) Set.univ s,
    Eq.{u_1 + 1} (α := R)
      ((eval x : (a : MvPolynomial σ R) → R)
          ((rename f : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R) p : MvPolynomial σ R) :
        R)
      (0 : R)
this : p = 0
rw : Eq (α := MvPolynomial σ R) ((rename f : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R) 0) 0
rw₁ rw₂ : Eq (α := MvPolynomial σ R) 0 0
⊢ Eq (α := MvPolynomial σ R) ((rename f : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R) p : MvPolynomial σ R)
    (0 : MvPolynomial σ R)

Tactic:
rw [this, map_zero]

Premises used: map_zero
-- Module: Mathlib.Algebra.MvPolynomial.Funext
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
σ : Type u_2
p_1 q : MvPolynomial σ R
s : σ → Set R
hs : ∀ (i : σ), (s i).Infinite
h_1 :
  ∀ x ∈ Set.pi (α := fun (i : σ) ↦ R) Set.univ s,
    Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) p_1 : R) ((eval x : (a : MvPolynomial σ R) → R) q : R)
n : ℕ
f : Fin n → σ
hf : Function.Injective f
p : MvPolynomial (Fin n) R
h :
  ∀ x ∈ Set.pi (α := fun (i : σ) ↦ R) Set.univ s,
    Eq.{u_1 + 1} (α := R)
      ((eval x : (a : MvPolynomial σ R) → R)
          ((rename f : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R) p : MvPolynomial σ R) :
        R)
      (0 : R)
suffices : p = 0
⊢ Eq (α := MvPolynomial σ R) ((rename f : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R) p : MvPolynomial σ R)
    (0 : MvPolynomial σ R)

Tactic:
suffices p = 0 by rw [this, map_zero]
-- Module: Mathlib.Algebra.MvPolynomial.Funext
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
σ : Type u_2
p_1 q : MvPolynomial σ R
s : σ → Set R
hs : ∀ (i : σ), (s i).Infinite
h_1 :
  ∀ x ∈ Set.pi (α := fun (i : σ) ↦ R) Set.univ s,
    Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) p_1 : R) ((eval x : (a : MvPolynomial σ R) → R) q : R)
n : ℕ
f : Fin n → σ
hf : Function.Injective f
p : MvPolynomial (Fin n) R
h :
  ∀ x ∈ Set.pi (α := fun (i : σ) ↦ R) Set.univ s,
    Eq.{u_1 + 1} (α := R)
      ((eval x : (a : MvPolynomial σ R) → R)
          ((rename f : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R) p : MvPolynomial σ R) :
        R)
      (0 : R)
⊢ p = 0

Tactic:
funext_fin (s ∘ f) (fun _ ↦ hs _) fun x hx ↦ ?_

Premises used: Function.comp, _private.0.MvPolynomial.funext_fin
-- Module: Mathlib.Algebra.MvPolynomial.Funext
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
σ : Type u_2
p_1 q : MvPolynomial σ R
s : σ → Set R
hs : ∀ (i : σ), (s i).Infinite
h_1 :
  ∀ x ∈ Set.pi (α := fun (i : σ) ↦ R) Set.univ s,
    Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) p_1 : R) ((eval x : (a : MvPolynomial σ R) → R) q : R)
n : ℕ
f : Fin n → σ
hf : Function.Injective f
p : MvPolynomial (Fin n) R
h :
  ∀ x ∈ Set.pi (α := fun (i : σ) ↦ R) Set.univ s,
    Eq.{u_1 + 1} (α := R)
      ((eval x : (a : MvPolynomial σ R) → R)
          ((rename f : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R) p : MvPolynomial σ R) :
        R)
      (0 : R)
refine :
  ∀ (x : (i : Fin n) → R) (hx : x ∈ Set.pi (α := fun (i : Fin n) ↦ R) Set.univ (s ∘ f)),
    Eq (α := R) ((eval x : (a : MvPolynomial (Fin n) R) → R) p : R) (0 : R)
⊢ p = 0

Tactic:
refine funext_fin (s ∘ f) (fun _ ↦ hs _) fun x hx ↦ ?_

Premises used: Function.comp, _private.0.MvPolynomial.funext_fin
-- Module: Mathlib.Algebra.MvPolynomial.Funext
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
σ : Type u_2
p_1 q : MvPolynomial σ R
s : σ → Set R
hs : ∀ (i : σ), (s i).Infinite
h_1 :
  ∀ x ∈ Set.pi (α := fun (i : σ) ↦ R) Set.univ s,
    Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) p_1 : R) ((eval x : (a : MvPolynomial σ R) → R) q : R)
n : ℕ
f : Fin n → σ
hf : Function.Injective f
p : MvPolynomial (Fin n) R
h :
  ∀ x ∈ Set.pi (α := fun (i : σ) ↦ R) Set.univ s,
    Eq.{u_1 + 1} (α := R)
      ((eval x : (a : MvPolynomial σ R) → R)
          ((rename f : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R) p : MvPolynomial σ R) :
        R)
      (0 : R)
x : (i : Fin n) → R
hx : x ∈ Set.pi (α := fun (i : Fin n) ↦ R) Set.univ (s ∘ f)
choose :
  ∀ (g : (i : σ) → R) (hg : ∀ (i : σ), g i ∈ s i),
    Eq (α := R) ((eval x : (a : MvPolynomial (Fin n) R) → R) p : R) (0 : R)
⊢ Eq (α := R) ((eval x : (a : MvPolynomial (Fin n) R) → R) p : R) (0 : R)

Tactic:
choose g hg using fun i ↦ (hs i).nonempty

Premises used: Set.Infinite.nonempty
-- Module: Mathlib.Algebra.MvPolynomial.Funext
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
σ : Type u_2
p_1 q : MvPolynomial σ R
s : σ → Set R
hs : ∀ (i : σ), (s i).Infinite
h_1 :
  ∀ x ∈ Set.pi (α := fun (i : σ) ↦ R) Set.univ s,
    Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) p_1 : R) ((eval x : (a : MvPolynomial σ R) → R) q : R)
n : ℕ
f : Fin n → σ
hf : Function.Injective f
p : MvPolynomial (Fin n) R
h :
  ∀ x ∈ Set.pi (α := fun (i : σ) ↦ R) Set.univ s,
    Eq.{u_1 + 1} (α := R)
      ((eval x : (a : MvPolynomial σ R) → R)
          ((rename f : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R) p : MvPolynomial σ R) :
        R)
      (0 : R)
x : (i : Fin n) → R
hx : x ∈ Set.pi (α := fun (i : Fin n) ↦ R) Set.univ (s ∘ f)
g : (i : σ) → R
hg : ∀ (i : σ), g i ∈ s i
⊢ Eq.{u_1 + 1} (α := R)
    ((eval (Function.extend f x g) : (a : MvPolynomial σ R) → R)
        ((rename f : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R) p : MvPolynomial σ R) :
      R)
    (0 : R)

Tactic:
h (Function.extend f x g) fun i _ ↦ ?_

Premises used: Function.extend
-- Module: Mathlib.Algebra.MvPolynomial.Funext
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
σ : Type u_2
p_1 q : MvPolynomial σ R
s : σ → Set R
hs : ∀ (i : σ), (s i).Infinite
h_1 :
  ∀ x ∈ Set.pi (α := fun (i : σ) ↦ R) Set.univ s,
    Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) p_1 : R) ((eval x : (a : MvPolynomial σ R) → R) q : R)
n : ℕ
f : Fin n → σ
hf : Function.Injective f
p : MvPolynomial (Fin n) R
h :
  ∀ x ∈ Set.pi (α := fun (i : σ) ↦ R) Set.univ s,
    Eq.{u_1 + 1} (α := R)
      ((eval x : (a : MvPolynomial σ R) → R)
          ((rename f : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R) p : MvPolynomial σ R) :
        R)
      (0 : R)
x : (i : Fin n) → R
hx : x ∈ Set.pi (α := fun (i : Fin n) ↦ R) Set.univ (s ∘ f)
g : (i : σ) → R
hg : ∀ (i : σ), g i ∈ s i
h₁ :
  Eq (α := R) ((eval x : (a : MvPolynomial (Fin n) R) → R) p : R)
    ((eval (Function.extend f x g) : (a : MvPolynomial σ R) → R)
        ((rename f : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R) p : MvPolynomial σ R) :
      R)
convert! : ∀ (i : σ), Membership.mem (γ := Set σ) Set.univ i → Function.extend f x g i ∈ s i
⊢ Eq (α := R) ((eval x : (a : MvPolynomial (Fin n) R) → R) p : R) (0 : R)

Tactic:
convert! h (Function.extend f x g) fun i _ ↦ ?_

Premises used: Function.extend
-- Module: Mathlib.Algebra.MvPolynomial.Funext
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
σ : Type u_2
p_1 q : MvPolynomial σ R
s : σ → Set R
hs : ∀ (i : σ), (s i).Infinite
h_1 :
  ∀ x ∈ Set.pi (α := fun (i : σ) ↦ R) Set.univ s,
    Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) p_1 : R) ((eval x : (a : MvPolynomial σ R) → R) q : R)
n : ℕ
f : Fin n → σ
hf : Function.Injective f
p : MvPolynomial (Fin n) R
h :
  ∀ x ∈ Set.pi (α := fun (i : σ) ↦ R) Set.univ s,
    Eq.{u_1 + 1} (α := R)
      ((eval x : (a : MvPolynomial σ R) → R)
          ((rename f : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R) p : MvPolynomial σ R) :
        R)
      (0 : R)
x : (i : Fin n) → R
hx : x ∈ Set.pi (α := fun (i : Fin n) ↦ R) Set.univ (s ∘ f)
g : (i : σ) → R
hg : ∀ (i : σ), g i ∈ s i
⊢ Eq (α := R) ((eval x : (a : MvPolynomial (Fin n) R) → R) p : R)
    ((eval (Function.extend f x g) : (a : MvPolynomial σ R) → R)
        ((rename f : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R) p : MvPolynomial σ R) :
      R)

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

Premises used: MvPolynomial.eval₂Hom_rename, MvPolynomial.eval, Function.extend_comp
-- Module: Mathlib.Algebra.MvPolynomial.Funext
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
σ : Type u_2
p_1 q : MvPolynomial σ R
s : σ → Set R
hs : ∀ (i : σ), (s i).Infinite
h_1 :
  ∀ x ∈ Set.pi (α := fun (i : σ) ↦ R) Set.univ s,
    Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) p_1 : R) ((eval x : (a : MvPolynomial σ R) → R) q : R)
n : ℕ
f : Fin n → σ
hf : Function.Injective f
p : MvPolynomial (Fin n) R
h :
  ∀ x ∈ Set.pi (α := fun (i : σ) ↦ R) Set.univ s,
    Eq.{u_1 + 1} (α := R)
      ((eval x : (a : MvPolynomial σ R) → R)
          ((rename f : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R) p : MvPolynomial σ R) :
        R)
      (0 : R)
x : (i : Fin n) → R
hx : x ∈ Set.pi (α := fun (i : Fin n) ↦ R) Set.univ (s ∘ f)
g : (i : σ) → R
hg : ∀ (i : σ), g i ∈ s i
i : σ
h_2 : Membership.mem (γ := Set σ) Set.univ i
inl : ∀ (i : Fin n), Membership.mem (γ := Set σ) Set.univ (f i) → Function.extend f x g (f i) ∈ s (f i)
inr : ∀ (nex : ¬∃ (x : Fin n), f x = i), Function.extend f x g i ∈ s i
⊢ Function.extend f x g i ∈ s i

Tactic:
obtain ⟨i, rfl⟩ | nex := em (∃ x, f x = i)

Premises used: Exists, em, Eq, rfl
-- Module: Mathlib.Algebra.MvPolynomial.Funext
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
σ : Type u_2
p_1 q : MvPolynomial σ R
s : σ → Set R
hs : ∀ (i : σ), (s i).Infinite
h_1 :
  ∀ x ∈ Set.pi (α := fun (i : σ) ↦ R) Set.univ s,
    Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) p_1 : R) ((eval x : (a : MvPolynomial σ R) → R) q : R)
n : ℕ
f : Fin n → σ
hf : Function.Injective f
p : MvPolynomial (Fin n) R
h :
  ∀ x ∈ Set.pi (α := fun (i : σ) ↦ R) Set.univ s,
    Eq.{u_1 + 1} (α := R)
      ((eval x : (a : MvPolynomial σ R) → R)
          ((rename f : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R) p : MvPolynomial σ R) :
        R)
      (0 : R)
x : (i : Fin n) → R
hx : x ∈ Set.pi (α := fun (i : Fin n) ↦ R) Set.univ (s ∘ f)
g : (i : σ) → R
hg : ∀ (i : σ), g i ∈ s i
i : Fin n
h_2 : Membership.mem (γ := Set σ) Set.univ (f i)
inl : x i ∈ s (f i)
⊢ Function.extend f x g (f i) ∈ s (f i)

Tactic:
rw [hf.extend_apply]

Premises used: Function.Injective.extend_apply
-- Module: Mathlib.Algebra.MvPolynomial.Funext
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
σ : Type u_2
p_1 q : MvPolynomial σ R
s : σ → Set R
hs : ∀ (i : σ), (s i).Infinite
h_1 :
  ∀ x ∈ Set.pi (α := fun (i : σ) ↦ R) Set.univ s,
    Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) p_1 : R) ((eval x : (a : MvPolynomial σ R) → R) q : R)
n : ℕ
f : Fin n → σ
hf : Function.Injective f
p : MvPolynomial (Fin n) R
h :
  ∀ x ∈ Set.pi (α := fun (i : σ) ↦ R) Set.univ s,
    Eq.{u_1 + 1} (α := R)
      ((eval x : (a : MvPolynomial σ R) → R)
          ((rename f : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R) p : MvPolynomial σ R) :
        R)
      (0 : R)
x : (i : Fin n) → R
hx : x ∈ Set.pi (α := fun (i : Fin n) ↦ R) Set.univ (s ∘ f)
g : (i : σ) → R
hg : ∀ (i : σ), g i ∈ s i
i : Fin n
h_2 : Membership.mem (γ := Set σ) Set.univ (f i)
⊢ x i ∈ s (f i)

Tactic:
hx _ ⟨⟩

Premises used: Set.Mem, True.intro
-- Module: Mathlib.Algebra.MvPolynomial.Funext
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
σ : Type u_2
p_1 q : MvPolynomial σ R
s : σ → Set R
hs : ∀ (i : σ), (s i).Infinite
h_1 :
  ∀ x ∈ Set.pi (α := fun (i : σ) ↦ R) Set.univ s,
    Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) p_1 : R) ((eval x : (a : MvPolynomial σ R) → R) q : R)
n : ℕ
f : Fin n → σ
hf : Function.Injective f
p : MvPolynomial (Fin n) R
h :
  ∀ x ∈ Set.pi (α := fun (i : σ) ↦ R) Set.univ s,
    Eq.{u_1 + 1} (α := R)
      ((eval x : (a : MvPolynomial σ R) → R)
          ((rename f : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R) p : MvPolynomial σ R) :
        R)
      (0 : R)
x : (i : Fin n) → R
hx : x ∈ Set.pi (α := fun (i : Fin n) ↦ R) Set.univ (s ∘ f)
g : (i : σ) → R
hg : ∀ (i : σ), g i ∈ s i
i : Fin n
h_2 : Membership.mem (γ := Set σ) Set.univ (f i)
⊢ x i ∈ s (f i)

Tactic:
exact hx _ ⟨⟩

Premises used: True.intro
-- Module: Mathlib.Algebra.MvPolynomial.Funext
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
σ : Type u_2
p_1 q : MvPolynomial σ R
s : σ → Set R
hs : ∀ (i : σ), (s i).Infinite
h_1 :
  ∀ x ∈ Set.pi (α := fun (i : σ) ↦ R) Set.univ s,
    Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) p_1 : R) ((eval x : (a : MvPolynomial σ R) → R) q : R)
n : ℕ
f : Fin n → σ
hf : Function.Injective f
p : MvPolynomial (Fin n) R
h :
  ∀ x ∈ Set.pi (α := fun (i : σ) ↦ R) Set.univ s,
    Eq.{u_1 + 1} (α := R)
      ((eval x : (a : MvPolynomial σ R) → R)
          ((rename f : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R) p : MvPolynomial σ R) :
        R)
      (0 : R)
x : (i : Fin n) → R
hx : x ∈ Set.pi (α := fun (i : Fin n) ↦ R) Set.univ (s ∘ f)
g : (i : σ) → R
hg : ∀ (i : σ), g i ∈ s i
i : σ
h_2 : Membership.mem (γ := Set σ) Set.univ i
nex : ¬∃ (x : Fin n), f x = i
inr inr₁ : Function.extend f x g i ∈ s i
inr₂ : (if h : ∃ (a : Fin n), f a = i then x (Classical.choose (p := fun (x : Fin n) ↦ f x = i) h) else g i) ∈ s i
inr₃ : g i ∈ s i
⊢ Function.extend f x g i ∈ s i

Tactic:
simp_rw [Function.extend, dif_neg nex, hg]

Premises used: dif_neg, Function.extend
-- Module: Mathlib.Algebra.MvPolynomial.Funext
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
σ : Type u_2
p : MvPolynomial σ R
s : σ → Set R
hs : ∀ (i : σ), (s i).Infinite
x : (i : σ) → R
h : x ∈ Set.pi (α := fun (i : σ) ↦ R) Set.univ s
⊢ Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) p : R) ((eval x : (a : MvPolynomial σ R) → R) p : R)

Tactic:
rfl
-- Module: Mathlib.Algebra.MvPolynomial.Funext
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Infinite R
σ : Type u_2
p q : MvPolynomial σ R
h :
  ∀ (x : σ → R),
    Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) p : R) ((eval x : (a : MvPolynomial σ R) → R) q : R)
⊢ p = q

Tactic:
funext_set _ (fun _ ↦ Set.infinite_univ) fun _ _ ↦ h _

Premises used: Set.infinite_univ, MvPolynomial.funext_set
-- Module: Mathlib.Algebra.MvPolynomial.Funext
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Infinite R
σ : Type u_2
p : MvPolynomial σ R
⊢ ∀ (x : σ → R),
    Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) p : R) ((eval x : (a : MvPolynomial σ R) → R) p : R)

Tactic:
simp only [forall_const]

Premises used: forall_const
-- Module: Mathlib.Algebra.MvPolynomial.Monad
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
f : σ → MvPolynomial τ R
⊢ aeval f = bind₁ f

Tactic:
rfl

Premises used: MvPolynomial.bind₁, rfl
-- Module: Mathlib.Algebra.MvPolynomial.Monad
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
f : σ → MvPolynomial τ R
⊢ eval₂Hom C f = (↑(bind₁ f) : MvPolynomial σ R →+* MvPolynomial τ R)

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, MvPolynomial.eval₂, MvPolynomial.eval₂Hom, MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, Finset.sum, rfl
-- Module: Mathlib.Algebra.MvPolynomial.Monad
Goal:
σ : Type u_1
R : Type u_3
S : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* MvPolynomial σ S
⊢ eval₂Hom f X = bind₂ f

Tactic:
rfl

Premises used: MvPolynomial.bind₂, rfl
-- Module: Mathlib.Algebra.MvPolynomial.Monad
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
⊢ Eq (α := MvPolynomial (MvPolynomial σ R) R →ₐ[R] MvPolynomial σ R) (aeval id) join₁

Tactic:
rfl

Premises used: MvPolynomial.join₁, rfl
-- Module: Mathlib.Algebra.MvPolynomial.Monad
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial (MvPolynomial σ R) R
⊢ Eq (α := MvPolynomial σ R)
    ((eval₂Hom C id : (a : MvPolynomial (MvPolynomial σ R) R) → MvPolynomial σ R) φ : MvPolynomial σ R)
    ((join₁ : (a : MvPolynomial (MvPolynomial σ R) R) → MvPolynomial σ R) φ : MvPolynomial σ R)

Tactic:
rfl

Premises used: MvPolynomial.C, rfl
-- Module: Mathlib.Algebra.MvPolynomial.Monad
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
⊢ Eq (α := MvPolynomial σ (MvPolynomial σ R) →+* MvPolynomial σ R) (eval₂Hom (RingHom.id (MvPolynomial σ R)) X) join₂

Tactic:
rfl

Premises used: MvPolynomial.join₂, rfl
-- Module: Mathlib.Algebra.MvPolynomial.Monad
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
f : σ → MvPolynomial τ R
i : σ
⊢ (bind₁ f : (a : MvPolynomial σ R) → MvPolynomial τ R) (X i) = f i

Tactic:
aeval_X f i

Premises used: MvPolynomial.aeval_X
-- Module: Mathlib.Algebra.MvPolynomial.Monad
Goal:
σ : Type u_1
R : Type u_3
S : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* MvPolynomial σ S
i : σ
⊢ Eq (α := MvPolynomial σ S) ((bind₂ f : (a : MvPolynomial σ R) → MvPolynomial σ S) (X i) : MvPolynomial σ S)
    (X i : MvPolynomial σ S)

Tactic:
eval₂Hom_X' f X i

Premises used: MvPolynomial.X, MvPolynomial.eval₂Hom_X'
-- Module: Mathlib.Algebra.MvPolynomial.Monad
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
hf :
  ∀ (i : σ),
    Eq (α := MvPolynomial σ R) ((bind₁ X : (a : MvPolynomial σ R) → MvPolynomial σ R) (X i) : MvPolynomial σ R)
      ((AlgHom.id R (MvPolynomial σ R) : (a : MvPolynomial σ R) → MvPolynomial σ R) (X i) : MvPolynomial σ R)
⊢ Eq (α := MvPolynomial σ R →ₐ[R] MvPolynomial σ R) (bind₁ X) (AlgHom.id R (MvPolynomial σ R))

Tactic:
ext1 i