# Zulip Chat Archive

## Stream: new members

### Topic: tactics to simplify this?

#### Chris M (Jul 05 2020 at 05:36):

Are there good tactics to simplify this? in particular, the three line proof of the two cases is literally the same. Can I somehow just say "do this twice"? Also, can I combine the three `apply`

into one command?

```
import order.lattice
import tactic
variables {α : Type*} [lattice α]
variables x y z : α
-- BEGIN
example : x ⊓ y = y ⊓ x :=
begin
apply le_antisymm,
{
apply le_inf,
apply inf_le_right,
apply inf_le_left,
},
{
apply le_inf,
apply inf_le_right,
apply inf_le_left,
}
end
```

#### Alex J. Best (Jul 05 2020 at 05:37):

There are a few, you can do `all_goals { blah }`

to run the tactic blah on all goals, or use a semicolon instead of a comma after one tactic to run the subsequent tactic on all goals produced by the first.

#### Bryan Gin-ge Chen (Jul 05 2020 at 05:39):

There's also tactic#repeat for your first question. For your second, you can combine the `apply`

like this: `apply le_inf inf_le_right inf_le_left, `

but at that point you may as well just write `exact le_inf inf_le_right inf_le_left`

.

#### Alex J. Best (Jul 05 2020 at 05:39):

And apply is applying functions / implications backwards from the goal, so you can chain them like so

```
example : x ⊓ y = y ⊓ x :=
begin
apply le_antisymm;
{ apply le_inf inf_le_right inf_le_left, },
end
```

#### Yury G. Kudryashov (Jul 05 2020 at 05:59):

Or just `:= le_antisymm (le_inf inf_le_right inf_le_left) (le_inf inf_le_right inf_le_left)`

without `begin ... end`

#### Yury G. Kudryashov (Jul 05 2020 at 06:00):

If you use `lemma`

instead of `example`

, then you'll be able to `#print`

this lemma and see the actual expression generated by tactics.

#### Kevin Buzzard (Jul 05 2020 at 08:07):

There might also be a WLOG trick?

Last updated: May 06 2021 at 23:11 UTC