case-split in emacs mode?

Stream: new members

[Jason Gross]

Is there a way to get emacs to insert a case split for me, a la match! of company-coq or C-c C-s of Agda's emacs mode?

[Johan Commelin]

In Lean3 there are hole commands. No idea whether they are implemented for Lean4 already

[Jason Gross]

https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Is.20there.20a.20way.20to.20build.20proof.20interactively/near/228710628 suggests that they are not, alas. Thanks for the pointer, though!