simp? failure

Stream: mathlib4

[Sebastien Gouezel]

simp? fails to take into account reverse directions:

import Mathlib.Data.Nat.Basic

def foo : ℕ → ℕ := sorry
theorem foo_eq_iff (z : ℕ) : z = 17 ↔ foo z = 3 := sorry

theorem fail (z : ℕ) (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].

[Sebastien Gouezel]

Issue registered at https://github.com/leanprover-community/mathlib4/issues/7182

[Alex J. Best]

simp? is defined in Std so really this should best be reported there as

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

[Sebastien Gouezel]

Ah, I hadn't noticed it was in std. Let me port the issue there. Thanks!