case a
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.45634
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : Multiset.Disjoint (degrees p) (degrees q)
⊢ ∀ (b : σ →₀ ℕ), b ∈ support p → ↑toMultiset b ≤ degrees (p + q)
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.45634
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : Multiset.Disjoint (degrees p) (degrees q)
⊢ degrees p ≤ degrees (p + q)
apply Finset.sup_le
case a
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.45634
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : Multiset.Disjoint (degrees p) (degrees q)
d : σ →₀ ℕ
hd : d ∈ support p
⊢ ↑toMultiset d ≤ degrees (p + q)
case a
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.45634
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : Multiset.Disjoint (degrees p) (degrees q)
⊢ ∀ (b : σ →₀ ℕ), b ∈ support p → ↑toMultiset b ≤ degrees (p + q)
intro d hd
case a
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.45634
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : ∀ (a : σ), a ∈ degrees p → ∀ (b : σ), b ∈ degrees q → a ≠ b
d : σ →₀ ℕ
hd : d ∈ support p
⊢ ↑toMultiset d ≤ degrees (p + q)
case a
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.45634
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : Multiset.Disjoint (degrees p) (degrees q)
d : σ →₀ ℕ
hd : d ∈ support p
⊢ ↑toMultiset d ≤ degrees (p + q)
rw [Multiset.disjoint_iff_ne] at h
case a
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.45634
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : ∀ (a : σ), a ∈ degrees p → ∀ (b : σ), b ∈ degrees q → a ≠ b
d : σ →₀ ℕ
hd : d ∈ support p
⊢ ∀ (a : σ), Multiset.count a (↑toMultiset d) ≤ Multiset.count a (degrees (p + q))
case a
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.45634
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : ∀ (a : σ), a ∈ degrees p → ∀ (b : σ), b ∈ degrees q → a ≠ b
d : σ →₀ ℕ
hd : d ∈ support p
⊢ ↑toMultiset d ≤ degrees (p + q)
rw [Multiset.le_iff_count]
case a
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.45634
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : ∀ (a : σ), a ∈ degrees p → ∀ (b : σ), b ∈ degrees q → a ≠ b
d : σ →₀ ℕ
hd : d ∈ support p
i : σ
⊢ Multiset.count i (↑toMultiset d) ≤ Multiset.count i (degrees (p + q))
case a
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.45634
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : ∀ (a : σ), a ∈ degrees p → ∀ (b : σ), b ∈ degrees q → a ≠ b
d : σ →₀ ℕ
hd : d ∈ support p
⊢ ∀ (a : σ), Multiset.count a (↑toMultiset d) ≤ Multiset.count a (degrees (p + q))
intro i
case a
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.45634
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : ∀ (a : σ), a ∈ degrees p → ∀ (b : σ), b ∈ degrees q → a ≠ b
d : σ →₀ ℕ
hd : d ∈ support p
i : σ
⊢ Multiset.count i (↑toMultiset d) ≤ Finset.sup (support (p + q)) fun a => Multiset.count i (↑toMultiset a)
case a
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.45634
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : ∀ (a : σ), a ∈ degrees p → ∀ (b : σ), b ∈ degrees q → a ≠ b
d : σ →₀ ℕ
hd : d ∈ support p
i : σ
⊢ Multiset.count i (↑toMultiset d) ≤ Multiset.count i (degrees (p + q))
rw [degrees, Multiset.count_finset_sup]
case a
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.45634
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : ∀ (a : σ), a ∈ degrees p → ∀ (b : σ), b ∈ degrees q → a ≠ b
d : σ →₀ ℕ
hd : d ∈ support p
i : σ
⊢ ↑d i ≤ Finset.sup (support (p + q)) fun a => ↑a i
case a
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.45634
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : ∀ (a : σ), a ∈ degrees p → ∀ (b : σ), b ∈ degrees q → a ≠ b
d : σ →₀ ℕ
hd : d ∈ support p
i : σ
⊢ Multiset.count i (↑toMultiset d) ≤ Finset.sup (support (p + q)) fun a => Multiset.count i (↑toMultiset a)
simp only [Finsupp.count_toMultiset]
case pos
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.45634
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : ∀ (a : σ), a ∈ degrees p → ∀ (b : σ), b ∈ degrees q → a ≠ b
d : σ →₀ ℕ
hd : d ∈ support p
i : σ
h0 : d = 0
⊢ ↑d i ≤ Finset.sup (support (p + q)) fun a => ↑a i

case neg
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.45634
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : ∀ (a : σ), a ∈ degrees p → ∀ (b : σ), b ∈ degrees q → a ≠ b
d : σ →₀ ℕ
hd : d ∈ support p
i : σ
h0 : ¬d = 0
⊢ ↑d i ≤ Finset.sup (support (p + q)) fun a => ↑a i
case a
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.45634
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : ∀ (a : σ), a ∈ degrees p → ∀ (b : σ), b ∈ degrees q → a ≠ b
d : σ →₀ ℕ
hd : d ∈ support p
i : σ
⊢ ↑d i ≤ Finset.sup (support (p + q)) fun a => ↑a i
by_cases h0 : d = 0
no goals
case pos
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.45634
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : ∀ (a : σ), a ∈ degrees p → ∀ (b : σ), b ∈ degrees q → a ≠ b
d : σ →₀ ℕ
hd : d ∈ support p
i : σ
h0 : d = 0
⊢ ↑d i ≤ Finset.sup (support (p + q)) fun a => ↑a i
simp only [h0, zero_le, Finsupp.zero_apply]
case neg
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.45634
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : ∀ (a : σ), a ∈ degrees p → ∀ (b : σ), b ∈ degrees q → a ≠ b
d : σ →₀ ℕ
hd : d ∈ support p
i : σ
h0 : ¬d = 0
⊢ d ∈ support (p + q)
case neg
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.45634
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : ∀ (a : σ), a ∈ degrees p → ∀ (b : σ), b ∈ degrees q → a ≠ b
d : σ →₀ ℕ
hd : d ∈ support p
i : σ
h0 : ¬d = 0
⊢ ↑d i ≤ Finset.sup (support (p + q)) fun a => ↑a i
refine' @Finset.le_sup _ _ _ _ (p + q).support (fun a => a i) d _
case neg
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.45634
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : ∀ (a : σ), a ∈ degrees p → ∀ (b : σ), b ∈ degrees q → a ≠ b
d : σ →₀ ℕ
hd : d ∈ support p
i : σ
h0 : ¬d = 0
⊢ coeff d p + coeff d q ≠ 0
case neg
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.45634
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : ∀ (a : σ), a ∈ degrees p → ∀ (b : σ), b ∈ degrees q → a ≠ b
d : σ →₀ ℕ
hd : d ∈ support p
i : σ
h0 : ¬d = 0
⊢ d ∈ support (p + q)
rw [mem_support_iff, coeff_add]
case neg
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.45634
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : ∀ (a : σ), a ∈ degrees p → ∀ (b : σ), b ∈ degrees q → a ≠ b
d : σ →₀ ℕ
hd : d ∈ support p
i : σ
h0 : ¬d = 0
⊢ coeff d q = 0
case neg
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.45634
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : ∀ (a : σ), a ∈ degrees p → ∀ (b : σ), b ∈ degrees q → a ≠ b
d : σ →₀ ℕ
hd : d ∈ support p
i : σ
h0 : ¬d = 0
⊢ coeff d p + coeff d q ≠ 0
suffices q.coeff d = 0 by rwa [this, add_zero, coeff, ← Finsupp.mem_support_iff]
case neg
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.45634
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : ∀ (a : σ), a ∈ degrees p → ∀ (b : σ), b ∈ degrees q → a ≠ b
d : σ →₀ ℕ
hd : d ∈ support p
i : σ
h0 : Finset.Nonempty d.support
⊢ coeff d q = 0
case neg
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.45634
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : ∀ (a : σ), a ∈ degrees p → ∀ (b : σ), b ∈ degrees q → a ≠ b
d : σ →₀ ℕ
hd : d ∈ support p
i : σ
h0 : ¬d = 0
⊢ coeff d q = 0
rw [← Finsupp.support_eq_empty, ← Ne.def, ← Finset.nonempty_iff_ne_empty] at h0
case neg.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.45634
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : ∀ (a : σ), a ∈ degrees p → ∀ (b : σ), b ∈ degrees q → a ≠ b
d : σ →₀ ℕ
hd : d ∈ support p
i j : σ
hj : j ∈ d.support
⊢ coeff d q = 0
case neg
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.45634
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : ∀ (a : σ), a ∈ degrees p → ∀ (b : σ), b ∈ degrees q → a ≠ b
d : σ →₀ ℕ
hd : d ∈ support p
i : σ
h0 : Finset.Nonempty d.support
⊢ coeff d q = 0
obtain ⟨j, hj⟩ := h0
case neg.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.45634
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
d : σ →₀ ℕ
hd : d ∈ support p
i j : σ
hj : j ∈ d.support
h : coeff d q ≠ 0
⊢ ∃ a, a ∈ degrees p ∧ ∃ b, b ∈ degrees q ∧ a = b
case neg.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.45634
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : ∀ (a : σ), a ∈ degrees p → ∀ (b : σ), b ∈ degrees q → a ≠ b
d : σ →₀ ℕ
hd : d ∈ support p
i j : σ
hj : j ∈ d.support
⊢ coeff d q = 0
contrapose! h
case neg.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.45634
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
d : σ →₀ ℕ
hd : coeff d p ≠ 0
i j : σ
hj : j ∈ d.support
h : coeff d q ≠ 0
⊢ ∃ a, a ∈ degrees p ∧ ∃ b, b ∈ degrees q ∧ a = b
case neg.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.45634
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
d : σ →₀ ℕ
hd : d ∈ support p
i j : σ
hj : j ∈ d.support
h : coeff d q ≠ 0
⊢ ∃ a, a ∈ degrees p ∧ ∃ b, b ∈ degrees q ∧ a = b
rw [mem_support_iff] at hd
case neg.intro.refine'_1
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.45634
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
d : σ →₀ ℕ
hd : coeff d p ≠ 0
i j : σ
hj : j ∈ d.support
h : coeff d q ≠ 0
⊢ j ∈ degrees p

case neg.intro.refine'_2
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.45634
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
d : σ →₀ ℕ
hd : coeff d p ≠ 0
i j : σ
hj : j ∈ d.support
h : coeff d q ≠ 0
⊢ j ∈ degrees q
case neg.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.45634
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
d : σ →₀ ℕ
hd : coeff d p ≠ 0
i j : σ
hj : j ∈ d.support
h : coeff d q ≠ 0
⊢ ∃ a, a ∈ degrees p ∧ ∃ b, b ∈ degrees q ∧ a = b
refine' ⟨j, _, j, _, rfl⟩
no goals
case neg.intro.refine'_1
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.45634
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
d : σ →₀ ℕ
hd : coeff d p ≠ 0
i j : σ
hj : j ∈ d.support
h : coeff d q ≠ 0
⊢ j ∈ degrees p

case neg.intro.refine'_2
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.45634
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
d : σ →₀ ℕ
hd : coeff d p ≠ 0
i j : σ
hj : j ∈ d.support
h : coeff d q ≠ 0
⊢ j ∈ degrees q
all_goals rw [mem_degrees]; refine' ⟨d, _, hj⟩; assumption
no goals
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.45634
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
h : ∀ (a : σ), a ∈ degrees p → ∀ (b : σ), b ∈ degrees q → a ≠ b
d : σ →₀ ℕ
hd : d ∈ support p
i : σ
h0 : ¬d = 0
this : coeff d q = 0
⊢ coeff d p + coeff d q ≠ 0
rwa [this, add_zero, coeff, ← Finsupp.mem_support_iff]
case neg.intro.refine'_2
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.45634
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
d : σ →₀ ℕ
hd : coeff d p ≠ 0
i j : σ
hj : j ∈ d.support
h : coeff d q ≠ 0
⊢ ∃ d, coeff d q ≠ 0 ∧ j ∈ d.support
case neg.intro.refine'_2
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.45634
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
d : σ →₀ ℕ
hd : coeff d p ≠ 0
i j : σ
hj : j ∈ d.support
h : coeff d q ≠ 0
⊢ j ∈ degrees q
rw [mem_degrees]
case neg.intro.refine'_2
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.45634
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
d : σ →₀ ℕ
hd : coeff d p ≠ 0
i j : σ
hj : j ∈ d.support
h : coeff d q ≠ 0
⊢ coeff d q ≠ 0
case neg.intro.refine'_2
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.45634
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
d : σ →₀ ℕ
hd : coeff d p ≠ 0
i j : σ
hj : j ∈ d.support
h : coeff d q ≠ 0
⊢ ∃ d, coeff d q ≠ 0 ∧ j ∈ d.support
refine' ⟨d, _, hj⟩
no goals
case neg.intro.refine'_2
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.45634
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q✝ p q : MvPolynomial σ R
d : σ →₀ ℕ
hd : coeff d p ≠ 0
i j : σ
hj : j ∈ d.support
h : coeff d q ≠ 0
⊢ coeff d q ≠ 0
assumption