golf eq_monomial_of_unique_weight: rcases → split_ifs

Phase 4 of /cleanup on the four added lemmas. The split_ifs variant
saves one line and is more direct than the rcases + if_pos/if_neg pattern.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: CBirkbeck

Mathlib/RingTheory/MvPolynomial/WeightedHomogeneous.lean

@@ -265,10 +265,9 @@ theorem eq_monomial_of_unique_weight {w : σ → M} (hφ : IsWeightedHomogeneous
   classical
   ext d
   rw [coeff_monomial]
-  rcases eq_or_ne d d₀ with rfl | hd
-  · rw [if_pos rfl]
-  rw [if_neg hd.symm]
-  exact hφ.coeff_eq_zero d fun h ↦ hd (huniq d h)
+  split_ifs with hd
+  · rw [hd]
+  exact hφ.coeff_eq_zero d fun h ↦ hd (huniq d h).symm
 
 /-- The sum of weighted homogeneous polynomials of degree `n` is weighted homogeneous of
   weighted degree `n`. -/