no goals
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.153194
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q f : MvPolynomial σ R
x : σ →₀ ℕ
H : x ∈ support f
v : σ
h : ¬v ∈ vars f
⊢ ↑x v = 0
classical
rw [vars_def, Multiset.mem_toFinset] at h
rw [← Finsupp.not_mem_support_iff]
contrapose! h
rw [degrees_def]
rw [show f.support = insert x f.support from Eq.symm <| Finset.insert_eq_of_mem H]
rw [Finset.sup_insert]
simp only [Multiset.mem_union, Multiset.sup_eq_union]
left
rwa [← toFinset_toMultiset, Multiset.mem_toFinset] at h
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.153194
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q f : MvPolynomial σ R
x : σ →₀ ℕ
H : x ∈ support f
v : σ
h✝ : ¬v ∈ vars f
h : ¬v ∈ degrees f
⊢ ↑x v = 0
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.153194
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q f : MvPolynomial σ R
x : σ →₀ ℕ
H : x ∈ support f
v : σ
h : ¬v ∈ vars f
⊢ ↑x v = 0
rw [vars_def, Multiset.mem_toFinset] at h
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.153194
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q f : MvPolynomial σ R
x : σ →₀ ℕ
H : x ∈ support f
v : σ
h✝ : ¬v ∈ vars f
h : ¬v ∈ degrees f
⊢ ¬v ∈ x.support
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.153194
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q f : MvPolynomial σ R
x : σ →₀ ℕ
H : x ∈ support f
v : σ
h✝ : ¬v ∈ vars f
h : ¬v ∈ degrees f
⊢ ↑x v = 0
rw [← Finsupp.not_mem_support_iff]
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.153194
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q f : MvPolynomial σ R
x : σ →₀ ℕ
H : x ∈ support f
v : σ
h✝ : ¬v ∈ vars f
h : v ∈ x.support
⊢ v ∈ degrees f
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.153194
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q f : MvPolynomial σ R
x : σ →₀ ℕ
H : x ∈ support f
v : σ
h✝ : ¬v ∈ vars f
h : ¬v ∈ degrees f
⊢ ¬v ∈ x.support
contrapose! h
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.153194
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q f : MvPolynomial σ R
x : σ →₀ ℕ
H : x ∈ support f
v : σ
h✝ : ¬v ∈ vars f
h : v ∈ x.support
⊢ v ∈ Finset.sup (support f) fun s => ↑toMultiset s
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.153194
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q f : MvPolynomial σ R
x : σ →₀ ℕ
H : x ∈ support f
v : σ
h✝ : ¬v ∈ vars f
h : v ∈ x.support
⊢ v ∈ degrees f
rw [degrees_def]
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.153194
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q f : MvPolynomial σ R
x : σ →₀ ℕ
H : x ∈ support f
v : σ
h✝ : ¬v ∈ vars f
h : v ∈ x.support
⊢ v ∈ Finset.sup (insert x (support f)) fun s => ↑toMultiset s
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.153194
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q f : MvPolynomial σ R
x : σ →₀ ℕ
H : x ∈ support f
v : σ
h✝ : ¬v ∈ vars f
h : v ∈ x.support
⊢ v ∈ Finset.sup (support f) fun s => ↑toMultiset s
rw [show f.support = insert x f.support from Eq.symm <| Finset.insert_eq_of_mem H]
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.153194
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q f : MvPolynomial σ R
x : σ →₀ ℕ
H : x ∈ support f
v : σ
h✝ : ¬v ∈ vars f
h : v ∈ x.support
⊢ v ∈ ↑toMultiset x ⊔ Finset.sup (support f) fun s => ↑toMultiset s
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.153194
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q f : MvPolynomial σ R
x : σ →₀ ℕ
H : x ∈ support f
v : σ
h✝ : ¬v ∈ vars f
h : v ∈ x.support
⊢ v ∈ Finset.sup (insert x (support f)) fun s => ↑toMultiset s
rw [Finset.sup_insert]
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.153194
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q f : MvPolynomial σ R
x : σ →₀ ℕ
H : x ∈ support f
v : σ
h✝ : ¬v ∈ vars f
h : v ∈ x.support
⊢ v ∈ ↑toMultiset x ∨ v ∈ Finset.sup (support f) fun s => ↑toMultiset s
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.153194
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q f : MvPolynomial σ R
x : σ →₀ ℕ
H : x ∈ support f
v : σ
h✝ : ¬v ∈ vars f
h : v ∈ x.support
⊢ v ∈ ↑toMultiset x ⊔ Finset.sup (support f) fun s => ↑toMultiset s
simp only [Multiset.mem_union, Multiset.sup_eq_union]
case h
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.153194
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q f : MvPolynomial σ R
x : σ →₀ ℕ
H : x ∈ support f
v : σ
h✝ : ¬v ∈ vars f
h : v ∈ x.support
⊢ v ∈ ↑toMultiset x
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.153194
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q f : MvPolynomial σ R
x : σ →₀ ℕ
H : x ∈ support f
v : σ
h✝ : ¬v ∈ vars f
h : v ∈ x.support
⊢ v ∈ ↑toMultiset x ∨ v ∈ Finset.sup (support f) fun s => ↑toMultiset s
left
no goals
case h
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.153194
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q f : MvPolynomial σ R
x : σ →₀ ℕ
H : x ∈ support f
v : σ
h✝ : ¬v ∈ vars f
h : v ∈ x.support
⊢ v ∈ ↑toMultiset x
rwa [← toFinset_toMultiset, Multiset.mem_toFinset] at h