-- Mathlib/Algebra/MvPolynomial/Basic.lean
lemma coeffsIn_eq_span_monomial : coeffsIn σ M = .span R {monomial i m | (m ∈ M) (i : σ →₀ ℕ)}

Proof state:
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Module R S
M : Submodule R S
⊢ coeffsIn σ M = Submodule.span R {x | ∃ m ∈ M, ∃ i, (monomial i) m = x}

Tactic:
refine le_antisymm ?_ <| Submodule.span_le.2 ?_

Result:
case refine_1
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Module R S
M : Submodule R S
⊢ coeffsIn σ M ≤ Submodule.span R {x | ∃ m ∈ M, ∃ i, (monomial i) m = x}

case refine_2
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Module R S
M : Submodule R S
⊢ {x | ∃ m ∈ M, ∃ i, (monomial i) m = x} ⊆ ↑(coeffsIn σ M)

Proof state:
case refine_2
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Module R S
M : Submodule R S
⊢ {x | ∃ m ∈ M, ∃ i, (monomial i) m = x} ⊆ ↑(coeffsIn σ M)

Tactic:
rintro _ ⟨m, hm, s, n, rfl⟩ i

Result:
case refine_2.intro.intro.intro.refl
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Module R S
M : Submodule R S
m : S
hm : m ∈ M
s i : σ →₀ ℕ
⊢ coeff i ((monomial s) m) ∈ M

Proof state:
case refine_2.intro.intro.intro.refl
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Module R S
M : Submodule R S
m : S
hm : m ∈ M
s i : σ →₀ ℕ
⊢ coeff i ((monomial s) m) ∈ M

Tactic:
simp [coeff_X_pow]

Result:
case refine_2.intro.intro.intro.refl
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Module R S
M : Submodule R S
m : S
hm : m ∈ M
s i : σ →₀ ℕ
⊢ (if s = i then m else 0) ∈ M

Proof state:
case refine_1
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Module R S
M : Submodule R S
p : MvPolynomial σ S
hp : p ∈ coeffsIn σ M
⊢ p ∈ Submodule.span R {x | ∃ m ∈ M, ∃ i, (monomial i) m = x}

Tactic:
rw [p.as_sum]

Result:
case refine_1
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Module R S
M : Submodule R S
p : MvPolynomial σ S
hp : p ∈ coeffsIn σ M
⊢ ∑ v ∈ p.support, (monomial v) (coeff v p) ∈ Submodule.span R {x | ∃ m ∈ M, ∃ i, (monomial i) m = x}

Proof state:
case refine_1
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Module R S
M : Submodule R S
p : MvPolynomial σ S
hp : p ∈ coeffsIn σ M
⊢ ∑ v ∈ p.support, (monomial v) (coeff v p) ∈ Submodule.span R {x | ∃ m ∈ M, ∃ i, (monomial i) m = x}

Tactic:
exact sum_mem fun i hi ↦ Submodule.subset_span ⟨_, hp i, _, rfl⟩

Result:
no goals

Proof state:
case refine_2.intro.intro.intro.refl
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Module R S
M : Submodule R S
m : S
hm : m ∈ M
s i : σ →₀ ℕ
⊢ (if s = i then m else 0) ∈ M

Tactic:
split <;> simp [hm]

Result:
no goals

Proof state:
case refine_1
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Module R S
M : Submodule R S
⊢ coeffsIn σ M ≤ Submodule.span R {x | ∃ m ∈ M, ∃ i, (monomial i) m = x}

Tactic:
rintro p hp

Result:
case refine_1
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Module R S
M : Submodule R S
p : MvPolynomial σ S
hp : p ∈ coeffsIn σ M
⊢ p ∈ Submodule.span R {x | ∃ m ∈ M, ∃ i, (monomial i) m = x}