Some special behavior of rw tactic

[znssong]

The following code would fail at exact test.symm:

axiom α : Type
axiom β : Type
axiom p : α → Prop
axiom q : α → Prop
axiom r : α → Prop
axiom rp : {x : α} → r x ↔ p x
axiom rq : {x : α} → r x ↔ q x
axiom f : (x : α) → p x → β
axiom g : (x : α) → q x → β
axiom y : β
axiom fx : (x : α) → (hx : r x) → f x (rp.mp hx) = g x (rq.mp hx)
example (x : α) (hx : r x) : g x (rq.mp hx) = y := by
  have test : y = f x (rp.mp hx) := by sorry
  have test₂ : 0 = 0 := by rfl
  rw [fx _] at test
  exact test.symm

If remove test₂, it would works. I posted this phenomenon to the Zulip channel at https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/A.20subtle.20detail.20about.20Lean.20.60rw.60.20tactic. I also posted some analysis of Lean source code on the thread, and Eric Wieser suggested me to file a bug.

[Kha]

I think this is a duplicate of #4885?