Simplified proof

Author: YuvalFilmus

Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev/RootsExtrema.lean

@@ -328,13 +328,11 @@ theorem abs_iterate_derivative_T_real_le (n k : ℕ) {x : ℝ} (hx : |x| ≤ 1)
   have := T_iterate_derivative_mem_span_T (R := ℝ) n k
   rw [setOf_T_eq_map] at this
   obtain ⟨f, hf⟩ := Submodule.mem_span_finset'.mp this
-  let g (m : ℕ) := if hm : m ∈ Finset.Icc 0 (n - k) then f ⟨(T ℝ m), by simp [hm]⟩ else 0
+  let g (m : ℕ) := if hm : m ∈ Finset.Icc 0 (n - k) then f ⟨(T ℝ m), by simp [Tnat, hm]⟩ else 0
   have : ∑ m ∈ Finset.Icc 0 (n - k), g m • (T ℝ m) = ∑ a, f a • a.val := by
     rw [Finset.univ_eq_attach]
-    apply Finset.sum_bij
-    case i => use fun m hm => ⟨T ℝ m, by simp [hm]⟩
-    case hi => simp
-    case i_inj => intro _ _ _ _ hm; convert congrArg (Polynomial.degree ·.1) hm; simp [degree_T]
+    apply Finset.sum_bij (fun m hm => ⟨T ℝ m, by simp [Tnat, hm]⟩) (by simp)
+    case i_inj => intros; grind
     case i_surj => aesop
     grind
   replace hf (y : ℝ) :

Mathlib/RingTheory/Polynomial/Chebyshev.lean

@@ -507,9 +507,15 @@ theorem U_mem_span_T (n : ℕ) : U R n ∈ Submodule.span ℕ {T R m | m ∈ Fin
     refine Submodule.add_mem _ ?_ ((Submodule.span_mono (by grind)) h₀)
     · exact Submodule.smul_of_tower_mem _ 2 (Submodule.mem_span_of_mem ⟨n + 2, by simp⟩)
 
+/-- `T` defines an injection from `ℕ` to `R[X]` given by `T R n` -/
+noncomputable def Tnat [IsDomain R] [NeZero (2 : R)] : ℕ ↪ R[X] :=
+{
+  toFun m := T R m
+  inj' m₁ m₂ hm := by convert congrArg Polynomial.degree hm; simp [degree_T]
+}
+
 theorem setOf_T_eq_map [IsDomain R] [NeZero (2 : R)] (n : ℕ) :
-    {T R m | m ∈ Finset.Icc 0 n} = (Finset.Icc 0 n).map ⟨fun (m : ℕ) => T R m,
-      by intro m₁ m₂ hm; convert congrArg Polynomial.degree hm; simp [degree_T]⟩ := by grind
+    {T R m | m ∈ Finset.Icc 0 n} = (Finset.Icc 0 n).map (Tnat (R := R)) := by grind
 
 /-- `C n` is the `n`th rescaled Chebyshev polynomial of the first kind (also known as a Vieta–Lucas
 polynomial), given by $C_n(2x) = 2T_n(x)$. See `Polynomial.Chebyshev.C_comp_two_mul_X`. -/