## Stream: general

### Topic: mem_eq_self

#### Kevin Buzzard (Dec 02 2018 at 17:58):

Harder than I expected!

theorem mem_eq_self {α : Type*} (a : α) : a ∈ {x : α | x = a} := sorry


#### Kevin Buzzard (Dec 02 2018 at 17:58):

Took me three attempts!

#### Kenny Lau (Dec 02 2018 at 17:59):

ok too me two attempts

theorem mem_eq_self {α : Type*} (a : α) : a ∈ {x : α | x = a} := eq.refl a


#### Kevin Buzzard (Dec 02 2018 at 18:00):

@[refl] theorem mem_eq_self {α : Type*} (a : α) : a ∈ {x : α | x = a} := eq.refl a

example : 3 ∈ {x : ℕ | x = 3} := by refl


@Reid Barton is this your suggestion? To those that didn't follow the other thread, the point is that without tagging mem_eq_self as refl, by refl doesn't work for the example.

#### Kevin Buzzard (Dec 02 2018 at 18:01):

example : 3 ∈ {x : ℕ | 3 = x} := by refl now works too. I don't really understand what is going on here.

#### Kenny Lau (Dec 02 2018 at 18:03):

-- all fail
example : 3 ∈ {x : ℕ | x = 3} := by refl
example : 3 ∈ {x : ℕ | x = x} := by refl
example : 3 ∈ {x : ℕ | 3 = 3} := by refl
example : 3 ∈ {x : ℕ | 3 = x} := by refl

@[refl] theorem mem_eq_self {α : Type*} (a : α) : a ∈ {x : α | x = a} := eq.refl a

-- all work
example : 3 ∈ {x : ℕ | x = 3} := by refl
example : 3 ∈ {x : ℕ | x = x} := by refl
example : 3 ∈ {x : ℕ | 3 = 3} := by refl
example : 3 ∈ {x : ℕ | 3 = x} := by refl


#### Kevin Buzzard (Dec 02 2018 at 18:04):

example : 3 ∈ {x : ℕ | 3 = 3} := by refl -- Doesn't that say 3 \in set.univ? Why is that by refl?

#### Kenny Lau (Dec 02 2018 at 18:05):

no, set.univ is true

#### Kevin Buzzard (Dec 02 2018 at 18:05):

We're evaluating lam x, 3 = 3 at x=3 :-)

#### Kevin Buzzard (Dec 02 2018 at 18:06):

so indeed it's refl

Last updated: May 08 2021 at 18:17 UTC