chore: make every Chebyshev polynomial argument a Gröbner basis compu…

…tation (#12001)

Replace every `calc` in the file by a list of algebraic identities followed by an appropriate `linear_combination`.

Mathlib/RingTheory/Polynomial/Chebyshev.lean

@@ -124,156 +124,117 @@ theorem U_of_two_le (n : ℕ) (h : 2 ≤ n) : U R n = 2 * X * U R (n - 1) - U R
 theorem U_eq_X_mul_U_add_T : ∀ n : ℕ, U R (n + 1) = X * U R n + T R (n + 1)
   | 0 => by simp only [T, U, two_mul, mul_one]
   | 1 => by simp only [T, U]; ring
-  | n + 2 =>
-    calc
-      U R (n + 2 + 1) = 2 * X * (X * U R (n + 1) + T R (n + 2)) - (X * U R n + T R (n + 1)) := by
-        rw [U_add_two, U_eq_X_mul_U_add_T n, U_eq_X_mul_U_add_T (n + 1), U_eq_X_mul_U_add_T n]
-      _ = X * (2 * X * U R (n + 1) - U R n) + (2 * X * T R (n + 2) - T R (n + 1)) := by ring
-      _ = X * U R (n + 2) + T R (n + 2 + 1) := by simp only [U_add_two, T_add_two]
+  | n + 2 => by
+    have H₁ := U_eq_X_mul_U_add_T (n + 1)
+    have H₂ := U_eq_X_mul_U_add_T n
+    have h₁ := U_add_two R (n + 1)
+    have h₂ := U_add_two R n
+    have h₃ := T_add_two R (n + 1)
+    linear_combination -h₃ - (X:R[X]) * h₂ + h₁ + 2 * (X:R[X]) * H₁ - H₂
 #align polynomial.chebyshev.U_eq_X_mul_U_add_T Polynomial.Chebyshev.U_eq_X_mul_U_add_T
 
 theorem T_eq_U_sub_X_mul_U (n : ℕ) : T R (n + 1) = U R (n + 1) - X * U R n := by
-  rw [U_eq_X_mul_U_add_T, add_comm (X * U R n), add_sub_cancel_right]
+  linear_combination - U_eq_X_mul_U_add_T R n
 #align polynomial.chebyshev.T_eq_U_sub_X_mul_U Polynomial.Chebyshev.T_eq_U_sub_X_mul_U
 
 theorem T_eq_X_mul_T_sub_pol_U : ∀ n : ℕ, T R (n + 2) = X * T R (n + 1) - (1 - X ^ 2) * U R n
   | 0 => by simp only [T, U]; ring
   | 1 => by simp only [T, U]; ring
-  | n + 2 =>
-    calc
-      T R (n + 2 + 2) = 2 * X * T R (n + 2 + 1) - T R (n + 2) := T_add_two _ _
-      _ = 2 * X * (X * T R (n + 2) - (1 - X ^ 2) * U R (n + 1)) -
-            (X * T R (n + 1) - (1 - X ^ 2) * U R n) :=
-        by simp only [T_eq_X_mul_T_sub_pol_U]
-      _ = X * (2 * X * T R (n + 2) - T R (n + 1)) - (1 - X ^ 2) * (2 * X * U R (n + 1) - U R n) :=
-        by ring
-      _ = X * T R (n + 2 + 1) - (1 - X ^ 2) * U R (n + 2) := by rw [T_add_two _ (n + 1), U_add_two]
+  | n + 2 => by
+    have H₁ := T_eq_X_mul_T_sub_pol_U (n + 1)
+    have H₂ := T_eq_X_mul_T_sub_pol_U n
+    have h₁ := T_add_two R (n + 1)
+    have h₂ := T_add_two R (n + 2)
+    have h₃ := U_add_two R n
+    linear_combination (-(X:R[X]) ^ 2 + 1) * h₃ + h₂ - (X:R[X]) * h₁ - H₂ + 2 * (X:R[X]) * H₁
 #align polynomial.chebyshev.T_eq_X_mul_T_sub_pol_U Polynomial.Chebyshev.T_eq_X_mul_T_sub_pol_U
 
 theorem one_sub_X_sq_mul_U_eq_pol_in_T (n : ℕ) :
     (1 - X ^ 2) * U R n = X * T R (n + 1) - T R (n + 2) := by
-  rw [T_eq_X_mul_T_sub_pol_U, ← sub_add, sub_self, zero_add]
+  linear_combination T_eq_X_mul_T_sub_pol_U R n
 #align polynomial.chebyshev.one_sub_X_sq_mul_U_eq_pol_in_T Polynomial.Chebyshev.one_sub_X_sq_mul_U_eq_pol_in_T
 
 variable {R S}
 
 @[simp]
 theorem map_T (f : R →+* S) : ∀ n : ℕ, map f (T R n) = T S n
-  | 0 => by simp only [T_zero, Polynomial.map_one]
-  | 1 => by simp only [T_one, map_X]
-  | n + 2 => by
-    simp only [T_add_two, Polynomial.map_mul, Polynomial.map_sub, map_X, Polynomial.map_add,
-      Polynomial.map_one, Polynomial.map_ofNat, map_T f (n + 1), map_T f n]
+  | 0 => by simp
+  | 1 => by simp
+  | n + 2 => by simp [map_T]
 #align polynomial.chebyshev.map_T Polynomial.Chebyshev.map_T
 
 @[simp]
 theorem map_U (f : R →+* S) : ∀ n : ℕ, map f (U R n) = U S n
-  | 0 => by simp only [U_zero, Polynomial.map_one]
-  | 1 => by
-    simp [U_one, map_X, Polynomial.map_mul, Polynomial.map_add, Polynomial.map_one]
-  | n + 2 => by
-    simp only [U_add_two, Polynomial.map_mul, Polynomial.map_sub, map_X, Polynomial.map_add,
-      Polynomial.map_one, map_U f (n + 1), map_U f n]
-    norm_num
+  | 0 => by simp
+  | 1 => by simp
+  | n + 2 => by simp [map_U]
 #align polynomial.chebyshev.map_U Polynomial.Chebyshev.map_U
 
 theorem T_derivative_eq_U : ∀ n : ℕ, derivative (T R (n + 1)) = (n + 1) * U R n
-  | 0 => by simp only [T_one, U_zero, derivative_X, Nat.cast_zero, zero_add, mul_one]
+  | 0 => by simp
   | 1 => by
     simp [T_two, U_one, derivative_sub, derivative_one, derivative_mul, derivative_X_pow, add_mul]
-  | n + 2 =>
-    calc
-      derivative (T R (n + 2 + 1)) =
-          2 * T R (n + 2) + 2 * X * derivative (T R (n + 1 + 1)) - derivative (T R (n + 1)) := by
-        rw [T_add_two _ (n + 1), derivative_sub, derivative_mul, derivative_mul, derivative_X,
-          derivative_ofNat]
-        ring_nf
-      _ = 2 * (U R (n + 1 + 1) - X * U R (n + 1)) + 2 * X * (((n + 1 + 1) : R[X]) * U R (n + 1))
-          - ((n + 1) : R[X]) * U R n := by
-        rw_mod_cast [T_derivative_eq_U (n + 1), T_derivative_eq_U n, T_eq_U_sub_X_mul_U _ (n + 1)]
-      _ = (n + 1 : R[X]) * (2 * X * U R (n + 1) - U R n) + 2 * U R (n + 2) := by ring
-      _ = (n + 1) * U R (n + 2) + 2 * U R (n + 2) := by rw [U_add_two]
-      _ = (n + 2 + 1) * U R (n + 2) := by ring
-      _ = (↑(n + 2) + 1) * U R (n + 2) := by norm_cast
+  | n + 2 => by
+    have h := congr_arg derivative <| T_add_two R (n + 1)
+    simp only [derivative_sub, derivative_mul, derivative_mul, derivative_X, derivative_ofNat] at h
+    have H₁ := T_derivative_eq_U (n + 1)
+    have H₂ := T_derivative_eq_U n
+    have H₃ := T_eq_U_sub_X_mul_U R (n + 1)
+    have H₄ := U_add_two R n
+    push_cast at *
+    linear_combination 2 * (X:R[X]) * H₁ + (-n - 1) * H₄ + 2 * H₃ - H₂ + h
 #align polynomial.chebyshev.T_derivative_eq_U Polynomial.Chebyshev.T_derivative_eq_U
 
 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)) :=
-  calc
-    (1 - X ^ 2) * derivative (T R (n + 1)) = (1 - X ^ 2) * ((n + 1 : R[X]) * U R n) := by
-      rw [T_derivative_eq_U]
-    _ = (n + 1 : R[X]) * ((1 - X ^ 2) * U R n) := by ring
-    _ = (n + 1 : R[X]) * (X * T R (n + 1) - (2 * X * T R (n + 1) - T R n)) := by
-      rw [one_sub_X_sq_mul_U_eq_pol_in_T, T_add_two]
-    _ = (n + 1 : R[X]) * (T R n - X * T R (n + 1)) := by ring
+    (1 - X ^ 2) * derivative (T R (n + 1)) = (n + 1 : R[X]) * (T R n - X * T R (n + 1)) := by
+  have H₁ := one_sub_X_sq_mul_U_eq_pol_in_T R n
+  have H₂ := T_derivative_eq_U (R := R) n
+  have h₁ := T_add_two R n
+  linear_combination (-n - 1) * h₁ + (-(X:R[X]) ^ 2 + 1) * H₂ + (n + 1) * H₁
 #align polynomial.chebyshev.one_sub_X_sq_mul_derivative_T_eq_poly_in_T Polynomial.Chebyshev.one_sub_X_sq_mul_derivative_T_eq_poly_in_T
 
 theorem add_one_mul_T_eq_poly_in_U (n : ℕ) :
     ((n : R[X]) + 1) * T R (n + 1) = X * U R n - (1 - X ^ 2) * derivative (U R n) := by
-  have h : derivative (T R (n + 2)) = U R (n + 1) - X * U R n + X * derivative (T R (n + 1)) +
-      2 * X * U R n - (1 - X ^ 2) * derivative (U R n) := by
-    conv_lhs => rw [T_eq_X_mul_T_sub_pol_U]
-    simp only [derivative_sub, derivative_mul, derivative_X, derivative_one, derivative_X_pow,
-      one_mul, T_derivative_eq_U]
-    rw [T_eq_U_sub_X_mul_U, C_eq_natCast]
-    ring
-  calc
-    ((n : R[X]) + 1) * T R (n + 1) =
-        ((n : R[X]) + 1 + 1) * (X * U R n + T R (n + 1)) - X * ((n + 1 : R[X]) * U R n) -
-          (X * U R n + T R (n + 1)) :=
-      by ring
-    _ = derivative (T R (n + 2)) - X * derivative (T R (n + 1)) - U R (n + 1) := by
-      rw [← U_eq_X_mul_U_add_T, ← T_derivative_eq_U, ← Nat.cast_one, ← Nat.cast_add, Nat.cast_one, ←
-        T_derivative_eq_U (n + 1)]
-    _ = U R (n + 1) - X * U R n + X * derivative (T R (n + 1)) + 2 * X * U R n -
-              (1 - X ^ 2) * derivative (U R n) -
-            X * derivative (T R (n + 1)) -
-          U R (n + 1) :=
-      by rw [h]
-    _ = X * U R n - (1 - X ^ 2) * derivative (U R n) := by ring
+  have h₁ := congr_arg derivative <| T_eq_X_mul_T_sub_pol_U R n
+  simp only [derivative_sub, derivative_mul, derivative_X, derivative_one, derivative_X_pow,
+    T_derivative_eq_U, C_eq_natCast] at h₁
+  have h₂ := T_eq_U_sub_X_mul_U R n
+  push_cast at *
+  linear_combination h₁ + (n + 2) * h₂
 #align polynomial.chebyshev.add_one_mul_T_eq_poly_in_U Polynomial.Chebyshev.add_one_mul_T_eq_poly_in_U
 
 variable (R)
 
 /-- The product of two Chebyshev polynomials is the sum of two other Chebyshev polynomials. -/
 theorem mul_T : ∀ m k, 2 * T R m * T R (m + k) = T R (2 * m + k) + T R k
-  | 0 => by simp [two_mul, add_mul]
-  | 1 => by simp [add_comm]
-  | m + 2 => by
-    intro k
-    -- clean up the `T` nat indices in the goal
-    suffices 2 * T R (m + 2) * T R (m + k + 2) = T R (2 * m + k + 4) + T R k by
-      have h_nat₁ : 2 * (m + 2) + k = 2 * m + k + 4 := by ring
-      have h_nat₂ : m + 2 + k = m + k + 2 := by ring
-      simpa [h_nat₁, h_nat₂] using this
-    -- clean up the `T` nat indices in the inductive hypothesis applied to `m + 1` and `k + 1`
-    have H₁ : 2 * T R (m + 1) * T R (m + k + 2) = T R (2 * m + k + 3) + T R (k + 1) := by
-      have h_nat₁ : m + 1 + (k + 1) = m + k + 2 := by ring
-      have h_nat₂ : 2 * (m + 1) + (k + 1) = 2 * m + k + 3 := by ring
-      simpa [h_nat₁, h_nat₂] using mul_T (m + 1) (k + 1)
-    -- clean up the `T` nat indices in the inductive hypothesis applied to `m` and `k + 2`
-    have H₂ : 2 * T R m * T R (m + k + 2) = T R (2 * m + k + 2) + T R (k + 2) := by
-      have h_nat₁ : 2 * m + (k + 2) = 2 * m + k + 2 := by simp [add_assoc]
-      have h_nat₂ : m + (k + 2) = m + k + 2 := by simp [add_assoc]
-      simpa [h_nat₁, h_nat₂] using mul_T m (k + 2)
+  | 0, _ => by simp [two_mul, add_mul]
+  | 1, _ => by simp [add_comm]
+  | m + 2, k => by
+    -- state the inductive hypothesis for a few useful indices
+    have H₁ := mul_T (m + 1) (k + 1)
+    have H₂ := mul_T m (k + 2)
     -- state the `T` recurrence relation for a few useful indices
     have h₁ := T_add_two R m
-    have h₂ : T R (2 * m + k + 4) = 2 * X * T R (2 * m + k + 3) - T R (2 * m + k + 2) :=
-      T_add_two R (2 * m + k + 2)
+    have h₂ := T_add_two R (2 * m + k + 2)
     have h₃ := T_add_two R k
+    -- clean up the `T` nat indices
+    ring_nf at H₁ H₂ h₁ h₂ h₃ ⊢
     -- the desired identity is an appropriate linear combination of H₁, H₂, h₁, h₂, h₃
-    linear_combination 2 * T R (m + k + 2) * h₁ + 2 * (X : R[X]) * H₁ - H₂ - h₂ - h₃
+    linear_combination 2 * T R (2 + m + k) * h₁ + 2 * (X : R[X]) * H₁ - H₂ - h₂ - h₃
 #align polynomial.chebyshev.mul_T Polynomial.Chebyshev.mul_T
 
 /-- The `(m * n)`-th Chebyshev polynomial is the composition of the `m`-th and `n`-th -/
 theorem T_mul : ∀ m n, T R (m * n) = (T R m).comp (T R n)
-  | 0 => by simp
-  | 1 => by simp
-  | m + 2 => by
-    intro n
-    have : 2 * T R n * T R ((m + 1) * n) = T R ((m + 2) * n) + T R (m * n) := by
-      convert mul_T R n (m * n) using 1 <;> ring_nf
-    simp [this, T_mul m, ← T_mul (m + 1)]
+  | 0, _ => by simp
+  | 1, _ => by simp
+  | m + 2, n => by
+    have H₁ := T_mul (m + 1) n
+    have H₂ := T_mul m n
+    have H₃ := mul_T R n (m * n)
+    have h := congr_arg (comp · (T R n)) <| T_add_two R m
+    simp only [sub_comp, mul_comp, ofNat_comp, X_comp] at h
+    ring_nf at *
+    linear_combination - H₂ - h - H₃ + 2 * T R n * H₁
 #align polynomial.chebyshev.T_mul Polynomial.Chebyshev.T_mul
 
 end Polynomial.Chebyshev