## 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