awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial.{u_1, u} (Option σ) R
m : Option σ →₀ ℕ
h : m ∈ p.support
⊢ ∃ (a : σ →₀ ℕ),
    Ne.{u + 1} (α := R)
      ((Polynomial.coeff ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) p)
              ((m : (a : Option σ) → ℕ) none) :
            (a : σ →₀ ℕ) → R)
          a :
        R)
      ((0 : (a : σ →₀ ℕ) → R) a : R)

Tactic:
⟨some m, ?_⟩

Premises used: Finsupp.some, Exists.intro
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial.{u_1, u} (Option σ) R
m : Option σ →₀ ℕ
h : m ∈ p.support
h₁ :
  Ne.{u + 1} (α := R)
    ((Polynomial.coeff ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) p)
            ((m : (a : Option σ) → ℕ) none) :
          (a : σ →₀ ℕ) → R)
        m.some :
      R)
    ((0 : (a : σ →₀ ℕ) → R) m.some : R)
⊢ ∃ (a : σ →₀ ℕ),
    Ne.{u + 1} (α := R)
      ((Polynomial.coeff ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) p)
              ((m : (a : Option σ) → ℕ) none) :
            (a : σ →₀ ℕ) → R)
          a :
        R)
      ((0 : (a : σ →₀ ℕ) → R) a : R)

Tactic:
refine ⟨some m, ?_⟩
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial.{u_1, u} (Option σ) R
m : Option σ →₀ ℕ
h : m ∈ p.support
h₁ :
  Ne.{u + 1} (α := R)
    (coeff m.some
        (Polynomial.coeff ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) p)
          ((m : (a : Option σ) → ℕ) none)) :
      R)
    ((0 : (a : σ →₀ ℕ) → R) m.some : R)
h₂ :
  Ne.{u + 1} (α := R)
    (coeff m.some
      (Polynomial.coeff ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) p)
        ((m : (a : Option σ) → ℕ) none)))
    0
h₃ :
  Membership.mem (γ := Finset (σ →₀ ℕ))
    (support.{u, u_1} (R := R)
      (Polynomial.coeff ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) p)
        ((m : (a : Option σ) → ℕ) none)))
    m.some
h₄ : Membership.mem (α := Option σ →₀ ℕ) p.support (optionElim ((m : (a : Option σ) → ℕ) none) m.some : Option σ →₀ ℕ)
h₅ h₆ h₇ h₈ : m ∈ p.support
⊢ Ne.{u + 1} (α := R)
    ((Polynomial.coeff ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) p)
            ((m : (a : Option σ) → ℕ) none) :
          (a : σ →₀ ℕ) → R)
        m.some :
      R)
    ((0 : (a : σ →₀ ℕ) → R) m.some : R)

Tactic:
rwa [← coeff, zero_apply, ← mem_support_iff, mem_support_coeff_optionEquivLeft, optionElim_some]

Premises used: MvPolynomial.mem_support_iff, Finsupp.optionElim_some, MvPolynomial.mem_support_coeff_optionEquivLeft, MvPolynomial.coeff, Finsupp.zero_apply
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
f : MvPolynomial.{u_1, u} (Option σ) R
h : f ≠ 0
rwa :
  Ne (α := (MvPolynomial σ R)[X])
    ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) f : (MvPolynomial σ R)[X])
    (0 : (MvPolynomial σ R)[X])
rwa₁ rwa₂ rwa₃ rwa₄ : f ≠ 0
⊢ (Polynomial.support (R := MvPolynomial σ R)
      ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ 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
σ : Type u_1
inst : CommSemiring R
f : MvPolynomial.{u_1, u} (Option σ) R
h : f ≠ 0
rw :
  Eq (α := ℕ)
    ((Polynomial.support (R := MvPolynomial σ R)
          ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) f)).sup
      fun (x : ℕ) ↦ x)
    (f.support.sup fun (m : Option σ →₀ ℕ) ↦ (m : (a : Option σ) → ℕ) none)
rw₁ :
  Eq (α := ℕ)
    (Finset.sup (Finset.image (fun (m : Option σ →₀ ℕ) ↦ (m : (a : Option σ) → ℕ) none) f.support) fun (x : ℕ) ↦ x)
    (f.support.sup fun (m : Option σ →₀ ℕ) ↦ (m : (a : Option σ) → ℕ) none)
rw₂ :
  Eq (α := ℕ) (f.support.sup ((fun (x : ℕ) ↦ x) ∘ fun (m : Option σ →₀ ℕ) ↦ (m : (a : Option σ) → ℕ) none))
    (f.support.sup fun (m : Option σ →₀ ℕ) ↦ (m : (a : Option σ) → ℕ) none)
rw₃ rw₄ :
  Eq (α := ℕ) (f.support.sup fun (x : Option σ →₀ ℕ) ↦ (x : (a : Option σ) → ℕ) none)
    (f.support.sup fun (m : Option σ →₀ ℕ) ↦ (m : (a : Option σ) → ℕ) none)
⊢ ((Polynomial.support (R := MvPolynomial σ R)
          ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) f)).sup
      fun (x : ℕ) ↦ x) =
    degreeOf none f

Tactic:
rw [degreeOf_eq_sup, support_optionEquivLeft, Finset.sup_image, Function.comp_def]

Premises used: Function.comp_def, MvPolynomial.degreeOf_eq_sup, MvPolynomial.support_optionEquivLeft, Finset.sup_image
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
f : MvPolynomial.{u_1, u} (Option σ) R
h : f ≠ 0
⊢ ((Polynomial.support (R := MvPolynomial σ R)
          ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) f)).sup
      fun (x : ℕ) ↦ x) =
    degreeOf none f

Tactic:
have h' : ((optionEquivLeft R σ f).support.sup fun x => x) = degreeOf none f := by
    rw [degreeOf_eq_sup, support_optionEquivLeft, Finset.sup_image, Function.comp_def]
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
f : MvPolynomial.{u_1, u} (Option σ) R
h : f ≠ 0
h' :
  ((Polynomial.support (R := MvPolynomial σ R)
          ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) f)).sup
      fun (x : ℕ) ↦ x) =
    degreeOf none f
rw :
  (Polynomial.support (R := MvPolynomial σ R)
        ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) f)).max =
    (↑(degreeOf none f) : WithBot ℕ)
rw₁ :
  (Polynomial.support (R := MvPolynomial σ R)
        ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) f)).max =
    (↑((Polynomial.support (R := MvPolynomial σ R)
              ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) f)).sup
          fun (x : ℕ) ↦ x) :
      WithBot ℕ)
rw₂ :
  (Polynomial.support (R := MvPolynomial σ R)
        ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) f)).max =
    (↑((Polynomial.support (R := MvPolynomial σ R)
              ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) f)).sup
          fun (x : ℕ) ↦ x) :
      WithBot ℕ)
rw₃ :
  (Polynomial.support (R := MvPolynomial σ R)
        ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) f)).max =
    (Polynomial.support (R := MvPolynomial σ R)
          ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) f)).sup
      (WithBot.some ∘ fun (x : ℕ) ↦ x)
rw₄ :
  (Polynomial.support (R := MvPolynomial σ R)
          ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) f)).sup
      WithBot.some =
    (Polynomial.support (R := MvPolynomial σ R)
          ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) f)).sup
      (WithBot.some ∘ fun (x : ℕ) ↦ x)
rw₅ rw₆ :
  (Polynomial.support (R := MvPolynomial σ R)
          ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) f)).sup
      WithBot.some =
    (Polynomial.support (R := MvPolynomial σ R)
          ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) f)).sup
      fun (x : ℕ) ↦ (↑x : WithBot ℕ)
⊢ degree (R := MvPolynomial σ R) ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) f) =
    (↑(degreeOf none f) : WithBot ℕ)

Tactic:
rw [Polynomial.degree, ← h', Nat.cast_withBot,
    Finset.coe_sup_of_nonempty (nonempty_support_optionEquivLeft R h), Finset.max_eq_sup_coe,
    Function.comp_def]

Premises used: Finset.max_eq_sup_coe, Finset.coe_sup_of_nonempty, Polynomial.degree, Function.comp_def, MvPolynomial.nonempty_support_optionEquivLeft, Nat.cast_withBot
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial.{u_1, u} (Option σ) R
pos :
  ∀ (c : p = 0),
    natDegree (R := MvPolynomial σ R)
        ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) p) =
      degreeOf none p
neg :
  ∀ (c : ¬p = 0),
    natDegree (R := MvPolynomial σ R)
        ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) p) =
      degreeOf none p
⊢ natDegree (R := MvPolynomial σ R)
      ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) p) =
    degreeOf none p

Tactic:
by_cases c : p = 0
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial.{u_1, u} (Option σ) R
c : p = 0
pos :
  natDegree (R := MvPolynomial σ R)
      ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) 0) =
    degreeOf.{u, u_1} (R := R) (σ := Option σ) none 0
pos₁ : natDegree (R := MvPolynomial σ R) 0 = degreeOf.{u, u_1} (R := R) (σ := Option σ) none 0
pos₂ : 0 = degreeOf.{u, u_1} (R := R) (σ := Option σ) none 0
pos₃ pos₄ : Eq (α := ℕ) 0 0
⊢ natDegree (R := MvPolynomial σ R)
      ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) p) =
    degreeOf none p

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
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial.{u_1, u} (Option σ) R
c : ¬p = 0
neg :
  WithBot.unbotD 0
      (degree (R := MvPolynomial σ R)
        ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) p)) =
    degreeOf none p
neg₁ : WithBot.unbotD 0 (↑(degreeOf none p) : WithBot ℕ) = degreeOf none p
neg₂ : WithBot.unbotD 0 (↑(degreeOf none p) : WithBot ℕ) = degreeOf none p
neg₃ neg₄ : degreeOf none p = degreeOf none p
⊢ natDegree (R := MvPolynomial σ R)
      ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) p) =
    degreeOf none p

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

Premises used: MvPolynomial.degree_optionEquivLeft, Nat.cast_withBot, WithBot.unbotD_coe, Polynomial.natDegree
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
S₁ : Type v
inst : CommSemiring R
p : MvPolynomial.{v, u} (Option S₁) R
i : ℕ
hi : i ≤ p.totalDegree
pos :
  ∀
    (hpi :
      Eq (α := MvPolynomial S₁ R)
        (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i) 0),
    totalDegree.{u, v} (R := R) (σ := S₁)
          (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i) +
        i ≤
      p.totalDegree
neg :
  ∀
    (hpi :
      ¬Eq (α := MvPolynomial S₁ R)
          (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i)
          0),
    totalDegree.{u, v} (R := R) (σ := S₁)
          (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i) +
        i ≤
      p.totalDegree
⊢ totalDegree.{u, v} (R := R) (σ := S₁)
        (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i) +
      i ≤
    p.totalDegree

Tactic:
by_cases hpi : (optionEquivLeft R S₁ p).coeff i = 0

Premises used: Polynomial.coeff, MvPolynomial.optionEquivLeft, DFunLike.coe
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
S₁ : Type v
inst : CommSemiring R
p : MvPolynomial.{v, u} (Option S₁) R
i : ℕ
hi : i ≤ p.totalDegree
hpi :
  Eq (α := MvPolynomial S₁ R)
    (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i) 0
pos : totalDegree.{u, v} (R := R) (σ := S₁) 0 + i ≤ p.totalDegree
⊢ totalDegree.{u, v} (R := R) (σ := S₁)
        (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i) +
      i ≤
    p.totalDegree

Tactic:
rw [hpi]
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
S₁ : Type v
inst : CommSemiring R
p : MvPolynomial.{v, u} (Option S₁) R
i : ℕ
hi : i ≤ p.totalDegree
hpi :
  Eq (α := MvPolynomial S₁ R)
    (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i) 0
⊢ totalDegree.{u, v} (R := R) (σ := S₁) 0 + i ≤ p.totalDegree

Tactic:
simpa
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
S₁ : Type v
inst : CommSemiring R
p : MvPolynomial.{v, u} (Option S₁) R
i : ℕ
hi : i ≤ p.totalDegree
hpi :
  ¬Eq (α := MvPolynomial S₁ R)
      (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i) 0
⊢ Finset.Nonempty.{v} (α := S₁ →₀ ℕ)
    (support.{u, v} (R := R)
      (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i))

Tactic:
simpa only [support_nonempty]

Premises used: MvPolynomial.support_nonempty
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
S₁ : Type v
inst : CommSemiring R
p : MvPolynomial.{v, u} (Option S₁) R
i : ℕ
hi : i ≤ p.totalDegree
hpi :
  ¬Eq (α := MvPolynomial S₁ R)
      (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i) 0
neg :
  ∀ (b : S₁ →₀ ℕ),
    Membership.mem (γ := Finset (S₁ →₀ ℕ))
        (support.{u, v} (R := R)
          (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i))
        b →
      (i + b.sum fun (x : S₁) (e : ℕ) ↦ e) ≤ p.totalDegree
⊢ totalDegree.{u, v} (R := R) (σ := S₁)
        (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i) +
      i ≤
    p.totalDegree

Tactic:
rw [totalDegree, add_comm, Finset.add_sup (by simpa only [support_nonempty]), Finset.sup_le_iff]

Premises used: add_comm, Finset.add_sup, MvPolynomial.totalDegree, Finset.sup_le_iff
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
S₁ : Type v
inst : CommSemiring R
p : MvPolynomial.{v, u} (Option S₁) R
i : ℕ
hi : i ≤ p.totalDegree
hpi :
  ¬Eq (α := MvPolynomial S₁ R)
      (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i) 0
σ : S₁ →₀ ℕ
hσ :
  Membership.mem (γ := Finset (S₁ →₀ ℕ))
    (support.{u, v} (R := R)
      (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i))
    σ
⊢ (i + σ.sum fun (x : S₁) (e : ℕ) ↦ e) ≤ p.totalDegree

Tactic:
le_trans ?_ (Finset.le_sup (b := σ.embDomain .some + .single .none i) ?_)

Premises used: Finset.le_sup, le_trans
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
S₁ : Type v
inst : CommSemiring R
p : MvPolynomial.{v, u} (Option S₁) R
i : ℕ
hi : i ≤ p.totalDegree
hpi :
  ¬Eq (α := MvPolynomial S₁ R)
      (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i) 0
σ : S₁ →₀ ℕ
hσ :
  Membership.mem (γ := Finset (S₁ →₀ ℕ))
    (support.{u, v} (R := R)
      (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i))
    σ
neg :
  (i + σ.sum fun (x : S₁) (e : ℕ) ↦ e) ≤
    (embDomain Embedding.some σ + Finsupp.single none i).sum fun (x : Option S₁) (e : ℕ) ↦ e
neg₁ : embDomain Embedding.some σ + Finsupp.single none i ∈ p.support
⊢ (i + σ.sum fun (x : S₁) (e : ℕ) ↦ e) ≤ p.totalDegree

Tactic:
refine le_trans ?_ (Finset.le_sup (b := σ.embDomain .some + .single .none i) ?_)

Premises used: Finset.le_sup, le_trans
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
S₁ : Type v
inst : CommSemiring R
p : MvPolynomial.{v, u} (Option S₁) R
i : ℕ
hi : i ≤ p.totalDegree
hpi :
  ¬Eq (α := MvPolynomial S₁ R)
      (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i) 0
σ : S₁ →₀ ℕ
hσ :
  Membership.mem (γ := Finset (S₁ →₀ ℕ))
    (support.{u, v} (R := R)
      (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i))
    σ
⊢ (i + σ.sum fun (x : S₁) (e : ℕ) ↦ e) ≤
    (embDomain Embedding.some σ + Finsupp.single none i).sum fun (x : Option S₁) (e : ℕ) ↦ e

Tactic:
simp [Finsupp.sum_add_index, Finsupp.sum_embDomain, add_comm i]

Premises used: Finsupp.sum_embDomain, add_comm, Finsupp.sum_add_index
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
S₁ : Type v
inst : CommSemiring R
p : MvPolynomial.{v, u} (Option S₁) R
i : ℕ
hi : i ≤ p.totalDegree
hpi :
  ¬Eq (α := MvPolynomial S₁ R)
      (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i) 0
σ : S₁ →₀ ℕ
hσ :
  Membership.mem (γ := Finset (S₁ →₀ ℕ))
    (support.{u, v} (R := R)
      (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i))
    σ
⊢ embDomain Embedding.some σ + Finsupp.single none i ∈ p.support

Tactic:
simpa [mem_support_iff, ← optionEquivLeft_coeff_some_coeff_none R S₁] using hσ

Premises used: MvPolynomial.mem_support_iff, MvPolynomial.optionEquivLeft_coeff_some_coeff_none
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
S₁ : Type v
inst : CommSemiring R
p : MvPolynomial.{v, u} (Option S₁) R
i : ℕ
pos :
  ∀
    (hpi :
      Eq (α := MvPolynomial S₁ R)
        (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i) 0),
    totalDegree.{u, v} (R := R) (σ := S₁)
        (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i) ≤
      p.totalDegree
neg :
  ∀
    (hpi :
      ¬Eq (α := MvPolynomial S₁ R)
          (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i)
          0),
    totalDegree.{u, v} (R := R) (σ := S₁)
        (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i) ≤
      p.totalDegree
⊢ totalDegree.{u, v} (R := R) (σ := S₁)
      (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i) ≤
    p.totalDegree

Tactic:
by_cases hpi : (optionEquivLeft R S₁ p).coeff i = 0

Premises used: Polynomial.coeff, MvPolynomial.optionEquivLeft, DFunLike.coe
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
S₁ : Type v
inst : CommSemiring R
p : MvPolynomial.{v, u} (Option S₁) R
i : ℕ
hpi :
  Eq (α := MvPolynomial S₁ R)
    (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i) 0
pos : totalDegree.{u, v} (R := R) (σ := S₁) 0 ≤ p.totalDegree
⊢ totalDegree.{u, v} (R := R) (σ := S₁)
      (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i) ≤
    p.totalDegree

Tactic:
rw [hpi]
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
S₁ : Type v
inst : CommSemiring R
p : MvPolynomial.{v, u} (Option S₁) R
i : ℕ
hpi :
  Eq (α := MvPolynomial S₁ R)
    (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i) 0
⊢ totalDegree.{u, v} (R := R) (σ := S₁) 0 ≤ p.totalDegree

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
S₁ : Type v
inst : CommSemiring R
p : MvPolynomial.{v, u} (Option S₁) R
i : ℕ
hpi :
  ¬Eq (α := MvPolynomial S₁ R)
      (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i) 0
neg :
  ∀ (b : S₁ →₀ ℕ),
    Membership.mem (γ := Finset (S₁ →₀ ℕ))
        (support.{u, v} (R := R)
          (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i))
        b →
      (b.sum fun (x : S₁) (e : ℕ) ↦ e) ≤ p.totalDegree
⊢ totalDegree.{u, v} (R := R) (σ := S₁)
      (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i) ≤
    p.totalDegree

Tactic:
rw [totalDegree, Finset.sup_le_iff]

Premises used: MvPolynomial.totalDegree, Finset.sup_le_iff
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
S₁ : Type v
inst : CommSemiring R
p : MvPolynomial.{v, u} (Option S₁) R
i : ℕ
hpi :
  ¬Eq (α := MvPolynomial S₁ R)
      (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i) 0
σ : S₁ →₀ ℕ
hσ :
  Membership.mem (γ := Finset (S₁ →₀ ℕ))
    (support.{u, v} (R := R)
      (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i))
    σ
⊢ (σ.sum fun (x : S₁) (e : ℕ) ↦ e) ≤ p.totalDegree

Tactic:
le_trans ?_ (Finset.le_sup (b := σ.embDomain .some + .single .none i) ?_)

Premises used: Finset.le_sup, le_trans
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
S₁ : Type v
inst : CommSemiring R
p : MvPolynomial.{v, u} (Option S₁) R
i : ℕ
hpi :
  ¬Eq (α := MvPolynomial S₁ R)
      (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i) 0
σ : S₁ →₀ ℕ
hσ :
  Membership.mem (γ := Finset (S₁ →₀ ℕ))
    (support.{u, v} (R := R)
      (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i))
    σ
neg :
  LE.le (α := ℕ) (σ.sum fun (x : S₁) (e : ℕ) ↦ e)
    ((embDomain Embedding.some σ + Finsupp.single none i).sum fun (x : Option S₁) (e : ℕ) ↦ e)
neg₁ : embDomain Embedding.some σ + Finsupp.single none i ∈ p.support
⊢ (σ.sum fun (x : S₁) (e : ℕ) ↦ e) ≤ p.totalDegree

Tactic:
refine le_trans ?_ (Finset.le_sup (b := σ.embDomain .some + .single .none i) ?_)

Premises used: Finset.le_sup, le_trans
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
S₁ : Type v
inst : CommSemiring R
p : MvPolynomial.{v, u} (Option S₁) R
i : ℕ
hpi :
  ¬Eq (α := MvPolynomial S₁ R)
      (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i) 0
σ : S₁ →₀ ℕ
hσ :
  Membership.mem (γ := Finset (S₁ →₀ ℕ))
    (support.{u, v} (R := R)
      (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i))
    σ
⊢ LE.le (α := ℕ) (σ.sum fun (x : S₁) (e : ℕ) ↦ e)
    ((embDomain Embedding.some σ + Finsupp.single none i).sum fun (x : Option S₁) (e : ℕ) ↦ e)

Tactic:
simp [Finsupp.sum_add_index, Finsupp.sum_embDomain]

Premises used: Finsupp.sum_embDomain, Finsupp.sum_add_index
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
S₁ : Type v
inst : CommSemiring R
p : MvPolynomial.{v, u} (Option S₁) R
i : ℕ
hpi :
  ¬Eq (α := MvPolynomial S₁ R)
      (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i) 0
σ : S₁ →₀ ℕ
hσ :
  Membership.mem (γ := Finset (S₁ →₀ ℕ))
    (support.{u, v} (R := R)
      (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i))
    σ
⊢ embDomain Embedding.some σ + Finsupp.single none i ∈ p.support

Tactic:
simpa [mem_support_iff, ← optionEquivLeft_coeff_some_coeff_none R S₁] using hσ

Premises used: MvPolynomial.mem_support_iff, MvPolynomial.optionEquivLeft_coeff_some_coeff_none