mathlib3

c25dad98 - refactor(analysis/calculus/mean_value): use `is_R_or_C` in more lemmas (#6022)

refactor(analysis/calculus/mean_value): use `is_R_or_C` in more lemmas (#6022) * use `is_R_or_C` in `convex.norm_image_sub_le*` lemmas; * replace `strict_fderiv_of_cont_diff` with `has_strict_fderiv_at_of_has_fderiv_at_of_continuous_at` and `has_strict_deriv_at_of_has_deriv_at_of_continuous_at`, slightly change assumptions; * add `has_ftaylor_series_up_to_on.has_fderiv_at`, `has_ftaylor_series_up_to_on.eventually_has_fderiv_at`, `has_ftaylor_series_up_to_on.differentiable_at`; * add `times_cont_diff_at.has_strict_deriv_at` and `times_cont_diff_at.has_strict_deriv_at'`; * prove that `complex.exp` is strictly differentiable and is an open map; * add `simp` lemma `interior_mem_nhds`.