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