{"cmd": "#eval 1 + 1"}

{"cmd": "def foo : (fun ((x, y, z) : Nat × Nat × Nat) => x = x) = fun x => True := by sorry", "env": 0}

{"tactic": "simp", "proofState": 0}

Expected: Goal closed
Actual: {"message": "Lean error:\nunknown constant 'foo.match_1'"}

This comes down to 6651502 which eliminates both foo and foo.match_1 from the env.

I'm not sure why the InfoTree env has foo actually, but I've made a question about this on Zulip.