-- Mathlib/Algebra/MvPolynomial/Degrees.lean
lemma degreesLE_add : degreesLE R σ (s + t) = degreesLE R σ s * degreesLE R σ t

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s t : Multiset σ
x : MvPolynomial σ R
hx : x ∈ degreesLE R σ (s + t)
i : σ →₀ ℕ
hi : toMultiset i ≤ s + t
a : σ →₀ ℕ := Multiset.toFinsupp (toMultiset i - t)
b : σ →₀ ℕ := Multiset.toFinsupp (toMultiset i ⊓ t)
this : a + b = i
ha : toMultiset a ≤ s
hb : toMultiset b ≤ t
⊢ (monomial i) (coeff i x) ∈ degreesLE R σ s * degreesLE R σ t

Tactic:
rw [show monomial i (x.coeff i) = monomial a (x.coeff i) * monomial b 1 by simp [this]]

Result:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s t : Multiset σ
x : MvPolynomial σ R
hx : x ∈ degreesLE R σ (s + t)
i : σ →₀ ℕ
hi : toMultiset i ≤ s + t
a : σ →₀ ℕ := Multiset.toFinsupp (toMultiset i - t)
b : σ →₀ ℕ := Multiset.toFinsupp (toMultiset i ⊓ t)
this : a + b = i
ha : toMultiset a ≤ s
hb : toMultiset b ≤ t
⊢ (monomial a) (coeff i x) * (monomial b) 1 ∈ degreesLE R σ s * degreesLE R σ t

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s t : Multiset σ
x : MvPolynomial σ R
hx : x ∈ degreesLE R σ (s + t)
i : σ →₀ ℕ
hi : toMultiset i ≤ s + t
a : σ →₀ ℕ := Multiset.toFinsupp (toMultiset i - t)
b : σ →₀ ℕ := Multiset.toFinsupp (toMultiset i ⊓ t)
this : a + b = i
ha : toMultiset a ≤ s
hb : toMultiset b ≤ t
⊢ (monomial i) (coeff i x) = (monomial a) (coeff i x) * (monomial b) 1

Tactic:
simp [this]

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s t : Multiset σ
x : MvPolynomial σ R
hx : x ∈ degreesLE R σ (s + t)
i : σ →₀ ℕ
hi : i ∈ x.support
⊢ (monomial i) (coeff i x) ∈ degreesLE R σ s * degreesLE R σ t

Tactic:
replace hi : i.toMultiset ≤ s + t := (Finset.le_sup hi).trans hx

Result:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s t : Multiset σ
x : MvPolynomial σ R
hx : x ∈ degreesLE R σ (s + t)
i : σ →₀ ℕ
hi : toMultiset i ≤ s + t
⊢ (monomial i) (coeff i x) ∈ degreesLE R σ s * degreesLE R σ t

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s t : Multiset σ
x : MvPolynomial σ R
hx : x ∈ degreesLE R σ (s + t)
i : σ →₀ ℕ
hi : toMultiset i ≤ s + t
a : σ →₀ ℕ := Multiset.toFinsupp (toMultiset i - t)
b : σ →₀ ℕ := Multiset.toFinsupp (toMultiset i ⊓ t)
this : a + b = i
ha : toMultiset a ≤ s
⊢ toMultiset b ≤ t

Tactic:
simp [b, Multiset.inter_le_right]

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s t : Multiset σ
x : MvPolynomial σ R
hx : x ∈ degreesLE R σ (s + t)
i : σ →₀ ℕ
hi : toMultiset i ≤ s + t
a : σ →₀ ℕ := Multiset.toFinsupp (toMultiset i - t)
b : σ →₀ ℕ := Multiset.toFinsupp (toMultiset i ⊓ t)
⊢ (monomial i) (coeff i x) ∈ degreesLE R σ s * degreesLE R σ t

Tactic:
have : a + b = i := Multiset.toFinsupp.symm.injective (by simp [a, b, Multiset.sub_add_inter])

Result:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s t : Multiset σ
x : MvPolynomial σ R
hx : x ∈ degreesLE R σ (s + t)
i : σ →₀ ℕ
hi : toMultiset i ≤ s + t
a : σ →₀ ℕ := Multiset.toFinsupp (toMultiset i - t)
b : σ →₀ ℕ := Multiset.toFinsupp (toMultiset i ⊓ t)
this : a + b = i
⊢ (monomial i) (coeff i x) ∈ degreesLE R σ s * degreesLE R σ t

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s t : Multiset σ
x : MvPolynomial σ R
hx : x ∈ degreesLE R σ (s + t)
i : σ →₀ ℕ
hi : toMultiset i ≤ s + t
a : σ →₀ ℕ := Multiset.toFinsupp (toMultiset i - t)
b : σ →₀ ℕ := Multiset.toFinsupp (toMultiset i ⊓ t)
this : a + b = i
⊢ toMultiset a ≤ s

Tactic:
simpa [a, add_comm (a := t)] using hi

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s t : Multiset σ
⊢ degreesLE R σ (s + t) = degreesLE R σ s * degreesLE R σ t

Tactic:
classical
rw [le_antisymm_iff, Submodule.mul_le]
refine ⟨fun x hx ↦ x.as_sum ▸ sum_mem fun i hi ↦ ?_,
  fun x hx y hy ↦ degrees_mul_le.trans (add_le_add hx hy)⟩
replace hi : i.toMultiset ≤ s + t := (Finset.le_sup hi).trans hx
let a := (i.toMultiset - t).toFinsupp
let b := (i.toMultiset ⊓ t).toFinsupp
have : a + b = i := Multiset.toFinsupp.symm.injective (by simp [a, b, Multiset.sub_add_inter])
have ha : a.toMultiset ≤ s := by simpa [a, add_comm (a := t)] using hi
have hb : b.toMultiset ≤ t := by simp [b, Multiset.inter_le_right]
rw [show monomial i (x.coeff i) = monomial a (x.coeff i) * monomial b 1 by simp [this]]
exact Submodule.mul_mem_mul ((degrees_monomial _ _).trans ha) ((degrees_monomial _ _).trans hb)

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s t : Multiset σ
x : MvPolynomial σ R
hx : x ∈ degreesLE R σ (s + t)
i : σ →₀ ℕ
hi : toMultiset i ≤ s + t
a : σ →₀ ℕ := Multiset.toFinsupp (toMultiset i - t)
⊢ (monomial i) (coeff i x) ∈ degreesLE R σ s * degreesLE R σ t

Tactic:
let b := (i.toMultiset ⊓ t).toFinsupp

Result:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s t : Multiset σ
x : MvPolynomial σ R
hx : x ∈ degreesLE R σ (s + t)
i : σ →₀ ℕ
hi : toMultiset i ≤ s + t
a : σ →₀ ℕ := Multiset.toFinsupp (toMultiset i - t)
b : σ →₀ ℕ := Multiset.toFinsupp (toMultiset i ⊓ t)
⊢ (monomial i) (coeff i x) ∈ degreesLE R σ s * degreesLE R σ t

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s t : Multiset σ
x : MvPolynomial σ R
hx : x ∈ degreesLE R σ (s + t)
i : σ →₀ ℕ
hi : toMultiset i ≤ s + t
a : σ →₀ ℕ := Multiset.toFinsupp (toMultiset i - t)
b : σ →₀ ℕ := Multiset.toFinsupp (toMultiset i ⊓ t)
⊢ Multiset.toFinsupp.symm (a + b) = Multiset.toFinsupp.symm i

Tactic:
simp [a, b, Multiset.sub_add_inter]

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s t : Multiset σ
⊢ degreesLE R σ (s + t) = degreesLE R σ s * degreesLE R σ t

Tactic:
rw [le_antisymm_iff, Submodule.mul_le]

Result:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s t : Multiset σ
⊢ degreesLE R σ (s + t) ≤ degreesLE R σ s * degreesLE R σ t ∧
    ∀ m ∈ degreesLE R σ s, ∀ n ∈ degreesLE R σ t, m * n ∈ degreesLE R σ (s + t)

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s t : Multiset σ
x : MvPolynomial σ R
hx : x ∈ degreesLE R σ (s + t)
i : σ →₀ ℕ
hi : toMultiset i ≤ s + t
a : σ →₀ ℕ := Multiset.toFinsupp (toMultiset i - t)
b : σ →₀ ℕ := Multiset.toFinsupp (toMultiset i ⊓ t)
this : a + b = i
⊢ (monomial i) (coeff i x) ∈ degreesLE R σ s * degreesLE R σ t

Tactic:
have ha : a.toMultiset ≤ s := by simpa [a, add_comm (a := t)] using hi

Result:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s t : Multiset σ
x : MvPolynomial σ R
hx : x ∈ degreesLE R σ (s + t)
i : σ →₀ ℕ
hi : toMultiset i ≤ s + t
a : σ →₀ ℕ := Multiset.toFinsupp (toMultiset i - t)
b : σ →₀ ℕ := Multiset.toFinsupp (toMultiset i ⊓ t)
this : a + b = i
ha : toMultiset a ≤ s
⊢ (monomial i) (coeff i x) ∈ degreesLE R σ s * degreesLE R σ t

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s t : Multiset σ
x : MvPolynomial σ R
hx : x ∈ degreesLE R σ (s + t)
i : σ →₀ ℕ
hi : toMultiset i ≤ s + t
a : σ →₀ ℕ := Multiset.toFinsupp (toMultiset i - t)
b : σ →₀ ℕ := Multiset.toFinsupp (toMultiset i ⊓ t)
this : a + b = i
ha : toMultiset a ≤ s
⊢ (monomial i) (coeff i x) ∈ degreesLE R σ s * degreesLE R σ t

Tactic:
have hb : b.toMultiset ≤ t := by simp [b, Multiset.inter_le_right]

Result:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s t : Multiset σ
x : MvPolynomial σ R
hx : x ∈ degreesLE R σ (s + t)
i : σ →₀ ℕ
hi : toMultiset i ≤ s + t
a : σ →₀ ℕ := Multiset.toFinsupp (toMultiset i - t)
b : σ →₀ ℕ := Multiset.toFinsupp (toMultiset i ⊓ t)
this : a + b = i
ha : toMultiset a ≤ s
hb : toMultiset b ≤ t
⊢ (monomial i) (coeff i x) ∈ degreesLE R σ s * degreesLE R σ t