x ∈ {y, z} ↔ (x = y ∨ x = z)

Stream: Is there code for X?

[Bernd Losert]

I couldn't find anything like this

example {α : Type*} (x y z : α) : x ∈ {y, z} ↔ (x = y ∨ x = z) := by library_search

I'm not sure how to prove this either. Any tips?

[Yaël Dillies]

by simpshould do. Maybe it's even refl.

[Bernd Losert]

For some reason, I'm getting a don't know how to synthesize placeholder error in the y of x ∈ {y, z}.

[Ruben Van de Velde]

You probably need to tell lean what type the {} is, like ({y, z} : set ...)

[Bernd Losert]

Ah, that was it. Thanks.

[Violeta Hernández]

This seems not to exist, and it should! We could have set.mem_pair_iff, finset.mem_pair_iff, and multiset.mem_pair_iff.

[Yaël Dillies]

Yes because it's just mem_insert + mem_singleton.

[Bernd Losert]

I'm adding it to my "extras".

[Violeta Hernández]

Yaël Dillies said:

Yes because it's just mem_insert + mem_singleton.

True, but it's not any less useful because of this. Worth mentioning is that multiset.mem_insert doesn't exist, and we have mismatched names finset.mem_insert and set.mem_insert_iff, and finset.mem_singleton and set.mem_singleton_iff.

[Yaël Dillies]

But then you will also want to write mem_triple, mem_quadruple, etc... Consider lemmas as shortcuts to tactic calls. Here you're effectively suggesting to replace one tactic call by a countable number of lemmas. This is loosely analogous to how we don't write down all inequalities between any two natural numbers, but instead use norm_num to generate them. This is a time vs space tradeoff.

[Violeta Hernández]

I would imagine that pairs are much more common than triples or higher n-tuples.

[Violeta Hernández]

We can just stop at two

[Yaël Dillies]

I see no point in doing so, because you won't ever need the lemmas in reverse (as opposed to docs#Inf_pair for example), so you can always just call one tactic that'll solve it.

[Bernd Losert]

This reminds me of those associative/commutative lemmas that involve 2,3,4 variables. I didn't expect specialized versions for e.g. 4 variables - I was expected some generalized tactic that handles all cases, but I was wrong.

[Yaël Dillies]

If you're thinking about op_op_op_comm lemmas, we have them because this specific pattern shows up all the time when doing convexity (and surely other things) and it's not always true for the same reasons (eg the sub version needs special treatment, and the add-tsub one is even worse).

[Yaël Dillies]

However, we do not have mul_assoc3 : ((a * b) * c) * d = a * (b * (c * d)) because this is always true for the same reasons and doesn't need a complicated rewriting scheme.

[Bernd Losert]

All these special concesions makes things complicated in my opinion, but c'est la vie.

[Yakov Pechersky]

For a left associative commutative op, like and or add, simp [and.comm, and.assoc, and.left_assoc] will normalize both sides of an equality

[Violeta Hernández]

Bernd Losert said:

This reminds me of those associative/commutative lemmas that involve 2,3,4 variables. I didn't expect specialized versions for e.g. 4 variables - I was expected some generalized tactic that handles all cases, but I was wrong.

We have rw_assoc but I've found it very finicky to use, and it doesn't deal with commutativity.