awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.MvPolynomial.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
f : MvPolynomial σ R
inl :
  ∀ (hp : p = 0),
    totalDegree.{u_3, u_1} (R := R) (σ := σ) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) f) =
      f.totalDegree * p
inr :
  ∀ (hp : p > 0),
    totalDegree.{u_3, u_1} (R := R) (σ := σ) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) f) =
      f.totalDegree * p
⊢ totalDegree.{u_3, u_1} (R := R) (σ := σ) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) f) =
    f.totalDegree * p

Tactic:
rcases p.eq_zero_or_pos with hp | hp

Premises used: Nat.eq_zero_or_pos
-- Module: Mathlib.Algebra.MvPolynomial.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
f : MvPolynomial σ R
hp : p = 0
⊢ totalDegree.{u_3, u_1} (R := R) (σ := σ) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) f) =
    f.totalDegree * p

Tactic:
simp [hp]
-- Module: Mathlib.Algebra.MvPolynomial.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
f : MvPolynomial σ R
hp : p > 0
pos :
  ∀ (hf : f = 0),
    totalDegree.{u_3, u_1} (R := R) (σ := σ) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) f) =
      f.totalDegree * p
neg :
  ∀ (hf : ¬f = 0),
    totalDegree.{u_3, u_1} (R := R) (σ := σ) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) f) =
      f.totalDegree * p
⊢ totalDegree.{u_3, u_1} (R := R) (σ := σ) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) f) =
    f.totalDegree * p

Tactic:
by_cases hf : f = 0
-- Module: Mathlib.Algebra.MvPolynomial.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
f : MvPolynomial σ R
hp : p > 0
hf : f = 0
pos :
  totalDegree.{u_3, u_1} (R := R) (σ := σ) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) 0) =
    totalDegree.{u_3, u_1} (R := R) (σ := σ) 0 * p
pos₁ : totalDegree.{u_3, u_1} (R := R) (σ := σ) 0 = totalDegree.{u_3, u_1} (R := R) (σ := σ) 0 * p
pos₂ : 0 = 0 * p
pos₃ pos₄ : Eq (α := ℕ) 0 0
⊢ totalDegree.{u_3, u_1} (R := R) (σ := σ) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) f) =
    f.totalDegree * p

Tactic:
rw [hf, map_zero, totalDegree_zero, zero_mul]

Premises used: MulZeroClass.zero_mul, map_zero, MvPolynomial.totalDegree_zero
-- Module: Mathlib.Algebra.MvPolynomial.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
f : MvPolynomial σ R
hp : p > 0
hf : ¬f = 0
neg :
  (Finset.sup (Finset.image (fun (x : σ →₀ ℕ) ↦ p • x) f.support) fun (m : σ →₀ ℕ) ↦
      Multiset.card.{u_1} (α := σ) ((Finsupp.toMultiset : (a : σ →₀ ℕ) → Multiset σ) m)) =
    (f.support.sup fun (m : σ →₀ ℕ) ↦
        Multiset.card.{u_1} (α := σ) ((Finsupp.toMultiset : (a : σ →₀ ℕ) → Multiset σ) m)) *
      p
⊢ totalDegree.{u_3, u_1} (R := R) (σ := σ) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) f) =
    f.totalDegree * p

Tactic:
simp_rw [totalDegree_eq, support_expand _ (p.ne_zero_iff_zero_lt.mpr hp)]

Premises used: Iff.mpr, MvPolynomial.totalDegree_eq, Nat.ne_zero_iff_zero_lt, MvPolynomial.support_expand
-- Module: Mathlib.Algebra.MvPolynomial.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
f : MvPolynomial σ R
hp : p > 0
hf : ¬f = 0
neg :
  Eq (α := ℕ) (f.support.sup fun (x : σ →₀ ℕ) ↦ (p • x).sum fun (x : σ) ↦ id)
    (f.support.sup fun (x : σ →₀ ℕ) ↦ (x.sum fun (x : σ) ↦ id) * p)
⊢ (Finset.sup (Finset.image (fun (x : σ →₀ ℕ) ↦ p • x) f.support) fun (m : σ →₀ ℕ) ↦
      Multiset.card.{u_1} (α := σ) ((Finsupp.toMultiset : (a : σ →₀ ℕ) → Multiset σ) m)) =
    (f.support.sup fun (m : σ →₀ ℕ) ↦
        Multiset.card.{u_1} (α := σ) ((Finsupp.toMultiset : (a : σ →₀ ℕ) → Multiset σ) m)) *
      p

Tactic:
simp only [Finsupp.card_toMultiset, Finset.sup_image, Finset.sup_mul₀, Function.comp_def]

Premises used: Finsupp.card_toMultiset, Function.comp_def, Finset.sup_image, Finset.sup_mul₀
-- Module: Mathlib.Algebra.MvPolynomial.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
f : MvPolynomial σ R
hp : p > 0
hf : ¬f = 0
neg : ∀ (d : σ →₀ ℕ), ((p • d).sum fun (x : σ) ↦ id) = (d.sum fun (x : σ) ↦ id) * p
⊢ Eq (α := ℕ) (f.support.sup fun (x : σ →₀ ℕ) ↦ (p • x).sum fun (x : σ) ↦ id)
    (f.support.sup fun (x : σ →₀ ℕ) ↦ (x.sum fun (x : σ) ↦ id) * p)

Tactic:
congr! 2 with d
-- Module: Mathlib.Algebra.MvPolynomial.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
f : MvPolynomial σ R
hp : p > 0
hf : ¬f = 0
d : σ →₀ ℕ
⊢ ∀ i ∈ d.support, Eq (α := ℕ) (id 0) 0

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
f : MvPolynomial σ R
hp : p > 0
hf : ¬f = 0
d : σ →₀ ℕ
neg : ∑ x ∈ d.support, id ((p • d : (a : σ) → ℕ) x) = (d.sum fun (x : σ) ↦ id) * p
⊢ ((p • d).sum fun (x : σ) ↦ id) = (d.sum fun (x : σ) ↦ id) * p

Tactic:
rw [Finsupp.sum_of_support_subset _ Finsupp.support_smul _ (by simp)]

Premises used: Finsupp.support_smul, Finsupp.sum_of_support_subset
-- Module: Mathlib.Algebra.MvPolynomial.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
f : MvPolynomial σ R
hp : p > 0
hf : ¬f = 0
d : σ →₀ ℕ
⊢ ∑ x ∈ d.support, id ((p • d : (a : σ) → ℕ) x) = (d.sum fun (x : σ) ↦ id) * p

Tactic:
simp [Finsupp.sum, Finset.sum_mul, mul_comm p]

Premises used: Finsupp.sum, mul_comm, Finset.sum_mul
-- Module: Mathlib.Algebra.MvPolynomial.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
f : MvPolynomial σ R
inl :
  ∀ (hp : p = 0),
    totalDegree.{u_3, u_1} (R := R) (σ := σ) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) f) =
      f.totalDegree * p
inr inr₁ :
  ∀ (hp : p > 0),
    totalDegree.{u_3, u_1} (R := R) (σ := σ) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) f) =
      f.totalDegree * p
pos :
  ∀ (hp : p > 0) (hf : f = 0),
    totalDegree.{u_3, u_1} (R := R) (σ := σ) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) f) =
      f.totalDegree * p
neg neg₁ :
  ∀ (hp : p > 0) (hf : ¬f = 0),
    totalDegree.{u_3, u_1} (R := R) (σ := σ) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) f) =
      f.totalDegree * p
neg₂ :
  ∀ (hp : p > 0) (hf : ¬f = 0),
    (Finset.sup (Finset.image (fun (x : σ →₀ ℕ) ↦ p • x) f.support) fun (m : σ →₀ ℕ) ↦
        Multiset.card.{u_1} (α := σ) ((Finsupp.toMultiset : (a : σ →₀ ℕ) → Multiset σ) m)) =
      (f.support.sup fun (m : σ →₀ ℕ) ↦
          Multiset.card.{u_1} (α := σ) ((Finsupp.toMultiset : (a : σ →₀ ℕ) → Multiset σ) m)) *
        p
neg₃ :
  ∀ (hp : p > 0) (hf : ¬f = 0),
    Eq (α := ℕ) (f.support.sup fun (x : σ →₀ ℕ) ↦ (p • x).sum fun (x : σ) ↦ id)
      (f.support.sup fun (x : σ →₀ ℕ) ↦ (x.sum fun (x : σ) ↦ id) * p)
neg₄ : ∀ (hp : p > 0) (hf : ¬f = 0) (d : σ →₀ ℕ), ((p • d).sum fun (x : σ) ↦ id) = (d.sum fun (x : σ) ↦ id) * p
neg₅ :
  ∀ (hp : p > 0) (hf : ¬f = 0) (d : σ →₀ ℕ),
    ∑ x ∈ d.support, id ((p • d : (a : σ) → ℕ) x) = (d.sum fun (x : σ) ↦ id) * p
⊢ totalDegree.{u_3, u_1} (R := R) (σ := σ) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) f) =
    f.totalDegree * p

Tactic:
classical
  rcases p.eq_zero_or_pos with hp | hp
  · simp [hp]
  by_cases hf : f = 0
  · rw [hf, map_zero, totalDegree_zero, zero_mul]
  simp_rw [totalDegree_eq, support_expand _ (p.ne_zero_iff_zero_lt.mpr hp)]
  simp only [Finsupp.card_toMultiset, Finset.sup_image, Finset.sup_mul₀, Function.comp_def]
  congr! 2 with d
  rw [Finsupp.sum_of_support_subset _ Finsupp.support_smul _ (by simp)]
  simp [Finsupp.sum, Finset.sum_mul, mul_comm p]

Premises used: MvPolynomial.totalDegree_eq, Finsupp.card_toMultiset, MulZeroClass.zero_mul, Finsupp.sum, map_zero, Function.comp_def, Finsupp.support_smul, Finset.sup_image, MvPolynomial.totalDegree_zero, mul_comm, Nat.eq_zero_or_pos, Finset.sum_mul, Finsupp.sum_of_support_subset, Finset.sup_mul₀
-- Module: Mathlib.Algebra.MvPolynomial.Expand
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
p : ℕ
hp : p ≠ 0
⊢ IsLocalHom (R := MvPolynomial σ R) (S := MvPolynomial σ R) (F := MvPolynomial σ R →ₐ[R] MvPolynomial σ R) (expand p)

Tactic:
⟨fun f hf => ?_⟩

Premises used: IsLocalHom.mk
-- Module: Mathlib.Algebra.MvPolynomial.Expand
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
p : ℕ
hp : p ≠ 0
refine :
  ∀ (f : MvPolynomial σ R)
    (hf : IsUnit (M := MvPolynomial σ R) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) f : MvPolynomial σ R)),
    IsUnit f
⊢ IsLocalHom (R := MvPolynomial σ R) (S := MvPolynomial σ R) (F := MvPolynomial σ R →ₐ[R] MvPolynomial σ R) (expand p)

Tactic:
refine ⟨fun f hf => ?_⟩
-- Module: Mathlib.Algebra.MvPolynomial.Expand
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
p : ℕ
hp : p ≠ 0
f : MvPolynomial σ R
hf :
  IsUnit.{u_1} (M := R) (coeff.{u_1, u_2} (σ := σ) 0 ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) f)) ∧
    ∀ (i : σ →₀ ℕ),
      i ≠ 0 → IsNilpotent.{u_1} (R := R) (coeff i ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) f))
⊢ IsUnit (coeff 0 f) ∧
    ∀ (i : σ →₀ ℕ),
      i ≠ 0 → IsNilpotent.{u_1} (R := R) (coeff i ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) f))

Tactic:
simp only [coeff_expand_zero p hp] at hf

Premises used: MvPolynomial.coeff_expand_zero
-- Module: Mathlib.Algebra.MvPolynomial.Expand
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
p : ℕ
hp : p ≠ 0
f : MvPolynomial σ R
hf :
  IsUnit (coeff 0 f) ∧
    ∀ (i : σ →₀ ℕ),
      i ≠ 0 → IsNilpotent.{u_1} (R := R) (coeff i ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) f))
⊢ IsUnit (coeff 0 f) ∧ ∀ (i : σ →₀ ℕ), i ≠ 0 → IsNilpotent (coeff i f)

Tactic:
⟨hf.1, fun i hi ↦ ?_⟩

Premises used: And.left, And.intro
-- Module: Mathlib.Algebra.MvPolynomial.Expand
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
p : ℕ
hp : p ≠ 0
f : MvPolynomial σ R
hf :
  IsUnit (coeff 0 f) ∧
    ∀ (i : σ →₀ ℕ),
      i ≠ 0 → IsNilpotent.{u_1} (R := R) (coeff i ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) f))
refine : ∀ (i : σ →₀ ℕ) (hi : i ≠ 0), IsNilpotent (coeff i f)
⊢ IsUnit (coeff 0 f) ∧ ∀ (i : σ →₀ ℕ), i ≠ 0 → IsNilpotent (coeff i f)

Tactic:
refine ⟨hf.1, fun i hi ↦ ?_⟩
-- Module: Mathlib.Algebra.MvPolynomial.Expand
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
p : ℕ
hp : p ≠ 0
f : MvPolynomial σ R
hf :
  IsUnit (coeff 0 f) ∧
    ∀ (i : σ →₀ ℕ),
      i ≠ 0 → IsNilpotent.{u_1} (R := R) (coeff i ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) f))
i : σ →₀ ℕ
hi : i ≠ 0
rw : IsNilpotent.{u_1} (R := R) (coeff (p • i) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) f))
⊢ IsNilpotent (coeff i f)

Tactic:
rw [← coeff_expand_smul p hp]

Premises used: MvPolynomial.coeff_expand_smul
-- Module: Mathlib.Algebra.MvPolynomial.Expand
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
p : ℕ
hp : p ≠ 0
f : MvPolynomial σ R
hf :
  IsUnit (coeff 0 f) ∧
    ∀ (i : σ →₀ ℕ),
      i ≠ 0 → IsNilpotent.{u_1} (R := R) (coeff i ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) f))
i : σ →₀ ℕ
hi : i ≠ 0
a : p • i ≠ 0
⊢ IsNilpotent.{u_1} (R := R) (coeff (p • i) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) f))

Tactic:
apply hf.2

Premises used: And.right
-- Module: Mathlib.Algebra.MvPolynomial.Expand
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
p : ℕ
hp : p ≠ 0
f : MvPolynomial σ R
hf :
  IsUnit (coeff 0 f) ∧
    ∀ (i : σ →₀ ℕ),
      i ≠ 0 → IsNilpotent.{u_1} (R := R) (coeff i ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) f))
i : σ →₀ ℕ
hi : i ≠ 0
⊢ p • i ≠ 0

Tactic:
simp [hi, hp]
-- Module: Mathlib.Algebra.MvPolynomial.Expand
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
p : ℕ
hp : p ≠ 0
f : MvPolynomial σ R
hf : Irreducible (M := MvPolynomial σ R) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
⊢ Irreducible f

Tactic:
let _ := isLocalHom_expand R σ hp
  hf.of_map

Premises used: MvPolynomial.isLocalHom_expand, Irreducible.of_map
-- Module: Mathlib.Algebra.MvPolynomial.Funext
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
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)
zero :
  Eq (α := R) ((isEmptyRingEquiv R (Fin 0) : (a : MvPolynomial (Fin 0) R) → R) p : R)
    ((isEmptyRingEquiv R (Fin 0) : (a : MvPolynomial (Fin 0) R) → R) 0 : R)
⊢ p = 0

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

Premises used: RingEquiv.injective, OfNat.ofNat, Fin, MvPolynomial.isEmptyRingEquiv
-- Module: Mathlib.Algebra.MvPolynomial.Funext
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
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)
zero : Eq (α := R) ((isEmptyRingEquiv R (Fin 0) : (a : MvPolynomial (Fin 0) R) → R) p : R) (0 : R)
⊢ Eq (α := R) ((isEmptyRingEquiv R (Fin 0) : (a : MvPolynomial (Fin 0) R) → R) p : R)
    ((isEmptyRingEquiv R (Fin 0) : (a : MvPolynomial (Fin 0) R) → R) 0 : R)

Tactic:
rw [map_zero]

Premises used: map_zero
-- Module: Mathlib.Algebra.MvPolynomial.Funext
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
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)
⊢ Eq (α := R)
    ((eval fun (a : Fin 0) ↦ isEmptyElim (p := fun (x : Fin 0) ↦ R) a : (a : MvPolynomial (Fin 0) R) → R) p : R) (0 : R)

Tactic:
h _ finZeroElim

Premises used: finZeroElim
-- Module: Mathlib.Algebra.MvPolynomial.Funext
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
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)
⊢ Eq (α := R) ((isEmptyRingEquiv R (Fin 0) : (a : MvPolynomial (Fin 0) R) → R) p : R) (0 : R)

Tactic:
convert! h _ finZeroElim

Premises used: finZeroElim
-- 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)
succ :
  Eq (α := Polynomial (MvPolynomial (Fin n) R))
    ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → Polynomial (MvPolynomial (Fin n) R)) p :
      Polynomial (MvPolynomial (Fin n) R))
    ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → Polynomial (MvPolynomial (Fin n) R)) 0 :
      Polynomial (MvPolynomial (Fin n) R))
⊢ p = 0

Tactic:
apply (finSuccEquiv R n).injective

Premises used: MvPolynomial.finSuccEquiv, AlgEquiv.injective
-- 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)
succ :
  Set.Infinite.{u_1} (α := MvPolynomial (Fin n) R)
    {x : MvPolynomial (Fin n) R |
      Polynomial.IsRoot
        ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → Polynomial (MvPolynomial (Fin n) R)) p) x}
⊢ Eq (α := Polynomial (MvPolynomial (Fin n) R))
    ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → Polynomial (MvPolynomial (Fin n) R)) p :
      Polynomial (MvPolynomial (Fin n) R))
    (0 : Polynomial (MvPolynomial (Fin n) R))

Tactic:
apply Polynomial.eq_zero_of_infinite_isRoot

Premises used: Polynomial.eq_zero_of_infinite_isRoot
-- 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)
succ :
  Subset (α := Set (MvPolynomial (Fin n) R)) ((⇑C : (a : R) → MvPolynomial (Fin n) R) '' s 0)
    {x : MvPolynomial (Fin n) R |
      Polynomial.IsRoot
        ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → Polynomial (MvPolynomial (Fin n) R)) p) x}
⊢ Set.Infinite.{u_1} (α := MvPolynomial (Fin n) R)
    {x : MvPolynomial (Fin n) R |
      Polynomial.IsRoot
        ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → Polynomial (MvPolynomial (Fin n) R)) p) x}

Tactic:
apply ((hs 0).image (C_injective ..).injOn).mono

Premises used: Set.Infinite.mono, Set.Infinite.image, Function.Injective.injOn, MvPolynomial.C_injective, OfNat.ofNat
-- 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
⊢ Membership.mem (α := MvPolynomial (Fin n) R) (γ := Set (MvPolynomial (Fin n) R))
    {x : MvPolynomial (Fin n) R |
      Polynomial.IsRoot
        ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → Polynomial (MvPolynomial (Fin n) R)) p) x}
    ((C : (a : R) → MvPolynomial (Fin n) R) r : MvPolynomial (Fin n) R)

Tactic:
ih (s ·.succ) (fun _ ↦ hs _) fun x hx ↦ ?_

Premises used: Fin.succ, Set.Mem, Polynomial.IsRoot, setOf
-- 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
succ :
  ∀ (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 x : (a : MvPolynomial (Fin n) R) → R)
          (Polynomial.eval ((C : (a : R) → MvPolynomial (Fin n) R) r)
              ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → Polynomial (MvPolynomial (Fin n) R)) p) :
            MvPolynomial (Fin n) R) :
        R)
      (0 : R)
⊢ Membership.mem (α := MvPolynomial (Fin n) R) (γ := Set (MvPolynomial (Fin n) R))
    {x : MvPolynomial (Fin n) R |
      Polynomial.IsRoot
        ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → Polynomial (MvPolynomial (Fin n) R)) p) x}
    ((C : (a : R) → MvPolynomial (Fin n) R) r : MvPolynomial (Fin n) R)

Tactic:
refine ih (s ·.succ) (fun _ ↦ hs _) fun x hx ↦ ?_

Premises used: Fin.succ
-- 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
succ :
  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)
⊢ Eq (α := R)
    ((eval x : (a : MvPolynomial (Fin n) R) → R)
        (Polynomial.eval ((C : (a : R) → MvPolynomial (Fin n) R) r)
            ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → Polynomial (MvPolynomial (Fin n) R)) p) :
          MvPolynomial (Fin n) R) :
      R)
    (0 : R)

Tactic:
rw [eval_polynomial_eval_finSuccEquiv]

Premises used: MvPolynomial.eval_polynomial_eval_finSuccEquiv
-- 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
i : Fin (n + 1)
h_1 : Membership.mem (γ := Set (Fin (n + 1))) Set.univ i
⊢ Membership.mem (α := (fun (i : Fin (n + 1)) ↦ R) 0) (s 0)
    (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 0 :
      R)

Tactic:
simpa using hr
-- 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
i : Fin (n + 1)
h_1 : Membership.mem (γ := Set (Fin (n + 1))) Set.univ i
⊢ ∀ (i : Fin n),
    Membership.mem (α := (fun (i : Fin (n + 1)) ↦ R) i.succ) (s i.succ)
      (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.succ :
        R)

Tactic:
simpa using hx