chore(*): simp lemmas for `tendsto`, `Ixx`, and `coe` (#5296)
* For `(f : α → β) (l : filter β)`, simplify `tendsto (λ a : Ixx*, f x) at_top l`
to `tendsto f _ l`, and similarly for `at_bot`.
* For `(f : α → Ixx*) (l : filter α)`, simplify
`tendsto f l at_top` to `tendsto (λ x, (f x : β)) l _`, and
similarly for `at_bot`.
Here `Ixx*` is one of the intervals `Ici a`, `Ioi a`, `Ioo a b` etc,
and `_` is a filter that depends on the choice of `Ixx` and
`at_top`/`at_bot`.
* Drop some “nontriviality” assumptions like `no_top_order` for lemmas
about `Ioi a`.
