Change Icc to Ico

Author: YuvalFilmus

Mathlib/RingTheory/Polynomial/Chebyshev.lean

@@ -869,12 +869,12 @@ theorem T_derivative_eq_U (n : ℤ) : derivative (T R n) = n * U R (n - 1) := by
       -ih2 + 2 * (X : R[X]) * ih1 + h₁ + 2 * h₃ + (n + 1) * h₂
 
 theorem T_derivative_mem_span_T (n : ℕ) :
-    derivative (T R n) ∈ Submodule.span ℕ ((fun m : ℕ => T R m) '' Set.Icc 0 (n - 1)) := by
+    derivative (T R n) ∈ Submodule.span ℕ ((fun m : ℕ => T R m) '' Set.Ico 0 n) := by
   by_cases! hn : n = 0
   · simp [hn]
   rw [T_derivative_eq_U, ← smul_eq_mul]; norm_cast
   refine Submodule.smul_of_tower_mem _ n ?_
-  convert U_mem_span_T R (n - 1) using 2; lia
+  convert U_mem_span_T R (n - 1) using 2 <;> grind
 
 theorem T_iterate_derivative_mem_span_T (n k : ℕ) :
     derivative^[k] (T R n) ∈ Submodule.span ℕ ((fun m : ℕ => T R m) '' Set.Icc 0 (n - k)) := by
@@ -894,8 +894,7 @@ theorem T_iterate_derivative_mem_span_T (n k : ℕ) :
       simp [Set.image, derivative']
     refine Submodule.span_le.mpr (fun x hx => ?_)
     obtain ⟨m, hm, rfl⟩ := hx
-    refine (Submodule.span_mono ?_) (T_derivative_mem_span_T (R := R) m)
-    grw [show m - 1 ≤ n - (k + 1) by grw [(Set.mem_Icc.mp hm).2]; lia]
+    refine (Submodule.span_mono (by grind)) (T_derivative_mem_span_T (R := R) m)
 
 theorem one_sub_X_sq_mul_derivative_T_eq_poly_in_T (n : ℤ) :
     (1 - X ^ 2) * derivative (T R (n + 1)) = (n + 1 : R[X]) * (T R n - X * T R (n + 1)) := by