How does this proof work?

Stream: general

[Joseph O]

I have this proof, and for the second line, library_search suggested exact singleton_injective, and it closed off the whole proof, and I looked at the definition, and wasn't able to understand why

theorem cantor_theorem {α : Type} (f : α → set α) : # α ≤ # (set α) :=
begin
  apply mk_le_of_injective,
  exact singleton_injective,
end

[Scott Morrison]

It seems pretty straightforward. Perhaps you could try describing (in English) the type signatures of mk_le_of_injective and singleton_injective, and see if by the time you've done that it makes sense?

[Scott Morrison]

Have you looked at the goal after the apply statement?

[Scott Morrison]

Also, please try to post a #mwe (that is a clickable link). You're much more likely to get helpful answers if others can copy and paste your code block into a new file and have it work immediately.

[Eric Wieser]

Didn't you already ask this here?

[Scott Morrison]

(Here you are missing an import statement, and open_locale, and two opens.)

[Joseph O]

Eric Wieser said:

Didn't you already ask this here?

No?

[Joseph O]

Scott Morrison said:

It seems pretty straightforward. Perhaps you could try describing (in English) the type signatures of mk_le_of_injective and singleton_injective, and see if by the time you've done that it makes sense?

wait is single_injective a singleton map?

[Joseph O]

Is it describing this?
There exists an injection from $S$ to $\mathcal{P}S$, given by the singleton map.

[Eric Wieser]

Why don't you look at docs#set.singleton_injective to find out?

[Eric Wieser]

And if you don't understand the statement, then click on the pieces of it (recursively) until you do

[Scott Morrison]

Maybe post here your attempts at translating the type signature of singleton_injective into English (=informal maths)...

[Joseph O]

Eric Wieser said:

Why don't you look at docs#set.singleton_injective to find out?

Yeah and it seems exactly like that statement.

[Joseph O]

Scott Morrison said:

Maybe post here your attempts at translating the type signature of singleton_injective into English (=informal maths)...

singleton_injective says the function from a an element of a set a to a subset is injective. Or, in other words, there exists an injective function from a set to its powerset

[Scott Morrison]

No

[Scott Morrison]

Or at least, what do you mean by "the function".

[Scott Morrison]

It's certainly not an existential statement.

[Joseph O]

Scott Morrison said:

Or at least, what do you mean by "the function".

Let me try again: the singleton map from a set and its poweset is injective