a or b or c or d

Stream: general

[Chris Hughes]

If I have a or b or c or d, can I split into four goals in one go?

[Kenny Lau]

rcases [identifier] with H | H | H | H

[Kenny Lau]

I can't interpret "split into four goals". If it's a hypothesis then you get four hypotheses. If it's a goal then you get one goal.

[Simon Hudon]

Alternatively, casesm* [_ ∨ _] also helps.

[Chris Hughes]

Thanks

[Mario Carneiro]

there is no brackets in rcases

[Kenny Lau]

[identifier] is a placeholder

[Mario Carneiro]

hm, it's hard to tell the difference between meta notation and lean notation... we need more brackets

rcases ⟅identifier⟆ with H | H | H | H

[Ali Sever]

On a similar note, if you want to prove ∃ a b c, ... is there a way to do something like existsi a b c? I triedrepeat {constructor} for fun, and I was surprised to see lean perfectly guess what a, b and c were.

[Ali Sever]

Also, when I used constructor, three times, lean did not guess them.

[Simon Hudon]

you could also do existsi [a,b,c] if you want to specify the witnesses yourself.

[Ali Sever]

Ah thank you, I had not tried those brackets. Is there a rule to know which type is used where?

[Simon Hudon]

Which types do you mean?

[Kevin Buzzard]

which type of bracket?

[Kevin Buzzard]

I guess you can look at the documentation for the tactic...

[Kevin Buzzard]

(by hovering over it)

[Nicholas Scheel]

brackets are syntax, so I don‘t think they can have _types_, nor kinds, nor sorts ... must be varieties, I guess? ;)

[Nicholas Scheel]

we’re going to run out of variants of words soon to describe these things