## Stream: general

### Topic: simp does not use mem_singleton_iff

#### Rémy Degenne (Feb 16 2021 at 16:12):

The lemma set.mem_singleton_iff is marked as simp, but simp does not use it in the following example:

import data.set.basic

example {α} (s t : α) (ht : t ∈ ({s} : set α)) : t = s :=
set.mem_singleton_iff.mp ht -- succeeds

example {α} (s t : α) (ht : t ∈ ({s} : set α)) : t = s :=
by simp [ht] -- fails


How can I find out what happens here? I don't know how to get information about what simp tries. Am I wrong to expect simp to work here?

#### Eric Wieser (Feb 16 2021 at 16:12):

docs#set.mem_singleton_iff for reference

#### Rémy Degenne (Feb 16 2021 at 16:24):

example {α} (s t : α) (ht : t ∈ ({s} : set α)) : t = s :=
by simpa using ht -- succeeds


But simpa works. I guess that the hypothesis ht can be simplified by simpa to match the goal. On the other hand the goal is already in its most simplified form and simp [ht] does not modify the hypothesis ht, which then never matches with the goal.

#### Yakov Pechersky (Feb 16 2021 at 16:29):

Correct. by simpa using ht simplifies both the goal and ht in a way to get them to align, and no further. So very similar to how this works:

example {α} (s t : α) (ht : t ∈ ({s} : set α)) : t = s :=
by { simp at ht, exact ht }


#### Yakov Pechersky (Feb 16 2021 at 16:29):

Other possibilties are:

example {α} (s t : α) (ht : t ∈ ({s} : set α)) : t = s :=
by rwa set.mem_singleton_iff at ht -- succeeds

example {α} (s t : α) (ht : t ∈ ({s} : set α)) : t = s :=
by rwa ←set.mem_singleton_iff -- succeeds


#### Rémy Degenne (Feb 16 2021 at 16:42):

Ok, thanks for the help.

Last updated: May 14 2021 at 03:27 UTC