case a
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.399378
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : totalDegree q < totalDegree p
⊢ totalDegree (p + q) ≤ totalDegree p

case a
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.399378
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : totalDegree q < totalDegree p
⊢ totalDegree p ≤ totalDegree (p + q)
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.399378
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : totalDegree q < totalDegree p
⊢ totalDegree (p + q) = totalDegree p
apply le_antisymm
case pos
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.399378
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : totalDegree q < totalDegree p
hp : p = 0
⊢ totalDegree p ≤ totalDegree (p + q)

case neg
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.399378
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : totalDegree q < totalDegree p
hp : ¬p = 0
⊢ totalDegree p ≤ totalDegree (p + q)
case a
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.399378
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : totalDegree q < totalDegree p
⊢ totalDegree p ≤ totalDegree (p + q)
by_cases hp : p = 0
case neg.intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.399378
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : totalDegree q < totalDegree p
hp : ¬p = 0
b : σ →₀ ℕ
hb₁ : b ∈ support p
hb₂ : (Finset.sup (support p) fun m => ↑Multiset.card (↑toMultiset m)) = ↑Multiset.card (↑toMultiset b)
⊢ totalDegree p ≤ totalDegree (p + q)
case neg
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.399378
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : totalDegree q < totalDegree p
hp : ¬p = 0
⊢ totalDegree p ≤ totalDegree (p + q)
obtain ⟨b, hb₁, hb₂⟩ :=
  p.support.exists_mem_eq_sup (Finsupp.support_nonempty_iff.mpr hp) fun m : σ →₀ ℕ =>
    Multiset.card (toMultiset m)
case neg.intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.399378
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : totalDegree q < totalDegree p
hp : ¬p = 0
b : σ →₀ ℕ
hb₁ : b ∈ support p
hb₂ : (Finset.sup (support p) fun m => ↑Multiset.card (↑toMultiset m)) = ↑Multiset.card (↑toMultiset b)
hb : ¬b ∈ support q
⊢ totalDegree p ≤ totalDegree (p + q)
case neg.intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.399378
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : totalDegree q < totalDegree p
hp : ¬p = 0
b : σ →₀ ℕ
hb₁ : b ∈ support p
hb₂ : (Finset.sup (support p) fun m => ↑Multiset.card (↑toMultiset m)) = ↑Multiset.card (↑toMultiset b)
⊢ totalDegree p ≤ totalDegree (p + q)
have hb : ¬b ∈ q.support := by
  contrapose! h
  rw [totalDegree_eq p, hb₂, totalDegree_eq]
  apply Finset.le_sup h
case neg.intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.399378
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : totalDegree q < totalDegree p
hp : ¬p = 0
b : σ →₀ ℕ
hb₁ : b ∈ support p
hb₂ : (Finset.sup (support p) fun m => ↑Multiset.card (↑toMultiset m)) = ↑Multiset.card (↑toMultiset b)
hb : ¬b ∈ support q
hbb : b ∈ support (p + q)
⊢ totalDegree p ≤ totalDegree (p + q)
case neg.intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.399378
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : totalDegree q < totalDegree p
hp : ¬p = 0
b : σ →₀ ℕ
hb₁ : b ∈ support p
hb₂ : (Finset.sup (support p) fun m => ↑Multiset.card (↑toMultiset m)) = ↑Multiset.card (↑toMultiset b)
hb : ¬b ∈ support q
⊢ totalDegree p ≤ totalDegree (p + q)
have hbb : b ∈ (p + q).support := by
  apply support_sdiff_support_subset_support_add
  rw [Finset.mem_sdiff]
  exact ⟨hb₁, hb⟩
case neg.intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.399378
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : totalDegree q < totalDegree p
hp : ¬p = 0
b : σ →₀ ℕ
hb₁ : b ∈ support p
hb₂ : (Finset.sup (support p) fun m => ↑Multiset.card (↑toMultiset m)) = ↑Multiset.card (↑toMultiset b)
hb : ¬b ∈ support q
hbb : b ∈ support (p + q)
⊢ ↑Multiset.card (↑toMultiset b) ≤ Finset.sup (support (p + q)) fun m => ↑Multiset.card (↑toMultiset m)
case neg.intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.399378
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : totalDegree q < totalDegree p
hp : ¬p = 0
b : σ →₀ ℕ
hb₁ : b ∈ support p
hb₂ : (Finset.sup (support p) fun m => ↑Multiset.card (↑toMultiset m)) = ↑Multiset.card (↑toMultiset b)
hb : ¬b ∈ support q
hbb : b ∈ support (p + q)
⊢ totalDegree p ≤ totalDegree (p + q)
rw [totalDegree_eq, hb₂, totalDegree_eq]
no goals
case neg.intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.399378
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : totalDegree q < totalDegree p
hp : ¬p = 0
b : σ →₀ ℕ
hb₁ : b ∈ support p
hb₂ : (Finset.sup (support p) fun m => ↑Multiset.card (↑toMultiset m)) = ↑Multiset.card (↑toMultiset b)
hb : ¬b ∈ support q
hbb : b ∈ support (p + q)
⊢ ↑Multiset.card (↑toMultiset b) ≤ Finset.sup (support (p + q)) fun m => ↑Multiset.card (↑toMultiset m)
exact Finset.le_sup (f := fun m => Multiset.card (Finsupp.toMultiset m)) hbb
case a
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.399378
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : totalDegree q < totalDegree p
⊢ totalDegree (p + q) ≤ max (totalDegree p) (totalDegree q)
case a
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.399378
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : totalDegree q < totalDegree p
⊢ totalDegree (p + q) ≤ totalDegree p
rw [← max_eq_left_of_lt h]
no goals
case a
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.399378
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : totalDegree q < totalDegree p
⊢ totalDegree (p + q) ≤ max (totalDegree p) (totalDegree q)
exact totalDegree_add p q
no goals
case pos
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.399378
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : totalDegree q < totalDegree p
hp : p = 0
⊢ totalDegree p ≤ totalDegree (p + q)
simp [hp]
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.399378
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
hp : ¬p = 0
b : σ →₀ ℕ
hb₁ : b ∈ support p
hb₂ : (Finset.sup (support p) fun m => ↑Multiset.card (↑toMultiset m)) = ↑Multiset.card (↑toMultiset b)
h : b ∈ support q
⊢ totalDegree p ≤ totalDegree q
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.399378
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : totalDegree q < totalDegree p
hp : ¬p = 0
b : σ →₀ ℕ
hb₁ : b ∈ support p
hb₂ : (Finset.sup (support p) fun m => ↑Multiset.card (↑toMultiset m)) = ↑Multiset.card (↑toMultiset b)
⊢ ¬b ∈ support q
contrapose! h
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.399378
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
hp : ¬p = 0
b : σ →₀ ℕ
hb₁ : b ∈ support p
hb₂ : (Finset.sup (support p) fun m => ↑Multiset.card (↑toMultiset m)) = ↑Multiset.card (↑toMultiset b)
h : b ∈ support q
⊢ ↑Multiset.card (↑toMultiset b) ≤ Finset.sup (support q) fun m => ↑Multiset.card (↑toMultiset m)
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.399378
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
hp : ¬p = 0
b : σ →₀ ℕ
hb₁ : b ∈ support p
hb₂ : (Finset.sup (support p) fun m => ↑Multiset.card (↑toMultiset m)) = ↑Multiset.card (↑toMultiset b)
h : b ∈ support q
⊢ totalDegree p ≤ totalDegree q
rw [totalDegree_eq p, hb₂, totalDegree_eq]
no goals
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.399378
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
hp : ¬p = 0
b : σ →₀ ℕ
hb₁ : b ∈ support p
hb₂ : (Finset.sup (support p) fun m => ↑Multiset.card (↑toMultiset m)) = ↑Multiset.card (↑toMultiset b)
h : b ∈ support q
⊢ ↑Multiset.card (↑toMultiset b) ≤ Finset.sup (support q) fun m => ↑Multiset.card (↑toMultiset m)
apply Finset.le_sup h
case a
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.399378
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : totalDegree q < totalDegree p
hp : ¬p = 0
b : σ →₀ ℕ
hb₁ : b ∈ support p
hb₂ : (Finset.sup (support p) fun m => ↑Multiset.card (↑toMultiset m)) = ↑Multiset.card (↑toMultiset b)
hb : ¬b ∈ support q
⊢ b ∈ support p \ support q
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.399378
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : totalDegree q < totalDegree p
hp : ¬p = 0
b : σ →₀ ℕ
hb₁ : b ∈ support p
hb₂ : (Finset.sup (support p) fun m => ↑Multiset.card (↑toMultiset m)) = ↑Multiset.card (↑toMultiset b)
hb : ¬b ∈ support q
⊢ b ∈ support (p + q)
apply support_sdiff_support_subset_support_add
case a
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.399378
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : totalDegree q < totalDegree p
hp : ¬p = 0
b : σ →₀ ℕ
hb₁ : b ∈ support p
hb₂ : (Finset.sup (support p) fun m => ↑Multiset.card (↑toMultiset m)) = ↑Multiset.card (↑toMultiset b)
hb : ¬b ∈ support q
⊢ b ∈ support p ∧ ¬b ∈ support q
case a
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.399378
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : totalDegree q < totalDegree p
hp : ¬p = 0
b : σ →₀ ℕ
hb₁ : b ∈ support p
hb₂ : (Finset.sup (support p) fun m => ↑Multiset.card (↑toMultiset m)) = ↑Multiset.card (↑toMultiset b)
hb : ¬b ∈ support q
⊢ b ∈ support p \ support q
rw [Finset.mem_sdiff]
no goals
case a
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.399378
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : totalDegree q < totalDegree p
hp : ¬p = 0
b : σ →₀ ℕ
hb₁ : b ∈ support p
hb₂ : (Finset.sup (support p) fun m => ↑Multiset.card (↑toMultiset m)) = ↑Multiset.card (↑toMultiset b)
hb : ¬b ∈ support q
⊢ b ∈ support p ∧ ¬b ∈ support q
exact ⟨hb₁, hb⟩