awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
hi :
  Ne.{u + 1} (α := MvPolynomial (Fin n) R)
    (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) i) 0
hf'_sup :
  Finset.Nonempty (α := Fin n →₀ ℕ)
    (support.{u, 0} (R := R)
      (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) i))
⊢ totalDegree.{u, 0} (R := R) (σ := Fin n)
        (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) i) +
      i ≤
    f.totalDegree
have have : ∀ (σ : Fin n →₀ ℕ)
  (hσ1 :
    Membership.mem (γ := Finset (Fin n →₀ ℕ))
      (support.{u, 0} (R := R)
        (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) i))
      σ)
  (hσ2 :
    Eq (α := ℕ)
      (Finset.sup
        (support.{u, 0} (R := R)
          (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)
            i))
        fun (s : Fin n →₀ ℕ) ↦ s.sum fun (x : Fin n) (e : ℕ) ↦ e)
      (σ.sum fun (x : Fin n) (e : ℕ) ↦ e)),
  totalDegree.{u, 0} (R := R) (σ := Fin n)
        (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) i) +
      i ≤
    f.totalDegree
Tactic: have ⟨σ, hσ1, hσ2⟩ := Finset.exists_mem_eq_sup (support _) hf'_sup
                          (fun s => Finsupp.sum s fun _ e => e)
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
hi :
  Ne.{u + 1} (α := MvPolynomial (Fin n) R)
    (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) i) 0
hf'_sup :
  Finset.Nonempty (α := Fin n →₀ ℕ)
    (support.{u, 0} (R := R)
      (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) i))
σ : Fin n →₀ ℕ
hσ1 :
  Membership.mem (γ := Finset (Fin n →₀ ℕ))
    (support.{u, 0} (R := R)
      (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) i))
    σ
hσ2 :
  Eq (α := ℕ)
    (Finset.sup
      (support.{u, 0} (R := R)
        (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) i))
      fun (s : Fin n →₀ ℕ) ↦ s.sum fun (x : Fin n) (e : ℕ) ↦ e)
    (σ.sum fun (x : Fin n) (e : ℕ) ↦ e)
σ' : Fin (n + 1) →₀ ℕ := cons i σ
⊢ totalDegree.{u, 0} (R := R) (σ := Fin n)
        (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) i) +
      i ≤
    f.totalDegree
have h : totalDegree.{u, 0} (R := R) (σ := Fin n)
      (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) i) +
    i =
  σ'.sum fun (x : Fin (n + 1)) (e : ℕ) ↦ e
Tactic: convert! le_totalDegree (s := σ') _
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
hi :
  Ne.{u + 1} (α := MvPolynomial (Fin n) R)
    (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) i) 0
hf'_sup :
  Finset.Nonempty (α := Fin n →₀ ℕ)
    (support.{u, 0} (R := R)
      (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) i))
σ : Fin n →₀ ℕ
hσ1 :
  Membership.mem (γ := Finset (Fin n →₀ ℕ))
    (support.{u, 0} (R := R)
      (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) i))
    σ
hσ2 :
  Eq (α := ℕ)
    (Finset.sup
      (support.{u, 0} (R := R)
        (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) i))
      fun (s : Fin n →₀ ℕ) ↦ s.sum fun (x : Fin n) (e : ℕ) ↦ e)
    (σ.sum fun (x : Fin n) (e : ℕ) ↦ e)
σ' : Fin (n + 1) →₀ ℕ := cons i σ
h :
  totalDegree.{u, 0} (R := R) (σ := Fin n)
        (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) i) +
      i =
    σ'.sum fun (x : Fin (n + 1)) (e : ℕ) ↦ e
⊢ totalDegree.{u, 0} (R := R) (σ := Fin n)
        (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) i) +
      i ≤
    f.totalDegree
have convert_4 : σ' ∈ f.support
Tactic: convert! le_totalDegree (s := σ') _
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
hi :
  Ne.{u + 1} (α := MvPolynomial (Fin n) R)
    (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) i) 0
hf'_sup :
  Finset.Nonempty (α := Fin n →₀ ℕ)
    (support.{u, 0} (R := R)
      (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) i))
σ : Fin n →₀ ℕ
hσ1 :
  Membership.mem (γ := Finset (Fin n →₀ ℕ))
    (support.{u, 0} (R := R)
      (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) i))
    σ
hσ2 :
  Eq (α := ℕ)
    (Finset.sup
      (support.{u, 0} (R := R)
        (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) i))
      fun (s : Fin n →₀ ℕ) ↦ s.sum fun (x : Fin n) (e : ℕ) ↦ e)
    (σ.sum fun (x : Fin n) (e : ℕ) ↦ e)
σ' : Fin (n + 1) →₀ ℕ := cons i σ
⊢ totalDegree.{u, 0} (R := R) (σ := Fin n)
        (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) i) +
      i =
    σ'.sum fun (x : Fin (n + 1)) (e : ℕ) ↦ e
have h : (Finset.sup
      (support.{u, 0} (R := R)
        (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) i))
      fun (s : Fin n →₀ ℕ) ↦ s.sum fun (x : Fin n) (e : ℕ) ↦ e) +
    i =
  σ'.sum fun (x : Fin (n + 1)) (e : ℕ) ↦ e
Tactic: rw [totalDegree, hσ2, sum_cons, add_comm]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
hi :
  Ne.{u + 1} (α := MvPolynomial (Fin n) R)
    (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) i) 0
hf'_sup :
  Finset.Nonempty (α := Fin n →₀ ℕ)
    (support.{u, 0} (R := R)
      (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) i))
σ : Fin n →₀ ℕ
hσ1 :
  Membership.mem (γ := Finset (Fin n →₀ ℕ))
    (support.{u, 0} (R := R)
      (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) i))
    σ
hσ2 :
  Eq (α := ℕ)
    (Finset.sup
      (support.{u, 0} (R := R)
        (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) i))
      fun (s : Fin n →₀ ℕ) ↦ s.sum fun (x : Fin n) (e : ℕ) ↦ e)
    (σ.sum fun (x : Fin n) (e : ℕ) ↦ e)
σ' : Fin (n + 1) →₀ ℕ := cons i σ
h :
  (Finset.sup
        (support.{u, 0} (R := R)
          (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)
            i))
        fun (s : Fin n →₀ ℕ) ↦ s.sum fun (x : Fin n) (e : ℕ) ↦ e) +
      i =
    σ'.sum fun (x : Fin (n + 1)) (e : ℕ) ↦ e
⊢ totalDegree.{u, 0} (R := R) (σ := Fin n)
        (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) i) +
      i =
    σ'.sum fun (x : Fin (n + 1)) (e : ℕ) ↦ e
have h₁ : (σ.sum fun (x : Fin n) (e : ℕ) ↦ e) + i = σ'.sum fun (x : Fin (n + 1)) (e : ℕ) ↦ e
Tactic: rw [totalDegree, hσ2, sum_cons, add_comm]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
hi :
  Ne.{u + 1} (α := MvPolynomial (Fin n) R)
    (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) i) 0
hf'_sup :
  Finset.Nonempty (α := Fin n →₀ ℕ)
    (support.{u, 0} (R := R)
      (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) i))
σ : Fin n →₀ ℕ
hσ1 :
  Membership.mem (γ := Finset (Fin n →₀ ℕ))
    (support.{u, 0} (R := R)
      (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) i))
    σ
hσ2 :
  Eq (α := ℕ)
    (Finset.sup
      (support.{u, 0} (R := R)
        (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) i))
      fun (s : Fin n →₀ ℕ) ↦ s.sum fun (x : Fin n) (e : ℕ) ↦ e)
    (σ.sum fun (x : Fin n) (e : ℕ) ↦ e)
σ' : Fin (n + 1) →₀ ℕ := cons i σ
h :
  (Finset.sup
        (support.{u, 0} (R := R)
          (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)
            i))
        fun (s : Fin n →₀ ℕ) ↦ s.sum fun (x : Fin n) (e : ℕ) ↦ e) +
      i =
    σ'.sum fun (x : Fin (n + 1)) (e : ℕ) ↦ e
h₁ : (σ.sum fun (x : Fin n) (e : ℕ) ↦ e) + i = σ'.sum fun (x : Fin (n + 1)) (e : ℕ) ↦ e
⊢ totalDegree.{u, 0} (R := R) (σ := Fin n)
        (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) i) +
      i =
    σ'.sum fun (x : Fin (n + 1)) (e : ℕ) ↦ e
have h₂ : (σ.sum fun (x : Fin n) (e : ℕ) ↦ e) + i = i + σ.sum fun (x : Fin n) (e : ℕ) ↦ e
Tactic: rw [totalDegree, hσ2, sum_cons, add_comm]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
hi :
  Ne.{u + 1} (α := MvPolynomial (Fin n) R)
    (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) i) 0
hf'_sup :
  Finset.Nonempty (α := Fin n →₀ ℕ)
    (support.{u, 0} (R := R)
      (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) i))
σ : Fin n →₀ ℕ
hσ1 :
  Membership.mem (γ := Finset (Fin n →₀ ℕ))
    (support.{u, 0} (R := R)
      (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) i))
    σ
hσ2 :
  Eq (α := ℕ)
    (Finset.sup
      (support.{u, 0} (R := R)
        (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) i))
      fun (s : Fin n →₀ ℕ) ↦ s.sum fun (x : Fin n) (e : ℕ) ↦ e)
    (σ.sum fun (x : Fin n) (e : ℕ) ↦ e)
σ' : Fin (n + 1) →₀ ℕ := cons i σ
h :
  (Finset.sup
        (support.{u, 0} (R := R)
          (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)
            i))
        fun (s : Fin n →₀ ℕ) ↦ s.sum fun (x : Fin n) (e : ℕ) ↦ e) +
      i =
    σ'.sum fun (x : Fin (n + 1)) (e : ℕ) ↦ e
h₁ : (σ.sum fun (x : Fin n) (e : ℕ) ↦ e) + i = σ'.sum fun (x : Fin (n + 1)) (e : ℕ) ↦ e
h₂ : (σ.sum fun (x : Fin n) (e : ℕ) ↦ e) + i = i + σ.sum fun (x : Fin n) (e : ℕ) ↦ e
⊢ totalDegree.{u, 0} (R := R) (σ := Fin n)
        (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) i) +
      i =
    σ'.sum fun (x : Fin (n + 1)) (e : ℕ) ↦ e
have h₃ : (i + σ.sum fun (x : Fin n) (e : ℕ) ↦ e) = i + σ.sum fun (x : Fin n) (e : ℕ) ↦ e
Tactic: rw [totalDegree, hσ2, sum_cons, add_comm]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
⊢ Polynomial.support.{u} (R := MvPolynomial (Fin n) R)
      ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) =
    Finset.image (fun (m : Fin (n + 1) →₀ ℕ) ↦ (m : (a : Fin (n + 1)) → ℕ) 0) f.support
have h : ∀ (i : ℕ),
  i ∈
      Polynomial.support.{u} (R := MvPolynomial (Fin n) R)
        ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) ↔
    Membership.mem (γ := Finset ℕ) (Finset.image (fun (m : Fin (n + 1) →₀ ℕ) ↦ (m : (a : Fin (n + 1)) → ℕ) 0) f.support)
      i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
⊢ i ∈
      Polynomial.support.{u} (R := MvPolynomial (Fin n) R)
        ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) ↔
    Membership.mem (γ := Finset ℕ) (Finset.image (fun (m : Fin (n + 1) →₀ ℕ) ↦ (m : (a : Fin (n + 1)) → ℕ) 0) f.support)
      i
have h : (∃ (a : Fin n →₀ ℕ),
    Ne.{u + 1} (α := R)
      ((Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) i :
            (a : Fin n →₀ ℕ) → R)
          a :
        R)
      ((0 : (a : Fin n →₀ ℕ) → R) a : R)) ↔
  ∃ a ∈ f.support, (a : (a : Fin (n + 1)) → ℕ) 0 = i
Tactic: rw [Polynomial.mem_support_iff, Finset.mem_image, Finsupp.ne_iff]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
⊢ (∃ (a : Fin n →₀ ℕ),
      Ne.{u + 1} (α := R)
        ((Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) i :
              (a : Fin n →₀ ℕ) → R)
            a :
          R)
        ((0 : (a : Fin n →₀ ℕ) → R) a : R)) ↔
    ∃ a ∈ f.support, (a : (a : Fin (n + 1)) → ℕ) 0 = i
have h : (∃ (a : Fin n →₀ ℕ),
    Ne.{u + 1} (α := R)
      ((Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) i :
            (a : Fin n →₀ ℕ) → R)
          a :
        R)
      ((0 : (a : Fin n →₀ ℕ) → R) a : R)) →
  ∃ a ∈ f.support, (a : (a : Fin (n + 1)) → ℕ) 0 = i
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
h :
  (∃ (a : Fin n →₀ ℕ),
      Ne.{u + 1} (α := R)
        ((Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) i :
              (a : Fin n →₀ ℕ) → R)
            a :
          R)
        ((0 : (a : Fin n →₀ ℕ) → R) a : R)) →
    ∃ a ∈ f.support, (a : (a : Fin (n + 1)) → ℕ) 0 = i
⊢ (∃ (a : Fin n →₀ ℕ),
      Ne.{u + 1} (α := R)
        ((Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) i :
              (a : Fin n →₀ ℕ) → R)
            a :
          R)
        ((0 : (a : Fin n →₀ ℕ) → R) a : R)) ↔
    ∃ a ∈ f.support, (a : (a : Fin (n + 1)) → ℕ) 0 = i
have h₁ : (∃ a ∈ f.support, (a : (a : Fin (n + 1)) → ℕ) 0 = i) →
  ∃ (a : Fin n →₀ ℕ),
    Ne.{u + 1} (α := R)
      ((Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) i :
            (a : Fin n →₀ ℕ) → R)
          a :
        R)
      ((0 : (a : Fin n →₀ ℕ) → R) a : R)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin n →₀ ℕ
hm :
  Ne.{u + 1} (α := R)
    ((Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) i :
          (a : Fin n →₀ ℕ) → R)
        m :
      R)
    ((0 : (a : Fin n →₀ ℕ) → R) m : R)
⊢ ∃ a ∈ f.support, (a : (a : Fin (n + 1)) → ℕ) 0 = i
have h : cons i m ∈ f.support
Tactic: refine ⟨cons i m, ?_, cons_zero _ _⟩
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin n →₀ ℕ
hm :
  Ne.{u + 1} (α := R)
    ((Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) i :
          (a : Fin n →₀ ℕ) → R)
        m :
      R)
    ((0 : (a : Fin n →₀ ℕ) → R) m : R)
⊢ cons i m ∈ f.support
have h : Membership.mem (γ := Finset (Fin n →₀ ℕ))
  (support.{u, 0} (R := R)
    (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) i))
  m
Tactic: rw [← mem_support_coeff_finSuccEquiv]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
m : Fin (n + 1) →₀ ℕ
h : m ∈ f.support
⊢ ∃ (a : Fin n →₀ ℕ),
    Ne.{u + 1} (α := R)
      ((Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)
              ((m : (a : Fin (n + 1)) → ℕ) 0) :
            (a : Fin n →₀ ℕ) → R)
          a :
        R)
      ((0 : (a : Fin n →₀ ℕ) → R) a : R)
have h₁ : Ne.{u + 1} (α := R)
  ((Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)
          ((m : (a : Fin (n + 1)) → ℕ) 0) :
        (a : Fin n →₀ ℕ) → R)
      m.tail :
    R)
  ((0 : (a : Fin n →₀ ℕ) → R) m.tail : R)
Tactic: refine ⟨tail m, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
m : Fin (n + 1) →₀ ℕ
h : m ∈ f.support
⊢ Ne.{u + 1} (α := R)
    ((Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)
            ((m : (a : Fin (n + 1)) → ℕ) 0) :
          (a : Fin n →₀ ℕ) → R)
        m.tail :
      R)
    ((0 : (a : Fin n →₀ ℕ) → R) m.tail : R)
have h₁ : Ne.{u + 1} (α := R)
  (coeff m.tail
      (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)
        ((m : (a : Fin (n + 1)) → ℕ) 0)) :
    R)
  ((0 : (a : Fin n →₀ ℕ) → R) m.tail : R)
Tactic: rwa [← coeff, zero_apply, ← mem_support_iff, mem_support_coeff_finSuccEquiv, cons_tail]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
m : Fin (n + 1) →₀ ℕ
h : m ∈ f.support
h₁ :
  Ne.{u + 1} (α := R)
    (coeff m.tail
        (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)
          ((m : (a : Fin (n + 1)) → ℕ) 0)) :
      R)
    ((0 : (a : Fin n →₀ ℕ) → R) m.tail : R)
⊢ Ne.{u + 1} (α := R)
    ((Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)
            ((m : (a : Fin (n + 1)) → ℕ) 0) :
          (a : Fin n →₀ ℕ) → R)
        m.tail :
      R)
    ((0 : (a : Fin n →₀ ℕ) → R) m.tail : R)
have h₂ : Ne.{u + 1} (α := R)
  (coeff m.tail
    (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)
      ((m : (a : Fin (n + 1)) → ℕ) 0)))
  0
Tactic: rwa [← coeff, zero_apply, ← mem_support_iff, mem_support_coeff_finSuccEquiv, cons_tail]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
m : Fin (n + 1) →₀ ℕ
h : m ∈ f.support
h₁ :
  Ne.{u + 1} (α := R)
    (coeff m.tail
        (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)
          ((m : (a : Fin (n + 1)) → ℕ) 0)) :
      R)
    ((0 : (a : Fin n →₀ ℕ) → R) m.tail : R)
h₂ :
  Ne.{u + 1} (α := R)
    (coeff m.tail
      (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)
        ((m : (a : Fin (n + 1)) → ℕ) 0)))
    0
⊢ Ne.{u + 1} (α := R)
    ((Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)
            ((m : (a : Fin (n + 1)) → ℕ) 0) :
          (a : Fin n →₀ ℕ) → R)
        m.tail :
      R)
    ((0 : (a : Fin n →₀ ℕ) → R) m.tail : R)
have h₃ : Membership.mem (γ := Finset (Fin n →₀ ℕ))
  (support.{u, 0} (R := R)
    (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)
      ((m : (a : Fin (n + 1)) → ℕ) 0)))
  m.tail
Tactic: rwa [← coeff, zero_apply, ← mem_support_iff, mem_support_coeff_finSuccEquiv, cons_tail]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
m : Fin (n + 1) →₀ ℕ
h : m ∈ f.support
h₁ :
  Ne.{u + 1} (α := R)
    (coeff m.tail
        (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)
          ((m : (a : Fin (n + 1)) → ℕ) 0)) :
      R)
    ((0 : (a : Fin n →₀ ℕ) → R) m.tail : R)
h₂ :
  Ne.{u + 1} (α := R)
    (coeff m.tail
      (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)
        ((m : (a : Fin (n + 1)) → ℕ) 0)))
    0
h₃ :
  Membership.mem (γ := Finset (Fin n →₀ ℕ))
    (support.{u, 0} (R := R)
      (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)
        ((m : (a : Fin (n + 1)) → ℕ) 0)))
    m.tail
⊢ Ne.{u + 1} (α := R)
    ((Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)
            ((m : (a : Fin (n + 1)) → ℕ) 0) :
          (a : Fin n →₀ ℕ) → R)
        m.tail :
      R)
    ((0 : (a : Fin n →₀ ℕ) → R) m.tail : R)
have h₄ : Membership.mem (α := Fin (n + 1) →₀ ℕ) f.support (cons ((m : (a : Fin (n + 1)) → ℕ) 0) m.tail : Fin (n + 1) →₀ ℕ)
Tactic: rwa [← coeff, zero_apply, ← mem_support_iff, mem_support_coeff_finSuccEquiv, cons_tail]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
⊢ Finset.image (cons i)
      (support.{u, 0} (R := R)
        (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)
          i)) =
    {m ∈ f.support | (m : (a : Fin (n + 1)) → ℕ) 0 = i}
have h : ∀ (m : Fin (n + 1) →₀ ℕ),
  Membership.mem (γ := Finset (Fin (n + 1) →₀ ℕ))
      (Finset.image (cons i)
        (support.{u, 0} (R := R)
          (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)
            i)))
      m ↔
    m ∈ {m ∈ f.support | (m : (a : Fin (n + 1)) → ℕ) 0 = i}
Tactic: ext m
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
⊢ Membership.mem (γ := Finset (Fin (n + 1) →₀ ℕ))
      (Finset.image (cons i)
        (support.{u, 0} (R := R)
          (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)
            i)))
      m ↔
    m ∈ {m ∈ f.support | (m : (a : Fin (n + 1)) → ℕ) 0 = i}
have h : (∃ (a : Fin n →₀ ℕ),
    Membership.mem (γ := Finset (Fin n →₀ ℕ))
        (support.{u, 0} (R := R)
          (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)
            i))
        a ∧
      cons i a = m) ↔
  coeff m f ≠ 0 ∧ (m : (a : Fin (n + 1)) → ℕ) 0 = i
Tactic: rw [Finset.mem_filter, Finset.mem_image, mem_support_iff]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
| ∃ (a : Fin n →₀ ℕ),
    Membership.mem (γ := Finset (Fin n →₀ ℕ))
        (support.{u, 0} (R := R)
          (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)
            i))
        a ∧
      cons i a = m
have p : fun (a : Fin n →₀ ℕ) ↦
  Membership.mem (γ := Finset (Fin n →₀ ℕ))
      (support.{u, 0} (R := R)
        (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) i))
      a ∧
    cons i a = m
Tactic: congr