Commit 2020-12-11 16:44 db712d59

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.