-- Mathlib/Algebra/MvPolynomial/Basic.lean
lemma coeffsIn_mul (M N : Submodule R S) : coeffsIn σ (M * N) = coeffsIn σ M * coeffsIn σ N

Proof state:
case refine_1.mem_mul_mem
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
M N : Submodule R S
r : S
s : σ →₀ ℕ
m : S
hm : m ∈ M
n : S
hn : n ∈ N
⊢ (monomial s) m * (monomial 0) n ∈ coeffsIn σ M * coeffsIn σ N

Tactic:
apply Submodule.mul_mem_mul <;> simpa

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✝ : Algebra R S
M N : Submodule R S
r : S
hr : r ∈ M * N
s : σ →₀ ℕ
⊢ (monomial s) r ∈ coeffsIn σ M * coeffsIn σ N

Tactic:
induction hr using Submodule.mul_induction_on' with
| mem_mul_mem m hm n hn =>
  rw [← add_zero s, ← monomial_mul]
  apply Submodule.mul_mem_mul <;> simpa
| add x _ y _ hx hy =>
  simpa [map_add] using add_mem hx hy

Result:
no goals

Proof state:
case refine_2
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
M N : Submodule R S
x : MvPolynomial σ S
hx : x ∈ coeffsIn σ M
y : MvPolynomial σ S
hy : y ∈ coeffsIn σ N
k : σ →₀ ℕ
⊢ coeff k (x * y) ∈ M * N

Tactic:
rw [MvPolynomial.coeff_mul]

Result:
case refine_2
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
M N : Submodule R S
x : MvPolynomial σ S
hx : x ∈ coeffsIn σ M
y : MvPolynomial σ S
hy : y ∈ coeffsIn σ N
k : σ →₀ ℕ
⊢ ∑ x_1 ∈ Finset.antidiagonal k, coeff x_1.1 x * coeff x_1.2 y ∈ M * N

Proof state:
case refine_2
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
M N : Submodule R S
⊢ ∀ m ∈ coeffsIn σ M, ∀ n ∈ coeffsIn σ N, m * n ∈ coeffsIn σ (M * N)

Tactic:
intros x hx y hy k

Result:
case refine_2
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
M N : Submodule R S
x : MvPolynomial σ S
hx : x ∈ coeffsIn σ M
y : MvPolynomial σ S
hy : y ∈ coeffsIn σ N
k : σ →₀ ℕ
⊢ coeff k (x * y) ∈ M * N

Proof state:
case refine_1
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
M N : Submodule R S
⊢ ∀ m ∈ M * N, ∀ (i : σ →₀ ℕ), (monomial i) m ∈ coeffsIn σ M * coeffsIn σ N

Tactic:
intros r hr s

Result:
case refine_1
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
M N : Submodule R S
r : S
hr : r ∈ M * N
s : σ →₀ ℕ
⊢ (monomial s) r ∈ coeffsIn σ M * coeffsIn σ N

Proof state:
case refine_2
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
M N : Submodule R S
⊢ coeffsIn σ M * coeffsIn σ N ≤ coeffsIn σ (M * N)

Tactic:
rw [Submodule.mul_le]

Result:
case refine_2
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
M N : Submodule R S
⊢ ∀ m ∈ coeffsIn σ M, ∀ n ∈ coeffsIn σ N, m * n ∈ coeffsIn σ (M * N)

Proof state:
case refine_2
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
M N : Submodule R S
x : MvPolynomial σ S
hx : x ∈ coeffsIn σ M
y : MvPolynomial σ S
hy : y ∈ coeffsIn σ N
k : σ →₀ ℕ
⊢ ∑ x_1 ∈ Finset.antidiagonal k, coeff x_1.1 x * coeff x_1.2 y ∈ M * N

Tactic:
exact sum_mem fun c hc ↦ Submodule.mul_mem_mul (hx _) (hy _)

Result:
no goals

Proof state:
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
M N : Submodule R S
⊢ coeffsIn σ (M * N) = coeffsIn σ M * coeffsIn σ N

Tactic:
refine le_antisymm (coeffsIn_le.2 ?_) ?_

Result:
case refine_1
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
M N : Submodule R S
⊢ ∀ m ∈ M * N, ∀ (i : σ →₀ ℕ), (monomial i) m ∈ coeffsIn σ M * coeffsIn σ N

case refine_2
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
M N : Submodule R S
⊢ coeffsIn σ M * coeffsIn σ N ≤ coeffsIn σ (M * N)

Proof state:
case refine_1.mem_mul_mem
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
M N : Submodule R S
r : S
s : σ →₀ ℕ
m : S
hm : m ∈ M
n : S
hn : n ∈ N
⊢ (monomial s) (m * n) ∈ coeffsIn σ M * coeffsIn σ N

Tactic:
rw [← add_zero s, ← monomial_mul]

Result:
case refine_1.mem_mul_mem
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
M N : Submodule R S
r : S
s : σ →₀ ℕ
m : S
hm : m ∈ M
n : S
hn : n ∈ N
⊢ (monomial s) m * (monomial 0) n ∈ coeffsIn σ M * coeffsIn σ N

Proof state:
case refine_1.add
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
M N : Submodule R S
r : S
s : σ →₀ ℕ
x : S
hx✝ : x ∈ M * N
y : S
hy✝ : y ∈ M * N
hx : (monomial s) x ∈ coeffsIn σ M * coeffsIn σ N
hy : (monomial s) y ∈ coeffsIn σ M * coeffsIn σ N
⊢ (monomial s) (x + y) ∈ coeffsIn σ M * coeffsIn σ N

Tactic:
simpa [map_add] using add_mem hx hy

Result:
no goals