rw? sometimes inserts propext in suggestions

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

The suggestions from rw? can contain unnecessary propext calls

Context

Found on zulip

Steps to Reproduce

import Mathlib
lemma theo1 (p : ℕ) (hp : p > 3) (hprime : Nat.Prime p) : ¬ (2 ∣ p) := by
  -- rw? finds:
  rw [propext (Nat.dvd_prime hprime)]

Expected behavior: output does not contain propext (for this suggestion, at least)

Actual behavior: it does

Versions

4.11.0-rc2 on live.lean-lang.org.

Additional Information

Apologies for the lack of reduction, I may have time to do that next week.

Impact

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

Start by reducing the rw? example in the Steps to Reproduce section and testing it against the latest nightly release. Investigate why the suggestion includes propext; done means a reproducible case and a suggestion that omits the unnecessary propext call.