## Stream: new members

### Topic: Prove set membership

#### Florestan (Mar 11 2021 at 15:18):

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 (Mar 11 2021 at 15:29):

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 (Mar 11 2021 at 15:31):

Great, thank you !

#### Rémy Degenne (Mar 11 2021 at 15:33):

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.

Last updated: Dec 20 2023 at 11:08 UTC