Is there a tactic similar to “replace with” in Coq?

Stream: lean4

[Qiancheng Fu]

In Coq, the ‘replace m with n’ tactic asks for a proof of ‘m = n’ and replaces all occurrences of ‘m’ in the current goal with ‘n’. Is there a similar tactic in Lean?

[Henrik Böving]

You can use subst on an equality proof

[Qiancheng Fu]

I will have to manually clear the equality proof from my context after the substitution right?

[Joachim Breitner]

conv tactic equals_to should help here.

Ah, but that doesn't replace all occurrences

[Joachim Breitner]

Then there is the idiom rw [show m = n by …]

[Kevin Buzzard]

Qiancheng Fu said:

I will have to manually clear the equality proof from my context after the substitution right?

Not with subst, although subst only works if one side is a variable.

[Qiancheng Fu]

Joachim Breitner said:

Then there is the idiom rw [show m = n by …]

The rw [show m = n by ...] is fairly close to what I want, though when writing the proof inside by ..., the goal doesn't seem to be updated. I've elected to just write my own tactic that implements the behavior of Coq's replace with.

[Kyle Miller]

A related idiom is using a named metavariable for the proof, like

example (m n : Nat) : m + 2 = n + 3 := by
  rw [show m = n from ?pf]
  case pf =>
    sorry

[Qiancheng Fu]

Ahh, that’s nice!

[Miguel Marco]

I usually do that kind of things using

example (m n : Nat) : m + 2 = n + 3 := by
  have hmn : m = n
  · sorry
  rw [hmn]

or if you prefer to do it in a different order:

example (m n : Nat) : m + 2 = n + 3 := by
  suffices hmn : m = n
  · rw [hmn]
   ...
  · sorry

[Joachim Breitner]

That’s a natural thing to do, and probably one of the earliest approach users find. What I don’t like about this is that it clutters the infoview with these additional assumptions hmn that I only meant to use once.