simplify the context of a hole before displaying it?

Stream: new members

[Jason Gross]

I have a hole where Lean says "don't know how to synthesize placeholder" and lists a bunch of things in the context. I want to run the equivalent of Coq's simpl tactic in the context and see the result. (I'd be willing to explicitly name the things I want to unfold if that's better, and, in this case, I'd also be fine with fully normalizing everything). How do I do this? (I'm in Lean 4 if it matters. (I'm not sure whether to ask newbie questions that seem not specific to Lean 4 here or over in the #lean4 channel...))

[Bryan Gin-ge Chen]

(I don't know how to answer your question, but I think newbie questions about Lean 4 should probably go in the #lean4 stream. For one, I think the Lean 4 developers are only watching that stream and not this one.)

[Mario Carneiro]

@Jason Gross The lean analogue of Coq's simpl is simp, and simp doesn't exist yet in lean 4, last I checked, but they are working on it so things might have changed since then