∀ (α : Type u_1) {β : Type u_2} [inst : Group α] [inst_1 : MulAction α β] (b : β),
  (Function.Injective fun g => ⟨MulAction.ofQuotientStabilizer α b g, ⋯⟩) ∧
    Function.Surjective fun g => ⟨MulAction.ofQuotientStabilizer α b g, ⋯⟩