chore: golf #10193 (#10205)

+ add `rename_isHomogeneous` without `Injective` assumption, and rename `rename_isHomogeneous` to `rename_isHomogeneous_iff`.

+ refactor `degreeOf_le_totalDegree` through `restrictTotalDegree_le_restrictDegree `



Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>

Mathlib/Data/MvPolynomial/Variables.lean

@@ -490,12 +490,12 @@ theorem degreeOf_eq_sup (n : σ) (f : MvPolynomial σ R) :
 
 theorem degreeOf_lt_iff {n : σ} {f : MvPolynomial σ R} {d : ℕ} (h : 0 < d) :
     degreeOf n f < d ↔ ∀ m : σ →₀ ℕ, m ∈ f.support → m n < d := by
-  rwa [degreeOf_eq_sup n f, Finset.sup_lt_iff]
+  rwa [degreeOf_eq_sup, Finset.sup_lt_iff]
 #align mv_polynomial.degree_of_lt_iff MvPolynomial.degreeOf_lt_iff
 
 lemma degreeOf_le_iff {n : σ} {f : MvPolynomial σ R} {d : ℕ} :
     degreeOf n f ≤ d ↔ ∀ m ∈ support f, m n ≤ d := by
-  simp only [← Nat.lt_succ_iff, degreeOf_lt_iff (Nat.succ_pos _)]
+  rw [degreeOf_eq_sup, Finset.sup_le_iff]
 
 @[simp]
 theorem degreeOf_zero (n : σ) : degreeOf n (0 : MvPolynomial σ R) = 0 := by
@@ -733,13 +733,10 @@ theorem totalDegree_finset_sum {ι : Type*} (s : Finset ι) (f : ι → MvPolyno
     exact (MvPolynomial.totalDegree_add _ _).trans (max_le_max le_rfl hind)
 #align mv_polynomial.total_degree_finset_sum MvPolynomial.totalDegree_finset_sum
 
-lemma degreeOf_le_totalDegree (f : MvPolynomial σ R) (i : σ) : f.degreeOf i ≤ f.totalDegree := by
-  rw [degreeOf_le_iff]
-  intro d hd
-  refine le_trans ?_ (le_totalDegree hd)
-  if hi : i ∈ d.support
-  then exact Finset.single_le_sum (fun _ _ ↦ zero_le') hi
-  else rw [Finsupp.not_mem_support_iff] at hi; simp only [hi, zero_le]
+lemma degreeOf_le_totalDegree (f : MvPolynomial σ R) (i : σ) : f.degreeOf i ≤ f.totalDegree :=
+  degreeOf_le_iff.mpr fun d hd ↦ (eq_or_ne (d i) 0).elim (·.trans_le zero_le') fun h ↦
+    (Finset.single_le_sum (fun _ _ ↦ zero_le') <| Finsupp.mem_support_iff.mpr h).trans
+    (le_totalDegree hd)
 
 theorem exists_degree_lt [Fintype σ] (f : MvPolynomial σ R) (n : ℕ)
     (h : f.totalDegree < n * Fintype.card σ) {d : σ →₀ ℕ} (hd : d ∈ f.support) : ∃ i, d i < n := by

Mathlib/RingTheory/MvPolynomial/Basic.lean

@@ -102,12 +102,6 @@ def restrictDegree (m : ℕ) : Submodule R (MvPolynomial σ R) :=
   restrictSupport R { n | ∀ i, n i ≤ m }
 #align mv_polynomial.restrict_degree MvPolynomial.restrictDegree
 
-theorem restrictTotalDegree_le_restrictDegree (m : ℕ) :
-    restrictTotalDegree σ R m ≤ restrictDegree σ R m :=
-  restrictSupport_mono R fun n hn i ↦ (eq_or_ne (n i) 0).elim
-    (fun h ↦ h.trans_le m.zero_le) fun h ↦
-      (Finset.single_le_sum (fun _ _ ↦ Nat.zero_le _) <| Finsupp.mem_support_iff.mpr h).trans hn
-
 variable {R}
 
 theorem mem_restrictTotalDegree (p : MvPolynomial σ R) :
@@ -131,6 +125,11 @@ theorem mem_restrictDegree_iff_sup [DecidableEq σ] (p : MvPolynomial σ R) (n :
 
 variable (R)
 
+theorem restrictTotalDegree_le_restrictDegree (m : ℕ) :
+    restrictTotalDegree σ R m ≤ restrictDegree σ R m :=
+  fun p hp ↦ (mem_restrictDegree _ _ _).mpr fun s hs i ↦ (degreeOf_le_iff.mp
+    (degreeOf_le_totalDegree p i) s hs).trans ((mem_restrictTotalDegree _ _ _).mp hp)
+
 /-- The monomials form a basis on `MvPolynomial σ R`. -/
 def basisMonomials : Basis (σ →₀ ℕ) R (MvPolynomial σ R) :=
   Finsupp.basisSingleOne

Mathlib/RingTheory/MvPolynomial/Homogeneous.lean

@@ -217,18 +217,18 @@ theorem totalDegree (hφ : IsHomogeneous φ n) (h : φ ≠ 0) : totalDegree φ =
     exact Finset.le_sup (f := fun s ↦ ∑ x in s.support, (⇑s) x) hd
 #align mv_polynomial.is_homogeneous.total_degree MvPolynomial.IsHomogeneous.totalDegree
 
-theorem rename_isHomogeneous {f : σ → τ} (hf : f.Injective) :
+theorem rename_isHomogeneous {f : σ → τ} (h : φ.IsHomogeneous n):
+    (rename f φ).IsHomogeneous n := by
+  rw [← φ.support_sum_monomial_coeff, map_sum]; simp_rw [rename_monomial]
+  exact IsHomogeneous.sum _ _ _ fun d hd ↦ isHomogeneous_monomial _ _ _
+    ((Finsupp.sum_mapDomain_index_addMonoidHom fun _ ↦ .id ℕ).trans <| h <| mem_support_iff.mp hd)
+
+theorem rename_isHomogeneous_iff {f : σ → τ} (hf : f.Injective) :
     (rename f φ).IsHomogeneous n ↔ φ.IsHomogeneous n := by
-  obtain ⟨f, rfl⟩ : ∃ f' : σ ↪ τ, f = f' := ⟨⟨f, hf⟩, rfl⟩
-  have aux : ∀ d : σ →₀ ℕ,
-    ∑ i in (d.embDomain f).support, (d.embDomain f) i = ∑ i in d.support, d i := fun d ↦ by
-    simp only [Finsupp.support_embDomain, Finset.sum_map, Finsupp.embDomain_apply]
-  constructor
-  · intro h d hd
-    rw [← (@h (d.embDomain f) (by rwa [coeff_rename_embDomain])), aux]
-  · intro h d hd
-    obtain ⟨d', rfl, hd'⟩ := coeff_rename_ne_zero _ _ _ hd
-    rw [← Finsupp.embDomain_eq_mapDomain, ← h hd', aux]
+  refine ⟨fun h d hd ↦ ?_, rename_isHomogeneous⟩
+  convert ← @h (d.mapDomain f) _
+  · exact Finsupp.sum_mapDomain_index_inj (h := fun _ ↦ id) hf
+  · rwa [coeff_rename_mapDomain f hf]
 
 /-- The homogeneous submodules form a graded ring. This instance is used by `DirectSum.commSemiring`
 and `DirectSum.algebra`. -/