awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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)
⊢ ∃ (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:
refine ⟨tail m, ?_⟩
-- 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
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
h₄ : Membership.mem (α := Fin (n + 1) →₀ ℕ) f.support (cons ((m : (a : Fin (n + 1)) → ℕ) 0) m.tail : Fin (n + 1) →₀ ℕ)
h₅ h₆ h₇ 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)

Tactic:
rwa [← coeff, zero_apply, ← mem_support_iff, mem_support_coeff_finSuccEquiv, cons_tail]

Premises used: MvPolynomial.mem_support_iff, Finsupp.cons_tail, MvPolynomial.coeff, Finsupp.zero_apply, MvPolynomial.mem_support_coeff_finSuccEquiv
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
x : ℕ
⊢ x ∈
      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 (γ := Set ℕ)
      ((fun (m : Fin (n + 1) →₀ ℕ) ↦ (m : (a : Fin (n + 1)) → ℕ) 0) '' (↑f.support : Set (Fin (n + 1) →₀ ℕ))) x

Tactic:
simpa using congr(x ∈ $(support_finSuccEquiv f))

Premises used: MvPolynomial.support_finSuccEquiv
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
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}
⊢ 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}

Tactic:
ext m
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
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
⊢ 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:
rw [Finset.mem_filter, Finset.mem_image, mem_support_iff]

Premises used: MvPolynomial.mem_support_iff, Finset.mem_image, Finset.mem_filter
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
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
| ∃ (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
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
p :
  ∀ (x : 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))
        x ∧
      cons i x = m
| 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:
ext
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
x : Fin n →₀ ℕ
p : ¬coeff (cons i x) f = 0 ∧ cons i x = 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))
      x ∧
    cons i x = m

Tactic:
rw [mem_support_iff, finSuccEquiv_coeff_coeff, Ne]

Premises used: MvPolynomial.mem_support_iff, MvPolynomial.finSuccEquiv_coeff_coeff, Ne
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
p : ∀ (x : Fin n →₀ ℕ), ¬coeff (cons i x) f = 0 ∧ cons i x = m
| ∃ (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
    ext
    rw [mem_support_iff, finSuccEquiv_coeff_coeff, Ne]

Premises used: MvPolynomial.mem_support_iff, MvPolynomial.finSuccEquiv_coeff_coeff, Ne
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
h : (∃ (x : Fin n →₀ ℕ), ¬coeff (cons i x) f = 0 ∧ cons i x = m) ↔ coeff m f ≠ 0 ∧ (m : (a : Fin (n + 1)) → ℕ) 0 = i
⊢ (∃ (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:
conv_lhs =>
    congr
    ext
    rw [mem_support_iff, finSuccEquiv_coeff_coeff, Ne]

Premises used: MvPolynomial.mem_support_iff, MvPolynomial.finSuccEquiv_coeff_coeff, Ne
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
h : (∃ (x : Fin n →₀ ℕ), ¬coeff (cons i x) f = 0 ∧ cons i x = m) → coeff m f ≠ 0 ∧ (m : (a : Fin (n + 1)) → ℕ) 0 = i
h₁ : coeff m f ≠ 0 ∧ (m : (a : Fin (n + 1)) → ℕ) 0 = i → ∃ (x : Fin n →₀ ℕ), ¬coeff (cons i x) f = 0 ∧ cons i x = m
⊢ (∃ (x : Fin n →₀ ℕ), ¬coeff (cons i x) f = 0 ∧ cons i x = m) ↔ coeff m f ≠ 0 ∧ (m : (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 + 1) →₀ ℕ
⊢ (∃ (x : Fin n →₀ ℕ), ¬coeff (cons i x) f = 0 ∧ cons i x = m) → coeff m f ≠ 0 ∧ (m : (a : Fin (n + 1)) → ℕ) 0 = i

Tactic:
grind [cons_zero]

Premises used: Finsupp.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 + 1) →₀ ℕ
h : coeff m f ≠ 0 ∧ (m : (a : Fin (n + 1)) → ℕ) 0 = i
h₁ : ¬coeff (cons i m.tail) f = 0 ∧ cons i m.tail = m
⊢ ∃ (x : Fin n →₀ ℕ), ¬coeff (cons i x) f = 0 ∧ cons i x = m

Tactic:
use tail m

Premises used: Finsupp.tail
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
h : coeff m f ≠ 0 ∧ (m : (a : Fin (n + 1)) → ℕ) 0 = i
h₁ : ¬coeff m f = 0 ∧ m = m
⊢ ¬coeff (cons i m.tail) f = 0 ∧ cons i m.tail = m

Tactic:
rw [← h.2, cons_tail]

Premises used: Finsupp.cons_tail, And.right
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
h : coeff m f ≠ 0 ∧ (m : (a : Fin (n + 1)) → ℕ) 0 = i
⊢ ¬coeff m f = 0 ∧ m = m

Tactic:
simp [h.1]

Premises used: And.left
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
x : Fin (n + 1) →₀ ℕ
⊢ x ∈
      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)) :
          Set (Fin n →₀ ℕ)) ↔
    x ∈ f.support ∧ (x : (a : Fin (n + 1)) → ℕ) 0 = i

Tactic:
simpa using congr(x ∈ $image_support_finSuccEquiv)

Premises used: MvPolynomial.image_support_finSuccEquiv
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
rwa :
  Ne (α := (MvPolynomial (Fin n) R)[X])
    ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f :
      (MvPolynomial (Fin n) R)[X])
    (0 : (MvPolynomial (Fin n) R)[X])
rwa₁ rwa₂ rwa₃ rwa₄ : f ≠ 0
⊢ (Polynomial.support.{u} (R := MvPolynomial (Fin n) R)
      ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)).Nonempty

Tactic:
rwa [Polynomial.support_nonempty, EmbeddingLike.map_ne_zero_iff]

Premises used: EmbeddingLike.map_ne_zero_iff, Polynomial.support_nonempty
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
⊢ ∀ {α β : Type} (f : α → β), (fun (x : β) ↦ x) ∘ f = f

Tactic:
have h₀ : ∀ {α β : Type _} (f : α → β), (fun x => x) ∘ f = f := fun f => rfl
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
h₀ : ∀ {α β : Type} (f : α → β), (fun (x : β) ↦ x) ∘ f = f
⊢ ∀ {α β : Type} (f : α → β), (f ∘ fun (x : α) ↦ x) = f

Tactic:
have h₁ : ∀ {α β : Type _} (f : α → β), f ∘ (fun x => x) = f := fun f => rfl
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
h₀ : ∀ {α β : Type} (f : α → β), (fun (x : β) ↦ x) ∘ f = f
h₁ : ∀ {α β : Type} (f : α → β), (f ∘ fun (x : α) ↦ x) = f
rw :
  Eq (α := ℕ)
    ((Polynomial.support.{u} (R := MvPolynomial (Fin n) R)
          ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)).sup
      fun (x : ℕ) ↦ x)
    (f.support.sup fun (m : Fin (n + 1) →₀ ℕ) ↦ (m : (a : Fin (n + 1)) → ℕ) 0)
rw₁ :
  Eq (α := ℕ)
    (Finset.sup (Finset.image (fun (m : Fin (n + 1) →₀ ℕ) ↦ (m : (a : Fin (n + 1)) → ℕ) 0) f.support) fun (x : ℕ) ↦ x)
    (f.support.sup fun (m : Fin (n + 1) →₀ ℕ) ↦ (m : (a : Fin (n + 1)) → ℕ) 0)
rw₂ :
  Eq (α := ℕ) (f.support.sup ((fun (x : ℕ) ↦ x) ∘ fun (m : Fin (n + 1) →₀ ℕ) ↦ (m : (a : Fin (n + 1)) → ℕ) 0))
    (f.support.sup fun (m : Fin (n + 1) →₀ ℕ) ↦ (m : (a : Fin (n + 1)) → ℕ) 0)
rw₃ rw₄ :
  Eq (α := ℕ) (f.support.sup fun (m : Fin (n + 1) →₀ ℕ) ↦ (m : (a : Fin (n + 1)) → ℕ) 0)
    (f.support.sup fun (m : Fin (n + 1) →₀ ℕ) ↦ (m : (a : Fin (n + 1)) → ℕ) 0)
⊢ ((Polynomial.support.{u} (R := MvPolynomial (Fin n) R)
          ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)).sup
      fun (x : ℕ) ↦ x) =
    degreeOf 0 f

Tactic:
rw [degreeOf_eq_sup, support_finSuccEquiv, Finset.sup_image, h₀]

Premises used: MvPolynomial.support_finSuccEquiv, MvPolynomial.degreeOf_eq_sup, Finset.sup_image
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
h₀ : ∀ {α β : Type} (f : α → β), (fun (x : β) ↦ x) ∘ f = f
h₁ : ∀ {α β : Type} (f : α → β), (f ∘ fun (x : α) ↦ x) = f
⊢ ((Polynomial.support.{u} (R := MvPolynomial (Fin n) R)
          ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)).sup
      fun (x : ℕ) ↦ x) =
    degreeOf 0 f

Tactic:
have h' : ((finSuccEquiv R n f).support.sup fun x => x) = degreeOf 0 f := by
    rw [degreeOf_eq_sup, support_finSuccEquiv, Finset.sup_image, h₀]
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
h₀ : ∀ {α β : Type} (f : α → β), (fun (x : β) ↦ x) ∘ f = f
h₁ : ∀ {α β : Type} (f : α → β), (f ∘ fun (x : α) ↦ x) = f
h' :
  ((Polynomial.support.{u} (R := MvPolynomial (Fin n) R)
          ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)).sup
      fun (x : ℕ) ↦ x) =
    degreeOf 0 f
rw :
  (Polynomial.support.{u} (R := MvPolynomial (Fin n) R)
        ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)).max =
    (↑(degreeOf 0 f) : WithBot ℕ)
rw₁ :
  (Polynomial.support.{u} (R := MvPolynomial (Fin n) R)
        ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)).max =
    (↑((Polynomial.support.{u} (R := MvPolynomial (Fin n) R)
              ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)).sup
          fun (x : ℕ) ↦ x) :
      WithBot ℕ)
rw₂ :
  (Polynomial.support.{u} (R := MvPolynomial (Fin n) R)
        ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)).max =
    (↑((Polynomial.support.{u} (R := MvPolynomial (Fin n) R)
              ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)).sup
          fun (x : ℕ) ↦ x) :
      WithBot ℕ)
rw₃ :
  (Polynomial.support.{u} (R := MvPolynomial (Fin n) R)
        ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)).max =
    (Polynomial.support.{u} (R := MvPolynomial (Fin n) R)
          ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)).sup
      (WithBot.some ∘ fun (x : ℕ) ↦ x)
rw₄ :
  (Polynomial.support.{u} (R := MvPolynomial (Fin n) R)
          ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)).sup
      WithBot.some =
    (Polynomial.support.{u} (R := MvPolynomial (Fin n) R)
          ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)).sup
      (WithBot.some ∘ fun (x : ℕ) ↦ x)
rw₅ rw₆ :
  (Polynomial.support.{u} (R := MvPolynomial (Fin n) R)
          ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)).sup
      WithBot.some =
    (Polynomial.support.{u} (R := MvPolynomial (Fin n) R)
          ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)).sup
      WithBot.some
⊢ degree.{u} (R := MvPolynomial (Fin n) R)
      ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) =
    (↑(degreeOf 0 f) : WithBot ℕ)

Tactic:
rw [Polynomial.degree, ← h', Nat.cast_withBot,
    Finset.coe_sup_of_nonempty (nonempty_support_finSuccEquiv h), Finset.max_eq_sup_coe, h₁]

Premises used: MvPolynomial.nonempty_support_finSuccEquiv, Finset.max_eq_sup_coe, Finset.coe_sup_of_nonempty, Polynomial.degree, Nat.cast_withBot
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
pos :
  ∀ (c : f = 0),
    natDegree.{u} (R := MvPolynomial (Fin n) R)
        ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) =
      degreeOf 0 f
neg :
  ∀ (c : ¬f = 0),
    natDegree.{u} (R := MvPolynomial (Fin n) R)
        ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) =
      degreeOf 0 f
⊢ natDegree.{u} (R := MvPolynomial (Fin n) R)
      ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) =
    degreeOf 0 f

Tactic:
by_cases c : f = 0
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
c : f = 0
pos :
  natDegree (R := MvPolynomial (Fin n) R)
      ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) 0) =
    degreeOf.{u, 0} (R := R) (σ := Fin (n + 1)) 0 0
pos₁ : natDegree.{u} (R := MvPolynomial (Fin n) R) 0 = degreeOf.{u, 0} (R := R) (σ := Fin (n + 1)) 0 0
pos₂ : 0 = degreeOf.{u, 0} (R := R) (σ := Fin (n + 1)) 0 0
pos₃ pos₄ : Eq (α := ℕ) 0 0
⊢ natDegree.{u} (R := MvPolynomial (Fin n) R)
      ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) =
    degreeOf 0 f

Tactic:
rw [c, map_zero, Polynomial.natDegree_zero, degreeOf_zero]

Premises used: map_zero, Polynomial.natDegree_zero, MvPolynomial.degreeOf_zero
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
c : ¬f = 0
neg :
  WithBot.unbotD 0
      (degree.{u} (R := MvPolynomial (Fin n) R)
        ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)) =
    degreeOf 0 f
neg₁ : WithBot.unbotD 0 (↑(degreeOf 0 f) : WithBot ℕ) = degreeOf 0 f
neg₂ : WithBot.unbotD 0 (↑(degreeOf 0 f) : WithBot ℕ) = degreeOf 0 f
neg₃ neg₄ : degreeOf 0 f = degreeOf 0 f
⊢ natDegree.{u} (R := MvPolynomial (Fin n) R)
      ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) =
    degreeOf 0 f

Tactic:
rw [Polynomial.natDegree, degree_finSuccEquiv c, Nat.cast_withBot, WithBot.unbotD_coe]

Premises used: MvPolynomial.degree_finSuccEquiv, Nat.cast_withBot, WithBot.unbotD_coe, Polynomial.natDegree
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
a : σ
p : MvPolynomial σ R
rw :
  degreeOf.{u, u_1} (R := R) (σ := Option { b : σ // b ≠ a }) none
      ((rename (⇑(Equiv.optionSubtypeNe a).symm : (a_1 : σ) → Option { b : σ // b ≠ a }) :
          (a_1 : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ a }) R)
        p) =
    degreeOf a p
⊢ degreeOf a p =
    natDegree (R := MvPolynomial.{u_1, u} { b : σ // b ≠ a } R)
      ((optionEquivLeft R { b : σ // b ≠ a } :
          (a_1 : MvPolynomial (Option { b : σ // b ≠ a }) R) → (MvPolynomial { b : σ // b ≠ a } R)[X])
        ((rename (⇑(Equiv.optionSubtypeNe a).symm : (a_1 : σ) → Option { b : σ // b ≠ a }) :
            (a_1 : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ a }) R)
          p))

Tactic:
rw [natDegree_optionEquivLeft, eq_comm]

Premises used: eq_comm, MvPolynomial.natDegree_optionEquivLeft
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
a : σ
p : MvPolynomial σ R
⊢ degreeOf.{u, u_1} (R := R) (σ := Option { b : σ // b ≠ a })
      (((Equiv.optionSubtypeNe a).symm : (a_1 : σ) → Option { b : σ // b ≠ a }) a : Option { b : σ // b ≠ a })
      ((rename (⇑(Equiv.optionSubtypeNe a).symm : (a_1 : σ) → Option { b : σ // b ≠ a }) :
            (a_1 : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ a }) R)
          p :
        MvPolynomial.{u_1, u} (Option { b : σ // b ≠ a }) R) =
    degreeOf a p

Tactic:
degreeOf_rename_of_injective (Equiv.injective (Equiv.optionSubtypeNe a).symm) a

Premises used: MvPolynomial.degreeOf_rename_of_injective, Equiv.optionSubtypeNe, Equiv.injective, Equiv.symm
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
a : σ
p : MvPolynomial σ R
h :
  Eq.{u_1 + 1} (α := Option { b : σ // b ≠ a }) none
    (((Equiv.optionSubtypeNe a).symm : (a_1 : σ) → Option { b : σ // b ≠ a }) a)
⊢ degreeOf.{u, u_1} (R := R) (σ := Option { b : σ // b ≠ a }) none
      ((rename (⇑(Equiv.optionSubtypeNe a).symm : (a_1 : σ) → Option { b : σ // b ≠ a }) :
          (a_1 : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ a }) R)
        p) =
    degreeOf a p

Tactic:
convert! degreeOf_rename_of_injective (Equiv.injective (Equiv.optionSubtypeNe a).symm) a

Premises used: MvPolynomial.degreeOf_rename_of_injective, Equiv.optionSubtypeNe, Equiv.injective, Equiv.symm
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
a : σ
p : MvPolynomial σ R
h :
  Eq.{u_1 + 1} (α := Option { b : σ // b ≠ a }) none
    (if h : a = a then none else Option.some (Subtype.mk (p := fun (y : σ) ↦ ¬y = a) a h))
h₁ h₂ : Eq.{u_1 + 1} (α := Option { b : σ // b ≠ a }) none none
⊢ Eq.{u_1 + 1} (α := Option { b : σ // b ≠ a }) none
    (((Equiv.optionSubtypeNe a).symm : (a_1 : σ) → Option { b : σ // b ≠ a }) a)

Tactic:
rw [Equiv.optionSubtypeNe_symm_apply, dif_pos rfl]

Premises used: dif_pos, Equiv.optionSubtypeNe_symm_apply, rfl
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
j : Fin n
i : ℕ
rw :
  ∀ (b : 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]) p)
            i))
        b →
      LE.le (α := ℕ) ((b : (a : Fin n) → ℕ) j : ℕ)
        (p.support.sup fun (m : Fin (n + 1) →₀ ℕ) ↦ (m : (a : Fin (n + 1)) → ℕ) j.succ : ℕ)
⊢ degreeOf.{u, 0} (R := R) j
      (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) p) i) ≤
    degreeOf j.succ p

Tactic:
rw [degreeOf_eq_sup, degreeOf_eq_sup, Finset.sup_le_iff]

Premises used: MvPolynomial.degreeOf_eq_sup, Finset.sup_le_iff
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
j : Fin n
i : ℕ
m : Fin n →₀ ℕ
hm :
  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]) p) i))
    m
rw :
  LE.le (α := ℕ) ((cons i m : (a : Fin (n + 1)) → ℕ) j.succ : ℕ)
    (p.support.sup fun (m : Fin (n + 1) →₀ ℕ) ↦ (m : (a : Fin (n + 1)) → ℕ) j.succ : ℕ)
⊢ LE.le (α := ℕ) ((m : (a : Fin n) → ℕ) j : ℕ)
    (p.support.sup fun (m : Fin (n + 1) →₀ ℕ) ↦ (m : (a : Fin (n + 1)) → ℕ) j.succ : ℕ)

Tactic:
rw [← Finsupp.cons_succ j i m]

Premises used: Finsupp.cons_succ