intro hyp; rw [hyp] at foo

Stream: lean4

[Martin Dvořák]

Let's say x ≠ y is my goal.
I typically want to start my proof as follows:

intro hyp
rw [hyp] at foo

Is there a single tactic that performs these two lines?

[Kevin Buzzard]

rintro rfl if you're lucky

[Martin Dvořák]

Is rintro rfl equivalent to the following?

intro hyp
rw [hyp] at *
clear hyp

[Scott Morrison]

No, it is more like

intro hyp
subst hyp

[Scott Morrison]

In particular it is only going to work if one side of hyp is a free variable.

[Damiano Testa]

Maybe by_contra should try subst as well.