simp? and squeeze_simp

[jcommelin]

simp? outputs a Try this: simp only [foo, bar] message using a different mechanism than squeeze_simp.
Hopefully it is more reliable and faster.

Eventually simp? could replace squeeze_simp, but at the moment squeeze_simp support more variants of simp in its Try this output:

• squeeze_simpa deals with simpa
• squeeze_simp can work with extra config options, such as squeeze_simp { contextual := tt }

[bryangingechen]

Here's an example from Zulip where simp? doesn't include all necessary lemmas:

import data.setoid.partition

example {α : Type} {r : setoid α} (a : α): ∃! (b : set α), b ∈ r.classes ∧ a ∈ b :=
begin
  convert @setoid.classes_eqv_classes _ r a,
  simp? -- Try this: simp only [eq_self_iff_true]
end

squeeze_simp returns simp only [exists_prop, exists_unique_iff_exists], which does work.

[YaelDillies]

Lean 4 is around the corner and avoids the problem completely, so I think it's not worth fixing anymore.