feat(Data/Polynomial/Expand): add leadingCoeff_expand and `monic_ex…

…pand_iff` (#9261)

The first states that `expand` preserves leading coefficient; the second states that `expand` preserves monicity, hence gives a converse to `Monic.expand`.

Mathlib/Data/Polynomial/Expand.lean

@@ -170,9 +170,14 @@ theorem natDegree_expand (p : ℕ) (f : R[X]) : (expand R p f).natDegree = f.nat
     exact mt leadingCoeff_eq_zero.1 hf
 #align polynomial.nat_degree_expand Polynomial.natDegree_expand
 
-theorem Monic.expand {p : ℕ} {f : R[X]} (hp : 0 < p) (h : f.Monic) : (expand R p f).Monic := by
-  rw [Monic.def, Polynomial.leadingCoeff, natDegree_expand, coeff_expand hp]
-  simp [hp, h]
+theorem leadingCoeff_expand {p : ℕ} {f : R[X]} (hp : 0 < p) :
+    (expand R p f).leadingCoeff = f.leadingCoeff := by
+  simp_rw [leadingCoeff, natDegree_expand, coeff_expand_mul hp]
+
+theorem monic_expand_iff {p : ℕ} {f : R[X]} (hp : 0 < p) : (expand R p f).Monic ↔ f.Monic := by
+  simp only [Monic, leadingCoeff_expand hp]
+
+alias ⟨_, Monic.expand⟩ := monic_expand_iff
 #align polynomial.monic.expand Polynomial.Monic.expand
 
 theorem map_expand {p : ℕ} {f : R →+* S} {q : R[X]} :