mathlib3

67821d26 - feat(analysis/special_functions/trigonometric/chebyshev): `T_real_cos` and `U_real_cos` (#15798)

feat(analysis/special_functions/trigonometric/chebyshev): `T_real_cos` and `U_real_cos` (#15798) We prove `T_real_cos` and `U_real_cos` matching `T_complex_cos` and `U_complex_cos`. We also remove two redundant theorems.