refactor(data/real/ennreal): golf, generalize (#14996)
## Add new lemmas
* `ennreal.bit0_strict_mono`, `ennreal.bit0_injective`, `ennreal.bit0_lt_bit0`, `ennreal.bit0_le_bit0`, `ennreal.bit0_top`;
* `ennreal.bit1_strict_mono`, `ennreal.bit1_injective`, `ennreal.bit1_lt_bit1`, `ennreal.bit1_le_bit1`, `ennreal.bit1_top`;
* `ennreal.div_eq_inv_mul`, `ennreal.of_real_mul'`;
* `filter.eventually.prod_nhds`.
## Generalize lemmas
* Drop unneeded assumption in `real.to_nnreal_bit0` and `ennreal.of_real_bit0`.
## Rename lemmas
* `ennreal.mul_div_cancel` → `ennreal.div_mul_cancel`, fixing a TODO;
* `prod_is_open.mem_nhds` → `prod_mem_nhds`: there are no open sets in the statement.
## Other changes
* Golf some proofs.
* Avoid non-final `simp`s here and there.
* Move `mul_inv_cancel` etc up to use them in other proofs.
* Move some `to_nnreal` lemmas above `to_real` lemmas, use them in `to_real` lemmas.
* Use `to_dual` in `order_iso.inv_ennreal`.
