simplify the context of a hole before displaying it?

Stream: lean4

[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?

[Leonardo de Moura]

Have you tried to use tactic mode? Suppose you have a hole _ that cannot be synthesized, you can replace it with (by done), where done is a tactic that fails when there are unsolved goals. Then, you can use tactics to simplify the context.
Example: (by clear h; simp; done). Note that simp is not Coq simpl since it will use theorems marked with [simp] as rewriting rules, but you can use simp only instead. Btw, simp only [foo] unfolds foo. simp only [foo] at h unfolds foo at hypothesis h.

[Jason Gross]

I'm now trying this out; thanks!