mathlib3

f72734a3 - chore(data/complex/exponential): add `inv_one_add_tan_sq` etc (#5299)

chore(data/complex/exponential): add `inv_one_add_tan_sq` etc (#5299) * mark `cos_sq_add_sin_sq` and `sin_sq_add_cos_sq` as `@[simp]`; * add lemmas representing `sin x` and `cos x` as functions of `tan x`.