-- Module: Mathlib.Algebra.MvPolynomial.Degrees
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
s t : Multiset σ
rw :
  degreesLE R σ (s + t) ≤ HMul.hMul (α := Submodule R (MvPolynomial σ R)) (degreesLE R σ s) (degreesLE R σ t) ∧
    HMul.hMul (α := Submodule R (MvPolynomial σ R)) (degreesLE R σ s) (degreesLE R σ t) ≤ degreesLE R σ (s + t)
rw₁ rw₂ rw₃ :
  degreesLE R σ (s + t) ≤ HMul.hMul (α := Submodule R (MvPolynomial σ R)) (degreesLE R σ s) (degreesLE R σ t) ∧
    ∀ (m : MvPolynomial σ R),
      Membership.mem (γ := Submodule R (MvPolynomial σ R)) (degreesLE R σ s) m →
        ∀ (n : MvPolynomial σ R),
          Membership.mem (γ := Submodule R (MvPolynomial σ R)) (degreesLE R σ t) n →
            Membership.mem (γ := Submodule R (MvPolynomial σ R)) (degreesLE R σ (s + t)) (m * n)
rw₄ :
  ∀ (x : MvPolynomial σ R) (hx : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (degreesLE R σ (s + t)) x)
    (i : σ →₀ ℕ) (hi : i ∈ x.support),
    Membership.mem (α := MvPolynomial σ R)
      (HMul.hMul (α := Submodule R (MvPolynomial σ R)) (degreesLE R σ s) (degreesLE R σ t))
      ((monomial i : (a : R) → MvPolynomial σ R) (coeff i x) : MvPolynomial σ R)
rw₅ rw₆ rw₇ :
  ∀ (x : MvPolynomial σ R) (hx : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (degreesLE R σ (s + t)) x)
    (i : σ →₀ ℕ) (hi : (toMultiset : (a : σ →₀ ℕ) → Multiset σ) i ≤ s + t),
    Membership.mem (α := MvPolynomial σ R)
      (HMul.hMul (α := Submodule R (MvPolynomial σ R)) (degreesLE R σ s) (degreesLE R σ t))
      ((monomial i : (a : R) → MvPolynomial σ R) (coeff i x) : MvPolynomial σ R)
rw₈ :
  ∀ (x : MvPolynomial σ R) (hx : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (degreesLE R σ (s + t)) x)
    (i : σ →₀ ℕ) (hi : (toMultiset : (a : σ →₀ ℕ) → Multiset σ) i ≤ s + t),
    let a : σ →₀ ℕ :=
      (Multiset.toFinsupp : (a : Multiset σ) → σ →₀ ℕ)
        (HSub.hSub (α := Multiset σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) i : Multiset σ) t);
    let b : σ →₀ ℕ :=
      (Multiset.toFinsupp : (a : Multiset σ) → σ →₀ ℕ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) i ⊓ t : Multiset σ);
    ∀ (this : a + b = i),
      Membership.mem (α := MvPolynomial σ R)
        (HMul.hMul (α := Submodule R (MvPolynomial σ R)) (degreesLE R σ s) (degreesLE R σ t))
        ((monomial i : (a : R) → MvPolynomial σ R) (coeff i x) : MvPolynomial σ R)
rw₉ :
  ∀ (x : MvPolynomial σ R) (hx : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (degreesLE R σ (s + t)) x)
    (i : σ →₀ ℕ) (hi : (toMultiset : (a : σ →₀ ℕ) → Multiset σ) i ≤ s + t),
    let a : σ →₀ ℕ :=
      (Multiset.toFinsupp : (a : Multiset σ) → σ →₀ ℕ)
        (HSub.hSub (α := Multiset σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) i : Multiset σ) t);
    let b : σ →₀ ℕ :=
      (Multiset.toFinsupp : (a : Multiset σ) → σ →₀ ℕ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) i ⊓ t : Multiset σ);
    ∀ (this : a + b = i) (ha : (toMultiset : (a : σ →₀ ℕ) → Multiset σ) a ≤ s),
      Membership.mem (α := MvPolynomial σ R)
        (HMul.hMul (α := Submodule R (MvPolynomial σ R)) (degreesLE R σ s) (degreesLE R σ t))
        ((monomial i : (a : R) → MvPolynomial σ R) (coeff i x) : MvPolynomial σ R)
rw₁₀ :
  ∀ (x : MvPolynomial σ R) (hx : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (degreesLE R σ (s + t)) x)
    (i : σ →₀ ℕ) (hi : (toMultiset : (a : σ →₀ ℕ) → Multiset σ) i ≤ s + t),
    let a : σ →₀ ℕ :=
      (Multiset.toFinsupp : (a : Multiset σ) → σ →₀ ℕ)
        (HSub.hSub (α := Multiset σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) i : Multiset σ) t);
    let b : σ →₀ ℕ :=
      (Multiset.toFinsupp : (a : Multiset σ) → σ →₀ ℕ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) i ⊓ t : Multiset σ);
    ∀ (this : a + b = i) (ha : (toMultiset : (a : σ →₀ ℕ) → Multiset σ) a ≤ s)
      (hb : (toMultiset : (a : σ →₀ ℕ) → Multiset σ) b ≤ t),
      Membership.mem (α := MvPolynomial σ R)
        (HMul.hMul (α := Submodule R (MvPolynomial σ R)) (degreesLE R σ s) (degreesLE R σ t))
        ((monomial i : (a : R) → MvPolynomial σ R) (coeff i x) : MvPolynomial σ R)
rw₁₁ :
  ∀ (x : MvPolynomial σ R) (hx : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (degreesLE R σ (s + t)) x)
    (i : σ →₀ ℕ) (hi : (toMultiset : (a : σ →₀ ℕ) → Multiset σ) i ≤ s + t),
    let a : σ →₀ ℕ :=
      (Multiset.toFinsupp : (a : Multiset σ) → σ →₀ ℕ)
        (HSub.hSub (α := Multiset σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) i : Multiset σ) t);
    let b : σ →₀ ℕ :=
      (Multiset.toFinsupp : (a : Multiset σ) → σ →₀ ℕ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) i ⊓ t : Multiset σ);
    ∀ (this : a + b = i) (ha : (toMultiset : (a : σ →₀ ℕ) → Multiset σ) a ≤ s)
      (hb : (toMultiset : (a : σ →₀ ℕ) → Multiset σ) b ≤ t),
      HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
          ((monomial a : (a : R) → MvPolynomial σ R) (coeff i x) : MvPolynomial σ R)
          ((monomial b : (a : R) → MvPolynomial σ R) 1 : MvPolynomial σ R) ∈
        HMul.hMul (α := Submodule R (MvPolynomial σ R)) (degreesLE R σ s) (degreesLE R σ t)
⊢ degreesLE R σ (s + t) = HMul.hMul (α := Submodule R (MvPolynomial σ R)) (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)

Premises used: le_antisymm_iff, Submodule.mul_le