feat(group_theory/group_action): some lemmas about orbits (#2928)
feat(group_theory/group_action): some lemmas about orbits (#2928)

also remove the simp attribute unfolding the definition of orbit.
Depends on #2924 



leanprover-community/mathlib,leanprover-community/mathlib