awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
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₁)
        (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i) +
      i ≤
    p.totalDegree
have 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
Tactic: rw [totalDegree, add_comm, Finset.add_sup (by simpa only [support_nonempty]), Finset.sup_le_iff]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
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
have neg : (i + σ.sum fun (x : S₁) (e : ℕ) ↦ e) ≤
  (embDomain Embedding.some σ + Finsupp.single none i).sum fun (x : Option S₁) (e : ℕ) ↦ e
Tactic: refine le_trans ?_ (Finset.le_sup (b := σ.embDomain .some + .single .none i) ?_)
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
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
⊢ (i + σ.sum fun (x : S₁) (e : ℕ) ↦ e) ≤ p.totalDegree
have neg₁ : embDomain Embedding.some σ + Finsupp.single none i ∈ p.support
Tactic: refine le_trans ?_ (Finset.le_sup (b := σ.embDomain .some + .single .none i) ?_)
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
S₁ : Type v
inst : CommSemiring R
p : MvPolynomial.{v, u} (Option S₁) R
i : ℕ
hi : 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
have 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
Tactic: classical
  by_cases hpi : (optionEquivLeft R S₁ p).coeff i = 0
  · rw [hpi]; simpa
  rw [totalDegree, add_comm, Finset.add_sup (by simpa only [support_nonempty]), Finset.sup_le_iff]
  intro σ hσ
  refine le_trans ?_ (Finset.le_sup (b := σ.embDomain .some + .single .none i) ?_)
  · simp [Finsupp.sum_add_index, Finsupp.sum_embDomain, add_comm i]
  · simpa [mem_support_iff, ← optionEquivLeft_coeff_some_coeff_none R S₁] using hσ
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
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
⊢ 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
have 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
Tactic: classical
  by_cases hpi : (optionEquivLeft R S₁ p).coeff i = 0
  · rw [hpi]; simpa
  rw [totalDegree, add_comm, Finset.add_sup (by simpa only [support_nonempty]), Finset.sup_le_iff]
  intro σ hσ
  refine le_trans ?_ (Finset.le_sup (b := σ.embDomain .some + .single .none i) ?_)
  · simp [Finsupp.sum_add_index, Finsupp.sum_embDomain, add_comm i]
  · simpa [mem_support_iff, ← optionEquivLeft_coeff_some_coeff_none R S₁] using hσ
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
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 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
have neg₂ : ∀
  (hpi :
    ¬Eq (α := MvPolynomial S₁ R)
        (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i) 0)
  (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
Tactic: classical
  by_cases hpi : (optionEquivLeft R S₁ p).coeff i = 0
  · rw [hpi]; simpa
  rw [totalDegree, add_comm, Finset.add_sup (by simpa only [support_nonempty]), Finset.sup_le_iff]
  intro σ hσ
  refine le_trans ?_ (Finset.le_sup (b := σ.embDomain .some + .single .none i) ?_)
  · simp [Finsupp.sum_add_index, Finsupp.sum_embDomain, add_comm i]
  · simpa [mem_support_iff, ← optionEquivLeft_coeff_some_coeff_none R S₁] using hσ
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
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 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
neg₂ neg₃ :
  ∀
    (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
⊢ 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
have neg₄ : ∀
  (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: classical
  by_cases hpi : (optionEquivLeft R S₁ p).coeff i = 0
  · rw [hpi]; simpa
  rw [totalDegree, add_comm, Finset.add_sup (by simpa only [support_nonempty]), Finset.sup_le_iff]
  intro σ hσ
  refine le_trans ?_ (Finset.le_sup (b := σ.embDomain .some + .single .none i) ?_)
  · simp [Finsupp.sum_add_index, Finsupp.sum_embDomain, add_comm i]
  · simpa [mem_support_iff, ← optionEquivLeft_coeff_some_coeff_none R S₁] using hσ
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
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 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
neg₂ neg₃ :
  ∀
    (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
neg₄ :
  ∀
    (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
⊢ 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
have neg₅ : ∀
  (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: classical
  by_cases hpi : (optionEquivLeft R S₁ p).coeff i = 0
  · rw [hpi]; simpa
  rw [totalDegree, add_comm, Finset.add_sup (by simpa only [support_nonempty]), Finset.sup_le_iff]
  intro σ hσ
  refine le_trans ?_ (Finset.le_sup (b := σ.embDomain .some + .single .none i) ?_)
  · simp [Finsupp.sum_add_index, Finsupp.sum_embDomain, add_comm i]
  · simpa [mem_support_iff, ← optionEquivLeft_coeff_some_coeff_none R S₁] using hσ
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
S₁ : Type v
inst : CommSemiring R
p : MvPolynomial.{v, u} (Option S₁) R
i : ℕ
⊢ totalDegree.{u, v} (R := R) (σ := S₁)
      (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i) ≤
    p.totalDegree
have 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
Tactic: by_cases hpi : (optionEquivLeft R S₁ p).coeff i = 0
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
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
⊢ totalDegree.{u, v} (R := R) (σ := S₁)
      (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i) ≤
    p.totalDegree
have 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
Tactic: by_cases hpi : (optionEquivLeft R S₁ p).coeff i = 0
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
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₁)
      (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i) ≤
    p.totalDegree
have pos : totalDegree.{u, v} (R := R) (σ := S₁) 0 ≤ p.totalDegree
Tactic: rw [hpi]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
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₁)
      (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i) ≤
    p.totalDegree
have 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
Tactic: rw [totalDegree, Finset.sup_le_iff]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
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
have neg : LE.le (α := ℕ) (σ.sum fun (x : S₁) (e : ℕ) ↦ e)
  ((embDomain Embedding.some σ + Finsupp.single none i).sum fun (x : Option S₁) (e : ℕ) ↦ e)
Tactic: refine le_trans ?_ (Finset.le_sup (b := σ.embDomain .some + .single .none i) ?_)
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
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)
⊢ (σ.sum fun (x : S₁) (e : ℕ) ↦ e) ≤ p.totalDegree
have neg₁ : embDomain Embedding.some σ + Finsupp.single none i ∈ p.support
Tactic: refine le_trans ?_ (Finset.le_sup (b := σ.embDomain .some + .single .none i) ?_)
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
S₁ : Type v
inst : CommSemiring R
p : MvPolynomial.{v, u} (Option S₁) R
i : ℕ
⊢ totalDegree.{u, v} (R := R) (σ := S₁)
      (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i) ≤
    p.totalDegree
have 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
Tactic: classical
  by_cases hpi : (optionEquivLeft R S₁ p).coeff i = 0
  · rw [hpi]; simp
  rw [totalDegree, Finset.sup_le_iff]
  intro σ hσ
  refine le_trans ?_ (Finset.le_sup (b := σ.embDomain .some + .single .none i) ?_)
  · simp [Finsupp.sum_add_index, Finsupp.sum_embDomain]
  · simpa [mem_support_iff, ← optionEquivLeft_coeff_some_coeff_none R S₁] using hσ
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
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
⊢ totalDegree.{u, v} (R := R) (σ := S₁)
      (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i) ≤
    p.totalDegree
have 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
Tactic: classical
  by_cases hpi : (optionEquivLeft R S₁ p).coeff i = 0
  · rw [hpi]; simp
  rw [totalDegree, Finset.sup_le_iff]
  intro σ hσ
  refine le_trans ?_ (Finset.le_sup (b := σ.embDomain .some + .single .none i) ?_)
  · simp [Finsupp.sum_add_index, Finsupp.sum_embDomain]
  · simpa [mem_support_iff, ← optionEquivLeft_coeff_some_coeff_none R S₁] using hσ
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
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 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
have neg₂ : ∀
  (hpi :
    ¬Eq (α := MvPolynomial S₁ R)
        (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i) 0)
  (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
Tactic: classical
  by_cases hpi : (optionEquivLeft R S₁ p).coeff i = 0
  · rw [hpi]; simp
  rw [totalDegree, Finset.sup_le_iff]
  intro σ hσ
  refine le_trans ?_ (Finset.le_sup (b := σ.embDomain .some + .single .none i) ?_)
  · simp [Finsupp.sum_add_index, Finsupp.sum_embDomain]
  · simpa [mem_support_iff, ← optionEquivLeft_coeff_some_coeff_none R S₁] using hσ