`If` inside `conv`

Prerequisites

• [ x] Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

if doesn't work inside of conv mode.

Steps to Reproduce

import Lean

open Lean

opaque foo : Int → Int
axiom foo.pos (x : Int) (h : x ≥ 0) : foo x =  1
axiom foo.neg (x : Int) (h : ¬(x ≥ 0)) : foo x = -1

example : foo = λ (x : Int) => if x ≥ 0 then 1 else -1 :=
by

  conv =>
    lhs; enter [x]

    if h : x ≥ 0 then
      rw [foo.pos x h]
    else
      rw [foo.neg x h]

  done

Expected behavior: This proof to work

Actual behavior: if tactic is not accepted, giving "expected command" error.

Reproduces how often: 100%

Versions

Lean (version 4.0.0-nightly-2023-01-21, commit a125a36bcc79, Release)
Windows 10.

Additional Information

On the Zulip Chat, Tomas Skrivan posted a working implementation for if and match inside of conv, including the example proof above:
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/If.20and.20match.20in.20conv.20mode

Start with the self-contained reproduction in the issue and compare it with the working implementation linked in the Zulip discussion. The work is done when the example proof accepts the if tactic inside conv mode, including both branches shown.