chore: golf Polynomial.degree_mul_le (#6263)

And other similar lemmas

With thanks to @adomani for adding these lemmas.

Author: eric-wieser

Mathlib/Data/MvPolynomial/Variables.lean

@@ -3,6 +3,7 @@ Copyright (c) 2017 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Johan Commelin, Mario Carneiro
 -/
+import Mathlib.Algebra.MonoidAlgebra.Degree
 import Mathlib.Algebra.BigOperators.Order
 import Mathlib.Data.MvPolynomial.Rename
 
@@ -640,13 +641,7 @@ set_option linter.uppercaseLean3 false in
 
 theorem totalDegree_add (a b : MvPolynomial σ R) :
     (a + b).totalDegree ≤ max a.totalDegree b.totalDegree :=
-  Finset.sup_le fun n hn => by
-    classical
-    have := Finsupp.support_add hn
-    rw [Finset.mem_union] at this
-    cases' this with h h
-    · exact le_max_of_le_left (le_totalDegree h)
-    · exact le_max_of_le_right (le_totalDegree h)
+  AddMonoidAlgebra.sup_support_add_le _ _ _
 #align mv_polynomial.total_degree_add MvPolynomial.totalDegree_add
 
 theorem totalDegree_add_eq_left_of_totalDegree_lt {p q : MvPolynomial σ R}
@@ -679,18 +674,8 @@ theorem totalDegree_add_eq_right_of_totalDegree_lt {p q : MvPolynomial σ R}
 
 theorem totalDegree_mul (a b : MvPolynomial σ R) :
     (a * b).totalDegree ≤ a.totalDegree + b.totalDegree :=
-  Finset.sup_le fun n hn => by
-    classical
-    have := AddMonoidAlgebra.support_mul a b hn
-    simp only [Finset.mem_biUnion, Finset.mem_singleton] at this
-    rcases this with ⟨a₁, h₁, a₂, h₂, rfl⟩
-    rw [Finsupp.sum_add_index']
-    · dsimp [totalDegree]
-      exact add_le_add (le_totalDegree h₁) (le_totalDegree h₂)
-    · intro _
-      rfl
-    · intro _ b₁ b₂
-      rfl
+  AddMonoidAlgebra.sup_support_mul_le
+    (by exact (Finsupp.sum_add_index' (fun _ => rfl) (fun _ _ _ => rfl)).le) _ _
 #align mv_polynomial.total_degree_mul MvPolynomial.totalDegree_mul
 
 theorem totalDegree_smul_le [CommSemiring S] [DistribMulAction R S] (a : R) (f : MvPolynomial σ S) :

Mathlib/Data/Polynomial/Basic.lean

@@ -392,6 +392,8 @@ def support : R[X] → Finset ℕ
 theorem support_ofFinsupp (p) : support (⟨p⟩ : R[X]) = p.support := by rw [support]
 #align polynomial.support_of_finsupp Polynomial.support_ofFinsupp
 
+theorem support_toFinsupp (p : R[X]) : p.toFinsupp.support = p.support := by rw [support]
+
 @[simp]
 theorem support_zero : (0 : R[X]).support = ∅ :=
   rfl

Mathlib/Data/Polynomial/Degree/Definitions.lean

@@ -3,6 +3,7 @@ Copyright (c) 2018 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Johannes Hölzl, Scott Morrison, Jens Wagemaker
 -/
+import Mathlib.Algebra.MonoidAlgebra.Degree
 import Mathlib.Data.Fintype.BigOperators
 import Mathlib.Data.Nat.WithBot
 import Mathlib.Data.Polynomial.Monomial
@@ -626,11 +627,9 @@ theorem degree_le_zero_iff : degree p ≤ 0 ↔ p = C (coeff p 0) :=
   ⟨eq_C_of_degree_le_zero, fun h => h.symm ▸ degree_C_le⟩
 #align polynomial.degree_le_zero_iff Polynomial.degree_le_zero_iff
 
-theorem degree_add_le (p q : R[X]) : degree (p + q) ≤ max (degree p) (degree q) :=
-  calc
-    degree (p + q) = (p + q).support.sup WithBot.some := rfl
-    _ ≤ (p.support ∪ q.support).sup WithBot.some := (sup_mono support_add)
-    _ = p.support.sup WithBot.some ⊔ q.support.sup WithBot.some := sup_union
+theorem degree_add_le (p q : R[X]) : degree (p + q) ≤ max (degree p) (degree q) := by
+  simpa only [degree, ←support_toFinsupp, toFinsupp_add]
+    using AddMonoidAlgebra.sup_support_add_le _ _ _
 #align polynomial.degree_add_le Polynomial.degree_add_le
 
 theorem degree_add_le_of_degree_le {p q : R[X]} {n : ℕ} (hp : degree p ≤ n) (hq : degree q ≤ n) :
@@ -776,21 +775,9 @@ theorem degree_sum_le (s : Finset ι) (f : ι → R[X]) :
       _ ≤ _ := by rw [sup_insert, sup_eq_max]; exact max_le_max le_rfl ih
 #align polynomial.degree_sum_le Polynomial.degree_sum_le
 
-theorem degree_mul_le (p q : R[X]) : degree (p * q) ≤ degree p + degree q :=
-  calc
-    degree (p * q) ≤
-        p.support.sup fun i => degree (sum q fun j a => C (coeff p i * a) * X ^ (i + j)) := by
-      -- Porting note: Was `simp only [..]; convert ..; exact mul_eq_sum_sum`.
-      simp only [← C_mul_X_pow_eq_monomial.symm, mul_eq_sum_sum (p := p) (q := q)]
-      exact degree_sum_le _ _
-    _ ≤ p.support.sup fun i => q.support.sup fun j =>
-          degree (C (coeff p i * coeff q j) * X ^ (i + j)) :=
-      (Finset.sup_mono_fun fun i _hi => degree_sum_le _ _)
-    _ ≤ degree p + degree q := by
-      refine Finset.sup_le fun a ha ↦ Finset.sup_le fun b hb ↦ (degree_C_mul_X_pow_le _ _).trans ?_
-      rw [Nat.cast_add]
-      rw [mem_support_iff] at ha hb
-      exact add_le_add (le_degree_of_ne_zero ha) (le_degree_of_ne_zero hb)
+theorem degree_mul_le (p q : R[X]) : degree (p * q) ≤ degree p + degree q := by
+  simpa only [degree, ←support_toFinsupp, toFinsupp_mul]
+    using AddMonoidAlgebra.sup_support_mul_le (WithBot.coe_add _ _).le _ _
 #align polynomial.degree_mul_le Polynomial.degree_mul_le
 
 theorem degree_mul_le_of_le {a b : WithBot ℕ} (hp : degree p ≤ a) (hq : degree q ≤ b) :