## Stream: new members

### Topic: goal with multiple ands

#### Nicolò Cavalleri (Jun 22 2020 at 14:32):

Is it possible to split a goal of the form A∧B∧C∧...∧H in subgoals A, B, ..., H with a single tactic?

#### Johan Commelin (Jun 22 2020 at 14:32):

refine \< _, _, _, _ \>

#### Johan Commelin (Jun 22 2020 at 14:33):

Or maybe repeat { split }?

#### Nicolò Cavalleri (Jun 22 2020 at 14:39):

Johan Commelin said:

Or maybe repeat { split }?

This looks cool as it does not require me to count subgoals but is a bit aggressive as it splits not only ∧  but also other goals (like the ones with \exists). Do you know if there is a way to only make it split the ∧ s?

#### Patrick Massot (Jun 22 2020 at 14:40):

This would be a very nice exercise after reading the tactic writing tutorial.

#### Patrick Massot (Jun 22 2020 at 14:41):

I promise you'll enjoy doing it, and you'll be happy with what you'll have learned.

#### Nicolò Cavalleri (Jun 22 2020 at 14:41):

Patrick Massot said:

This would be a very nice exercise after reading the tactic writing tutorial.

You mean the one in the natural numbers game or in the book?

#### Patrick Massot (Jun 22 2020 at 14:41):

https://leanprover-community.github.io/extras/tactic_writing.html

Ok thanks

#### Patrick Massot (Jun 22 2020 at 14:47):

Don't hesitate to ask questions if you get stuck. Simon will answer them.

Last updated: May 13 2021 at 18:26 UTC