feat(data/nat/log): review/extend API (#17809)
* Add `nat.lt_mul_self_iff`.
* Mark `nat.log_eq_zero_iff` as `@[simp]`.
* Add a `@[simp]` lemma `nat.log_pos_iff`.
* Assume `≠ 0` instead of `0 <` in `nat.pow_le_iff_le_log` and
`nat.lt_pow_iff_log_lt`, add implications with weaker assumptions:
- `nat.le_log_of_pow_le`,
- `nat.log_lt_of_lt_pow`,
- `nat.lt_pow_of_log_lt`,
- `nat.pow_le_of_le_log`.
* Add `nat.log_eq_iff` and `nat.log_eq_of_pow_le_of_lt_pow`.
* Assume `n ≠ 0` instead of `0 < n` in `nat.log_mul_base`, use implicit arguments.
* Add `nat.log_eq_iff` and `nat.log_eq_of_pow_le_of_lt_pow`.
* Add `nat.log_eq_one_iff'`, a version of `log_eq_one_iff` with seemingly weaker RHS.
* Drop assumption `1 < b` in `nat.pow_log_le_self`.
