[GOAL]
σ : 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
[PROOFSTEP]
refine' AddMonoidAlgebra.mem_ideal_span_of'_image.trans _
[GOAL]
σ : 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
[PROOFSTEP]
simp_rw [le_iff_exists_add, add_comm]
[GOAL]
σ : 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
[PROOFSTEP]
rfl
[GOAL]
σ : 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 ∧ ↑(monomial si) 1 ∣ ↑(monomial xi) (coeff xi x)
[PROOFSTEP]
refine' mem_ideal_span_monomial_image.trans (forall₂_congr fun xi hxi => _)
[GOAL]
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : MvPolynomial σ R
s : Set (σ →₀ ℕ)
xi : σ →₀ ℕ
hxi : xi ∈ support x
⊢ (∃ si, si ∈ s ∧ si ≤ xi) ↔ ∃ si, si ∈ s ∧ ↑(monomial si) 1 ∣ ↑(monomial xi) (coeff xi x)
[PROOFSTEP]
simp_rw [monomial_dvd_monomial, one_dvd, and_true_iff, mem_support_iff.mp hxi, false_or_iff]
[GOAL]
σ : 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
[PROOFSTEP]
have := @mem_ideal_span_monomial_image σ R _ x ((fun i => Finsupp.single i 1) '' s)
[GOAL]
σ : 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
[PROOFSTEP]
rw [Set.image_image] at this 
[GOAL]
σ : 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
[PROOFSTEP]
refine' this.trans _
[GOAL]
σ : 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
[PROOFSTEP]
simp [Nat.one_le_iff_ne_zero]
