Effros' theorem on transitive group actions with a glimpse into descriptive set theory

The main aim of this note is to prove a version of a celebrated theorem of Effros about transitive group actions in a non-metrizable setting, these parts have been formalized and verified with Lean by Lara Toledano. We do not claim any originality since the given proof is in fact very close to one of van Mill. Our presentation is however completely self-contained and may serve as an appetizer to descriptive set theory. It also contains a few results about Suslin spaces (continuous images of separable completely metrizable spaces, which are often called analytic) which are extremely useful in measure theory.