feat(*/{group,mul}_action): more lemmas (#10308)
* add several lemmas about orbits and pointwise scalar multiplication;
* generalize `mul_action.orbit.mul_action` to a monoid action;
* more lemmas about pretransitive actions, use `to_additive` more;
* add dot notation lemmas `is_open.smul` and `is_closed.smul`.
