∀ {G : Type u_2} [inst : Group G] {α : Type u_1} [inst_1 : MulAction G α] {g : G} {a b : α},
  b = g • a → ∀ (x : ↥(MulAction.stabilizer G a)) (x_1 : ↥(SubMulAction.ofStabilizer G a)), g • ↑(x • x_1) ∈ {b} → False