chore(data/set_like): Add coe_strict_mono and coe_mono (#7004)
This adds the following monotonicity lemmas:
* `set_like.coe_mono`, `set_like.coe_strict_mono`
* `submodule.to_add_submonoid_mono`, `submodule.to_add_submonoid_strict_mono`
* `submodule.to_add_subgroup_mono`, `submodule.to_add_subgroup_strict_mono`
* `subsemiring.to_submonoid_mono`, `submodule.to_submonoid_strict_mono`
* `subsemiring.to_add_submonoid_mono`, `submodule.to_add_submonoid_strict_mono`
* `subring.to_subsemiring_mono`, `subring.to_subsemiring_strict_mono`
* `subring.to_add_subgroup_mono`, `subring.to_add_subgroup_strict_mono`
* `subring.to_submonoid_mono`, `subring.to_submonoid_strict_mono`
This also makes `tactic.monotonicity.basic` a lighter-weight import, so that the `@[mono]` attribute is accessible in more places.
