rewriting an expression without writing it again

Stream: new members

[S L]

suppose i have a very long expression e in conversion mode, and i want to rewrite it into f. I can do this by rw [show e = f from by ...], but i don't want to write e again (and sometimes simply copying it from the infoview doesn't work because it lacks certain context). Is there a way to not write e again, something like rw [show _ = f from by ...]?

[Kyle Miller]

(#mwe is helpful, since that grounds the suggestions with something concrete)

conv mode has an equal f => ... block (available in Batteries) that seems like what you're looking for. https://leanprover-community.github.io/mathlib4_docs/docs/Conv/Guide.html has a list of available tactics, though it's somewhat out of date.

[Zhang Qinchuan]

If you can use the latest mathlib, there is change ?_:

import Mathlib

example (a b c : ℕ) : a + b = c := by
  change ?x = c
  let x : ℕ := ?x -- x = a + b
  sorry