Jordan curve theorem in Lean 4/Mathlib: a ~1000-line route via Maehara

Mathlib has Poincaré–Miranda-capable Brouwer in 2D but no Jordan curve theorem. Route that worked: (1) crossing lemma, stated with JoinedIn: a path in S from a to b and one in T from c to d meet if T lies in a.re ≤ re ≤ b.re and S lies in c.im ≤ im ≤ d.im. This is Poincaré–Miranda applied to (s,t) ↦ (p s - q t) after reparametrizing [-1,1] → unitInterval with projIcc. (2) Arcs do not separate the plane: Tietze-extend the inverse of the arc parametrization (IsClosedEmbedding + IsEmbedding.toHomeomorph + ContinuousMap.exists_restrict_eq) to get a retraction r. If a component W were bounded, z ↦ if z ∈ W then r z else z (continuous_if; frontier W ⊆ arc) is the identity on a big circle and misses a point of W. A degree argument (or no-retraction) gives the contradiction. (3) Each component has frontier J: otherwise frontier W lies in an arc A ⊆ J, and IsPreconnected.subset_or_subset with W and (closure W)ᶜ on Aᶜ gives a contradiction. (4) Normalize by z ↦ c(z-d) so that ±1 realize the diameter, then run Maehara's argument with a box [-1,1]×[-2,2]. Encode 'highest/lowest point on the imaginary axis' as IsGreatest/IsLeast of the compact preimage (fun y => y*I) ⁻¹' P. Use the range of JoinedIn.somePath as a compact top-to-bottom path, which gives ε-balls around ±1 avoiding it. Gotchas: for 'a path leaving the box', the coordinatewise clamp does not work, because it maps the real rays onto ±1 ∈ J. Use a first-exit lemma instead (IsCompact.exists_isLeast on {t | p t ∉ Ω} plus closure_Ico). After set U := connectedComponentIn ..., rw with connectedComponentIn_eq fails to find the pattern, so rewrite with show U = W from ... instead.