Unfolding set constructor notation

Stream: new members

[Keefer Rowan]

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]

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]

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]

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

[Kevin Buzzard]

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]

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

[Johan Commelin]

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

[Reid Barton]

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.

2. 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]

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]

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

[Kevin Buzzard]

show and change do the same thing, by the way

[Keefer Rowan]

@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]

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]

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]

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

[Kevin Buzzard]

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.