Most Lean-onic way to do `byCases` in tactic mode

Stream: new members

[Lars Ericson]

I am doing Exercise 1 at the end of the Tactic Mode chapter in the TPIL book. I am working on an example that requires Classical. I want to do a byCases proof. I learned about byCases in the earlier term-style chapters of the book. I see cases in the tactic mode chapter but it doesn't seem to be byCases. Here is my approximation of byCases in tactic mode. I apply Or.elim on em p where p and ¬p is what I want to do cases on:

example : (p → q ∨ r) → ((p → q) ∨ (p → r)) := by
  intro h
  apply Or.elim (em p)
  . admit
  . admit

Is there a more Lean-onic way to express this? I.e. something like a byCases tactic for tactic mode, not term mode?

[Matt Diamond]

I think the tactic you're looking for is by_cases (docs#Classical.«tacticBy_cases_:_»)

[Lars Ericson]

It would be helpful to show docs#by_cases and docs#by_contradiction for tactic mode proofs in the More Tactics section of the Tactics chapter, to mirror the presentation of docs#Classical.byCases and docs#Classical.byContradiction for term mode proofs in the Classical section of the Propositions and Proofs chapter.

[Martin Dvořák]

I've also seen if then else in tactic mode lately.