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 : σ
s : σ →₀ ℕ
h : s ∈ p.support
si : LT.lt (α := ℕ) (0 : ℕ) ((s : (a : σ) → ℕ) i : ℕ)
w : σ →₀ ℕ
⊢ ∃ b ∈ p.support, LE.le (α := ℕ) ((s : (a : σ) → ℕ) i : ℕ) ((b : (a : σ) → ℕ) i : ℕ)
have h₁ : s ∈ p.support ∧ LE.le (α := ℕ) ((s : (a : σ) → ℕ) i : ℕ) ((s : (a : σ) → ℕ) i : ℕ)
Tactic: use s
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
i : σ
s : σ →₀ ℕ
h : degreeOf i p < (s : (a : σ) → ℕ) i
⊢ s ∉ p.support
have contrapose! : ∀ (h : s ∈ p.support), (s : (a : σ) → ℕ) i ≤ degreeOf i p
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
i : σ
f g : MvPolynomial σ R
⊢ Multiset.count i (f * g).degrees ≤ Multiset.count i f.degrees + Multiset.count i g.degrees
have h : Multiset.count i f.degrees + Multiset.count i g.degrees = Multiset.count i (f.degrees + g.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
i : σ
f g : MvPolynomial σ R
⊢ Multiset.count i f.degrees + Multiset.count i g.degrees = Multiset.count i (f.degrees + g.degrees)
have h : Multiset.count i f.degrees + Multiset.count i g.degrees = Multiset.count i f.degrees + Multiset.count i g.degrees
Tactic: rw [Multiset.count_add]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
i : σ
f g : MvPolynomial σ R
⊢ degreeOf i (f * g) ≤ degreeOf i f + degreeOf i g
have simp : Multiset.count i (f * g).degrees ≤ Multiset.count i f.degrees + Multiset.count i g.degrees
Tactic: classical
  simp only [degreeOf]
  convert! Multiset.count_le_of_le i degrees_mul_le
  rw [Multiset.count_add]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
i : σ
f g : MvPolynomial σ R
simp : Multiset.count i (f * g).degrees ≤ Multiset.count i f.degrees + Multiset.count i g.degrees
⊢ degreeOf i (f * g) ≤ degreeOf i f + degreeOf i g
have h : Multiset.count i f.degrees + Multiset.count i g.degrees = Multiset.count i (f.degrees + g.degrees)
Tactic: classical
  simp only [degreeOf]
  convert! Multiset.count_le_of_le i degrees_mul_le
  rw [Multiset.count_add]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
ι : Type u_3
i : σ
s : Finset ι
f : ι → MvPolynomial σ R
⊢ degreeOf.{u, u_1} (R := R) i (∑ j ∈ s, f j) ≤ s.sup fun (j : ι) ↦ degreeOf i (f j)
have simp_rw : LE.le (α := ℕ) (Finset.sup (support.{u, u_1} (R := R) (∑ j ∈ s, f j)) fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) i)
  (s.sup fun (j : ι) ↦ (f j).support.sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) i)
Tactic: simp_rw [degreeOf_eq_sup]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
ι : Type u_3
i : σ
s : Finset ι
f : ι → MvPolynomial σ R
⊢ degreeOf.{u, u_1} (R := R) i (∏ j ∈ s, f j) ≤ ∑ j ∈ s, degreeOf i (f j)
have simp_rw : LE.le (α := ℕ) (Finset.sup (support.{u, u_1} (R := R) (∏ j ∈ s, f j)) fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) i)
  (∑ x ∈ s, (f x).support.sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) i)
Tactic: simp_rw [degreeOf_eq_sup]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
i j : σ
f : MvPolynomial σ R
h : i ≠ j
⊢ degreeOf i (f * X j) = degreeOf i f
have simp : Eq (α := ℕ)
  (f.support.sup
    ((fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) i) ∘ (⇑(addRightEmbedding (Finsupp.single j 1)) : (a : σ →₀ ℕ) → σ →₀ ℕ)))
  (f.support.sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) i)
Tactic: simp only [degreeOf_eq_sup i, support_mul_X, Finset.sup_map]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
i j : σ
f : MvPolynomial σ R
h : i ≠ j
⊢ Eq (α := ℕ)
    (f.support.sup
      ((fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) i) ∘ (⇑(addRightEmbedding (Finsupp.single j 1)) : (a : σ →₀ ℕ) → σ →₀ ℕ)))
    (f.support.sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) i)
have e_f : Eq (α := (σ →₀ ℕ) → ℕ)
  ((fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) i) ∘ (⇑(addRightEmbedding (Finsupp.single j 1)) : (a : σ →₀ ℕ) → σ →₀ ℕ))
  fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) i
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
i j : σ
f : MvPolynomial σ R
h : i ≠ j
⊢ Eq (α := (σ →₀ ℕ) → ℕ)
    ((fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) i) ∘ (⇑(addRightEmbedding (Finsupp.single j 1)) : (a : σ →₀ ℕ) → σ →₀ ℕ))
    fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) i
have e_f : ∀ (x : σ →₀ ℕ),
  Eq (α := ℕ)
    (((fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) i) ∘ (⇑(addRightEmbedding (Finsupp.single j 1)) : (a : σ →₀ ℕ) → σ →₀ ℕ))
        x :
      ℕ)
    ((x : (a : σ) → ℕ) i : ℕ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
i j : σ
f : MvPolynomial σ R
h : i ≠ j
⊢ degreeOf i (f * X j) = degreeOf i f
have simp : Eq (α := ℕ)
  (f.support.sup
    ((fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) i) ∘ (⇑(addRightEmbedding (Finsupp.single j 1)) : (a : σ →₀ ℕ) → σ →₀ ℕ)))
  (f.support.sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) i)
Tactic: classical
  simp only [degreeOf_eq_sup i, support_mul_X, Finset.sup_map]
  congr
  ext
  simp only [Finsupp.single, addRightEmbedding_apply, coe_mk,
    Pi.add_apply, comp_apply, Finsupp.coe_add, Pi.single_eq_of_ne h, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
i j : σ
f : MvPolynomial σ R
h : i ≠ j
simp :
  Eq (α := ℕ)
    (f.support.sup
      ((fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) i) ∘ (⇑(addRightEmbedding (Finsupp.single j 1)) : (a : σ →₀ ℕ) → σ →₀ ℕ)))
    (f.support.sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) i)
⊢ degreeOf i (f * X j) = degreeOf i f
have e_f : Eq (α := (σ →₀ ℕ) → ℕ)
  ((fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) i) ∘ (⇑(addRightEmbedding (Finsupp.single j 1)) : (a : σ →₀ ℕ) → σ →₀ ℕ))
  fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) i
Tactic: classical
  simp only [degreeOf_eq_sup i, support_mul_X, Finset.sup_map]
  congr
  ext
  simp only [Finsupp.single, addRightEmbedding_apply, coe_mk,
    Pi.add_apply, comp_apply, Finsupp.coe_add, Pi.single_eq_of_ne h, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
i j : σ
f : MvPolynomial σ R
h : i ≠ j
simp :
  Eq (α := ℕ)
    (f.support.sup
      ((fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) i) ∘ (⇑(addRightEmbedding (Finsupp.single j 1)) : (a : σ →₀ ℕ) → σ →₀ ℕ)))
    (f.support.sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) i)
e_f :
  Eq (α := (σ →₀ ℕ) → ℕ)
    ((fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) i) ∘ (⇑(addRightEmbedding (Finsupp.single j 1)) : (a : σ →₀ ℕ) → σ →₀ ℕ))
    fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) i
⊢ degreeOf i (f * X j) = degreeOf i f
have e_f₁ : ∀ (x : σ →₀ ℕ),
  Eq (α := ℕ)
    (((fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) i) ∘ (⇑(addRightEmbedding (Finsupp.single j 1)) : (a : σ →₀ ℕ) → σ →₀ ℕ))
        x :
      ℕ)
    ((x : (a : σ) → ℕ) i : ℕ)
Tactic: classical
  simp only [degreeOf_eq_sup i, support_mul_X, Finset.sup_map]
  congr
  ext
  simp only [Finsupp.single, addRightEmbedding_apply, coe_mk,
    Pi.add_apply, comp_apply, Finsupp.coe_add, Pi.single_eq_of_ne h, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
j : σ
f : MvPolynomial σ R
⊢ Multiset.count j (f * X j).degrees ≤ Multiset.count j f.degrees + 1
have apply : Multiset.count j (f.degrees + degrees.{u, u_1} (R := R) (X j)) ≤ Multiset.count j f.degrees + 1
Tactic: apply (Multiset.count_le_of_le j degrees_mul_le).trans
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
j : σ
f : MvPolynomial σ R
⊢ Multiset.count j (f.degrees + degrees.{u, u_1} (R := R) (X j)) ≤ Multiset.count j f.degrees + 1
have simp : Multiset.count j (degrees.{u, u_1} (R := R) (X j)) ≤ 1
Tactic: simp only [Multiset.count_add, add_le_add_iff_left]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
j : σ
f : MvPolynomial σ R
⊢ Multiset.count j (degrees.{u, u_1} (R := R) (X j)) ≤ 1
have h : 1 = Multiset.count j {j}
Tactic: convert! Multiset.count_le_of_le j <| degrees_X' j
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
j : σ
f : MvPolynomial σ R
⊢ 1 = Multiset.count j {j}
have h : Eq (α := ℕ) 1 1
Tactic: rw [Multiset.count_singleton_self]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
j : σ
f : MvPolynomial σ R
⊢ degreeOf j (f * X j) ≤ degreeOf j f + 1
have simp : Multiset.count j (f * X j).degrees ≤ Multiset.count j f.degrees + 1
Tactic: classical
  simp only [degreeOf]
  apply (Multiset.count_le_of_le j degrees_mul_le).trans
  simp only [Multiset.count_add, add_le_add_iff_left]
  convert! Multiset.count_le_of_le j <| degrees_X' j
  rw [Multiset.count_singleton_self]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
j : σ
f : MvPolynomial σ R
simp : Multiset.count j (f * X j).degrees ≤ Multiset.count j f.degrees + 1
⊢ degreeOf j (f * X j) ≤ degreeOf j f + 1
have simp₁ : Multiset.count j (f.degrees + degrees.{u, u_1} (R := R) (X j)) ≤ Multiset.count j f.degrees + 1
Tactic: classical
  simp only [degreeOf]
  apply (Multiset.count_le_of_le j degrees_mul_le).trans
  simp only [Multiset.count_add, add_le_add_iff_left]
  convert! Multiset.count_le_of_le j <| degrees_X' j
  rw [Multiset.count_singleton_self]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
j : σ
f : MvPolynomial σ R
simp : Multiset.count j (f * X j).degrees ≤ Multiset.count j f.degrees + 1
simp₁ : Multiset.count j (f.degrees + degrees.{u, u_1} (R := R) (X j)) ≤ Multiset.count j f.degrees + 1
⊢ degreeOf j (f * X j) ≤ degreeOf j f + 1
have simp₂ : Multiset.count j (degrees.{u, u_1} (R := R) (X j)) ≤ 1
Tactic: classical
  simp only [degreeOf]
  apply (Multiset.count_le_of_le j degrees_mul_le).trans
  simp only [Multiset.count_add, add_le_add_iff_left]
  convert! Multiset.count_le_of_le j <| degrees_X' j
  rw [Multiset.count_singleton_self]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
j : σ
f : MvPolynomial σ R
simp : Multiset.count j (f * X j).degrees ≤ Multiset.count j f.degrees + 1
simp₁ : Multiset.count j (f.degrees + degrees.{u, u_1} (R := R) (X j)) ≤ Multiset.count j f.degrees + 1
simp₂ : Multiset.count j (degrees.{u, u_1} (R := R) (X j)) ≤ 1
⊢ degreeOf j (f * X j) ≤ degreeOf j f + 1
have h : 1 = Multiset.count j {j}
Tactic: classical
  simp only [degreeOf]
  apply (Multiset.count_le_of_le j degrees_mul_le).trans
  simp only [Multiset.count_add, add_le_add_iff_left]
  convert! Multiset.count_le_of_le j <| degrees_X' j
  rw [Multiset.count_singleton_self]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
i j : σ
h : i ≠ j
⊢ degreeOf i (HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (X j) 0) = 0
have zero : degreeOf.{u, u_1} (R := R) i 1 = 0
Tactic: rw [pow_zero, ← C_1, degreeOf_C]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
i j : σ
h : i ≠ j
zero : degreeOf.{u, u_1} (R := R) i 1 = 0
⊢ degreeOf i (HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (X j) 0) = 0
have zero₁ : degreeOf.{u, u_1} (R := R) i ((C : (a : R) → MvPolynomial σ R) 1) = 0
Tactic: rw [pow_zero, ← C_1, degreeOf_C]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
i j : σ
h : i ≠ j
zero : degreeOf.{u, u_1} (R := R) i 1 = 0
zero₁ : degreeOf.{u, u_1} (R := R) i ((C : (a : R) → MvPolynomial σ R) 1) = 0
⊢ degreeOf i (HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (X j) 0) = 0
have zero₂ : Eq (α := ℕ) 0 0
Tactic: rw [pow_zero, ← C_1, degreeOf_C]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
i j : σ
h : i ≠ j
k : ℕ
hk : degreeOf i (HPow.hPow (α := MvPolynomial σ R) (X j) k) = 0
⊢ degreeOf i (HPow.hPow (α := MvPolynomial σ R) (X j) (k + 1)) = 0
have succ : degreeOf i (HPow.hPow (α := MvPolynomial σ R) (X j) k * HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (X j) 1) = 0
Tactic: rw [pow_add, pow_one, 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
i j : σ
h : i ≠ j
k : ℕ
hk : degreeOf i (HPow.hPow (α := MvPolynomial σ R) (X j) k) = 0
succ : degreeOf i (HPow.hPow (α := MvPolynomial σ R) (X j) k * HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (X j) 1) = 0
⊢ degreeOf i (HPow.hPow (α := MvPolynomial σ R) (X j) (k + 1)) = 0
have succ₁ : degreeOf i (HPow.hPow (α := MvPolynomial σ R) (X j) k * X j) = 0
Tactic: rw [pow_add, pow_one, 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
i j : σ
h : i ≠ j
k : ℕ
hk : degreeOf i (HPow.hPow (α := MvPolynomial σ R) (X j) k) = 0
succ : degreeOf i (HPow.hPow (α := MvPolynomial σ R) (X j) k * HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (X j) 1) = 0
succ₁ : degreeOf i (HPow.hPow (α := MvPolynomial σ R) (X j) k * X j) = 0
succ₂ : degreeOf i (HPow.hPow (α := MvPolynomial σ R) (X j) k) = 0
⊢ degreeOf i (HPow.hPow (α := MvPolynomial σ R) (X j) (k + 1)) = 0
have succ₃ : Eq (α := ℕ) 0 0
Tactic: rw [pow_add, pow_one, 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
i j : σ
k : ℕ
h : i ≠ j
⊢ degreeOf i (HPow.hPow (α := MvPolynomial σ R) (X j) k) = 0
have zero : degreeOf i (HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (X j) 0) = 0
Tactic: induction k with
  | zero => rw [pow_zero, ← C_1, degreeOf_C]
  | succ k hk => rw [pow_add, pow_one, 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
i j : σ
k : ℕ
h : i ≠ j
zero : degreeOf i (HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (X j) 0) = 0
⊢ degreeOf i (HPow.hPow (α := MvPolynomial σ R) (X j) k) = 0
have succ : ∀ (k : ℕ) (hk : degreeOf i (HPow.hPow (α := MvPolynomial σ R) (X j) k) = 0),
  degreeOf i (HPow.hPow (α := MvPolynomial σ R) (X j) (k + 1)) = 0
Tactic: induction k with
  | zero => rw [pow_zero, ← C_1, degreeOf_C]
  | succ k hk => rw [pow_add, pow_one, 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
j : σ
f : MvPolynomial σ R
⊢ degreeOf j (f * X j) = degreeOf j f + 1 ↔ f ≠ 0
have refine : ∀ (h : f ≠ 0), degreeOf j (f * X j) = degreeOf j f + 1
Tactic: refine ⟨fun h => by by_contra ha; simp [ha] at h, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
j : σ
f : MvPolynomial σ R
h : f ≠ 0
⊢ degreeOf j (f * X j) = degreeOf j f + 1
have apply : degreeOf j f + 1 ≤ degreeOf j (f * X j)
Tactic: apply Nat.le_antisymm (degreeOf_mul_X_self j f)
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (hypothesis)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
j : σ
f : MvPolynomial σ R
h : f ≠ 0
⊢ degreeOf j f + 1 ≤ degreeOf j (f * X j)
have this : HAdd.hAdd (α := ℕ) (f.support.sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) j) 1 =
  f.support.sup fun (m : σ →₀ ℕ) ↦ HAdd.hAdd (α := ℕ) (β := ℕ) ((m : (a : σ) → ℕ) j : ℕ) (1 : ℕ)
Tactic: have : (f.support.sup fun m ↦ m j) + 1 = (f.support.sup fun m ↦ (m j + 1)) :=
    Finset.apply_sup_eq_sup_comp_of_nonempty @Nat.succ_le_succ (support_nonempty.mpr h)
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
j : σ
f : MvPolynomial σ R
h : f ≠ 0
this :
  HAdd.hAdd (α := ℕ) (f.support.sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) j) 1 =
    f.support.sup fun (m : σ →₀ ℕ) ↦ HAdd.hAdd (α := ℕ) (β := ℕ) ((m : (a : σ) → ℕ) j : ℕ) (1 : ℕ)
⊢ degreeOf j f + 1 ≤ degreeOf j (f * X j)
have simp : LE.le (α := ℕ) (f.support.sup fun (m : σ →₀ ℕ) ↦ HAdd.hAdd (α := ℕ) (β := ℕ) ((m : (a : σ) → ℕ) j : ℕ) (1 : ℕ))
  ((Finset.map (addRightEmbedding (Finsupp.single j 1)) f.support).sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) j)
Tactic: simp only [degreeOf_eq_sup, support_mul_X, this]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
j : σ
f : MvPolynomial σ R
h : f ≠ 0
this :
  HAdd.hAdd (α := ℕ) (f.support.sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) j) 1 =
    f.support.sup fun (m : σ →₀ ℕ) ↦ HAdd.hAdd (α := ℕ) (β := ℕ) ((m : (a : σ) → ℕ) j : ℕ) (1 : ℕ)
⊢ LE.le (α := ℕ) (f.support.sup fun (m : σ →₀ ℕ) ↦ HAdd.hAdd (α := ℕ) (β := ℕ) ((m : (a : σ) → ℕ) j : ℕ) (1 : ℕ))
    ((Finset.map (addRightEmbedding (Finsupp.single j 1)) f.support).sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) j)
have a : ∀ b ∈ f.support,
  HAdd.hAdd (α := ℕ) (β := ℕ) ((b : (a : σ) → ℕ) j : ℕ) (1 : ℕ) ≤
    (Finset.map (addRightEmbedding (Finsupp.single j 1)) f.support).sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) j
Tactic: apply Finset.sup_le
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
j : σ
f : MvPolynomial σ R
h : f ≠ 0
this :
  HAdd.hAdd (α := ℕ) (f.support.sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) j) 1 =
    f.support.sup fun (m : σ →₀ ℕ) ↦ HAdd.hAdd (α := ℕ) (β := ℕ) ((m : (a : σ) → ℕ) j : ℕ) (1 : ℕ)
x : σ →₀ ℕ
hx : x ∈ f.support
⊢ HAdd.hAdd (α := ℕ) (β := ℕ) ((x : (a : σ) → ℕ) j : ℕ) (1 : ℕ) ≤
    (Finset.map (addRightEmbedding (Finsupp.single j 1)) f.support).sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) j
have a : ∃ b ∈ f.support,
  HAdd.hAdd (α := ℕ) (β := ℕ) ((x : (a : σ) → ℕ) j : ℕ) (1 : ℕ) ≤
    ((fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) j) ∘ (⇑(addRightEmbedding (Finsupp.single j 1)) : (a : σ →₀ ℕ) → σ →₀ ℕ)) b
Tactic: simp only [Finset.sup_map, bot_eq_zero', add_pos_iff, zero_lt_one, or_true, Finset.le_sup_iff]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
j : σ
f : MvPolynomial σ R
h : f ≠ 0
this :
  HAdd.hAdd (α := ℕ) (f.support.sup fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) j) 1 =
    f.support.sup fun (m : σ →₀ ℕ) ↦ HAdd.hAdd (α := ℕ) (β := ℕ) ((m : (a : σ) → ℕ) j : ℕ) (1 : ℕ)
x : σ →₀ ℕ
hx : x ∈ f.support
⊢ ∃ b ∈ f.support,
    HAdd.hAdd (α := ℕ) (β := ℕ) ((x : (a : σ) → ℕ) j : ℕ) (1 : ℕ) ≤
      ((fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) j) ∘ (⇑(addRightEmbedding (Finsupp.single j 1)) : (a : σ →₀ ℕ) → σ →₀ ℕ)) b
have h₁ : x ∈ f.support ∧
  HAdd.hAdd (α := ℕ) (β := ℕ) ((x : (a : σ) → ℕ) j : ℕ) (1 : ℕ) ≤
    ((fun (m : σ →₀ ℕ) ↦ (m : (a : σ) → ℕ) j) ∘ (⇑(addRightEmbedding (Finsupp.single j 1)) : (a : σ →₀ ℕ) → σ →₀ ℕ)) x
Tactic: use x
-- 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
⊢ degreeOf i (p * HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (X i) 0) = degreeOf i p + 0
have zero : degreeOf i (p * 1) = degreeOf i p + 0
Tactic: rw [pow_zero, mul_one, add_zero]
-- 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
zero : degreeOf i (p * 1) = degreeOf i p + 0
⊢ degreeOf i (p * HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (X i) 0) = degreeOf i p + 0
have zero₁ : degreeOf i p = degreeOf i p + 0
Tactic: rw [pow_zero, mul_one, add_zero]
-- 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
zero : degreeOf i (p * 1) = degreeOf i p + 0
zero₁ : degreeOf i p = degreeOf i p + 0
⊢ degreeOf i (p * HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (X i) 0) = degreeOf i p + 0
have zero₂ : degreeOf i p = degreeOf i p
Tactic: rw [pow_zero, mul_one, add_zero]
-- 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
⊢ p * HPow.hPow (α := MvPolynomial σ R) (X i) k ≠ 0
have rcases : ∀ (s : σ →₀ ℕ) (hs : coeff s p ≠ 0), p * HPow.hPow (α := MvPolynomial σ R) (X i) k ≠ 0
Tactic: rcases ne_zero_iff.mp h with ⟨s, hs⟩
-- 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
s : σ →₀ ℕ
hs : coeff s p ≠ 0
⊢ p * HPow.hPow (α := MvPolynomial σ R) (X i) k ≠ 0
have refine : coeff (s + Finsupp.single i k) (p * HPow.hPow (α := MvPolynomial σ R) (X i) k) ≠ 0
Tactic: refine ne_zero_iff.mpr ⟨s + Finsupp.single i 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 : σ
h : p ≠ 0
k : ℕ
hk : degreeOf i (p * HPow.hPow (α := MvPolynomial σ R) (X i) k) = degreeOf i p + k
s : σ →₀ ℕ
hs : coeff s p ≠ 0
⊢ coeff (s + Finsupp.single i k) (p * HPow.hPow (α := MvPolynomial σ R) (X i) k) ≠ 0
have rwa : coeff (s + Finsupp.single i k) (p * (monomial (Finsupp.single i k) : (a : R) → MvPolynomial σ R) 1) ≠ 0
Tactic: rwa [X_pow_eq_monomial, coeff_mul_monomial, 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 : σ
h : p ≠ 0
k : ℕ
hk : degreeOf i (p * HPow.hPow (α := MvPolynomial σ R) (X i) k) = degreeOf i p + k
s : σ →₀ ℕ
hs : coeff s p ≠ 0
rwa : coeff (s + Finsupp.single i k) (p * (monomial (Finsupp.single i k) : (a : R) → MvPolynomial σ R) 1) ≠ 0
⊢ coeff (s + Finsupp.single i k) (p * HPow.hPow (α := MvPolynomial σ R) (X i) k) ≠ 0
have rwa₁ : coeff s p * 1 ≠ 0
Tactic: rwa [X_pow_eq_monomial, coeff_mul_monomial, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (hypothesis)
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
⊢ degreeOf i (p * HPow.hPow (α := MvPolynomial σ R) (X i) (k + 1)) = degreeOf i p + (k + 1)
have this : p * HPow.hPow (α := MvPolynomial σ R) (X i) k ≠ 0
Tactic: 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]
-- 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
⊢ 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 * HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (X i) 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]