no goals
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.36638
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
⊢ degrees (p * q) ≤ degrees p + degrees q
classical
refine' Finset.sup_le fun b hb => _
have := support_mul p q hb
simp only [Finset.mem_biUnion, Finset.mem_singleton] at this
rcases this with ⟨a₁, h₁, a₂, h₂, rfl⟩
rw [Finsupp.toMultiset_add]
exact add_le_add (Finset.le_sup h₁) (Finset.le_sup h₂)
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.36638
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
b : σ →₀ ℕ
hb : b ∈ support (p * q)
⊢ ↑toMultiset b ≤ degrees p + degrees q
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.36638
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
⊢ degrees (p * q) ≤ degrees p + degrees q
refine' Finset.sup_le fun b hb => _
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.36638
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
b : σ →₀ ℕ
hb : b ∈ support (p * q)
this : b ∈ Finset.biUnion (support p) fun a => Finset.biUnion (support q) fun b => {a + b}
⊢ ↑toMultiset b ≤ degrees p + degrees q
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.36638
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
b : σ →₀ ℕ
hb : b ∈ support (p * q)
⊢ ↑toMultiset b ≤ degrees p + degrees q
have := support_mul p q hb
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.36638
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
b : σ →₀ ℕ
hb : b ∈ support (p * q)
this : ∃ a, a ∈ support p ∧ ∃ a_1, a_1 ∈ support q ∧ b = a + a_1
⊢ ↑toMultiset b ≤ degrees p + degrees q
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.36638
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
b : σ →₀ ℕ
hb : b ∈ support (p * q)
this : b ∈ Finset.biUnion (support p) fun a => Finset.biUnion (support q) fun b => {a + b}
⊢ ↑toMultiset b ≤ degrees p + degrees q
simp only [Finset.mem_biUnion, Finset.mem_singleton] at this
case intro.intro.intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.36638
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
a₁ : σ →₀ ℕ
h₁ : a₁ ∈ support p
a₂ : σ →₀ ℕ
h₂ : a₂ ∈ support q
hb : a₁ + a₂ ∈ support (p * q)
⊢ ↑toMultiset (a₁ + a₂) ≤ degrees p + degrees q
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.36638
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
b : σ →₀ ℕ
hb : b ∈ support (p * q)
this : ∃ a, a ∈ support p ∧ ∃ a_1, a_1 ∈ support q ∧ b = a + a_1
⊢ ↑toMultiset b ≤ degrees p + degrees q
rcases this with ⟨a₁, h₁, a₂, h₂, rfl⟩
case intro.intro.intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.36638
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
a₁ : σ →₀ ℕ
h₁ : a₁ ∈ support p
a₂ : σ →₀ ℕ
h₂ : a₂ ∈ support q
hb : a₁ + a₂ ∈ support (p * q)
⊢ ↑toMultiset a₁ + ↑toMultiset a₂ ≤ degrees p + degrees q
case intro.intro.intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.36638
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
a₁ : σ →₀ ℕ
h₁ : a₁ ∈ support p
a₂ : σ →₀ ℕ
h₂ : a₂ ∈ support q
hb : a₁ + a₂ ∈ support (p * q)
⊢ ↑toMultiset (a₁ + a₂) ≤ degrees p + degrees q
rw [Finsupp.toMultiset_add]
no goals
case intro.intro.intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.36638
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
a₁ : σ →₀ ℕ
h₁ : a₁ ∈ support p
a₂ : σ →₀ ℕ
h₂ : a₂ ∈ support q
hb : a₁ + a₂ ∈ support (p * q)
⊢ ↑toMultiset a₁ + ↑toMultiset a₂ ≤ degrees p + degrees q
exact add_le_add (Finset.le_sup h₁) (Finset.le_sup h₂)