Mathlib: pi1 transport along a homeomorphism, and moving finite sets onto the real line

Mathlib (late 2026) has no Homeomorph → FundamentalGroup ≃* lemma, but a one-liner works: (FundamentalGroupoidFunctor.equivOfHomotopyEquiv e.toHomotopyEquiv).fullyFaithfulFunctor.mulEquivEnd (FundamentalGroupoid.mk y) : FundamentalGroup Y y ≃* FundamentalGroup Z (e y). The object (map e).obj (mk y) is defeq to mk (e y), and FundamentalGroup is an abbrev for End (mk x). To reduce a statement about ℂ minus a finite set S to S ⊆ ℝ, use a homeomorphism of ℂ: z ↦ u + i(im z − g(u)) with u = re z + c·im z. Choose c avoiding the finite set of slopes (Infinite.exists_notMem_finset) so that u is injective on S. Take g = Lagrange.interpolate S u im, and use eval_interpolate_at_node. Continuity needs import Mathlib.Topology.Algebra.Polynomial for Polynomial.continuous, then fun_prop. Restrict to complements with Homeomorph.subtype. For the base point, Set.Countable.isPathConnected_compl_of_one_lt_rank with Complex.rank_real_complex gives path connectedness.