awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
pos : ∀ (hp : p = 0), p.totalDegree ≤ (p + q).totalDegree
⊢ p.totalDegree ≤ (p + q).totalDegree
have neg : ∀ (hp : ¬p = 0), p.totalDegree ≤ (p + q).totalDegree
Tactic: by_cases hp : p = 0
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
hp : ¬p = 0
⊢ p.totalDegree ≤ (p + q).totalDegree
have neg : ∀ (b : σ →₀ ℕ) (hb₁ : b ∈ p.support)
  (hb₂ :
    (p.support.sup fun (m : σ →₀ ℕ) ↦ Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) m)) =
      Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) b)),
  p.totalDegree ≤ (p + q).totalDegree
Tactic: obtain ⟨b, hb₁, hb₂⟩ :=
      p.support.exists_mem_eq_sup (Finsupp.support_nonempty_iff.mpr hp) fun m : σ →₀ ℕ =>
        Multiset.card (toMultiset m)
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
hp : ¬p = 0
b : σ →₀ ℕ
hb₁ : b ∈ p.support
hb₂ :
  (p.support.sup fun (m : σ →₀ ℕ) ↦ Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) m)) =
    Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) b)
⊢ b ∉ q.support
have contrapose! : ∀ (h : b ∈ q.support), p.totalDegree ≤ q.totalDegree
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
hp : ¬p = 0
b : σ →₀ ℕ
hb₁ : b ∈ p.support
hb₂ :
  (p.support.sup fun (m : σ →₀ ℕ) ↦ Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) m)) =
    Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) b)
h : b ∈ q.support
⊢ p.totalDegree ≤ q.totalDegree
have rw : Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) b) ≤
  q.support.sup fun (m : σ →₀ ℕ) ↦ Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) m)
Tactic: rw [totalDegree_eq p, hb₂, totalDegree_eq]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (hypothesis)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
hp : ¬p = 0
b : σ →₀ ℕ
hb₁ : b ∈ p.support
hb₂ :
  (p.support.sup fun (m : σ →₀ ℕ) ↦ Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) m)) =
    Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) b)
⊢ p.totalDegree ≤ (p + q).totalDegree
have hb : b ∉ q.support
Tactic: have hb : b ∉ q.support := by
      contrapose! h
      rw [totalDegree_eq p, hb₂, totalDegree_eq]
      apply Finset.le_sup h
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
hp : ¬p = 0
b : σ →₀ ℕ
hb₁ : b ∈ p.support
hb₂ :
  (p.support.sup fun (m : σ →₀ ℕ) ↦ Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) m)) =
    Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) b)
hb : b ∉ q.support
⊢ b ∈ (p + q).support
have a : b ∈ p.support \ q.support
Tactic: apply support_sdiff_support_subset_support_add
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
hp : ¬p = 0
b : σ →₀ ℕ
hb₁ : b ∈ p.support
hb₂ :
  (p.support.sup fun (m : σ →₀ ℕ) ↦ Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) m)) =
    Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) b)
hb : b ∉ q.support
⊢ b ∈ p.support \ q.support
have a : b ∈ p.support ∧ b ∉ q.support
Tactic: rw [Finset.mem_sdiff]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (hypothesis)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
hp : ¬p = 0
b : σ →₀ ℕ
hb₁ : b ∈ p.support
hb₂ :
  (p.support.sup fun (m : σ →₀ ℕ) ↦ Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) m)) =
    Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) b)
hb : b ∉ q.support
⊢ p.totalDegree ≤ (p + q).totalDegree
have hbb : b ∈ (p + q).support
Tactic: have hbb : b ∈ (p + q).support := by
      apply support_sdiff_support_subset_support_add
      rw [Finset.mem_sdiff]
      exact ⟨hb₁, hb⟩
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
hp : ¬p = 0
b : σ →₀ ℕ
hb₁ : b ∈ p.support
hb₂ :
  (p.support.sup fun (m : σ →₀ ℕ) ↦ Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) m)) =
    Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) b)
hb : b ∉ q.support
hbb : b ∈ (p + q).support
⊢ p.totalDegree ≤ (p + q).totalDegree
have neg : Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) b) ≤
  (p + q).support.sup fun (m : σ →₀ ℕ) ↦ Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) m)
Tactic: rw [totalDegree_eq, hb₂, totalDegree_eq]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
⊢ (p + q).totalDegree = p.totalDegree
have a : (p + q).totalDegree ≤ p.totalDegree
Tactic: classical
    apply le_antisymm
    · rw [← max_eq_left_of_lt h]
      exact totalDegree_add p q
    by_cases hp : p = 0
    · simp [hp]
    obtain ⟨b, hb₁, hb₂⟩ :=
      p.support.exists_mem_eq_sup (Finsupp.support_nonempty_iff.mpr hp) fun m : σ →₀ ℕ =>
        Multiset.card (toMultiset m)
    have hb : b ∉ q.support := by
      contrapose! h
      rw [totalDegree_eq p, hb₂, totalDegree_eq]
      apply Finset.le_sup h
    have hbb : b ∈ (p + q).support := by
      apply support_sdiff_support_subset_support_add
      rw [Finset.mem_sdiff]
      exact ⟨hb₁, hb⟩
    rw [totalDegree_eq, hb₂, totalDegree_eq]
    exact Finset.le_sup (f := fun m => Multiset.card (Finsupp.toMultiset m)) hbb
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
a : (p + q).totalDegree ≤ p.totalDegree
⊢ (p + q).totalDegree = p.totalDegree
have a₁ : p.totalDegree ≤ (p + q).totalDegree
Tactic: classical
    apply le_antisymm
    · rw [← max_eq_left_of_lt h]
      exact totalDegree_add p q
    by_cases hp : p = 0
    · simp [hp]
    obtain ⟨b, hb₁, hb₂⟩ :=
      p.support.exists_mem_eq_sup (Finsupp.support_nonempty_iff.mpr hp) fun m : σ →₀ ℕ =>
        Multiset.card (toMultiset m)
    have hb : b ∉ q.support := by
      contrapose! h
      rw [totalDegree_eq p, hb₂, totalDegree_eq]
      apply Finset.le_sup h
    have hbb : b ∈ (p + q).support := by
      apply support_sdiff_support_subset_support_add
      rw [Finset.mem_sdiff]
      exact ⟨hb₁, hb⟩
    rw [totalDegree_eq, hb₂, totalDegree_eq]
    exact Finset.le_sup (f := fun m => Multiset.card (Finsupp.toMultiset m)) hbb
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
a : (p + q).totalDegree ≤ p.totalDegree
a₁ a₂ : p.totalDegree ≤ (p + q).totalDegree
⊢ (p + q).totalDegree = p.totalDegree
have pos : ∀ (hp : p = 0), p.totalDegree ≤ (p + q).totalDegree
Tactic: classical
    apply le_antisymm
    · rw [← max_eq_left_of_lt h]
      exact totalDegree_add p q
    by_cases hp : p = 0
    · simp [hp]
    obtain ⟨b, hb₁, hb₂⟩ :=
      p.support.exists_mem_eq_sup (Finsupp.support_nonempty_iff.mpr hp) fun m : σ →₀ ℕ =>
        Multiset.card (toMultiset m)
    have hb : b ∉ q.support := by
      contrapose! h
      rw [totalDegree_eq p, hb₂, totalDegree_eq]
      apply Finset.le_sup h
    have hbb : b ∈ (p + q).support := by
      apply support_sdiff_support_subset_support_add
      rw [Finset.mem_sdiff]
      exact ⟨hb₁, hb⟩
    rw [totalDegree_eq, hb₂, totalDegree_eq]
    exact Finset.le_sup (f := fun m => Multiset.card (Finsupp.toMultiset m)) hbb
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
a : (p + q).totalDegree ≤ p.totalDegree
a₁ a₂ : p.totalDegree ≤ (p + q).totalDegree
pos : ∀ (hp : p = 0), p.totalDegree ≤ (p + q).totalDegree
⊢ (p + q).totalDegree = p.totalDegree
have neg : ∀ (hp : ¬p = 0), p.totalDegree ≤ (p + q).totalDegree
Tactic: classical
    apply le_antisymm
    · rw [← max_eq_left_of_lt h]
      exact totalDegree_add p q
    by_cases hp : p = 0
    · simp [hp]
    obtain ⟨b, hb₁, hb₂⟩ :=
      p.support.exists_mem_eq_sup (Finsupp.support_nonempty_iff.mpr hp) fun m : σ →₀ ℕ =>
        Multiset.card (toMultiset m)
    have hb : b ∉ q.support := by
      contrapose! h
      rw [totalDegree_eq p, hb₂, totalDegree_eq]
      apply Finset.le_sup h
    have hbb : b ∈ (p + q).support := by
      apply support_sdiff_support_subset_support_add
      rw [Finset.mem_sdiff]
      exact ⟨hb₁, hb⟩
    rw [totalDegree_eq, hb₂, totalDegree_eq]
    exact Finset.le_sup (f := fun m => Multiset.card (Finsupp.toMultiset m)) hbb
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
a : (p + q).totalDegree ≤ p.totalDegree
a₁ a₂ : p.totalDegree ≤ (p + q).totalDegree
pos : ∀ (hp : p = 0), p.totalDegree ≤ (p + q).totalDegree
neg neg₁ : ∀ (hp : ¬p = 0), p.totalDegree ≤ (p + q).totalDegree
⊢ (p + q).totalDegree = p.totalDegree
have neg₂ : ∀ (hp : ¬p = 0) (b : σ →₀ ℕ) (hb₁ : b ∈ p.support)
  (hb₂ :
    (p.support.sup fun (m : σ →₀ ℕ) ↦ Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) m)) =
      Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) b)),
  p.totalDegree ≤ (p + q).totalDegree
Tactic: classical
    apply le_antisymm
    · rw [← max_eq_left_of_lt h]
      exact totalDegree_add p q
    by_cases hp : p = 0
    · simp [hp]
    obtain ⟨b, hb₁, hb₂⟩ :=
      p.support.exists_mem_eq_sup (Finsupp.support_nonempty_iff.mpr hp) fun m : σ →₀ ℕ =>
        Multiset.card (toMultiset m)
    have hb : b ∉ q.support := by
      contrapose! h
      rw [totalDegree_eq p, hb₂, totalDegree_eq]
      apply Finset.le_sup h
    have hbb : b ∈ (p + q).support := by
      apply support_sdiff_support_subset_support_add
      rw [Finset.mem_sdiff]
      exact ⟨hb₁, hb⟩
    rw [totalDegree_eq, hb₂, totalDegree_eq]
    exact Finset.le_sup (f := fun m => Multiset.card (Finsupp.toMultiset m)) hbb
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
a : (p + q).totalDegree ≤ p.totalDegree
a₁ a₂ : p.totalDegree ≤ (p + q).totalDegree
pos : ∀ (hp : p = 0), p.totalDegree ≤ (p + q).totalDegree
neg neg₁ : ∀ (hp : ¬p = 0), p.totalDegree ≤ (p + q).totalDegree
neg₂ :
  ∀ (hp : ¬p = 0) (b : σ →₀ ℕ) (hb₁ : b ∈ p.support)
    (hb₂ :
      (p.support.sup fun (m : σ →₀ ℕ) ↦ Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) m)) =
        Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) b)),
    p.totalDegree ≤ (p + q).totalDegree
⊢ (p + q).totalDegree = p.totalDegree
have neg₃ : ∀ (hp : ¬p = 0) (b : σ →₀ ℕ) (hb₁ : b ∈ p.support)
  (hb₂ :
    (p.support.sup fun (m : σ →₀ ℕ) ↦ Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) m)) =
      Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) b))
  (hb : b ∉ q.support), p.totalDegree ≤ (p + q).totalDegree
Tactic: classical
    apply le_antisymm
    · rw [← max_eq_left_of_lt h]
      exact totalDegree_add p q
    by_cases hp : p = 0
    · simp [hp]
    obtain ⟨b, hb₁, hb₂⟩ :=
      p.support.exists_mem_eq_sup (Finsupp.support_nonempty_iff.mpr hp) fun m : σ →₀ ℕ =>
        Multiset.card (toMultiset m)
    have hb : b ∉ q.support := by
      contrapose! h
      rw [totalDegree_eq p, hb₂, totalDegree_eq]
      apply Finset.le_sup h
    have hbb : b ∈ (p + q).support := by
      apply support_sdiff_support_subset_support_add
      rw [Finset.mem_sdiff]
      exact ⟨hb₁, hb⟩
    rw [totalDegree_eq, hb₂, totalDegree_eq]
    exact Finset.le_sup (f := fun m => Multiset.card (Finsupp.toMultiset m)) hbb
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
a : (p + q).totalDegree ≤ p.totalDegree
a₁ a₂ : p.totalDegree ≤ (p + q).totalDegree
pos : ∀ (hp : p = 0), p.totalDegree ≤ (p + q).totalDegree
neg neg₁ : ∀ (hp : ¬p = 0), p.totalDegree ≤ (p + q).totalDegree
neg₂ :
  ∀ (hp : ¬p = 0) (b : σ →₀ ℕ) (hb₁ : b ∈ p.support)
    (hb₂ :
      (p.support.sup fun (m : σ →₀ ℕ) ↦ Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) m)) =
        Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) b)),
    p.totalDegree ≤ (p + q).totalDegree
neg₃ :
  ∀ (hp : ¬p = 0) (b : σ →₀ ℕ) (hb₁ : b ∈ p.support)
    (hb₂ :
      (p.support.sup fun (m : σ →₀ ℕ) ↦ Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) m)) =
        Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) b))
    (hb : b ∉ q.support), p.totalDegree ≤ (p + q).totalDegree
⊢ (p + q).totalDegree = p.totalDegree
have neg₄ : ∀ (hp : ¬p = 0) (b : σ →₀ ℕ) (hb₁ : b ∈ p.support)
  (hb₂ :
    (p.support.sup fun (m : σ →₀ ℕ) ↦ Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) m)) =
      Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) b))
  (hb : b ∉ q.support) (hbb : b ∈ (p + q).support), p.totalDegree ≤ (p + q).totalDegree
Tactic: classical
    apply le_antisymm
    · rw [← max_eq_left_of_lt h]
      exact totalDegree_add p q
    by_cases hp : p = 0
    · simp [hp]
    obtain ⟨b, hb₁, hb₂⟩ :=
      p.support.exists_mem_eq_sup (Finsupp.support_nonempty_iff.mpr hp) fun m : σ →₀ ℕ =>
        Multiset.card (toMultiset m)
    have hb : b ∉ q.support := by
      contrapose! h
      rw [totalDegree_eq p, hb₂, totalDegree_eq]
      apply Finset.le_sup h
    have hbb : b ∈ (p + q).support := by
      apply support_sdiff_support_subset_support_add
      rw [Finset.mem_sdiff]
      exact ⟨hb₁, hb⟩
    rw [totalDegree_eq, hb₂, totalDegree_eq]
    exact Finset.le_sup (f := fun m => Multiset.card (Finsupp.toMultiset m)) hbb
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
a : (p + q).totalDegree ≤ p.totalDegree
a₁ a₂ : p.totalDegree ≤ (p + q).totalDegree
pos : ∀ (hp : p = 0), p.totalDegree ≤ (p + q).totalDegree
neg neg₁ : ∀ (hp : ¬p = 0), p.totalDegree ≤ (p + q).totalDegree
neg₂ :
  ∀ (hp : ¬p = 0) (b : σ →₀ ℕ) (hb₁ : b ∈ p.support)
    (hb₂ :
      (p.support.sup fun (m : σ →₀ ℕ) ↦ Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) m)) =
        Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) b)),
    p.totalDegree ≤ (p + q).totalDegree
neg₃ :
  ∀ (hp : ¬p = 0) (b : σ →₀ ℕ) (hb₁ : b ∈ p.support)
    (hb₂ :
      (p.support.sup fun (m : σ →₀ ℕ) ↦ Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) m)) =
        Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) b))
    (hb : b ∉ q.support), p.totalDegree ≤ (p + q).totalDegree
neg₄ :
  ∀ (hp : ¬p = 0) (b : σ →₀ ℕ) (hb₁ : b ∈ p.support)
    (hb₂ :
      (p.support.sup fun (m : σ →₀ ℕ) ↦ Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) m)) =
        Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) b))
    (hb : b ∉ q.support) (hbb : b ∈ (p + q).support), p.totalDegree ≤ (p + q).totalDegree
⊢ (p + q).totalDegree = p.totalDegree
have neg₅ : ∀ (hp : ¬p = 0) (b : σ →₀ ℕ) (hb₁ : b ∈ p.support)
  (hb₂ :
    (p.support.sup fun (m : σ →₀ ℕ) ↦ Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) m)) =
      Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) b))
  (hb : b ∉ q.support) (hbb : b ∈ (p + q).support),
  Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) b) ≤
    (p + q).support.sup fun (m : σ →₀ ℕ) ↦ Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) m)
Tactic: classical
    apply le_antisymm
    · rw [← max_eq_left_of_lt h]
      exact totalDegree_add p q
    by_cases hp : p = 0
    · simp [hp]
    obtain ⟨b, hb₁, hb₂⟩ :=
      p.support.exists_mem_eq_sup (Finsupp.support_nonempty_iff.mpr hp) fun m : σ →₀ ℕ =>
        Multiset.card (toMultiset m)
    have hb : b ∉ q.support := by
      contrapose! h
      rw [totalDegree_eq p, hb₂, totalDegree_eq]
      apply Finset.le_sup h
    have hbb : b ∈ (p + q).support := by
      apply support_sdiff_support_subset_support_add
      rw [Finset.mem_sdiff]
      exact ⟨hb₁, hb⟩
    rw [totalDegree_eq, hb₂, totalDegree_eq]
    exact Finset.le_sup (f := fun m => Multiset.card (Finsupp.toMultiset m)) hbb
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
⊢ (q + p).totalDegree = p.totalDegree
have rw : (p + q).totalDegree = p.totalDegree
Tactic: rw [add_comm, totalDegree_add_eq_left_of_totalDegree_lt h]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
rw : (p + q).totalDegree = p.totalDegree
⊢ (q + p).totalDegree = p.totalDegree
have rw₁ : p.totalDegree = p.totalDegree
Tactic: rw [add_comm, totalDegree_add_eq_left_of_totalDegree_lt h]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
a : MvPolynomial σ R
n : ℕ
⊢ (a ^ n).totalDegree ≤ n * a.totalDegree
have rw : totalDegree.{u, u_1} (R := R) (σ := σ) (∏ _k ∈ Finset.range n, a) ≤ ∑ _k ∈ Finset.range n, a.totalDegree
Tactic: rw [Finset.pow_eq_prod_const, ← Nat.nsmul_eq_mul, Finset.nsmul_eq_sum_const]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
a : MvPolynomial σ R
n : ℕ
⊢ totalDegree.{u, u_1} (R := R) (σ := σ) (∏ _k ∈ Finset.range n, a) ≤ ∑ _k ∈ Finset.range n, a.totalDegree
have refine : ∀ (x x_1 : σ →₀ ℕ),
  ((x + x_1).sum fun (x : σ) (e : ℕ) ↦ e) =
    HAdd.hAdd (α := ℕ) (x.sum fun (x : σ) (e : ℕ) ↦ e) (x_1.sum fun (x : σ) (e : ℕ) ↦ e)
Tactic: refine supDegree_prod_le rfl (fun _ _ => ?_)
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
s : σ →₀ ℕ
c : R
hc : ¬c = 0
⊢ totalDegree.{u, u_1} (R := R) (σ := σ) ((monomial s : (a : R) → MvPolynomial σ R) c) ≤ s.sum fun (x : σ) ↦ id
have rw : LE.le (α := ℕ) (s.sum fun (x : σ) (e : ℕ) ↦ e) (s.sum fun (x : σ) ↦ id)
Tactic: rw [totalDegree_monomial _ hc, Function.id_def]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
s : σ →₀ ℕ
c : R
hc : ¬c = 0
rw : LE.le (α := ℕ) (s.sum fun (x : σ) (e : ℕ) ↦ e) (s.sum fun (x : σ) ↦ id)
⊢ totalDegree.{u, u_1} (R := R) (σ := σ) ((monomial s : (a : R) → MvPolynomial σ R) c) ≤ s.sum fun (x : σ) ↦ id
have rw₁ : LE.le (α := ℕ) (s.sum fun (x : σ) (e : ℕ) ↦ e) (s.sum fun (x : σ) (e : ℕ) ↦ e)
Tactic: rw [totalDegree_monomial _ hc, Function.id_def]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
s : σ →₀ ℕ
c : R
⊢ totalDegree.{u, u_1} (R := R) (σ := σ) ((monomial s : (a : R) → MvPolynomial σ R) c) ≤ s.sum fun (x : σ) ↦ id
have if : ∀ (hc : c = 0),
  totalDegree.{u, u_1} (R := R) (σ := σ) ((monomial s : (a : R) → MvPolynomial σ R) c) ≤ s.sum fun (x : σ) ↦ id
Tactic: if hc : c = 0 then
    simp only [hc, map_zero, totalDegree_zero, zero_le]
  else
    rw [totalDegree_monomial _ hc, Function.id_def]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
s : σ →₀ ℕ
c : R
if :
  ∀ (hc : c = 0),
    totalDegree.{u, u_1} (R := R) (σ := σ) ((monomial s : (a : R) → MvPolynomial σ R) c) ≤ s.sum fun (x : σ) ↦ id
⊢ totalDegree.{u, u_1} (R := R) (σ := σ) ((monomial s : (a : R) → MvPolynomial σ R) c) ≤ s.sum fun (x : σ) ↦ id
have if₁ : ∀ (hc : ¬c = 0),
  totalDegree.{u, u_1} (R := R) (σ := σ) ((monomial s : (a : R) → MvPolynomial σ R) c) ≤ s.sum fun (x : σ) ↦ id
Tactic: if hc : c = 0 then
    simp only [hc, map_zero, totalDegree_zero, zero_le]
  else
    rw [totalDegree_monomial _ hc, Function.id_def]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
ι : Type u_3
f : ι → MvPolynomial σ R
a : ι
s : Finset ι
has : a ∉ s
hind : (s.sum f).totalDegree ≤ s.sup fun (i : ι) ↦ (f i).totalDegree
⊢ ((Finset.cons a s has).sum f).totalDegree ≤ (Finset.cons a s has).sup fun (i : ι) ↦ (f i).totalDegree
have cons : (f a + ∑ x ∈ s, f x).totalDegree ≤ max (f a).totalDegree (s.sup fun (i : ι) ↦ (f i).totalDegree)
Tactic: rw [Finset.sum_cons, Finset.sup_cons]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
ι : Type u_3
s : Finset ι
f : ι → MvPolynomial σ R
⊢ (s.sum f).totalDegree ≤ s.sup fun (i : ι) ↦ (f i).totalDegree
have empty : (Finset.sum ∅ f).totalDegree ≤ Finset.sup ∅ fun (i : ι) ↦ (f i).totalDegree
Tactic: induction s using Finset.cons_induction with
  | empty => exact zero_le
  | cons a s has hind =>
    rw [Finset.sum_cons, Finset.sup_cons]
    exact (MvPolynomial.totalDegree_add _ _).trans (max_le_max le_rfl hind)
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
ι : Type u_3
s : Finset ι
f : ι → MvPolynomial σ R
empty : (Finset.sum ∅ f).totalDegree ≤ Finset.sup ∅ fun (i : ι) ↦ (f i).totalDegree
⊢ (s.sum f).totalDegree ≤ s.sup fun (i : ι) ↦ (f i).totalDegree
have cons : ∀ (a : ι) (s : Finset ι) (has : a ∉ s) (hind : (s.sum f).totalDegree ≤ s.sup fun (i : ι) ↦ (f i).totalDegree),
  ((Finset.cons a s has).sum f).totalDegree ≤ (Finset.cons a s has).sup fun (i : ι) ↦ (f i).totalDegree
Tactic: induction s using Finset.cons_induction with
  | empty => exact zero_le
  | cons a s has hind =>
    rw [Finset.sum_cons, Finset.sup_cons]
    exact (MvPolynomial.totalDegree_add _ _).trans (max_le_max le_rfl hind)
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : Fintype σ
f : MvPolynomial σ R
n : ℕ
h : f.totalDegree < n * Fintype.card σ
d : σ →₀ ℕ
hd : d ∈ f.support
⊢ ∃ (i : σ), (d : (a : σ) → ℕ) i < n
have contrapose! : ∀ (h : ∀ (i : σ), n ≤ (d : (a : σ) → ℕ) i), n * Fintype.card σ ≤ f.totalDegree
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : Fintype σ
f : MvPolynomial σ R
n : ℕ
d : σ →₀ ℕ
hd : d ∈ f.support
h : ∀ (i : σ), n ≤ (d : (a : σ) → ℕ) i
⊢ n * Fintype.card σ = ∑ _s : σ, n
have rw : n * Fintype.card σ = Finset.card.{u_1} (α := σ) Finset.univ • n
Tactic: rw [Finset.sum_const, Nat.nsmul_eq_mul, mul_comm, Finset.card_univ]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : Fintype σ
f : MvPolynomial σ R
n : ℕ
d : σ →₀ ℕ
hd : d ∈ f.support
h : ∀ (i : σ), n ≤ (d : (a : σ) → ℕ) i
rw : n * Fintype.card σ = Finset.card.{u_1} (α := σ) Finset.univ • n
⊢ n * Fintype.card σ = ∑ _s : σ, n
have rw₁ : n * Fintype.card σ = Finset.card.{u_1} (α := σ) Finset.univ * n
Tactic: rw [Finset.sum_const, Nat.nsmul_eq_mul, mul_comm, Finset.card_univ]