simp does not use mem_singleton_iff

Stream: general

[Rémy Degenne]

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]

docs#set.mem_singleton_iff for reference

[Rémy Degenne]

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]

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]

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]

Ok, thanks for the help.