awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
f : MvPolynomial σ R
hp : p > 0
hf : ¬f = 0
d : σ →₀ ℕ
⊢ ((p • d).sum fun (x : σ) ↦ id) = (d.sum fun (x : σ) ↦ id) * p
have neg : ∑ x ∈ d.support, id ((p • d : (a : σ) → ℕ) x) = (d.sum fun (x : σ) ↦ id) * p
Tactic: rw [Finsupp.sum_of_support_subset _ Finsupp.support_smul _ (by simp)]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
f : MvPolynomial σ R
⊢ totalDegree.{u_3, u_1} (R := R) (σ := σ) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) f) =
    f.totalDegree * p
have inl : ∀ (hp : p = 0),
  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]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Expand (goal)
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
⊢ totalDegree.{u_3, u_1} (R := R) (σ := σ) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) f) =
    f.totalDegree * p
have inr : ∀ (hp : p > 0),
  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]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Expand (goal)
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
⊢ totalDegree.{u_3, u_1} (R := R) (σ := σ) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) f) =
    f.totalDegree * p
have 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
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]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Expand (goal)
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
⊢ totalDegree.{u_3, u_1} (R := R) (σ := σ) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) f) =
    f.totalDegree * p
have 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
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]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Expand (goal)
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
⊢ totalDegree.{u_3, u_1} (R := R) (σ := σ) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) f) =
    f.totalDegree * p
have 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
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]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Expand (goal)
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
⊢ totalDegree.{u_3, u_1} (R := R) (σ := σ) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) f) =
    f.totalDegree * p
have 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)
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]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Expand (goal)
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)
⊢ totalDegree.{u_3, u_1} (R := R) (σ := σ) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) f) =
    f.totalDegree * p
have neg₄ : ∀ (hp : p > 0) (hf : ¬f = 0) (d : σ →₀ ℕ), ((p • d).sum fun (x : σ) ↦ id) = (d.sum fun (x : σ) ↦ id) * 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]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Expand (goal)
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
⊢ totalDegree.{u_3, u_1} (R := R) (σ := σ) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) f) =
    f.totalDegree * p
have neg₅ : ∀ (hp : p > 0) (hf : ¬f = 0) (d : σ →₀ ℕ), ∑ x ∈ d.support, id ((p • d : (a : σ) → ℕ) x) = (d.sum fun (x : σ) ↦ id) * 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]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Expand (goal)
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)
have refine : ∀ (f : MvPolynomial σ R)
  (hf : IsUnit (M := MvPolynomial σ R) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) f : MvPolynomial σ R)),
  IsUnit f
Tactic: refine ⟨fun f hf => ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Expand (hypothesis)
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 (coeff i f)
have hf₁ : 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
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Expand (goal)
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)
have refine : ∀ (i : σ →₀ ℕ) (hi : i ≠ 0), IsNilpotent (coeff i f)
Tactic: refine ⟨hf.1, fun i hi ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Expand (goal)
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
⊢ IsNilpotent (coeff i f)
have rw : IsNilpotent.{u_1} (R := R) (coeff (p • i) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) f))
Tactic: rw [← coeff_expand_smul p hp]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Expand (goal)
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
⊢ IsNilpotent.{u_1} (R := R) (coeff (p • i) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) f))
have a : p • i ≠ 0
Tactic: apply hf.2
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Funext (goal)
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)
⊢ p = 0
have 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)
Tactic: apply (MvPolynomial.isEmptyRingEquiv R (Fin 0)).injective
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Funext (goal)
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)
    ((isEmptyRingEquiv R (Fin 0) : (a : MvPolynomial (Fin 0) R) → R) 0 : R)
have zero : Eq (α := R) ((isEmptyRingEquiv R (Fin 0) : (a : MvPolynomial (Fin 0) R) → R) p : R) (0 : R)
Tactic: rw [map_zero]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Funext (goal)
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)
⊢ p = 0
have 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))
Tactic: apply (finSuccEquiv R n).injective
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Funext (goal)
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)
⊢ 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))
have 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}
Tactic: apply Polynomial.eq_zero_of_infinite_isRoot
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Funext (goal)
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)
⊢ 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}
have 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}
Tactic: apply ((hs 0).image (C_injective ..).injOn).mono
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Funext (goal)
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)
have 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)
Tactic: refine ih (s ·.succ) (fun _ ↦ hs _) fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Funext (goal)
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 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)
have 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)
Tactic: rw [eval_polynomial_eval_finSuccEquiv]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Funext (goal)
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)
⊢ p = 0
have 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
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)
Cleared hypotheses: n, p, s, hs, h