mathlib

e8f383c0 - refactor(analysis/special_functions/trigonometric): simpler proof (#6133)

refactor(analysis/special_functions/trigonometric): simpler proof (#6133) ... of `complex.tan_int_mul_pi` 3X faster elaboration, 2X smaller proof term Co-authors: `lean-gptf`, Stanislas Polu This was found by `formal-lean-wm-to-tt-m1-m2-v4-c4` when we evaluated it on theorems added to `mathlib` after we last extracted training data.