σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : MvPolynomial σ R
s : Set σ
this :
  x ∈ Ideal.span ((fun s => ↑(monomial s) 1) '' ((fun i => Finsupp.single i 1) '' s)) ↔
    ∀ (xi : σ →₀ ℕ), xi ∈ support x → ∃ si, si ∈ (fun i => Finsupp.single i 1) '' s ∧ si ≤ xi
⊢ x ∈ Ideal.span (X '' s) ↔ ∀ (m : σ →₀ ℕ), m ∈ support x → ∃ i, i ∈ s ∧ ↑m i ≠ 0
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : MvPolynomial σ R
s : Set σ
⊢ x ∈ Ideal.span (X '' s) ↔ ∀ (m : σ →₀ ℕ), m ∈ support x → ∃ i, i ∈ s ∧ ↑m i ≠ 0
have := @mem_ideal_span_monomial_image σ R _ x ((fun i => Finsupp.single i 1) '' s)
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : MvPolynomial σ R
s : Set σ
this :
  x ∈ Ideal.span ((fun x => ↑(monomial (Finsupp.single x 1)) 1) '' s) ↔
    ∀ (xi : σ →₀ ℕ), xi ∈ support x → ∃ si, si ∈ (fun i => Finsupp.single i 1) '' s ∧ si ≤ xi
⊢ x ∈ Ideal.span (X '' s) ↔ ∀ (m : σ →₀ ℕ), m ∈ support x → ∃ i, i ∈ s ∧ ↑m i ≠ 0
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : MvPolynomial σ R
s : Set σ
this :
  x ∈ Ideal.span ((fun s => ↑(monomial s) 1) '' ((fun i => Finsupp.single i 1) '' s)) ↔
    ∀ (xi : σ →₀ ℕ), xi ∈ support x → ∃ si, si ∈ (fun i => Finsupp.single i 1) '' s ∧ si ≤ xi
⊢ x ∈ Ideal.span (X '' s) ↔ ∀ (m : σ →₀ ℕ), m ∈ support x → ∃ i, i ∈ s ∧ ↑m i ≠ 0
rw [Set.image_image] at this
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : MvPolynomial σ R
s : Set σ
this :
  x ∈ Ideal.span ((fun x => ↑(monomial (Finsupp.single x 1)) 1) '' s) ↔
    ∀ (xi : σ →₀ ℕ), xi ∈ support x → ∃ si, si ∈ (fun i => Finsupp.single i 1) '' s ∧ si ≤ xi
⊢ (∀ (xi : σ →₀ ℕ), xi ∈ support x → ∃ si, si ∈ (fun i => Finsupp.single i 1) '' s ∧ si ≤ xi) ↔
    ∀ (m : σ →₀ ℕ), m ∈ support x → ∃ i, i ∈ s ∧ ↑m i ≠ 0
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : MvPolynomial σ R
s : Set σ
this :
  x ∈ Ideal.span ((fun x => ↑(monomial (Finsupp.single x 1)) 1) '' s) ↔
    ∀ (xi : σ →₀ ℕ), xi ∈ support x → ∃ si, si ∈ (fun i => Finsupp.single i 1) '' s ∧ si ≤ xi
⊢ x ∈ Ideal.span (X '' s) ↔ ∀ (m : σ →₀ ℕ), m ∈ support x → ∃ i, i ∈ s ∧ ↑m i ≠ 0
refine' this.trans _
no goals
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : MvPolynomial σ R
s : Set σ
this :
  x ∈ Ideal.span ((fun x => ↑(monomial (Finsupp.single x 1)) 1) '' s) ↔
    ∀ (xi : σ →₀ ℕ), xi ∈ support x → ∃ si, si ∈ (fun i => Finsupp.single i 1) '' s ∧ si ≤ xi
⊢ (∀ (xi : σ →₀ ℕ), xi ∈ support x → ∃ si, si ∈ (fun i => Finsupp.single i 1) '' s ∧ si ≤ xi) ↔
    ∀ (m : σ →₀ ℕ), m ∈ support x → ∃ i, i ∈ s ∧ ↑m i ≠ 0
simp [Nat.one_le_iff_ne_zero]