mem_eq_self

Stream: general

[Kevin Buzzard]

Harder than I expected!

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

[Kevin Buzzard]

Took me three attempts!

[Kenny Lau]

ok too me two attempts

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

[Kevin Buzzard]

@[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]

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

[Kenny Lau]

-- 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]

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

[Kenny Lau]

no, set.univ is true

[Kevin Buzzard]

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

[Kevin Buzzard]

so indeed it's refl