Odd simp? behavior

Stream: new members

[Michael Levenkov]

I have found some odd behavior with the simp? tactic. In certain cases, it closes the goal, but the "Try this" simp only command it suggests doesn't actually work to close the goal. A MWE is below. Is this a bug or just something strange happening on my end? On the latest version of mathlib if that matters.

import data.real.basic

example : 0 + 0 ^ 2 = 0 :=
begin
  simp?,
  -- simp? suggests simp only [add_zero, eq_self_iff_true, zero_pow'],
  -- which does not close the goal
  -- squeeze_simp suggests simp only [zero_pow', ne.def, bit0_eq_zero,
  -- nat.one_ne_zero, not_false_iff], which does close the goal
end

[Johan Commelin]

Unfortunately simp? is buggy. squeeze_simp is slower, but much more reliable.

[Johan Commelin]

I don't know how to fix simp? and I think everybody is just hoping that in a few months we'll be using the Lean 4 version where everything will "Just Work".