tactics to simplify this?

Stream: new members

[Chris M]

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]

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]

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]

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]

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]

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]

There might also be a WLOG trick?