R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.397208
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q a b : MvPolynomial σ R
n : σ →₀ ℕ
hn : n ∈ support (a + b)
this : n ∈ a.support ∪ b.support
⊢ (sum n fun x e => e) ≤ max (totalDegree a) (totalDegree b)
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.397208
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) ≤ max (totalDegree a) (totalDegree b)
have := Finsupp.support_add hn
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.397208
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q a b : MvPolynomial σ R
n : σ →₀ ℕ
hn : n ∈ support (a + b)
this : n ∈ a.support ∨ n ∈ b.support
⊢ (sum n fun x e => e) ≤ max (totalDegree a) (totalDegree b)
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.397208
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q a b : MvPolynomial σ R
n : σ →₀ ℕ
hn : n ∈ support (a + b)
this : n ∈ a.support ∪ b.support
⊢ (sum n fun x e => e) ≤ max (totalDegree a) (totalDegree b)
rw [Finset.mem_union] at this
case inl
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.397208
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q a b : MvPolynomial σ R
n : σ →₀ ℕ
hn : n ∈ support (a + b)
h : n ∈ a.support
⊢ (sum n fun x e => e) ≤ max (totalDegree a) (totalDegree b)

case inr
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.397208
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q a b : MvPolynomial σ R
n : σ →₀ ℕ
hn : n ∈ support (a + b)
h : n ∈ b.support
⊢ (sum n fun x e => e) ≤ max (totalDegree a) (totalDegree b)
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.397208
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q a b : MvPolynomial σ R
n : σ →₀ ℕ
hn : n ∈ support (a + b)
this : n ∈ a.support ∨ n ∈ b.support
⊢ (sum n fun x e => e) ≤ max (totalDegree a) (totalDegree b)
cases' this with h h
no goals
case inl
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.397208
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q a b : MvPolynomial σ R
n : σ →₀ ℕ
hn : n ∈ support (a + b)
h : n ∈ a.support
⊢ (sum n fun x e => e) ≤ max (totalDegree a) (totalDegree b)
exact le_max_of_le_left (le_totalDegree h)
no goals
case inr
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.397208
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q a b : MvPolynomial σ R
n : σ →₀ ℕ
hn : n ∈ support (a + b)
h : n ∈ b.support
⊢ (sum n fun x e => e) ≤ max (totalDegree a) (totalDegree b)
exact le_max_of_le_right (le_totalDegree h)