mathlib3

33483a3d - chore(analysis/special_functions/trigonometric): golf a few more proofs (#5423)