Idiomatic match vs cases

Stream: new members

[Mark Fischer]

Sometimes it's clear when one makes more sense than the other. If you need pattern matching, you'll need match. If you're relying on the shape of your type as a shorthand (like cases d <;> simp), then you'll need cases.

What about places where either will do?
Are there style/other considerations at play?

[Henrik Böving]

I'd say you will generally see cases and rcases dominate in proofs

[Kyle Miller]

I know match generalizes the context differently from how cases does (cases is generally "better" at this I think), though I don't immediately have an example of this.

There's not much match in tactic proofs out there yet, since it's new to Lean 4. For inductive proofs though, there are lots of examples of a match term since it can be a lot easier to do induction via recursion. That gives you the full power of the termination checker, which figures out what you actually are inducting on.

[Mark Fischer]

Sounds like cases is typically preferred when either would work.