Bug: simp? does not take reverse directions into account

[sgouezel]

MWE:

import Std
def foo : Nat → Nat := sorry
theorem foo_eq_iff (z : Nat) : z = 17 ↔ foo z = 3 := sorry
theorem fail (z : Nat) (h : z = 17) : foo z = 3 := by
  simp? [← foo_eq_iff]
  exact h

The simp? works fine, but the suggestion is to use simp only [foo_eq_iff].

[JLimperg]

Caused by core: leanprover/lean4#2131

[dwrensha]

It looks like this is fixed.

import Batteries
def foo : Nat → Nat := sorry
theorem foo_eq_iff (z : Nat) : z = 17 ↔ foo z = 3 := sorry
theorem fail (z : Nat) (h : z = 17) : foo z = 3 := by
  simp? [← foo_eq_iff]
  exact h

The suggestion is now Try this: simp only [← foo_eq_iff]