mathlib3

6676917e - feat(analysis/special_functions/*): a few more simp lemmas (#4550)

feat(analysis/special_functions/*): a few more simp lemmas (#4550) Add more lemmas for simplifying inequalities with `exp`, `log`, and `rpow`. Lemmas that generate more than one inequality are not marked as `simp`.