σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : MvPolynomial σ R
s : Set (σ →₀ ℕ)
⊢ (∀ (m : σ →₀ ℕ), m ∈ x.support → ∃ m', m' ∈ s ∧ ∃ d, m = d + m') ↔
    ∀ (xi : σ →₀ ℕ), xi ∈ support x → ∃ si, si ∈ s ∧ si ≤ xi
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : MvPolynomial σ R
s : Set (σ →₀ ℕ)
⊢ x ∈ Ideal.span ((fun s => ↑(monomial s) 1) '' s) ↔ ∀ (xi : σ →₀ ℕ), xi ∈ support x → ∃ si, si ∈ s ∧ si ≤ xi
refine' AddMonoidAlgebra.mem_ideal_span_of'_image.trans _
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : MvPolynomial σ R
s : Set (σ →₀ ℕ)
⊢ (∀ (m : σ →₀ ℕ), m ∈ x.support → ∃ m', m' ∈ s ∧ ∃ d, m = m' + d) ↔
    ∀ (xi : σ →₀ ℕ), xi ∈ support x → ∃ si, si ∈ s ∧ ∃ c, xi = si + c
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : MvPolynomial σ R
s : Set (σ →₀ ℕ)
⊢ (∀ (m : σ →₀ ℕ), m ∈ x.support → ∃ m', m' ∈ s ∧ ∃ d, m = d + m') ↔
    ∀ (xi : σ →₀ ℕ), xi ∈ support x → ∃ si, si ∈ s ∧ si ≤ xi
simp_rw [le_iff_exists_add, add_comm]
no goals
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : MvPolynomial σ R
s : Set (σ →₀ ℕ)
⊢ (∀ (m : σ →₀ ℕ), m ∈ x.support → ∃ m', m' ∈ s ∧ ∃ d, m = m' + d) ↔
    ∀ (xi : σ →₀ ℕ), xi ∈ support x → ∃ si, si ∈ s ∧ ∃ c, xi = si + c
rfl