R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.449883
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q a b : MvPolynomial σ R
n : σ →₀ ℕ
hn : n ∈ support (a * b)
this : n ∈ Finset.biUnion a.support fun a₁ => Finset.biUnion b.support fun a₂ => {a₁ + a₂}
⊢ (sum n fun x e => e) ≤ totalDegree a + totalDegree b
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.449883
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q a b : MvPolynomial σ R
n : σ →₀ ℕ
hn : n ∈ support (a * b)
⊢ (sum n fun x e => e) ≤ totalDegree a + totalDegree b
have := AddMonoidAlgebra.support_mul a b hn
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.449883
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q a b : MvPolynomial σ R
n : σ →₀ ℕ
hn : n ∈ support (a * b)
this : ∃ a_1, a_1 ∈ a.support ∧ ∃ a, a ∈ b.support ∧ n = a_1 + a
⊢ (sum n fun x e => e) ≤ totalDegree a + totalDegree b
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.449883
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q a b : MvPolynomial σ R
n : σ →₀ ℕ
hn : n ∈ support (a * b)
this : n ∈ Finset.biUnion a.support fun a₁ => Finset.biUnion b.support fun a₂ => {a₁ + a₂}
⊢ (sum n fun x e => e) ≤ totalDegree a + totalDegree b
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.449883
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q a b : MvPolynomial σ R
a₁ : σ →₀ ℕ
h₁ : a₁ ∈ a.support
a₂ : σ →₀ ℕ
h₂ : a₂ ∈ b.support
hn : a₁ + a₂ ∈ support (a * b)
⊢ (sum (a₁ + a₂) fun x e => e) ≤ totalDegree a + totalDegree b
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.449883
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q a b : MvPolynomial σ R
n : σ →₀ ℕ
hn : n ∈ support (a * b)
this : ∃ a_1, a_1 ∈ a.support ∧ ∃ a, a ∈ b.support ∧ n = a_1 + a
⊢ (sum n fun x e => e) ≤ totalDegree a + totalDegree b
rcases this with ⟨a₁, h₁, a₂, h₂, rfl⟩
case intro.intro.intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.449883
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q a b : MvPolynomial σ R
a₁ : σ →₀ ℕ
h₁ : a₁ ∈ a.support
a₂ : σ →₀ ℕ
h₂ : a₂ ∈ b.support
hn : a₁ + a₂ ∈ support (a * b)
⊢ ((sum a₁ fun x e => e) + sum a₂ fun x e => e) ≤ totalDegree a + totalDegree b

case intro.intro.intro.intro.h_zero
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.449883
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q a b : MvPolynomial σ R
a₁ : σ →₀ ℕ
h₁ : a₁ ∈ a.support
a₂ : σ →₀ ℕ
h₂ : a₂ ∈ b.support
hn : a₁ + a₂ ∈ support (a * b)
⊢ σ → 0 = 0

case intro.intro.intro.intro.h_add
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.449883
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q a b : MvPolynomial σ R
a₁ : σ →₀ ℕ
h₁ : a₁ ∈ a.support
a₂ : σ →₀ ℕ
h₂ : a₂ ∈ b.support
hn : a₁ + a₂ ∈ support (a * b)
⊢ σ → ∀ (b₁ b₂ : ℕ), b₁ + b₂ = b₁ + b₂
case intro.intro.intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.449883
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q a b : MvPolynomial σ R
a₁ : σ →₀ ℕ
h₁ : a₁ ∈ a.support
a₂ : σ →₀ ℕ
h₂ : a₂ ∈ b.support
hn : a₁ + a₂ ∈ support (a * b)
⊢ (sum (a₁ + a₂) fun x e => e) ≤ totalDegree a + totalDegree b
rw [Finsupp.sum_add_index']
case intro.intro.intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.449883
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q a b : MvPolynomial σ R
a₁ : σ →₀ ℕ
h₁ : a₁ ∈ a.support
a₂ : σ →₀ ℕ
h₂ : a₂ ∈ b.support
hn : a₁ + a₂ ∈ support (a * b)
⊢ ((sum a₁ fun x e => e) + sum a₂ fun x e => e) ≤
    (Finset.sup (support a) fun s => sum s fun x e => e) + Finset.sup (support b) fun s => sum s fun x e => e
case intro.intro.intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.449883
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q a b : MvPolynomial σ R
a₁ : σ →₀ ℕ
h₁ : a₁ ∈ a.support
a₂ : σ →₀ ℕ
h₂ : a₂ ∈ b.support
hn : a₁ + a₂ ∈ support (a * b)
⊢ ((sum a₁ fun x e => e) + sum a₂ fun x e => e) ≤ totalDegree a + totalDegree b
dsimp [totalDegree]
no goals
case intro.intro.intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.449883
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q a b : MvPolynomial σ R
a₁ : σ →₀ ℕ
h₁ : a₁ ∈ a.support
a₂ : σ →₀ ℕ
h₂ : a₂ ∈ b.support
hn : a₁ + a₂ ∈ support (a * b)
⊢ ((sum a₁ fun x e => e) + sum a₂ fun x e => e) ≤
    (Finset.sup (support a) fun s => sum s fun x e => e) + Finset.sup (support b) fun s => sum s fun x e => e
exact add_le_add (le_totalDegree h₁) (le_totalDegree h₂)
case intro.intro.intro.intro.h_zero
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.449883
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q a b : MvPolynomial σ R
a₁ : σ →₀ ℕ
h₁ : a₁ ∈ a.support
a₂ : σ →₀ ℕ
h₂ : a₂ ∈ b.support
hn : a₁ + a₂ ∈ support (a * b)
a✝ : σ
⊢ 0 = 0
case intro.intro.intro.intro.h_zero
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.449883
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q a b : MvPolynomial σ R
a₁ : σ →₀ ℕ
h₁ : a₁ ∈ a.support
a₂ : σ →₀ ℕ
h₂ : a₂ ∈ b.support
hn : a₁ + a₂ ∈ support (a * b)
⊢ σ → 0 = 0
intro _
no goals
case intro.intro.intro.intro.h_zero
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.449883
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q a b : MvPolynomial σ R
a₁ : σ →₀ ℕ
h₁ : a₁ ∈ a.support
a₂ : σ →₀ ℕ
h₂ : a₂ ∈ b.support
hn : a₁ + a₂ ∈ support (a * b)
a✝ : σ
⊢ 0 = 0
rfl
case intro.intro.intro.intro.h_add
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.449883
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q a b : MvPolynomial σ R
a₁ : σ →₀ ℕ
h₁ : a₁ ∈ a.support
a₂ : σ →₀ ℕ
h₂ : a₂ ∈ b.support
hn : a₁ + a₂ ∈ support (a * b)
a✝ : σ
b₁ b₂ : ℕ
⊢ b₁ + b₂ = b₁ + b₂
case intro.intro.intro.intro.h_add
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.449883
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q a b : MvPolynomial σ R
a₁ : σ →₀ ℕ
h₁ : a₁ ∈ a.support
a₂ : σ →₀ ℕ
h₂ : a₂ ∈ b.support
hn : a₁ + a₂ ∈ support (a * b)
⊢ σ → ∀ (b₁ b₂ : ℕ), b₁ + b₂ = b₁ + b₂
intro _ b₁ b₂
no goals
case intro.intro.intro.intro.h_add
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.449883
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q a b : MvPolynomial σ R
a₁ : σ →₀ ℕ
h₁ : a₁ ∈ a.support
a₂ : σ →₀ ℕ
h₂ : a₂ ∈ b.support
hn : a₁ + a₂ ∈ support (a * b)
a✝ : σ
b₁ b₂ : ℕ
⊢ b₁ + b₂ = b₁ + b₂
rfl