match in tactic mode

Stream: general

[Eric Rodriguez]

am I just meant to avoid match in tactic mode? I want to do something like this:

example {n : ℕ} (hn : 0 < n) : false :=
begin
  have hn' : 2 < n :=
  match n with
    0 := begin /- hn : 0 < n, NOT 0 < 0 -/ sorry end,
    (n+1) := sorry
  end,
end

I could just use cases n, I know, but I have like 4 cases and I'd rather structure it this way if I can

[Alex J. Best]

You can do

example {n : ℕ} (hn : 0 < n) : false :=
begin
  have hn' : 2 < n := match n, hn with
    0, h := begin /- hn : 0 < n, NOT 0 < 0 -/ sorry end,
    (n+1), h := sorry
  end,
end

it seems, but I've never really tried this, or seen anyone do it so I have not idea how well it works in practice

[Reid Barton]

Also, match works the same way in term mode too

[Alex J. Best]

The only instance of this I can see in mathlib is src#pell.eq_pell

[Alex J. Best]

Thats term mode though still

[Eric Rodriguez]

I'll try this out, thanks! Didn't know it didn't explicitly rewrite automatically unlike the eqn compiler...