`rw?` regression from `v4.7.0`

[Seasawher]

Description

in Lean v4.7.0 and mathlib 4.7.0, this code success: (see https://github.com/Seasawher/v470playground/blob/main/V470playground/Basic.lean)

import Mathlib.Tactic

variable (n m : Nat)

example (h : n + m = 0) : n = 0 ↔ m = 0 := by
  /-
  Try this: rw [propext (eq_zero_iff_eq_zero_of_add_eq_zero h)]
  -- "no goals"
  -/
  rw?
  done

But in v4.8.0-rc1, we get "unsolved goals" error.

Additional Information

I am unable to find an example without mathlib dependencies. rw? is not in Lean v4.7.0.

Impact

Add :+1: to issues you consider important. If others are impacted by this issue, please ask them to add :+1: to it.

[semorrison]

Oh, sorry, this is a known regression, that rw? no longer works on Iff goals. No immediate plans to work on this.

[semorrison]

(But I'd review a PR.)