Zulip Chat Archive

Stream: general

Topic: mem_eq_self


view this post on Zulip Kevin Buzzard (Dec 02 2018 at 17:58):

Harder than I expected!

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

view this post on Zulip Kevin Buzzard (Dec 02 2018 at 17:58):

Took me three attempts!

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Kenny Lau (Dec 02 2018 at 18:05):

no, set.univ is true

view this post on Zulip Kevin Buzzard (Dec 02 2018 at 18:05):

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

view this post on Zulip Kevin Buzzard (Dec 02 2018 at 18:06):

so indeed it's refl


Last updated: May 08 2021 at 18:17 UTC