From 1f2f2d520eea5af74916b6800dd5ea4bcb785f54 Mon Sep 17 00:00:00 2001
From: Johan Commelin <johan@commelin.net>
Date: Sat, 17 Feb 2024 11:46:06 +0100
Subject: [PATCH 1/2] chore(Data/Polynomial/Degree/TrailingDegree): some basic
 api lemmas

---
 .../Polynomial/Degree/TrailingDegree.lean     | 30 +++++++++++++++++--
 1 file changed, 28 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Data/Polynomial/Degree/TrailingDegree.lean b/Mathlib/Data/Polynomial/Degree/TrailingDegree.lean
index 2afe0949fffd7..ab0b5dff18de1 100644
--- a/Mathlib/Data/Polynomial/Degree/TrailingDegree.lean
+++ b/Mathlib/Data/Polynomial/Degree/TrailingDegree.lean
@@ -26,7 +26,7 @@ noncomputable section
 
 open Function Polynomial Finsupp Finset
 
-open BigOperators Polynomial
+open scoped BigOperators Polynomial
 
 namespace Polynomial
 
@@ -450,6 +450,16 @@ theorem natTrailingDegree_X : (X : R[X]).natTrailingDegree = 1 :=
 set_option linter.uppercaseLean3 false in
 #align polynomial.nat_trailing_degree_X Polynomial.natTrailingDegree_X
 
+@[simp]
+lemma trailingDegree_X_pow (n : ℕ) :
+    (X (R := R) ^ n).trailingDegree = n := by
+  rw [X_pow_eq_monomial, trailingDegree_monomial one_ne_zero]
+
+@[simp]
+lemma natTrailingDegree_X_pow (n : ℕ) :
+    (X (R := R) ^ n).natTrailingDegree = n := by
+  rw [X_pow_eq_monomial, natTrailingDegree_monomial one_ne_zero]
+
 end NonzeroSemiring
 
 section Ring
@@ -501,7 +511,7 @@ end Semiring
 
 section Semiring
 
-variable [Semiring R] {p q : R[X]} {ι : Type*}
+variable [Semiring R] {p q : R[X]}
 
 theorem coeff_natTrailingDegree_eq_zero_of_trailingDegree_lt
     (h : trailingDegree p < trailingDegree q) : coeff q (natTrailingDegree p) = 0 :=
@@ -512,6 +522,22 @@ theorem ne_zero_of_trailingDegree_lt {n : ℕ∞} (h : trailingDegree p < n) : p
   h.not_le (by simp [h₀])
 #align polynomial.ne_zero_of_trailing_degree_lt Polynomial.ne_zero_of_trailingDegree_lt
 
+lemma natTrailingDegree_eq_zero_of_constantCoeff_ne_zero (h : constantCoeff p ≠ 0) :
+    p.natTrailingDegree = 0 :=
+  le_antisymm (natTrailingDegree_le_of_ne_zero h) zero_le'
+
+lemma Monic.eq_X_pow_of_natTrailingDegree_eq_natDegree
+    (h₁ : p.Monic) (h₂ : p.natTrailingDegree = p.natDegree) :
+    p = X ^ p.natDegree := by
+  ext n
+  rw [coeff_X_pow]
+  obtain hn|rfl|hn := lt_trichotomy n p.natDegree
+  · rw [if_neg hn.ne, coeff_eq_zero_of_lt_natTrailingDegree]
+    rwa [h₂]
+  · rw [if_pos rfl]
+    exact h₁.leadingCoeff
+  · rw [if_neg hn.ne', coeff_eq_zero_of_natDegree_lt hn]
+
 end Semiring
 
 end Polynomial

From 489290af28f7f3e8cd76454a47b935deabcc49c2 Mon Sep 17 00:00:00 2001
From: Johan Commelin <johan@commelin.net>
Date: Sat, 17 Feb 2024 20:24:18 +0100
Subject: [PATCH 2/2] Apply suggestions from code review

Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
Co-authored-by: Jz Pan <acme_pjz@hotmail.com>
---
 Mathlib/Data/Polynomial/Degree/TrailingDegree.lean | 12 +++++-------
 1 file changed, 5 insertions(+), 7 deletions(-)

diff --git a/Mathlib/Data/Polynomial/Degree/TrailingDegree.lean b/Mathlib/Data/Polynomial/Degree/TrailingDegree.lean
index ab0b5dff18de1..b354dd927c4ec 100644
--- a/Mathlib/Data/Polynomial/Degree/TrailingDegree.lean
+++ b/Mathlib/Data/Polynomial/Degree/TrailingDegree.lean
@@ -452,12 +452,12 @@ set_option linter.uppercaseLean3 false in
 
 @[simp]
 lemma trailingDegree_X_pow (n : ℕ) :
-    (X (R := R) ^ n).trailingDegree = n := by
+    (X ^ n : R[X]).trailingDegree = n := by
   rw [X_pow_eq_monomial, trailingDegree_monomial one_ne_zero]
 
 @[simp]
 lemma natTrailingDegree_X_pow (n : ℕ) :
-    (X (R := R) ^ n).natTrailingDegree = n := by
+    (X ^ n : R[X]).natTrailingDegree = n := by
   rw [X_pow_eq_monomial, natTrailingDegree_monomial one_ne_zero]
 
 end NonzeroSemiring
@@ -531,11 +531,9 @@ lemma Monic.eq_X_pow_of_natTrailingDegree_eq_natDegree
     p = X ^ p.natDegree := by
   ext n
   rw [coeff_X_pow]
-  obtain hn|rfl|hn := lt_trichotomy n p.natDegree
-  · rw [if_neg hn.ne, coeff_eq_zero_of_lt_natTrailingDegree]
-    rwa [h₂]
-  · rw [if_pos rfl]
-    exact h₁.leadingCoeff
+  obtain hn | rfl | hn := lt_trichotomy n p.natDegree
+  · rw [if_neg hn.ne, coeff_eq_zero_of_lt_natTrailingDegree (h₂ ▸ hn)]
+  · simpa only [if_pos rfl] using h₁.leadingCoeff
   · rw [if_neg hn.ne', coeff_eq_zero_of_natDegree_lt hn]
 
 end Semiring