refactor(group_theory/group_action/basic): Golf definition of action on cosets (#12823)
refactor(group_theory/group_action/basic): Golf definition of action on cosets (#12823)

This PR golfs the definition of the left-multiplication action on left cosets.

I deleted `mul_left_cosets` since it's the same as `•` and has no API.



Co-authored-by: Eric Wieser <da64e90baec5d084ce3d8e05f3b022ae6d118ff5@gmail.com>

leanprover-community/mathlib,leanprover-community/mathlib