the order of goals

Stream: new members

[Alex Zhang]

If I have several goals in an info view, how can I choose a goal to do first?

[Adam Topaz]

tactic#show or tactic#swap

[Kevin Buzzard]

You shouldn't have several goals in scope though, it makes your code much harder to read. Use { } to keep your number of goals down to 1.

[Alex Zhang]

I mean, if I have two goals, use {} will automatically choose the first.

[Eric Wieser]

Do you have a reason for not wanting to solve that goal first? If you just don't want to solve it right now, you can use { sorry }, to put it off till later

[Eric Wieser]

The only other situation I can think of is when the first goal has metavariables that you want to fill in - but usually there's a way to get the goals in the right order to start with in those cases.

[Yakov Pechersky]

Even if the second has metavariables, it is likely solvable

[Mario Carneiro]

case is also a good way to select goals, especially after induction, which will label the goals

[Mario Carneiro]

swap n will bring the nth goal to the front

[Mario Carneiro]

work_on_goal n will apply a tactic to the nth goal

[Mario Carneiro]

finally tac; [skip, skip, tac2] can be used to different tactics to the goals coming out of another tactic

[Eric Wieser]

rotate hadn't been mentioned yet