rewrite in match head

Stream: lean4

[Vasilii Nesterov]

Hi there! Is there any way to use rw/simp/something else inside match-expression's head keeping the rest of expression the same? conv isn't able to navigate there.

[Joachim Breitner]

Can you give a #mwe?

For simp I plan to add a -underLambda flag that would prevent it from rewriting the alternatives of a match.

[Joachim Breitner]

That said, in this small example, I can use the arg 2 conv tactic to navigate to the match target (one has to know that arg 1 would select the motive of the matcher):

example (o : Option Nat) (h : o = some 4) (x : Nat) : (match o with | some n => n+1 | none => 0) = x := by
  conv =>
    lhs
    arg 2
    rw [h]
  dsimp

[Vasilii Nesterov]

Thank you! The problem was that I was using the old version of Lean.