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.

[Colin Jones ⚛️]

How would I prove this?

import Mathlib
example {x : ℕ} : x ∈ {1, 3} ↔ x = 1 ∨ x = 3 := by apply?

It's giving me an error due to metavariables which says "typeclass instance problem is stuck, it is often due to metavariables Membership ℕ ?m.394534".

[Ruben Van de Velde]

Is {1, 3} a Set, Finset, something else? Lean doesn't know

[Colin Jones ⚛️]

Ruben Van de Velde said:

Is {1, 3} a Set, Finset, something else? Lean doesn't know

How would I let lean know that it's a Finset?

[Bolton Bailey]

import Mathlib

example {x : ℕ} : x ∈ ({1, 3} : Finset ℕ) ↔ x = 1 ∨ x = 3 := by apply?

[Colin Jones ⚛️]

Okay that fixes the metavariable problem, but I still need help with the proof. The tactic apply? and rw? aren't helping me out.

[Colin Jones ⚛️]

Oh nevermind here's is how I proved it:

import Mathlib
example {x : ℕ} : x ∈ ({1, 3} : Finset ℕ) ↔ x = 1 ∨ x = 3 := by simp only [mem_singleton, mem_insert]

Thank you for your help

[Bolton Bailey]

FWIW, rw? gives the suggestion rw [@Finset.mem_insert], which is a good start.

[Bolton Bailey]

I agree it is not particularly helpful that apply? gives suggestions which are errors though.

[Kevin Buzzard]

import Mathlib

example {x : ℕ} : x ∈ ({1, 3} : Finset ℕ) ↔ x = 1 ∨ x = 3 := by aesop

[Kevin Buzzard]

import Mathlib

example {x : ℕ} : x ∈ ({1, 3} : Finset ℕ) ↔ x = 1 ∨ x = 3 := by simp