cases/induction code action generate only necessary arms

Stream: lean4

[Shreyas Srinivas]

I was wondering if the cases and induction code action could generate only the arms that remain unproved. A common pattern in my proofs is something like

intro h
cases f with (simp_all[..., h])

which leaves only a few cases goals unsolved. But the code action generates all case arms. So I usually have to delete the unnecessary case arms one by one. I was wondering if it is possible for the code actions to only generate match arms for the unclosed goals.