simp? message unhelpful in some case " Try this: simp only"

Stream: new members

[Nicolas Rolland]

I am wondering why there is no indication in the second case below.
(I tried with 4.0 and 4.3.0-rc1 it seems the same)

import Mathlib

def MySet2 : Set ℕ := {1,2}
example : 1 ∈ MySet2 := by
  rw [MySet2]
  simp?  -- Try this: simp only [Set.mem_singleton_iff, Set.mem_insert_iff]

example : 1 ∈ MySet2 := by
  rw [MySet2]
  rw [@Set.mem_insert_iff]
  simp? -- Try this: simp only

[Ruben Van de Velde]

Well, simp only seems to solve it?

[Nicolas Rolland]

Yes, but I imagined it would tell me by which lemma, just like in the other case.

isn't simp only [lemma, lemma'm ..] supposed to restrict simp. I imagine simp only without anything just does simp

https://leanprover-community.github.io/extras/simp.html

[Patrick Massot]

No, it does simp only with an empty list.

[Eric Wieser]

simp? (config := {decide := false}) gives you a list of lemmas

[Eric Wieser]

(this will be the default in the next lean release)

[Mauricio Collares]

This is probably clear from Eric's message, but just to be sure: simp only is not the same as simp, but in the current version of Lean both simp only and simp try to use decidability instances. Since decide closes your goal, so does simp only. simp (config := {decide := false}) only does not close your goal.