∀ (M : Type u_2) {α : Type u_1} [inst : Group M] [inst_1 : MulAction M α] (a : α) (x : ↥(fixingSubgroup M {a}))
  (x_1 : ↥(SubMulAction.ofFixingSubgroup M {a})), ↑(x • x_1) ∈ SubMulAction.ofStabilizer M a