mathlib3

1f309c52 - feat(analysis/special_functions): `real.log` is infinitely smooth away from zero (#5116)

feat(analysis/special_functions): `real.log` is infinitely smooth away from zero (#5116) Also redefine it using `order_iso.to_homeomorph` and prove more lemmas about limits of `exp`/`log`.