breaking up a long conjunction

Stream: new members

[Michael Beeson]

There has to be a better way to break up a conjunction of four conjuncts than this:

  cases h13 with h15 h16,
  cases h16 with h17 h18,
  cases h18 with h18 h20,

[Mario Carneiro]

Have I mentioned that rcases is awesome yet today?

[Mario Carneiro]

tactic#rcases

[Mario Carneiro]

your example would be rcases h13 with ⟨h15, h17, h18, h20⟩

[Kenny Lau]

don't name them as hXX: instead name them as hxab if the variables involved are x and a and b

[Michael Beeson]

Thank you.

[Michael Beeson]

And similarly, if my goal is a conjunction with four conjuncts, how do a split into four goals all at once instead of three different "split" commands?

[Bryan Gin-ge Chen]

Something like refine ⟨_, _, _, _⟩ should work.

[Rob Lewis]

Or repeat {split}

[Anatole Dedecker]

repeat {split} doesn't really work because the "splittable "part is now the second goal, so it's not focused anymore.

[Adam Topaz]

I think repeat applies the tactic to all goals, right?

[Rob Lewis]

The n+1st iteration of the tactic will apply to all goals generated by the nth.

[Anatole Dedecker]

Oh indeed, my bad. Is that new, or am I just creating memories out of nowhere ?

[Adam Topaz]

There is also iterate which works only on the first goal, if I recall correctly.