should `rw` elaborate using `elabTermForApply`?

Stream: lean4

[Jovan Gerbscheid]

When you pass a constant to the rewrite tactic, the rewrite tactic fills in the hypotheses with metavariables. However, direct implicit arguments are already filled in with metavariables by elaboration. In the apply tactic this is avoided by using elabTermForApply. For example, in

abbrev fakeLE : LE Nat := ⟨(· = ·)⟩

example : (letI := fakeLE; 4 ≥ 2) := by
  rw [@ge_iff_le]

it only works if you write the @. Otherwise, the metavariable ?m : LE Nat will be synthesized with type class search. This problem appears in Mathlib for example in https://github.com/leanprover-community/mathlib4/blob/8aa3ccd118e52fd65e13435d2d1c743c5a129d75/Mathlib/CategoryTheory/Monoidal/Rigid/Basic.lean#L545.

cc @Kyle Miller