awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
s : Fin n → R
y : R
f : MvPolynomial (Fin (n + 1)) R
φ : (MvPolynomial (Fin n) R)[X] →ₐ[R] R[X] :=
  let __src : (MvPolynomial (Fin n) R)[X] →+* R[X] := Polynomial.mapRingHom (eval s);
  { toRingHom := __src, commutes' := ⋯ }
e_a :
  Eq (α := R)
      ((aeval (Fin.cons (α := fun (a : Fin (n + 1)) ↦ R) y s) : (a : MvPolynomial (Fin (n + 1)) R) → R) (X 0) : R)
      ((AlgHom.comp (Polynomial.aeval y)
              (φ.comp (↑(finSuccEquiv R n) : MvPolynomial (Fin (n + 1)) R →ₐ[R] (MvPolynomial (Fin n) R)[X])) :
            (a : MvPolynomial (Fin (n + 1)) R) → R)
          (X 0) :
        R) ∧
    ∀ (i : Fin n),
      Eq (α := R)
        ((aeval (Fin.cons (α := fun (a : Fin (n + 1)) ↦ R) y s) : (a : MvPolynomial (Fin (n + 1)) R) → R) (X i.succ) :
          R)
        ((AlgHom.comp (Polynomial.aeval y)
                (φ.comp (↑(finSuccEquiv R n) : MvPolynomial (Fin (n + 1)) R →ₐ[R] (MvPolynomial (Fin n) R)[X])) :
              (a : MvPolynomial (Fin (n + 1)) R) → R)
            (X i.succ) :
          R)
⊢ ∀ (i : Fin (n + 1)),
    Eq (α := R)
      ((aeval (Fin.cons (α := fun (a : Fin (n + 1)) ↦ R) y s) : (a : MvPolynomial (Fin (n + 1)) R) → R) (X i) : R)
      ((AlgHom.comp (Polynomial.aeval y)
              (φ.comp (↑(finSuccEquiv R n) : MvPolynomial (Fin (n + 1)) R →ₐ[R] (MvPolynomial (Fin n) R)[X])) :
            (a : MvPolynomial (Fin (n + 1)) R) → R)
          (X i) :
        R)

Tactic:
rw [Fin.forall_iff_succ]

Premises used: Fin.forall_iff_succ
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
s : Fin n → R
y : R
f : MvPolynomial (Fin (n + 1)) R
φ : (MvPolynomial (Fin n) R)[X] →ₐ[R] R[X] :=
  let __src : (MvPolynomial (Fin n) R)[X] →+* R[X] := Polynomial.mapRingHom (eval s);
  { toRingHom := __src, commutes' := ⋯ }
⊢ Eq (α := R)
      ((aeval (Fin.cons (α := fun (a : Fin (n + 1)) ↦ R) y s) : (a : MvPolynomial (Fin (n + 1)) R) → R) (X 0) : R)
      ((AlgHom.comp (Polynomial.aeval y)
              (φ.comp (↑(finSuccEquiv R n) : MvPolynomial (Fin (n + 1)) R →ₐ[R] (MvPolynomial (Fin n) R)[X])) :
            (a : MvPolynomial (Fin (n + 1)) R) → R)
          (X 0) :
        R) ∧
    ∀ (i : Fin n),
      Eq (α := R)
        ((aeval (Fin.cons (α := fun (a : Fin (n + 1)) ↦ R) y s) : (a : MvPolynomial (Fin (n + 1)) R) → R) (X i.succ) :
          R)
        ((AlgHom.comp (Polynomial.aeval y)
                (φ.comp (↑(finSuccEquiv R n) : MvPolynomial (Fin (n + 1)) R →ₐ[R] (MvPolynomial (Fin n) R)[X])) :
              (a : MvPolynomial (Fin (n + 1)) R) → R)
            (X i.succ) :
          R)

Tactic:
simp only [aeval_X, Fin.cons_zero, AlgHom.coe_comp, Polynomial.coe_aeval_eq_eval,
    AlgHom.coe_mk, Polynomial.coe_mapRingHom, AlgEquiv.coe_algHom,
    comp_apply, finSuccEquiv_apply, eval₂Hom_X', Fin.cases_zero, Polynomial.map_X,
    Polynomial.eval_X, Fin.cons_succ, Fin.cases_succ, Polynomial.map_C, eval_X, Polynomial.eval_C,
    implies_true, and_self, φ]

Premises used: Fin.cons_succ, AlgHom.coe_mk, MvPolynomial.aeval_X, Polynomial.eval_C, and_self, Polynomial.eval_X, Fin.cases_zero, MvPolynomial.eval₂Hom_X', Polynomial.map_X, AlgHom.coe_comp, Polynomial.coe_mapRingHom, AlgEquiv.coe_algHom, MvPolynomial.finSuccEquiv_apply, Function.comp_apply, implies_true, Fin.cases_succ, Polynomial.coe_aeval_eq_eval, Polynomial.map_C, MvPolynomial.eval_X, Fin.cons_zero
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
S₁ : Type v
inst : CommSemiring R
s' : S₁ → R
f : (MvPolynomial S₁ R)[X]
i : ℕ
⊢ (Polynomial.map (eval s') f).coeff i = (eval s' : (a : MvPolynomial S₁ R) → R) (f.coeff i)

Tactic:
simp only [Polynomial.coeff_map]

Premises used: Polynomial.coeff_map
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin n →₀ ℕ
mp :
  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 →
    cons i m ∈ f.support
mpr :
  cons i m ∈ f.support →
    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
⊢ 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 ↔
    cons i m ∈ f.support

Tactic:
apply Iff.intro

Premises used: Iff.intro
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin n →₀ ℕ
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
⊢ cons i m ∈ f.support

Tactic:
simpa [← finSuccEquiv_coeff_coeff] using h

Premises used: MvPolynomial.finSuccEquiv_coeff_coeff
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin n →₀ ℕ
h : cons i m ∈ f.support
⊢ 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:
simpa [mem_support_iff, ← finSuccEquiv_coeff_coeff m f i] using h

Premises used: MvPolynomial.mem_support_iff, MvPolynomial.finSuccEquiv_coeff_coeff
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
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
rw :
  ¬Eq.{max (u + 1) 1} (α := MvPolynomial (Fin n) R)
      (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) i) 0
⊢ 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))

Tactic:
rw [Finset.nonempty_iff_ne_empty, ne_eq, support_eq_empty]

Premises used: MvPolynomial.support_eq_empty, Finset.nonempty_iff_ne_empty, ne_eq
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
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
⊢ ¬Eq.{max (u + 1) 1} (α := MvPolynomial (Fin n) R)
      (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) i) 0

Tactic:
hi
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
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
⊢ ¬Eq.{max (u + 1) 1} (α := MvPolynomial (Fin n) R)
      (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) i) 0

Tactic:
exact hi
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
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
⊢ 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))

Tactic:
have hf'_sup : ((finSuccEquiv R n f).coeff i).support.Nonempty := by
    rw [Finset.nonempty_iff_ne_empty, ne_eq, support_eq_empty]
    exact hi
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
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))
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
⊢ 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)
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
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 σ
⊢ (σ'.sum fun (x : Fin (n + 1)) (e : ℕ) ↦ e) ≤ f.totalDegree

Tactic:
le_totalDegree (s := σ') _

Premises used: MvPolynomial.le_totalDegree
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
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
convert_4 : σ' ∈ f.support
⊢ 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:
convert! le_totalDegree (s := σ') _

Premises used: MvPolynomial.le_totalDegree
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
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
h₃ h₄ : (i + σ.sum fun (x : Fin n) (e : ℕ) ↦ e) = 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

Tactic:
rw [totalDegree, hσ2, sum_cons, add_comm]

Premises used: Finsupp.sum_cons, add_comm, MvPolynomial.totalDegree
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
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 σ
convert_4 :
  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))
    σ
⊢ σ' ∈ f.support

Tactic:
rw [← mem_support_coeff_finSuccEquiv]

Premises used: MvPolynomial.mem_support_coeff_finSuccEquiv
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
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 σ
⊢ 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))
    σ

Tactic:
hσ1
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
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 σ
⊢ 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))
    σ

Tactic:
exact hσ1
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
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
⊢ 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

Tactic:
ext i
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
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
⊢ 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:
rw [Polynomial.mem_support_iff, Finset.mem_image, Finsupp.ne_iff]

Premises used: Finset.mem_image, Polynomial.mem_support_iff, Finsupp.ne_iff
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
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
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)
⊢ (∃ (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
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
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

Tactic:
⟨cons i m, ?_, cons_zero _ _⟩

Premises used: Finsupp.cons_zero, And.intro, Exists.intro, Finsupp.cons
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
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)
h : cons i m ∈ f.support
⊢ ∃ a ∈ f.support, (a : (a : Fin (n + 1)) → ℕ) 0 = i

Tactic:
refine ⟨cons i m, ?_, cons_zero _ _⟩
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
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)
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
⊢ cons i m ∈ f.support

Tactic:
rw [← mem_support_coeff_finSuccEquiv]

Premises used: MvPolynomial.mem_support_coeff_finSuccEquiv
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
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)
⊢ 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:
simpa using hm
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
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)

Tactic:
⟨tail m, ?_⟩

Premises used: Finsupp.tail, Exists.intro