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 : MvPolynomial σ R
i : σ
h : p ≠ 0
k : ℕ
hk : degreeOf i (p * HPow.hPow (α := MvPolynomial σ R) (X i) k) = degreeOf i p + k
this : p * HPow.hPow (α := MvPolynomial σ R) (X i) k ≠ 0
succ :
  degreeOf i (p * (HPow.hPow (α := MvPolynomial σ R) (X i) k * HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (X i) 1)) =
    degreeOf i p + (k + 1)
⊢ degreeOf i (p * HPow.hPow (α := MvPolynomial σ R) (X i) (k + 1)) = degreeOf i p + (k + 1)
have succ₁ : degreeOf i (p * (HPow.hPow (α := MvPolynomial σ R) (X i) k * X i)) = degreeOf i p + (k + 1)
Tactic: rw [pow_add, pow_one, ← mul_assoc,
      (degreeOf_mul_X_eq_degreeOf_add_one_iff i _).mpr this, hk, add_assoc]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
i : σ
h : p ≠ 0
k : ℕ
hk : degreeOf i (p * HPow.hPow (α := MvPolynomial σ R) (X i) k) = degreeOf i p + k
this : p * HPow.hPow (α := MvPolynomial σ R) (X i) k ≠ 0
succ :
  degreeOf i (p * (HPow.hPow (α := MvPolynomial σ R) (X i) k * HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (X i) 1)) =
    degreeOf i p + (k + 1)
succ₁ : degreeOf i (p * (HPow.hPow (α := MvPolynomial σ R) (X i) k * X i)) = degreeOf i p + (k + 1)
⊢ degreeOf i (p * HPow.hPow (α := MvPolynomial σ R) (X i) (k + 1)) = degreeOf i p + (k + 1)
have succ₂ : degreeOf i (p * HPow.hPow (α := MvPolynomial σ R) (X i) k * X i) = degreeOf i p + (k + 1)
Tactic: rw [pow_add, pow_one, ← mul_assoc,
      (degreeOf_mul_X_eq_degreeOf_add_one_iff i _).mpr this, hk, add_assoc]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
i : σ
h : p ≠ 0
k : ℕ
hk : degreeOf i (p * HPow.hPow (α := MvPolynomial σ R) (X i) k) = degreeOf i p + k
this : p * HPow.hPow (α := MvPolynomial σ R) (X i) k ≠ 0
succ :
  degreeOf i (p * (HPow.hPow (α := MvPolynomial σ R) (X i) k * HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (X i) 1)) =
    degreeOf i p + (k + 1)
succ₁ : degreeOf i (p * (HPow.hPow (α := MvPolynomial σ R) (X i) k * X i)) = degreeOf i p + (k + 1)
succ₂ : degreeOf i (p * HPow.hPow (α := MvPolynomial σ R) (X i) k * X i) = degreeOf i p + (k + 1)
⊢ degreeOf i (p * HPow.hPow (α := MvPolynomial σ R) (X i) (k + 1)) = degreeOf i p + (k + 1)
have succ₃ : degreeOf i (p * HPow.hPow (α := MvPolynomial σ R) (X i) k) + 1 = degreeOf i p + (k + 1)
Tactic: rw [pow_add, pow_one, ← mul_assoc,
      (degreeOf_mul_X_eq_degreeOf_add_one_iff i _).mpr this, hk, add_assoc]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
i : σ
h : p ≠ 0
k : ℕ
hk : degreeOf i (p * HPow.hPow (α := MvPolynomial σ R) (X i) k) = degreeOf i p + k
this : p * HPow.hPow (α := MvPolynomial σ R) (X i) k ≠ 0
succ :
  degreeOf i (p * (HPow.hPow (α := MvPolynomial σ R) (X i) k * HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (X i) 1)) =
    degreeOf i p + (k + 1)
succ₁ : degreeOf i (p * (HPow.hPow (α := MvPolynomial σ R) (X i) k * X i)) = degreeOf i p + (k + 1)
succ₂ : degreeOf i (p * HPow.hPow (α := MvPolynomial σ R) (X i) k * X i) = degreeOf i p + (k + 1)
succ₃ : degreeOf i (p * HPow.hPow (α := MvPolynomial σ R) (X i) k) + 1 = degreeOf i p + (k + 1)
⊢ degreeOf i (p * HPow.hPow (α := MvPolynomial σ R) (X i) (k + 1)) = degreeOf i p + (k + 1)
have succ₄ : degreeOf i p + k + 1 = degreeOf i p + (k + 1)
Tactic: rw [pow_add, pow_one, ← mul_assoc,
      (degreeOf_mul_X_eq_degreeOf_add_one_iff i _).mpr this, hk, add_assoc]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
i : σ
h : p ≠ 0
k : ℕ
hk : degreeOf i (p * HPow.hPow (α := MvPolynomial σ R) (X i) k) = degreeOf i p + k
this : p * HPow.hPow (α := MvPolynomial σ R) (X i) k ≠ 0
succ :
  degreeOf i (p * (HPow.hPow (α := MvPolynomial σ R) (X i) k * HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (X i) 1)) =
    degreeOf i p + (k + 1)
succ₁ : degreeOf i (p * (HPow.hPow (α := MvPolynomial σ R) (X i) k * X i)) = degreeOf i p + (k + 1)
succ₂ : degreeOf i (p * HPow.hPow (α := MvPolynomial σ R) (X i) k * X i) = degreeOf i p + (k + 1)
succ₃ : degreeOf i (p * HPow.hPow (α := MvPolynomial σ R) (X i) k) + 1 = degreeOf i p + (k + 1)
succ₄ : degreeOf i p + k + 1 = degreeOf i p + (k + 1)
⊢ degreeOf i (p * HPow.hPow (α := MvPolynomial σ R) (X i) (k + 1)) = degreeOf i p + (k + 1)
have succ₅ : degreeOf i p + (k + 1) = degreeOf i p + (k + 1)
Tactic: rw [pow_add, pow_one, ← mul_assoc,
      (degreeOf_mul_X_eq_degreeOf_add_one_iff i _).mpr this, hk, add_assoc]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
i : σ
k : ℕ
h : p ≠ 0
⊢ degreeOf i (p * HPow.hPow (α := MvPolynomial σ R) (X i) k) = degreeOf i p + k
have zero : degreeOf i (p * HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (X i) 0) = degreeOf i p + 0
Tactic: induction k with
  | zero => rw [pow_zero, mul_one, add_zero]
  | succ k hk =>
    have : p * X i ^ k ≠ 0 := by
      rcases ne_zero_iff.mp h with ⟨s, hs⟩
      refine ne_zero_iff.mpr ⟨s + Finsupp.single i k, ?_⟩
      rwa [X_pow_eq_monomial, coeff_mul_monomial, mul_one]
    rw [pow_add, pow_one, ← mul_assoc,
      (degreeOf_mul_X_eq_degreeOf_add_one_iff i _).mpr this, hk, add_assoc]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
i : σ
k : ℕ
h : p ≠ 0
zero : degreeOf i (p * HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (X i) 0) = degreeOf i p + 0
⊢ degreeOf i (p * HPow.hPow (α := MvPolynomial σ R) (X i) k) = degreeOf i p + k
have succ : ∀ (k : ℕ) (hk : degreeOf i (p * HPow.hPow (α := MvPolynomial σ R) (X i) k) = degreeOf i p + k),
  degreeOf i (p * HPow.hPow (α := MvPolynomial σ R) (X i) (k + 1)) = degreeOf i p + (k + 1)
Tactic: induction k with
  | zero => rw [pow_zero, mul_one, add_zero]
  | succ k hk =>
    have : p * X i ^ k ≠ 0 := by
      rcases ne_zero_iff.mp h with ⟨s, hs⟩
      refine ne_zero_iff.mpr ⟨s + Finsupp.single i k, ?_⟩
      rwa [X_pow_eq_monomial, coeff_mul_monomial, mul_one]
    rw [pow_add, pow_one, ← mul_assoc,
      (degreeOf_mul_X_eq_degreeOf_add_one_iff i _).mpr this, hk, add_assoc]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
i j : σ
h : i ≠ j
⊢ degreeOf i (p * HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (X j) 0) = degreeOf i p
have zero : degreeOf i (p * 1) = degreeOf i p
Tactic: rw [pow_zero, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
i j : σ
h : i ≠ j
zero : degreeOf i (p * 1) = degreeOf i p
⊢ degreeOf i (p * HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (X j) 0) = degreeOf i p
have zero₁ : degreeOf i p = degreeOf i p
Tactic: rw [pow_zero, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
i j : σ
h : i ≠ j
k : ℕ
hk : degreeOf i (p * HPow.hPow (α := MvPolynomial σ R) (X j) k) = degreeOf i p
⊢ degreeOf i (p * HPow.hPow (α := MvPolynomial σ R) (X j) (k + 1)) = degreeOf i p
have succ : degreeOf i (p * (HPow.hPow (α := MvPolynomial σ R) (X j) k * HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (X j) 1)) =
  degreeOf i p
Tactic: rw [pow_add, pow_one, ← mul_assoc, degreeOf_mul_X_of_ne _ h, hk]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
i j : σ
h : i ≠ j
k : ℕ
hk : degreeOf i (p * HPow.hPow (α := MvPolynomial σ R) (X j) k) = degreeOf i p
succ :
  degreeOf i (p * (HPow.hPow (α := MvPolynomial σ R) (X j) k * HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (X j) 1)) =
    degreeOf i p
⊢ degreeOf i (p * HPow.hPow (α := MvPolynomial σ R) (X j) (k + 1)) = degreeOf i p
have succ₁ : degreeOf i (p * (HPow.hPow (α := MvPolynomial σ R) (X j) k * X j)) = degreeOf i p
Tactic: rw [pow_add, pow_one, ← mul_assoc, degreeOf_mul_X_of_ne _ h, hk]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
i j : σ
h : i ≠ j
k : ℕ
hk : degreeOf i (p * HPow.hPow (α := MvPolynomial σ R) (X j) k) = degreeOf i p
succ :
  degreeOf i (p * (HPow.hPow (α := MvPolynomial σ R) (X j) k * HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (X j) 1)) =
    degreeOf i p
succ₁ : degreeOf i (p * (HPow.hPow (α := MvPolynomial σ R) (X j) k * X j)) = degreeOf i p
⊢ degreeOf i (p * HPow.hPow (α := MvPolynomial σ R) (X j) (k + 1)) = degreeOf i p
have succ₂ : degreeOf i (p * HPow.hPow (α := MvPolynomial σ R) (X j) k * X j) = degreeOf i p
Tactic: rw [pow_add, pow_one, ← mul_assoc, degreeOf_mul_X_of_ne _ h, hk]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
i j : σ
h : i ≠ j
k : ℕ
hk : degreeOf i (p * HPow.hPow (α := MvPolynomial σ R) (X j) k) = degreeOf i p
succ :
  degreeOf i (p * (HPow.hPow (α := MvPolynomial σ R) (X j) k * HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (X j) 1)) =
    degreeOf i p
succ₁ : degreeOf i (p * (HPow.hPow (α := MvPolynomial σ R) (X j) k * X j)) = degreeOf i p
succ₂ : degreeOf i (p * HPow.hPow (α := MvPolynomial σ R) (X j) k * X j) = degreeOf i p
succ₃ : degreeOf i (p * HPow.hPow (α := MvPolynomial σ R) (X j) k) = degreeOf i p
⊢ degreeOf i (p * HPow.hPow (α := MvPolynomial σ R) (X j) (k + 1)) = degreeOf i p
have succ₄ : degreeOf i p = degreeOf i p
Tactic: rw [pow_add, pow_one, ← mul_assoc, degreeOf_mul_X_of_ne _ h, hk]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
i j : σ
k : ℕ
h : i ≠ j
⊢ degreeOf i (p * HPow.hPow (α := MvPolynomial σ R) (X j) k) = degreeOf i p
have zero : degreeOf i (p * HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (X j) 0) = degreeOf i p
Tactic: induction k with
  | zero => rw [pow_zero, mul_one]
  | succ k hk => rw [pow_add, pow_one, ← mul_assoc, degreeOf_mul_X_of_ne _ h, hk]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
i j : σ
k : ℕ
h : i ≠ j
zero : degreeOf i (p * HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (X j) 0) = degreeOf i p
⊢ degreeOf i (p * HPow.hPow (α := MvPolynomial σ R) (X j) k) = degreeOf i p
have succ : ∀ (k : ℕ) (hk : degreeOf i (p * HPow.hPow (α := MvPolynomial σ R) (X j) k) = degreeOf i p),
  degreeOf i (p * HPow.hPow (α := MvPolynomial σ R) (X j) (k + 1)) = degreeOf i p
Tactic: induction k with
  | zero => rw [pow_zero, mul_one]
  | succ k hk => rw [pow_add, pow_one, ← mul_assoc, degreeOf_mul_X_of_ne _ h, hk]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
i : σ
h : degreeOf i q < degreeOf i p
⊢ degreeOf i (p + q) = degreeOf i p
have a : degreeOf i (p + q) ≤ degreeOf i p
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
i : σ
h : degreeOf i q < degreeOf i p
a : degreeOf i (p + q) ≤ degreeOf i p
⊢ degreeOf i (p + q) = degreeOf i p
have a₁ : degreeOf i p ≤ degreeOf i (p + q)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
i : σ
h : degreeOf i q < degreeOf i p
⊢ degreeOf i (p + q) ≤ degreeOf i p
have a : degreeOf i (p + q) ≤ max (degreeOf i p) (degreeOf i q)
Tactic: rw [← max_eq_left_of_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
i : σ
h : degreeOf i q < degreeOf i p
⊢ degreeOf i p ≤ degreeOf i (p + q)
have a : degreeOf i p ≤ (p + q).support.sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) i
Tactic: nth_rw 2 [degreeOf_eq_sup]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
i : σ
h : degreeOf i q < degreeOf i p
⊢ degreeOf i p ≤ (p + q).support.sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) i
have a : ∃ b ∈ (p + q).support, degreeOf i p ≤ (b : (a : σ) → ℕ) i
Tactic: apply (Finset.le_sup_iff <| Nat.zero_lt_of_lt h).mpr
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (hypothesis)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
i : σ
h : degreeOf i q < degreeOf i p
⊢ ∃ b ∈ (p + q).support, degreeOf i p ≤ (b : (a : σ) → ℕ) i
have this : p.support.Nonempty
Tactic: have : p.support.Nonempty := by aesop
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
i : σ
h : degreeOf i q < degreeOf i p
this : p.support.Nonempty
⊢ ∃ b ∈ (p + q).support, degreeOf i p ≤ (b : (a : σ) → ℕ) i
have a : ∀ (s : σ →₀ ℕ) (hs1 : s ∈ p.support)
  (hs2 : Eq (α := ℕ) (p.support.sup fun (s : σ →₀ ℕ) ↦ (s : (a : σ) → ℕ) i : ℕ) ((s : (a : σ) → ℕ) i : ℕ)),
  ∃ b ∈ (p + q).support, degreeOf i p ≤ (b : (a : σ) → ℕ) i
Tactic: have ⟨s, hs1, hs2⟩ := Finset.exists_mem_eq_sup _ this (fun s ↦ s i)
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (hypothesis)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
i : σ
h : degreeOf i q < degreeOf i p
this : p.support.Nonempty
s : σ →₀ ℕ
hs1 : s ∈ p.support
hs2 : Eq (α := ℕ) (p.support.sup fun (s : σ →₀ ℕ) ↦ (s : (a : σ) → ℕ) i : ℕ) ((s : (a : σ) → ℕ) i : ℕ)
⊢ ∃ b ∈ (p + q).support, degreeOf i p ≤ (b : (a : σ) → ℕ) i
have hs2₁ : degreeOf i p = (s : (a : σ) → ℕ) i
Tactic: rw [← degreeOf_eq_sup i p] at hs2
Cleared hypotheses: hs2
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
i : σ
h : degreeOf i q < degreeOf i p
this : p.support.Nonempty
s : σ →₀ ℕ
hs1 : s ∈ p.support
hs2 : degreeOf i p = (s : (a : σ) → ℕ) i
⊢ degreeOf i p ≤ (s : (a : σ) → ℕ) i
have rw : LE.le (α := ℕ) ((s : (a : σ) → ℕ) i : ℕ) ((s : (a : σ) → ℕ) i : ℕ)
Tactic: rw [hs2]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
i : σ
h : degreeOf i q < degreeOf i p
this : p.support.Nonempty
s : σ →₀ ℕ
hs1 : s ∈ p.support
hs2 : degreeOf i p = (s : (a : σ) → ℕ) i
⊢ ∃ b ∈ (p + q).support, degreeOf i p ≤ (b : (a : σ) → ℕ) i
have a : s ∈ (p + q).support
Tactic: refine ⟨s, ?_, by rw [hs2]⟩
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
i : σ
h : degreeOf i q < degreeOf i p
this : p.support.Nonempty
s : σ →₀ ℕ
hs1 : s ∈ p.support
hs2 : degreeOf i p = (s : (a : σ) → ℕ) i
⊢ s ∉ q.support
have contrapose! : ∀ (h : s ∈ q.support), degreeOf i p ≤ degreeOf i q
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
i : σ
this : p.support.Nonempty
s : σ →₀ ℕ
hs1 : s ∈ p.support
hs2 : degreeOf i p = (s : (a : σ) → ℕ) i
h : s ∈ q.support
⊢ degreeOf i p ≤ degreeOf i q
have rw : (s : (a : σ) → ℕ) i ≤ degreeOf i q
Tactic: rw [hs2]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (hypothesis)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
i : σ
h : degreeOf i q < degreeOf i p
this : p.support.Nonempty
s : σ →₀ ℕ
hs1 : s ∈ p.support
hs2 : degreeOf i p = (s : (a : σ) → ℕ) i
⊢ s ∈ (p + q).support
have this₁ : s ∉ q.support
Tactic: have : s ∉ q.support := by
    contrapose! h
    rw [hs2]
    exact le_degreeOf_of_mem_support i 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
i : σ
h : degreeOf i q < degreeOf i p
this_1 : p.support.Nonempty
s : σ →₀ ℕ
hs1 : s ∈ p.support
hs2 : degreeOf i p = (s : (a : σ) → ℕ) i
this : s ∉ q.support
⊢ s ∈ (p + q).support
have a : ∀ (hs1 : ¬coeff s p = 0) (this : coeff s q = 0), ¬coeff s p + coeff s q = 0
Tactic: simp only [mem_support_iff, ne_eq, coeff_add, not_not] at hs1 ⊢ this
Cleared hypotheses: hs1, this
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
i : σ
h : degreeOf i q < degreeOf i p
this_1 : p.support.Nonempty
s : σ →₀ ℕ
hs2 : degreeOf i p = (s : (a : σ) → ℕ) i
hs1 : ¬coeff s p = 0
this : coeff s q = 0
⊢ ¬coeff s p + coeff s q = 0
have a : ¬coeff s p + 0 = 0
Tactic: rwa [this, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
i : σ
h : degreeOf i (p + q) < degreeOf i p
⊢ degreeOf i p = degreeOf i q
have contrapose! : ∀ (h : degreeOf i p ≠ degreeOf i q), degreeOf i p ≤ degreeOf i (p + q)
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
i : σ
h : degreeOf i p ≠ degreeOf i q
⊢ degreeOf i p ≤ degreeOf i (p + q)
have apply : max (degreeOf i p) (degreeOf i q) ≤ degreeOf i (p + q)
Tactic: apply le_trans (Nat.le_max_left _ (q.degreeOf i))
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
i : σ
h : degreeOf i p ≠ degreeOf i q
⊢ max (degreeOf i p) (degreeOf i q) ≤ degreeOf i (p + q)
have inl : ∀ (h : degreeOf i p < degreeOf i q), max (degreeOf i p) (degreeOf i q) ≤ degreeOf i (p + q)
Tactic: rcases Nat.lt_or_lt_of_ne h with h | 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
i : σ
h : degreeOf i p ≠ degreeOf i q
inl : ∀ (h : degreeOf i p < degreeOf i q), max (degreeOf i p) (degreeOf i q) ≤ degreeOf i (p + q)
⊢ max (degreeOf i p) (degreeOf i q) ≤ degreeOf i (p + q)
have inr : ∀ (h : degreeOf i q < degreeOf i p), max (degreeOf i p) (degreeOf i q) ≤ degreeOf i (p + q)
Tactic: rcases Nat.lt_or_lt_of_ne h with h | h
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
i : σ
c : R
⊢ Multiset.count i
      (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R) p).degrees ≤
    Multiset.count i p.degrees
have h : p.degrees = degrees.{u, u_1} (R := R) ((C : (a : R) → MvPolynomial σ R) c) + p.degrees
Tactic: convert! Multiset.count_le_of_le i degrees_mul_le
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
i : σ
c : R
⊢ Multiset.count i
      (HMul.hMul (β := MvPolynomial σ R) p ((C : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R)).degrees ≤
    Multiset.count i p.degrees
have h : p.degrees = p.degrees + degrees.{u, u_1} (R := R) ((C : (a : R) → MvPolynomial σ R) c)
Tactic: convert! Multiset.count_le_of_le i degrees_mul_le
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
⊢ Eq (α := ℕ) (p.support.sup fun (s : σ →₀ ℕ) ↦ s.sum fun (x : σ) (e : ℕ) ↦ e)
    (p.support.sup fun (m : σ →₀ ℕ) ↦ Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) m))
have e_f : Eq.{u_1 + 1} (α := (σ →₀ ℕ) → ℕ) (fun (s : σ →₀ ℕ) ↦ s.sum fun (x : σ) (e : ℕ) ↦ e) fun (m : σ →₀ ℕ) ↦
  Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) m)
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
⊢ Eq.{u_1 + 1} (α := (σ →₀ ℕ) → ℕ) (fun (s : σ →₀ ℕ) ↦ s.sum fun (x : σ) (e : ℕ) ↦ e) fun (m : σ →₀ ℕ) ↦
    Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) m)
have e_f : ∀ (m : σ →₀ ℕ),
  (m.sum fun (x : σ) (e : ℕ) ↦ e) = Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) m)
Tactic: funext m
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
⊢ p.totalDegree ≤ p.degrees.card
have rw : (p.support.sup fun (m : σ →₀ ℕ) ↦ Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) m)) ≤
  p.degrees.card
Tactic: rw [totalDegree_eq]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
⊢ p.totalDegree ≤ p.degrees.card
have rw : (p.support.sup fun (m : σ →₀ ℕ) ↦ Multiset.card.{u_1} (α := σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) m)) ≤
  p.degrees.card
Tactic: classical
  rw [totalDegree_eq]
  exact Finset.sup_le fun s hs => Multiset.card_le_card <| Finset.le_sup hs
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
a : R
⊢ Eq (α := ℕ) (if a = 0 then ⊥ else sum 0 fun (x : σ) (e : ℕ) ↦ e) 0
have rw : Eq (α := ℕ) (if a = 0 then ⊥ else 0) 0
Tactic: rw [sum_zero_index, bot_eq_zero', ite_self]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
a : R
rw : Eq (α := ℕ) (if a = 0 then ⊥ else 0) 0
⊢ Eq (α := ℕ) (if a = 0 then ⊥ else sum 0 fun (x : σ) (e : ℕ) ↦ e) 0
have rw₁ : Eq (α := ℕ) (if a = 0 then 0 else 0) 0
Tactic: rw [sum_zero_index, bot_eq_zero', ite_self]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
a : R
rw : Eq (α := ℕ) (if a = 0 then ⊥ else 0) 0
rw₁ : Eq (α := ℕ) (if a = 0 then 0 else 0) 0
⊢ Eq (α := ℕ) (if a = 0 then ⊥ else sum 0 fun (x : σ) (e : ℕ) ↦ e) 0
have rw₂ : Eq (α := ℕ) 0 0
Tactic: rw [sum_zero_index, bot_eq_zero', ite_self]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
⊢ totalDegree.{u, u_1} (R := R) (σ := σ) 0 = 0
have rw : totalDegree.{u, u_1} (R := R) (σ := σ) ((C : (a : R) → MvPolynomial σ R) 0) = 0
Tactic: rw [← C_0]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
inst_1 : Nontrivial R
s : σ
⊢ totalDegree.{u_3, u_1} (R := R) (X s) = 1
have rw : Eq (α := ℕ) (Finset.sup {Finsupp.single s 1} fun (s : σ →₀ ℕ) ↦ s.sum fun (x : σ) (e : ℕ) ↦ e) 1
Tactic: rw [totalDegree, support_X]
-- 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: apply le_antisymm
-- 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: apply le_antisymm
-- 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 ≤ max p.totalDegree q.totalDegree
Tactic: rw [← max_eq_left_of_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
⊢ p.totalDegree ≤ (p + q).totalDegree
have pos : ∀ (hp : p = 0), p.totalDegree ≤ (p + q).totalDegree
Tactic: by_cases hp : p = 0