mathlib3

86d65f8d - chore(topology/instances/ennreal): prove `nnreal.not_summable_iff_tendsto_nat_at_top` (#4670)

chore(topology/instances/ennreal): prove `nnreal.not_summable_iff_tendsto_nat_at_top` (#4670) * use `ℝ≥0` notation in `data/real/ennreal`; * add `ennreal.forall_ne_top`, `ennreal.exists_ne_top`, `ennreal.ne_top_equiv_nnreal`, `ennreal.cinfi_ne_top`, `ennreal.infi_ne_top`, `ennreal.csupr_ne_top`, `ennreal.sup_ne_top`, `ennreal.supr_ennreal`; * add `nnreal.injective_coe`, add `@[simp, norm_cast]` to `nnreal.tendsto_coe`, and add `nnreal.tendsto_coe_at_top`; move `nnreal.infi_real_pos_eq_infi_nnreal_pos` from `ennreal` to `nnreal`; * use `function.injective` instead of an unfolded definition in `filter.comap_map`; * add `ennreal.nhds_top'`, `ennreal.tendsto_nhds_top_iff_nnreal`, `ennreal.tendsto_nhds_top_iff_nat`; * upgrade `ennreal.tendsto_coe_nnreal_nhds_top` to an `iff`, rename to `ennreal.tendsto_coe_nhds_top`; * `nnreal.has_sum_iff_tendsto_nat` now takes `r` as an implicit argument; * add `nnreal.not_summable_iff_tendsto_nat_at_top` and `not_summable_iff_tendsto_nat_at_top_of_nonneg`.