no goals
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.318009
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
j : σ
f : MvPolynomial σ R
⊢ degreeOf j (f * X j) ≤ degreeOf j f + 1
classical
repeat' rw [degreeOf]
apply (Multiset.count_le_of_le j (degrees_mul f (X j))).trans
simp only [Multiset.count_add, add_le_add_iff_left]
convert Multiset.count_le_of_le j (degrees_X' (R:=R) j)
rw [Multiset.count_singleton_self]
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.318009
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
j : σ
f : MvPolynomial σ R
⊢ Multiset.count j (degrees (f * X j)) ≤ Multiset.count j (degrees f) + 1
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.318009
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
j : σ
f : MvPolynomial σ R
⊢ degreeOf j (f * X j) ≤ degreeOf j f + 1
repeat' rw [degreeOf]
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.318009
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
j : σ
f : MvPolynomial σ R
⊢ Multiset.count j (degrees f + degrees (X j)) ≤ Multiset.count j (degrees f) + 1
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.318009
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
j : σ
f : MvPolynomial σ R
⊢ Multiset.count j (degrees (f * X j)) ≤ Multiset.count j (degrees f) + 1
apply (Multiset.count_le_of_le j (degrees_mul f (X j))).trans
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.318009
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
j : σ
f : MvPolynomial σ R
⊢ Multiset.count j (degrees (X j)) ≤ 1
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.318009
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
j : σ
f : MvPolynomial σ R
⊢ Multiset.count j (degrees f + degrees (X j)) ≤ Multiset.count j (degrees f) + 1
simp only [Multiset.count_add, add_le_add_iff_left]
case h.e'_4
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.318009
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
j : σ
f : MvPolynomial σ R
⊢ 1 = Multiset.count j {j}
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.318009
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
j : σ
f : MvPolynomial σ R
⊢ Multiset.count j (degrees (X j)) ≤ 1
convert Multiset.count_le_of_le j (degrees_X' (R:=R) j)
no goals
case h.e'_4
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.318009
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
j : σ
f : MvPolynomial σ R
⊢ 1 = Multiset.count j {j}
rw [Multiset.count_singleton_self]
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.318009
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
j : σ
f : MvPolynomial σ R
⊢ Multiset.count j (degrees (f * X j)) ≤ Multiset.count j (degrees f) + 1
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.318009
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
j : σ
f : MvPolynomial σ R
⊢ Multiset.count j (degrees (f * X j)) ≤ Multiset.count j (degrees f) + 1
rw [degreeOf]