One thing Herbie does is simplify stuff, and one that I am personally interested in is simplifying trigonometric expressions. For example, did you know that sin(x) / (1 + cos(x)) and (1 - sin(x)) / cos(x) are the same? Or that both are equal to tan(x / 2)? But how can we do this automatically? Before I move on, a thank you to ChatGPT, mostly o3 and 4.1, for generative discussions. The Weirstrass Substitution One key to any discussion of trigonometric stuff is the Weirstrass substitution.1 [1 ...
