Prove that the image of a map is finite

Stream: general

[Klaus Mattis]

Hello,
I'm relatively new to lean (I learned about lean a year ago, I did the natural numbers game, but only started to use it more seriously the last week).
So I thought a good starting project would be "a cont. bij. map from a compact space to a hausdorff space is a homeo".
At the moment I have a mostly working proof of "compact subset in a hausdorff space is closed", but I'm stuck at the following problem:

(To remind you, the proof is roughly the following: Let A be the compact set, let x be a point not in A, for every point in A choose a neighborhood disjoint to a neighborhood of x, get a finite subcover, and use the intersection of the corresponding neighborhoods of x as open nbhd of x disjoint to A)

So I have the finite subcover of A, and I built a "function" of the following type:

have f: Π u : subcover, { p : nhds_of X x | p.1 ∩ u = ∅ }, by ...

(for every open u in the subcover, we get a nbhd of x, which is disjoint to u)
Then our finite set of nbhds of x would be the range of this subcover, this works.

Now I have trouble showing that the range is finite.
I used finite_image, but this does not work, because the function's domain is not the Type set X, but a subtype of it,
for it to work, one apparently needs a function set X -> set X, and then it gives you that the image of subcover is finite.

So I built the following "workaround":

I defined a function
let tempfun : set X → set X := λ u, if hu : u ∈ subcover then (f ⟨u, by assumption⟩).1.1 else ∅,

Then I proofed that the image of subcover is finite by using finite_image

First question: Can we avoid this weird workarounds?

Second question: Later I need to use that tempfun u = f (<u, hu>), (where hu : u ∈ subcover),
which should be a trivial proof, but I don't know how to do it.

Thanks in advance!
Apologies if these questions are dumb or obvious, but I searched the web for quite a while and found nothing helpful :(

[Klaus Mattis]

To be precise in the second question: I made a mistake, I want to show tempfun u = f (<u, hu>).1.1. which gets the underlying set of the neighborhood with the condition that it is disjoint to u.

[Eric Wieser]

I think you'd be a lot more likely to get help with an #mwe, it's difficult to solve "how do I do this trivial proof" questions without having exactly the same set of lean-based hurdles in front of us as you do.

[Kevin Buzzard]

I proved compact subspace of a Hausdorff space is closed using this "classical" approach in one of my Twitch streams over the summer: the code is here. I wrote a lot of comments. In mathlib they give a completely different proof using filters.

[Klaus Mattis]

Ok, yeah looks like a great idea to make a mwe :)
So it would be the following code:

import topology.basic
open set

lemma image_of_fin_set_is_finite
  (A : Type) (B : Type) (s : set A) (hs : finite s) (f : s → B)
: finite (range f) := begin
  --exact finite_image f hs, does not work, since finite_image expects f to start at A
  sorry,
end

And thanks, @Kevin Buzzard , I will look at your code!

[Johan Commelin]

@Klaus Mattis that code snippet is a bit "too minimal". Please include import foobar.quux in the code snippets, so that people can copy paste them into a new file and immediately have compiling code.

[Klaus Mattis]

I edited it in the above code.

[Johan Commelin]

lemma image_of_fin_set_is_finite
  (A : Type) (B : Type) (s : set A) (hs : finite s) (f : s → B) :
  finite (range f) :=
begin
  convert finite_range _,
  exact hs.fintype
end

[Klaus Mattis]

Ok, thanks a lot!