feat(order/filter/basic): add more lemmas about `tendsto _ _ at_top` (#1713)
feat(order/filter/basic): add more lemmas about `tendsto _ _ at_top` (#1713)

* feat(order/filter/basic): add more lemmas about `tendsto _ _ at_top`

* Use explicit arguments as suggested by @sgouezel

* Add lemmas for an `ordered_comm_group`

* Add a missing lemma

leanprover-community/mathlib,leanprover-community/mathlib