(d)simp at goal

Stream: mathlib4

[Adam Topaz]

Often in Lean3 it is convenient to use simp at ⊢ h. The ⊢ seems to be unacceptable in lean4. Do we have some way to do this in lean4?

[Heather Macbeth]

I've missed this too.

[Yakov Pechersky]

Not a total solution, but how about simp_all?

[Adam Topaz]

Well, we can still do simp at *, which does less than simp_all, but I still want to have control over what I simplify.

[Adam Topaz]

We also don't have dsimp_all

[Joël Riou]

I had noticed that also, but if you change the order, it works: (d)simp at h ⊢.

[Kyle Miller]

The at location syntax requires that ⊢ comes last

[Adam Topaz]

Aha! Okay thanks!