Convert dite to tactic

Stream: new members

[Felipe]

I'm trying to get better at writing tactics. One pattern I end up using often is:

by
  ...
  exact
    if h: someCondition
    then by <tactics using h>
    else by <other tactics using h>

Is there a way to 'lift' the dite into tactics directly?

[Junyan Xu]

by_cases h : someCondition