Potential PR to implement ApplyNewGoals in lean4

Stream: lean4

[Edward Ayers]

Hi I've started on a TODO in core Lean to implement ApplyNewGoals. This means that we can implement fapply and eapply in mathlib. I've read https://github.com/leanprover/lean4/blob/master/CONTRIBUTING.md and it indicates that I should just check on here first whether this is a suitable PR.

[Edward Ayers]

I think the main design challenge is deciding on what the syntax should be for apply config options in tactics

[Edward Ayers]

I've added an RFC https://github.com/leanprover/lean4/issues/1045

[Leonardo de Moura]

Thanks for submitting the PR. I will comment there.