Is there a way to normalize the current goal like in Agda?

Stream: lean4

[André Muricy Santos]

In a hole in Agda, one can do C-c C-. to show the type of a current goal, but one can also do C-y C-. to show the type normalized - that is all computations that Agda can figure out about a type are performed. If some type is a result of a complex type-level function or something, the first command will show all these calls, and the second one will actually show the result. Often it reduces to just a sigma or pi type. In Lean I'm always looking at the infoview and performing these computations in my head or typing out patterns blindly to see the squiggles disappear.

[Jireh Loreaux]

This is not exactly what you want, but I think the closest we have is probably dsimp.

[Jireh Loreaux]

But that requires that the relevant definitional lemmas are tagged @[simp].

[Kyle Miller]

Are you looking for whnf or reduce? These are in Mathlib.Tactic.DefEqTransformations (which is imported by nearly anything in mathlib via Mathlib.Tactic.Common), but they might make their way into core Lean at some point.

[Jireh Loreaux]

ooh, I didn't know we had those as tactics