diff --git a/Mathlib/Algebra/Polynomial/BigOperators.lean b/Mathlib/Algebra/Polynomial/BigOperators.lean
index 6cead554cb7a02..9c45f3aa3e918b 100644
--- a/Mathlib/Algebra/Polynomial/BigOperators.lean
+++ b/Mathlib/Algebra/Polynomial/BigOperators.lean
@@ -59,6 +59,10 @@ theorem natDegree_sum_le (f : ι → S[X]) :
   simpa using natDegree_multiset_sum_le (s.val.map f)
 #align polynomial.nat_degree_sum_le Polynomial.natDegree_sum_le
 
+lemma natDegree_sum_le_of_forall_le {n : ℕ} (f : ι → S[X]) (h : ∀ i ∈ s, natDegree (f i) ≤ n) :
+    natDegree (∑ i in s, f i) ≤ n :=
+  le_trans (natDegree_sum_le s f) <| (Finset.fold_max_le n).mpr <| by simpa
+
 theorem degree_list_sum_le (l : List S[X]) : degree l.sum ≤ (l.map natDegree).maximum := by
   by_cases h : l.sum = 0
   · simp [h]
diff --git a/Mathlib/Data/Fin/Basic.lean b/Mathlib/Data/Fin/Basic.lean
index 6b9e1f2e148540..e6cca96ab7ff56 100644
--- a/Mathlib/Data/Fin/Basic.lean
+++ b/Mathlib/Data/Fin/Basic.lean
@@ -673,9 +673,9 @@ theorem val_cast_of_lt {n : ℕ} [NeZero n] {a : ℕ} (h : a < n) : (a : Fin n).
   Nat.mod_eq_of_lt h
 #align fin.coe_val_of_lt Fin.val_cast_of_lt
 
-/-- Converting the value of a `Fin (n + 1)` to `Fin (n + 1)` results
+/-- If `n` is non-zero, converting the value of a `Fin n` to `Fin n` results
 in the same value.  -/
-theorem cast_val_eq_self {n : ℕ} [NeZero n] (a : Fin n) : (a.val : Fin n) = a :=
+@[simp] theorem cast_val_eq_self {n : ℕ} [NeZero n] (a : Fin n) : (a.val : Fin n) = a :=
   ext <| val_cast_of_lt a.isLt
 #align fin.coe_val_eq_self Fin.cast_val_eq_self
 
diff --git a/Mathlib/Data/Polynomial/Basic.lean b/Mathlib/Data/Polynomial/Basic.lean
index e956f8de346e6e..db3f4cfc0e6f85 100644
--- a/Mathlib/Data/Polynomial/Basic.lean
+++ b/Mathlib/Data/Polynomial/Basic.lean
@@ -1039,6 +1039,7 @@ theorem sum_smul_index {S : Type*} [AddCommMonoid S] (p : R[X]) (b : R) (f : ℕ
   Finsupp.sum_smul_index hf
 #align polynomial.sum_smul_index Polynomial.sum_smul_index
 
+@[simp]
 theorem sum_monomial_eq : ∀ p : R[X], (p.sum fun n a => monomial n a) = p
   | ⟨_p⟩ => (ofFinsupp_sum _ _).symm.trans (congr_arg _ <| Finsupp.sum_single _)
 #align polynomial.sum_monomial_eq Polynomial.sum_monomial_eq