I believe that compactness has a different meaning in topology than in logic btw (though my degree was so long ago now that I'm rusty on it all!).
I do find it implausible that you'd need the type of background that I had in logic back then, which included the type of stuff mentioned, for doing stuff in Lean though.
I do find it implausible that you'd need the type of background that I had in logic back then, which included the type of stuff mentioned, for doing stuff in Lean though.