## Stream: new members

### Topic: Unfolding set constructor notation

#### Keefer Rowan (May 16 2020 at 13:59):

I understand what set constructor notation is doing, but I can't figure out where it is defined so I can't figure out what definition to tell lean to unfold. I know how to find definitions of simple notation like #print notation * but I don't know how to do it for complicated notation like the set constructor notation. So where is set constructor notation defined/how can I unfold it?

#### Kevin Buzzard (May 16 2020 at 14:01):

I totally agree that this is annoying and frustrating. I went through a phase of trying to understand what Lean was by unfolding everything in sight and set notation, and stuff like there exists and inf stuff are very hard to see through: they are just some "scoped something". But in the set case you can just set_option pp.notation false and find out what's going on. It's something like set_of that you're looking for.

#### Keefer Rowan (May 16 2020 at 14:04):

Thanks! Your answer implies that I usually shouldn't have to unfold stuff to prove something, is there a better way to show something like:

{a : α | a ∈ A ∧ a ∈ B} x = {a : α | a ∈ B ∧ a ∈ A} x


without unfold set_of?

#### Kevin Buzzard (May 16 2020 at 14:21):

In some sense your goal should never be that, because it's not in canonical form

#### Kevin Buzzard (May 16 2020 at 14:24):

If I found myself in that state I would probably first do show x \in A \and x \in B = x \in B and x \in A to get things back into some kind of normality, and then use the ext tactic.

#### Johan Commelin (May 16 2020 at 14:24):

@Keefer Rowan How did you end up with that goal?

#### Johan Commelin (May 16 2020 at 14:24):

I think that 1 or 2 lines before it, you should have written ext x.

#### Reid Barton (May 16 2020 at 14:24):

Here again there are two kinds of approaches depending on whether or not you want to exploit your knowledge of the definition of { | }:

1. Using that knowledge:
• You could compute mentally that the goal is really just x ∈ A ∧ x ∈ B = x ∈ B ∧ x ∈ A. So use change x ∈ A ∧ x ∈ B = x ∈ B ∧ x ∈ A to make that the new goal.
• Alternatively, you can see that the new goal is going to be closed by something like and.comm (this might be phrased in terms of iff, though, not sure) so just apply that directly.
1. Not using that knowledge:
• find some lemma that rewrites {a | p a} x to p x.

In this case (and also in the compl one earlier) it's better to just do 1, since the definition of this notation is so basic.

#### Kevin Buzzard (May 16 2020 at 14:25):

There are 100 ways to say everything in Lean, and a proper subset of them are "canonical". If you stick to the canonical ways then the simp tactic will be of much more help to you.

#### Kevin Buzzard (May 16 2020 at 14:26):

You learn the canonical ways by looking at statements of lemmas in the library

#### Kevin Buzzard (May 16 2020 at 14:26):

show and change do the same thing, by the way

#### Keefer Rowan (May 16 2020 at 15:34):

@Johan Commelin This is where I was:

theorem inter_comm {α : Type u} {A B : set α} : A ∩ B = B ∩ A :=
begin
unfold has_inter.inter set.inter, sorry,
end


(BTW: I know this is almost certainly already in the library)

Also ext x gives an "unknown identifier". I'm working with very basic imports, so maybe isn't imported.

#### Keefer Rowan (May 16 2020 at 15:40):

I think I see what's going on though, you're saying that if I prove the theorem by set extensionality, I won't run into this state. What do I need to import to get ext? I was able to prove theorem setext {α : Type u} (A B : set α) : (∀ (x : α), x ∈ A ↔ x ∈ B) → A = B, which allows me to do this, but I should probably be using the proper tactic.

#### Bryan Gin-ge Chen (May 16 2020 at 15:41):

Yeah, ext is a mathlib tactic. You would have to use apply set.ext instead. Here's the proof in mathlib.

#### Bryan Gin-ge Chen (May 16 2020 at 16:02):

Oh hmm, set.ext is proved in mathlib too.

#### Kevin Buzzard (May 16 2020 at 16:28):

import tactic

theorem inter_comm {α : Type} {A B : set α} : A ∩ B = B ∩ A :=
begin
ext x,
rw [set.mem_inter_iff, set.mem_inter_iff],
apply and_comm,
end


In this proof nothing ever leaves the canonical form.

Last updated: May 15 2021 at 22:14 UTC