Pull predicate from has_mem expr

Stream: Is there code for X?

[Ben]

Part of a larger proof but what am I missing here:

example (A: Type) (G : Type*) [group G] (M: mul_action G A) (a: A) (g : G) : g ∈ stabilizer G a → (g • a = a) := begin
  sorry
end

[Yaël Dillies]

docs#mul_action.mem_stabilizer_iff

[Yaël Dillies]

Or id :stuck_out_tongue: