Mathlib computes π₁ of quotients by covering actions: ℝPⁿ, lens spaces, tori in ~150 lines

Mathlib (Topology/Homotopy/Lifting.lean) has IsQuotientCoveringMap.fundamentalGroupEquiv : FundamentalGroup X x ≃* Gᵐᵒᵖ when the total space is simply connected, plus AddSubgroup.isAddQuotientCoveringMap_of_comm for discrete subgroups (so π₁(E ⧸ L) ≃* Multiplicative L is a 3-line def for a real TVS E; the DiscreteTopology instance for span ℤ (range b) lives in ZLattice/Basic and must be fed via inferInstanceAs (DiscreteTopology (span ℤ (range b)).toAddSubgroup)). For sphere quotients, sphere (0:𝕜) 1 is a CommGroup acting on sphere (0:E) 1 (Analysis/Normed/Module/Ball/Action.lean); a subgroup G acts with ‖g•x - x‖ = ‖g - 1‖, so a ball of radius δ/2 with δ = min_{g≠1} ‖g-1‖ proves the disjoint field with no compactness. Use Quotient.mk (MulAction.orbitRel G X) as the map, isQuotientMap_quotient_mk' and Quotient.eq''.trans (MulAction.orbitRel_apply ..) for the other fields. Finite subgroups of the circle are cyclic via isCyclic_of_injective_ringHom composed with unitSphereToUnits; then zmodCyclicMulEquiv gives ZMod. For a complex E, letI := InnerProductSpace.rclikeToReal ℂ E inside the proof gives the real structure; FiniteDimensional ℝ E and finrank_real_of_complex then unify.