## Stream: new members

### Topic: focusing goals

#### Jiekai (Mar 27 2020 at 02:56):

Just learned to use begin ... end { ... } to structure tactics. The first begin ... end block focuses on the first goal. Is it possible to work on the second goal first bypassing the the first goal?

#### Alastair Horn (Mar 27 2020 at 02:58):

You could use sorry to move to the next goal

#### Bryan Gin-ge Chen (Mar 27 2020 at 03:01):

You can also use show:

example : ℕ × bool :=
begin
split,
show bool,
{ exact tt },
exact 1
end


or if you are using mathlib, swap:

import tactic.basic

example : ℕ × bool :=
begin
split,
swap,
{ exact tt },
exact 1
end


#### Scott Morrison (Mar 27 2020 at 05:28):

There's also work_on_goal n { ... }.

#### Scott Morrison (Mar 27 2020 at 05:28):

(This requires that you finish the goal by the end of the { ... } block.)

#### Scott Morrison (Mar 27 2020 at 05:29):

As well as swap n which swaps the 1st and nth goals, there's rotate n which rotates (left) n times.

#### Johan Commelin (Mar 27 2020 at 05:55):

Scott Morrison said:

(This requires that you finish the goal by the end of the { ... } block.)

Oooh, I thought it didn't... :bulb:

#### Mario Carneiro (Mar 27 2020 at 06:08):

That actually sounds like a misfeature. If you are going to close the goal, you can just use swap n, { ... }

#### Scott Morrison (Mar 27 2020 at 13:14):

Sorry, my mistake, work_on_goal does what everyone thought: you're allowed to make partial progress.

#### Johan Commelin (Mar 27 2020 at 13:15):

Pretty prescient of its author (-;

#### Johan Commelin (Mar 27 2020 at 13:15):

That guy is a genius!

Last updated: May 14 2021 at 04:22 UTC