mathlib

b1a619c0 - refactor(analysis/special_functions/trigonometric/inverse): `cos_arcsin`, `sin_arccos` degenerate cases (#17026)

refactor(analysis/special_functions/trigonometric/inverse): `cos_arcsin`, `sin_arccos` degenerate cases (#17026) The definitions of `arcsin`, `arccos` and `sqrt` in degenerate cases mean that the lemmas `cos_arcsin` and `sin_arccos` are actually true for all real arguments (including those outside the interval from -1 to 1), without needing any inequality hypotheses. Remove those inequality hypotheses from the lemmas, so simplifying use of those lemmas elsewhere.