goal with multiple ands

Stream: new members

[Nicolò Cavalleri]

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]

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

[Johan Commelin]

Or maybe repeat { split }?

[Nicolò Cavalleri]

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]

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

[Patrick Massot]

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

[Nicolò Cavalleri]

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]

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

[Nicolò Cavalleri]

Ok thanks

[Patrick Massot]

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