Covering structure off the branch locus

• RS.exists_openPartialHomeomorph_coe_eq — at an unramified point, the local homeomorphism from local-multiplicity's Forster 2.5 export upgrades to one whose coercion is literally F (mathlib's covering constructor needs ⇑φ = F on the nose, not just EqOn on the source).
• RS.isCoveringMapOn_compl_branchLocus — F is a covering map on (branchLocus F)ᶜ (Mathlib's IsCoveringMapOn.of_openPartialHomeomorph: compact T2 source, T2 target, local homeomorphism at every point of the fiber ⇒ evenly covered).
• RS.isEvenlyCovered_of_isRegularValue — the covering statement specialized to a single regular value.

Downstream may further compose with mathlib's IsCoveringMapOn.isCoveringMap_restrictPreimage (Topology/Covering/Basic.lean) for a genuine IsCoveringMap of the subtype restriction, and with Topology/Homotopy/Lifting.lean for path/homotopy lifting — no extra exports needed here.

theorem RS.exists_openPartialHomeomorph_coe_eq {X : Type u_1} [TopologicalSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {Y : Type u_2} [TopologicalSpace Y] [T2Space Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] {F : X → Y} (hF : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ F) (hne : ¬∃ (c : Y), ∀ (x : X), F x = c) {x : X} (h1 : ¬IsRamifiedAt F x) : ∃ (φ : OpenPartialHomeomorph X Y), x ∈ φ.source ∧ ↑φ = F

Multiplicity-1 points admit an OpenPartialHomeomorph whose coercion is literally F (the coe-exact upgrade of local-multiplicity's Forster 2.5 export; mathlib's covering constructor requires ⇑φ = F on the nose).

theorem RS.isCoveringMapOn_compl_branchLocus {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {Y : Type u_2} [TopologicalSpace Y] [T2Space Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] {F : X → Y} (hF : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ F) (hne : ¬∃ (c : Y), ∀ (x : X), F x = c) : IsCoveringMapOn F (branchLocus F)ᶜ

F is a covering map away from the (finite) branch locus.

theorem RS.isEvenlyCovered_of_isRegularValue {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {Y : Type u_2} [TopologicalSpace Y] [T2Space Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] {F : X → Y} (hF : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ F) (hne : ¬∃ (c : Y), ∀ (x : X), F x = c) {y : Y} (hy : IsRegularValue F y) : IsEvenlyCovered F y ↑(F ⁻¹' {y})

The covering statement specialized to a single regular value.