Multiple cases at once

Stream: Is there code for X?

[Marcus Rossel]

I have three optional instances t1 t2 t3 : option nat and need to prove something about them case by case.
Is there a tactic that automatically produces all cases at once, such that all combinations of the instances being some _ or none are covered?
(That would be 8 goals in this example).

[Eric Wieser]

cases t1; cases t2; cases t3, should do the job

[Marcus Rossel]

Ahh I should have thought of that myself, thanks!

[Scott Morrison]

There is also a case_bash tactic somewhere... Apparently undocumented.

[Eric Wieser]

I think this should work too, but my orange bars are stuck so I can't confirm:

import tactic

example : ∀ (t1 t2 t3 : option nat), true :=
begin
  rintros (a|_) (b|_) (c|_),
end