feat(data/real/ennreal,topology/*): assorted lemmas (#6663)
* add `@[simp]` to `ennreal.coe_nat_lt_coe_nat` and `ennreal.coe_nat_le_coe_nat`;
* add `ennreal.le_of_add_le_add_right`;
* add `set.nonempty.preimage`;
* add `ennreal.infi_mul_left'` and `ennreal.infi_mul_right'`;
* add `ennreal.tsum_top`;
* add `emetric.diam_closure`;
* add `edist_pos`;
* add `isometric.bijective`, `isometric.injective`, and `isometric.surjective`.
