chore(RingTheory/Polynomial/Basic): golf degreeLTEquiv (leanprover-community#39514)

Also extracts the `monomial i a ∈ degreeLT R n` proof to a lemma.

Author: SnirBroshi

Mathlib/RingTheory/Polynomial/Basic.lean

@@ -88,6 +88,9 @@ theorem degreeLE_eq_span_X_pow [DecidableEq R] {n : ℕ} :
 theorem mem_degreeLT {n : ℕ} {f : R[X]} : f ∈ degreeLT R n ↔ degree f < n := by
   simpa [degreeLT, Submodule.mem_iInf] using (degree_lt_iff_coeff_zero _ _).symm
 
+theorem monomial_coe_mem_degreeLT {n : ℕ} (i : Fin n) (a : R) : monomial i a ∈ degreeLT R n :=
+  mem_degreeLT.mpr <| degree_monomial_le i a |>.trans_lt <| by simp
+
 @[gcongr, mono]
 theorem degreeLT_mono {m n : ℕ} (H : m ≤ n) : degreeLT R m ≤ degreeLT R n := fun _ hf =>
   mem_degreeLT.2 (lt_of_lt_of_le (mem_degreeLT.1 hf) <| WithBot.coe_le_coe.2 H)
@@ -105,43 +108,19 @@ theorem degreeLT_eq_span_X_pow [DecidableEq R] {n : ℕ} :
   rw [Submodule.span_le, Finset.coe_image, Set.image_subset_iff]
   intro k hk
   apply mem_degreeLT.2
-  exact lt_of_le_of_lt (degree_X_pow_le _) (WithBot.coe_lt_coe.2 <| Finset.mem_range.1 hk)
+  exact degree_X_pow_le _ |>.trans_lt <| WithBot.coe_lt_coe.2 <| Finset.mem_range.1 hk
 
+variable (R) in
 /-- The first `n` coefficients on `degreeLT n` form a linear equivalence with `Fin n → R`. -/
-def degreeLTEquiv (R) [Semiring R] (n : ℕ) : degreeLT R n ≃ₗ[R] Fin n → R where
+def degreeLTEquiv (n : ℕ) : degreeLT R n ≃ₗ[R] Fin n → R where
   toFun p n := (↑p : R[X]).coeff n
   invFun f :=
     ⟨∑ i : Fin n, monomial i (f i),
-      (degreeLT R n).sum_mem fun i _ =>
-        mem_degreeLT.mpr
-          (lt_of_le_of_lt (degree_monomial_le i (f i)) (WithBot.coe_lt_coe.mpr i.is_lt))⟩
-  map_add' p q := by
-    ext
-    dsimp
-    rw [coeff_add]
-  map_smul' x p := by
-    ext
-    dsimp
-    rw [coeff_smul]
-    rfl
-  left_inv := by
-    rintro ⟨p, hp⟩
-    ext1
-    simp only
-    by_cases hp0 : p = 0
-    · subst hp0
-      simp only [coeff_zero, map_zero, Finset.sum_const_zero]
-    rw [mem_degreeLT, degree_eq_natDegree hp0, Nat.cast_lt] at hp
-    conv_rhs => rw [p.as_sum_range' n hp, ← Fin.sum_univ_eq_sum_range]
-  right_inv f := by
-    ext i
-    simp only [finsetSum_coeff]
-    rw [Finset.sum_eq_single i, coeff_monomial, if_pos rfl]
-    · rintro j - hji
-      rw [coeff_monomial, if_neg]
-      rwa [← Fin.ext_iff]
-    · intro h
-      exact (h (Finset.mem_univ _)).elim
+      degreeLT R n |>.sum_mem fun i _ ↦ monomial_coe_mem_degreeLT i (f i)⟩
+  map_add' p q := by ext; simp
+  map_smul' x p := by ext; simp
+  left_inv := fun ⟨p, hp⟩ ↦ by simpa using p.sum_fin (monomial ·) (by simp) (mem_degreeLT.mp hp)
+  right_inv f := by ext i; grind [finsetSum_coeff, Finset.sum_eq_single i, coeff_monomial]
 
 theorem degreeLTEquiv_eq_zero_iff_eq_zero {n : ℕ} {p : R[X]} (hp : p ∈ degreeLT R n) :
     degreeLTEquiv _ _ ⟨p, hp⟩ = 0 ↔ p = 0 := by simp