Prove set membership

Stream: new members

[Florestan]

I'm trying to understand the construction of set.
I would like to prove that something is a member a of a set defined by a predicate, for example:

def S := {x : real | x*x <= 2}
example : coe 0 ∈ S :=
begin
sorry
end

but the goal is

⊢ ↑0 ∈ S

when I want it to be

↑0*↑0  <= 2

[Sebastien Gouezel]

Two approaches:

def S := {x : real | x*x <= 2}
example : (0 : ℝ) ∈ S :=
begin
  dsimp [S],
  norm_num,
end

example : (0 : ℝ) ∈ S :=
begin
  change (0 : ℝ) * 0 ≤ 2,
  norm_num
end

In the first one, you ask Lean to expand the definition of S. In the second one, you do the expansion yourself, but you ask Lean to check that this is still the same question (this is the role of change)

[Florestan]

Great, thank you !

[Rémy Degenne]

And instead of using change you can also write rw set.mem_set_of_eq (docs#set.mem_set_of_eq). That lemma states a ∈ {a : α | p a} = p a.