mathlib

1a2eb0b5 - feat(analysis/special_functions/trigonometric): add mistakenly omitted lemma (#6036)