chore(data/real/pi, analysis/special_functions/trigonometric.lean): speed up/simplify proofs (#7868)
These are mostly cosmetic changes, simplifying a couple of proofs. I tried to remove the calls to `linarith` or `norm_num`, when the alternatives were either single lemmas or faster than automation.
The main motivation is to reduce the diff in the bigger PR #7645.