set equality

Stream: Is there code for X?

[Bernd Losert]

I'm looking for the lemma that says that two sets are equal if and only if they have the same members. I can't seem to find it, not even with library_search.

[Ruben Van de Velde]

That's called extensionality, so probably set.ext or use the ext tactic

[Kalle Kytölä]

import set_theory.cardinal.basic -- import something

example (X : Type*) (A B : set X) : A = B ↔ (∀ x, x ∈ A ↔ x ∈ B) :=
by library_search -- Found: `refine ext_iff`

[Bernd Losert]

Ah, I see it now. I wonder why it gave me such a hard time.

[Bernd Losert]

I was trying this:

example (s t : set α) (heq : s = t) : ∀ x, x ∈ s ↔ x ∈ t := by library_search

[Kyle Miller]

That one is true because you can substitute t for s (by subst heq, cases heq, simp [heq], etc.)

[Ruben Van de Velde]

In that direction, subst heq, probably also works... Yeah, that

[Bernd Losert]

I see. I was trying simp alone and it wasn't working.

[Kevin Buzzard]

simp proves equalities and iff statements but it doesn't look in your tactic state, so simp alone won't know about heq. Probably simp [heq] would work?