Equivalent to `_match_1` in Lean 4

Stream: lean4

[Arien Malec]

Apologies if this is Mathlib4 material.

I have Lean 3 code that makes use of _match_1 (which, if I understand, refers to the first branch of a match statement) and don't know how to translate to a Lean 4 equivalent...

[Adam Topaz]

I think it should just be match_1

[Kevin Buzzard]

I'm not sure that that lean 3 code is hygienic.

[Mario Carneiro]

it probably either corresponds to some kind of let rec definition, or something that rewrites a match expression after declaration (which should not be necessary in lean 4 anymore, things like simp will automatically work directly on match expressions)

[Arien Malec]

It’s a giant sequence of function calls that create match expressions. Requires more invasive surgery to do this one I guess.