feat: simple lemmas about polynomials and their degrees (#6220)

This PR extracts some lemmas about polynomials that are helpful for the tactic `compute_degree` (#6221).

The signature of a theorem changed:
```lean
theorem coeff_pow_of_natDegree_le (pn : p.natDegree ≤ n) :
    (p ^ m).coeff (n * m) = p.coeff n ^ m  -- <-- the order of the product was `n * m`
    (p ^ m).coeff (m * n) = p.coeff n ^ m  -- <-- and it became `m * n`
```
Modified files:
```
Data/Polynomial/Basic.lean
Data/Polynomial/Degree/Lemmas.lean
Data/Polynomial/Degree/Definitions.lean
Data/Polynomial/Coeff.lean  -- for a "`simp` can prove this" golf
```

Mathlib/Data/Polynomial/Basic.lean

@@ -729,6 +729,10 @@ theorem coeff_C_zero : coeff (C a) 0 = a :=
 theorem coeff_C_ne_zero (h : n ≠ 0) : (C a).coeff n = 0 := by rw [coeff_C, if_neg h]
 #align polynomial.coeff_C_ne_zero Polynomial.coeff_C_ne_zero
 
+@[simp]
+theorem coeff_nat_cast_ite : (Nat.cast m : R[X]).coeff n = ite (n = 0) m 0 := by
+  simp only [← C_eq_nat_cast, coeff_C, Nat.cast_ite, Nat.cast_zero]
+
 theorem C_mul_X_pow_eq_monomial : ∀ {n : ℕ}, C a * X ^ n = monomial n a
   | 0 => mul_one _
   | n + 1 => by

Mathlib/Data/Polynomial/Coeff.lean

@@ -370,11 +370,8 @@ end Coeff
 
 section cast
 
-@[simp]
 theorem nat_cast_coeff_zero {n : ℕ} {R : Type _} [Semiring R] : (n : R[X]).coeff 0 = n := by
-  induction' n with n ih
-  · simp
-  · simp [ih]
+  simp only [coeff_nat_cast_ite, ite_true]
 #align polynomial.nat_cast_coeff_zero Polynomial.nat_cast_coeff_zero
 
 @[norm_cast] -- @[simp] -- Porting note: simp can prove this

Mathlib/Data/Polynomial/Degree/Definitions.lean

@@ -1077,6 +1077,20 @@ theorem coeff_pow_mul_natDegree (p : R[X]) (n : ℕ) :
       exact coeff_mul_degree_add_degree _ _
 #align polynomial.coeff_pow_mul_nat_degree Polynomial.coeff_pow_mul_natDegree
 
+theorem coeff_mul_add_eq_of_natDegree_le {df dg : ℕ} {g : R[X]}
+    (hdf : natDegree f ≤ df) (hdg : natDegree g ≤ dg) :
+    (f * g).coeff (df + dg) = f.coeff df * g.coeff dg := by
+  rw [coeff_mul, Finset.sum_eq_single_of_mem (df, dg)]
+  · rw [Finset.Nat.mem_antidiagonal]
+  rintro ⟨df', dg'⟩ hmem hne
+  obtain h | hdf' := lt_or_le df df'
+  · rw [coeff_eq_zero_of_natDegree_lt (hdf.trans_lt h), zero_mul]
+  obtain h | hdg' := lt_or_le dg dg'
+  · rw [coeff_eq_zero_of_natDegree_lt (hdg.trans_lt h), mul_zero]
+  obtain ⟨rfl, rfl⟩ :=
+    eq_and_eq_of_le_of_le_of_add_le hdf' hdg' (Finset.Nat.mem_antidiagonal.1 hmem).ge
+  exact (hne rfl).elim
+
 theorem zero_le_degree_iff : 0 ≤ degree p ↔ p ≠ 0 := by
   rw [← not_lt, Nat.WithBot.lt_zero_iff, degree_eq_bot]
 #align polynomial.zero_le_degree_iff Polynomial.zero_le_degree_iff

Mathlib/Data/Polynomial/Degree/Lemmas.lean

@@ -173,14 +173,22 @@ theorem coeff_mul_of_natDegree_le (pm : p.natDegree ≤ m) (qn : q.natDegree ≤
 #align polynomial.coeff_mul_of_nat_degree_le Polynomial.coeff_mul_of_natDegree_le
 
 theorem coeff_pow_of_natDegree_le (pn : p.natDegree ≤ n) :
-    (p ^ m).coeff (n * m) = p.coeff n ^ m := by
+    (p ^ m).coeff (m * n) = p.coeff n ^ m := by
   induction' m with m hm
   · simp
-  · rw [pow_succ', pow_succ', ← hm, Nat.mul_succ, coeff_mul_of_natDegree_le _ pn]
-    refine' natDegree_pow_le.trans (le_trans _ (mul_comm _ _).le)
+  · rw [pow_succ', pow_succ', ← hm, Nat.succ_mul, coeff_mul_of_natDegree_le _ pn]
+    refine' natDegree_pow_le.trans (le_trans _ (le_refl _))
     exact mul_le_mul_of_nonneg_left pn m.zero_le
 #align polynomial.coeff_pow_of_nat_degree_le Polynomial.coeff_pow_of_natDegree_le
 
+theorem coeff_pow_eq_ite_of_natDegree_le_of_le {o : ℕ}
+    (pn : natDegree p ≤ n) (mno : m * n ≤ o) :
+    coeff (p ^ m) o = if o = m * n then (coeff p n) ^ m else 0 := by
+  rcases eq_or_ne o (m * n) with rfl | h
+  · simpa only [ite_true] using coeff_pow_of_natDegree_le pn
+  · simpa only [h, ite_false] using coeff_eq_zero_of_natDegree_lt $
+      lt_of_le_of_lt (natDegree_pow_le_of_le m pn) (lt_of_le_of_ne mno h.symm)
+
 theorem coeff_add_eq_left_of_lt (qn : q.natDegree < n) : (p + q).coeff n = p.coeff n :=
   (coeff_add _ _ _).trans <|
     (congr_arg _ <| coeff_eq_zero_of_natDegree_lt <| qn).trans <| add_zero _