diff --git a/Rubin.lean b/Rubin.lean
index 0fd1a8d..d49d1e7 100644
--- a/Rubin.lean
+++ b/Rubin.lean
@@ -26,6 +26,7 @@ import Rubin.RigidStabilizer
 import Rubin.Period
 import Rubin.AlgebraicDisjointness
 import Rubin.RegularSupport
+import Rubin.RegularSupportBasis
 import Rubin.HomeoGroup
 
 #align_import rubin
diff --git a/Rubin/HomeoGroup.lean b/Rubin/HomeoGroup.lean
index 357ea39..ee725cd 100644
--- a/Rubin/HomeoGroup.lean
+++ b/Rubin/HomeoGroup.lean
@@ -155,405 +155,6 @@ theorem HomeoGroup.smulImage_eq_image (g : HomeoGroup α) (S : Set α) :
 
 namespace Rubin
 
-section RegularSupportBasis.Prelude
-
-variable {α : Type _}
-variable [TopologicalSpace α]
-variable [DecidableEq α]
-
-/--
-Maps a "seed" of homeorphisms in α to the intersection of their regular support in α.
-
-Note that the condition that the resulting set is non-empty is introduced later in `RegularSupportBasis₀`
---/
-def RegularSupportInter₀ (S : Finset (HomeoGroup α)): Set α :=
-  ⋂ (g ∈ S), RegularSupport α g
-
-theorem RegularSupportInter₀.eq_sInter (S : Finset (HomeoGroup α)) :
-  RegularSupportInter₀ S = ⋂₀ ((fun (g : HomeoGroup α) => RegularSupport α g) '' S) :=
-by
-  rw [Set.sInter_image]
-  rfl
-
-/--
-This is a predecessor type to `RegularSupportBasis`, where equality is defined on the `seed` used, rather than the `val`.
---/
-structure RegularSupportBasis₀ (α : Type _) [TopologicalSpace α] where
-  seed : Finset (HomeoGroup α)
-  val_nonempty : Set.Nonempty (RegularSupportInter₀ seed)
-
-theorem RegularSupportBasis₀.eq_iff_seed_eq (S T : RegularSupportBasis₀ α) : S = T ↔ S.seed = T.seed := by
-  -- Spooky :3c
-  rw [mk.injEq]
-
-def RegularSupportBasis₀.val (S : RegularSupportBasis₀ α) : Set α := RegularSupportInter₀ S.seed
-
-theorem RegularSupportBasis₀.val_def (S : RegularSupportBasis₀ α) : S.val = RegularSupportInter₀ S.seed := rfl
-
-@[simp]
-theorem RegularSupportBasis₀.nonempty (S : RegularSupportBasis₀ α) : Set.Nonempty S.val := S.val_nonempty
-
-@[simp]
-theorem RegularSupportBasis₀.regular (S : RegularSupportBasis₀ α) : Regular S.val := by
-  rw [S.val_def]
-  rw [RegularSupportInter₀.eq_sInter]
-
-  apply regular_sInter
-  · have set_decidable : DecidableEq (Set α) := Classical.typeDecidableEq (Set α)
-    let fin : Finset (Set α) := S.seed.image ((fun g => RegularSupport α g))
-
-    apply Set.Finite.ofFinset fin
-    simp
-  · intro S S_in_set
-    simp at S_in_set
-    let ⟨g, ⟨_, Heq⟩⟩ := S_in_set
-    rw [<-Heq]
-    exact regularSupport_regular α g
-
-lemma RegularSupportInter₀.mul_seed (seed : Finset (HomeoGroup α)) [DecidableEq (HomeoGroup α)] (f : HomeoGroup α):
-  RegularSupportInter₀ (Finset.image (fun g => f * g * f⁻¹) seed) = f •'' RegularSupportInter₀ seed :=
-by
-  unfold RegularSupportInter₀
-  simp
-  conv => {
-    rhs
-    ext; lhs; ext x; ext; lhs
-    ext
-    rw [regularSupport_smulImage]
-  }
-
-variable [DecidableEq (HomeoGroup α)]
-
-/--
-A `HomeoGroup α` group element `f` acts on an `RegularSupportBasis₀ α` set `S`,
-by mapping each element `g` of `S.seed` to `f * g * f⁻¹`
---/
-instance homeoGroup_smul₂ : SMul (HomeoGroup α) (RegularSupportBasis₀ α) where
-  smul := fun f S => ⟨
-    (Finset.image (fun g => f * g * f⁻¹) S.seed),
-    by
-      rw [RegularSupportInter₀.mul_seed]
-      simp
-      exact S.val_nonempty
-  ⟩
-
-theorem RegularSupportBasis₀.smul_seed (f : HomeoGroup α) (S : RegularSupportBasis₀ α) :
-  (f • S).seed = (Finset.image (fun g => f * g * f⁻¹) S.seed) := rfl
-
-theorem RegularSupportBasis₀.smul_val (f : HomeoGroup α) (S : RegularSupportBasis₀ α) :
-  (f • S).val = RegularSupportInter₀ (Finset.image (fun g => f * g * f⁻¹) S.seed) := rfl
-
-theorem RegularSupportBasis₀.smul_val' (f : HomeoGroup α) (S : RegularSupportBasis₀ α) :
-  (f • S).val = f •'' S.val :=
-by
-  unfold val
-  rw [<-RegularSupportInter₀.mul_seed]
-  rw [RegularSupportBasis₀.smul_seed]
-
--- We define a "preliminary" group action from `HomeoGroup α` to `RegularSupportBasis₀`
-instance homeoGroup_mulAction₂ : MulAction (HomeoGroup α) (RegularSupportBasis₀ α) where
-  one_smul := by
-    intro S
-    rw [RegularSupportBasis₀.eq_iff_seed_eq]
-    rw [RegularSupportBasis₀.smul_seed]
-    simp
-  mul_smul := by
-    intro f g S
-    rw [RegularSupportBasis₀.eq_iff_seed_eq]
-    repeat rw [RegularSupportBasis₀.smul_seed]
-    rw [Finset.image_image]
-    ext x
-    simp
-    group
-
-end RegularSupportBasis.Prelude
-
-
-/--
-A partially-ordered set, associated to Rubin's proof.
-Any element in that set is made up of a `seed`,
-such that `val = RegularSupportInter₀ seed` and `Set.Nonempty val`.
-
-Actions on this set are first defined in terms of `RegularSupportBasis₀`,
-as the proofs otherwise get hairy with a bunch of `Exists.choose` appearing.
---/
-structure RegularSupportBasis (α : Type _) [TopologicalSpace α] where
-  val : Set α
-  val_has_seed : ∃ po_seed : RegularSupportBasis₀ α, po_seed.val = val
-
-namespace RegularSupportBasis
-
-variable {α : Type _}
-variable [TopologicalSpace α]
-variable [DecidableEq α]
-
-theorem eq_iff_val_eq (S T : RegularSupportBasis α) : S = T ↔ S.val = T.val := by
-  rw [mk.injEq]
-
-def fromSeed (seed : RegularSupportBasis₀ α) : RegularSupportBasis α := ⟨
-  seed.val,
-  ⟨seed, seed.val_def⟩
-⟩
-
-noncomputable def full_seed (S : RegularSupportBasis α) : RegularSupportBasis₀ α :=
-  (Exists.choose S.val_has_seed)
-
-noncomputable def seed (S : RegularSupportBasis α) : Finset (HomeoGroup α) :=
-  S.full_seed.seed
-
-@[simp]
-theorem full_seed_seed (S : RegularSupportBasis α) : S.full_seed.seed = S.seed := rfl
-
-@[simp]
-theorem fromSeed_val (seed : RegularSupportBasis₀ α) :
-  (fromSeed seed).val = seed.val :=
-by
-  unfold fromSeed
-  simp
-
-@[simp]
-theorem val_from_seed (S : RegularSupportBasis α) : RegularSupportInter₀ S.seed = S.val := by
-  unfold seed full_seed
-  rw [<-RegularSupportBasis₀.val_def]
-  rw [Exists.choose_spec S.val_has_seed]
-
-@[simp]
-theorem val_from_seed₂ (S : RegularSupportBasis α) : S.full_seed.val = S.val := by
-  unfold full_seed
-  rw [RegularSupportBasis₀.val_def]
-  nth_rw 2 [<-val_from_seed]
-  unfold seed full_seed
-  rfl
-
--- Allows one to prove properties of RegularSupportBasis without jumping through `Exists.choose`-shaped hoops
-theorem prop_from_val {p : Set α → Prop}
-  (any_seed : ∀ po_seed : RegularSupportBasis₀ α, p po_seed.val) :
-  ∀ (S : RegularSupportBasis α), p S.val :=
-by
-  intro S
-  rw [<-val_from_seed]
-  have res := any_seed S.full_seed
-  rw [val_from_seed₂] at res
-  rw [val_from_seed]
-  exact res
-
-@[simp]
-theorem nonempty : ∀ (S : RegularSupportBasis α), Set.Nonempty S.val :=
-  prop_from_val RegularSupportBasis₀.nonempty
-
-@[simp]
-theorem regular : ∀ (S : RegularSupportBasis α), Regular S.val :=
-  prop_from_val RegularSupportBasis₀.regular
-
-variable [DecidableEq (HomeoGroup α)]
-
-instance homeoGroup_smul₃ : SMul (HomeoGroup α) (RegularSupportBasis α) where
-  smul := fun f S => ⟨
-    f •'' S.val,
-    by
-      use f • S.full_seed
-      rw [RegularSupportBasis₀.smul_val']
-      simp
-  ⟩
-
-theorem smul_val (f : HomeoGroup α) (S : RegularSupportBasis α) :
-  (f • S).val = f •'' S.val := rfl
-
-theorem smul_seed' (f : HomeoGroup α) (S : RegularSupportBasis α) (seed : Finset (HomeoGroup α)) :
-  S.val = RegularSupportInter₀ seed →
-  (f • S).val = RegularSupportInter₀ (Finset.image (fun g => f * g * f⁻¹) seed) :=
-by
-  intro S_val_eq
-  rw [smul_val]
-  rw [RegularSupportInter₀.mul_seed]
-  rw [S_val_eq]
-
-theorem smul_seed (f : HomeoGroup α) (S : RegularSupportBasis α) :
-  (f • S).val = RegularSupportInter₀ (Finset.image (fun g => f * g * f⁻¹) S.seed) :=
-by
-  apply smul_seed'
-  symm
-  exact val_from_seed S
-
--- Note: we could potentially implement MulActionHom
-instance homeoGroup_mulAction₃ : MulAction (HomeoGroup α) (RegularSupportBasis α) where
-  one_smul := by
-    intro S
-    rw [eq_iff_val_eq]
-    repeat rw [smul_val]
-    rw [one_smulImage]
-  mul_smul := by
-    intro S f g
-    rw [eq_iff_val_eq]
-    repeat rw [smul_val]
-    rw [smulImage_mul]
-
-instance associatedPoset_le : LE (RegularSupportBasis α) where
-  le := fun S T => S.val ⊆ T.val
-
-theorem le_def (S T : RegularSupportBasis α) : S ≤ T ↔ S.val ⊆ T.val := by
-  rw [iff_eq_eq]
-  rfl
-
-instance associatedPoset_partialOrder : PartialOrder (RegularSupportBasis α) where
-  le_refl := fun S => (le_def S S).mpr (le_refl S.val)
-  le_trans := fun S T U S_le_T S_le_U => (le_def S U).mpr (le_trans
-    ((le_def _ _).mp S_le_T)
-    ((le_def _ _).mp S_le_U)
-  )
-  le_antisymm := by
-    intro S T S_le_T T_le_S
-    rw [le_def] at S_le_T
-    rw [le_def] at T_le_S
-    rw [eq_iff_val_eq]
-    apply le_antisymm <;> assumption
-
-theorem smul_mono {S T : RegularSupportBasis α} (f : HomeoGroup α) (S_le_T : S ≤ T) :
-  f • S ≤ f • T :=
-by
-  rw [le_def]
-  repeat rw [smul_val]
-  apply smulImage_mono
-  assumption
-
-instance associatedPoset_coeSet : Coe (RegularSupportBasis α) (Set α) where
-  coe := RegularSupportBasis.val
-
-def asSet (α : Type _) [TopologicalSpace α]: Set (Set α) :=
-  { S : Set α | ∃ T : RegularSupportBasis α, T.val = S }
-
-theorem asSet_def :
-  RegularSupportBasis.asSet α = { S : Set α | ∃ T : RegularSupportBasis α, T.val = S } := rfl
-
-theorem mem_asSet (S : Set α) :
-  S ∈ RegularSupportBasis.asSet α ↔ ∃ T : RegularSupportBasis α, T.val = S :=
-by
-  rw [asSet_def]
-  simp
-
-theorem mem_asSet' (S : Set α) :
-  S ∈ RegularSupportBasis.asSet α ↔ Set.Nonempty S ∧ ∃ seed : Finset (HomeoGroup α), S = RegularSupportInter₀ seed :=
-by
-  rw [asSet_def]
-  simp
-  constructor
-  · intro ⟨T, T_eq⟩
-    rw [<-T_eq]
-    constructor
-    simp
-
-    let ⟨⟨seed, _⟩, eq⟩ := T.val_has_seed
-    rw [RegularSupportBasis₀.val_def] at eq
-    simp at eq
-    use seed
-    exact eq.symm
-  · intro ⟨S_nonempty, ⟨seed, val_from_seed⟩⟩
-    rw [val_from_seed] at S_nonempty
-    use fromSeed ⟨seed, S_nonempty⟩
-    rw [val_from_seed]
-    simp
-    rw [RegularSupportBasis₀.val_def]
-
-instance membership : Membership α (RegularSupportBasis α) where
-  mem := fun x S => x ∈ S.val
-
-theorem mem_iff (x : α) (S : RegularSupportBasis α) : x ∈ S ↔ x ∈ (S : Set α) := iff_eq_eq ▸ rfl
-
-section Basis
-open Topology
-
--- TODO: clean this lemma to not mention W anymore?
-lemma proposition_3_2_subset (G : Type _) {α : Type _} [Group G] [TopologicalSpace α] [MulAction G α]
-  [T2Space α] [LocallyCompactSpace α] [h_ld : LocallyDense G α] [HasNoIsolatedPoints α]
-  [ContinuousMulAction G α]
-  {U : Set α} (U_open : IsOpen U) {p : α} (p_in_U : p ∈ U) :
-  ∃ (W : Set α), W ∈ 𝓝 p ∧ closure W ⊆ U ∧
-  ∃ (g : G), g ∈ RigidStabilizer G W ∧ p ∈ RegularSupport α g ∧ RegularSupport α g ⊆ closure W :=
-by
-  have U_in_nhds : U ∈ 𝓝 p := by
-    rw [mem_nhds_iff]
-    use U
-
-  let ⟨W', W'_in_nhds, W'_ss_U, W'_compact⟩ := local_compact_nhds U_in_nhds
-
-  -- This feels like black magic, but okay
-  let ⟨W, _W_compact, W_closed, W'_ss_int_W, W_ss_U⟩ := exists_compact_closed_between W'_compact U_open W'_ss_U
-  have W_cl_eq_W : closure W = W := IsClosed.closure_eq W_closed
-
-  have W_in_nhds : W ∈ 𝓝 p := by
-    rw [mem_nhds_iff]
-    use interior W
-    repeat' apply And.intro
-    · exact interior_subset
-    · simp
-    · exact W'_ss_int_W (mem_of_mem_nhds W'_in_nhds)
-
-  use W
-
-  repeat' apply And.intro
-  exact W_in_nhds
-  {
-    rw [W_cl_eq_W]
-    exact W_ss_U
-  }
-
-  have p_in_int_W : p ∈ interior W := W'_ss_int_W (mem_of_mem_nhds W'_in_nhds)
-
-  let ⟨g, g_in_rist, g_moves_p⟩ := get_moving_elem_in_rigidStabilizer G isOpen_interior p_in_int_W
-
-  use g
-  repeat' apply And.intro
-  · apply rigidStabilizer_mono interior_subset
-    simp
-    exact g_in_rist
-  · rw [<-mem_support] at g_moves_p
-    apply support_subset_regularSupport
-    exact g_moves_p
-  · rw [rigidStabilizer_support] at g_in_rist
-    apply subset_trans
-    exact regularSupport_subset_closure_support
-    apply closure_mono
-    apply subset_trans
-    exact g_in_rist
-    exact interior_subset
-
-/--
-## Proposition 3.2 : RegularSupportBasis is a topological basis of `α`
--/
-theorem isBasis (G α : Type _) [Group G] [TopologicalSpace α] [MulAction G α]
-  [T2Space α] [LocallyCompactSpace α] [h_ld : LocallyDense G α] [HasNoIsolatedPoints α]
-  [hc : ContinuousMulAction G α] :
-  TopologicalSpace.IsTopologicalBasis (RegularSupportBasis.asSet α) :=
-by
-  apply TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds
-  {
-    intro U U_in_poset
-    rw [RegularSupportBasis.mem_asSet] at U_in_poset
-    let ⟨T, T_val⟩ := U_in_poset
-    rw [<-T_val]
-    exact T.regular.isOpen
-  }
-  intro p U p_in_U U_open
-
-  let ⟨W, _, clW_ss_U, ⟨g, _, p_in_rsupp, rsupp_ss_clW⟩⟩ := proposition_3_2_subset G U_open p_in_U
-  use RegularSupport α g
-  repeat' apply And.intro
-  · rw [RegularSupportBasis.mem_asSet']
-    constructor
-    exact ⟨p, p_in_rsupp⟩
-    use {(ContinuousMulAction.toHomeomorph α g : HomeoGroup α)}
-    unfold RegularSupportInter₀
-    simp
-    unfold RegularSupport
-    rw [<-homeoGroup_support_eq_support_toHomeomorph g]
-  · exact p_in_rsupp
-  · apply subset_trans
-    exact rsupp_ss_clW
-    exact clW_ss_U
-
-end Basis
-end RegularSupportBasis
-
 section Other
 
 /--
diff --git a/Rubin/RegularSupportBasis.lean b/Rubin/RegularSupportBasis.lean
new file mode 100644
index 0000000..8b4b271
--- /dev/null
+++ b/Rubin/RegularSupportBasis.lean
@@ -0,0 +1,414 @@
+/-
+This files defines `RegularSupportBasis`, which is a basis of the topological space α,
+made up of finite intersections of `RegularSupport α g` for `g : HomeoGroup α`.
+-/
+
+import Mathlib.Topology.Basic
+import Mathlib.Topology.Homeomorph
+
+import Rubin.LocallyDense
+import Rubin.Topology
+import Rubin.Support
+import Rubin.RegularSupport
+import Rubin.HomeoGroup
+
+namespace Rubin
+section RegularSupportBasis.Prelude
+
+variable {α : Type _}
+variable [TopologicalSpace α]
+variable [DecidableEq α]
+
+/--
+Maps a "seed" of homeorphisms in α to the intersection of their regular support in α.
+
+Note that the condition that the resulting set is non-empty is introduced later in `RegularSupportBasis₀`
+--/
+def RegularSupportInter₀ (S : Finset (HomeoGroup α)): Set α :=
+  ⋂ (g ∈ S), RegularSupport α g
+
+theorem RegularSupportInter₀.eq_sInter (S : Finset (HomeoGroup α)) :
+  RegularSupportInter₀ S = ⋂₀ ((fun (g : HomeoGroup α) => RegularSupport α g) '' S) :=
+by
+  rw [Set.sInter_image]
+  rfl
+
+/--
+This is a predecessor type to `RegularSupportBasis`, where equality is defined on the `seed` used, rather than the `val`.
+--/
+structure RegularSupportBasis₀ (α : Type _) [TopologicalSpace α] where
+  seed : Finset (HomeoGroup α)
+  val_nonempty : Set.Nonempty (RegularSupportInter₀ seed)
+
+theorem RegularSupportBasis₀.eq_iff_seed_eq (S T : RegularSupportBasis₀ α) : S = T ↔ S.seed = T.seed := by
+  -- Spooky :3c
+  rw [mk.injEq]
+
+def RegularSupportBasis₀.val (S : RegularSupportBasis₀ α) : Set α := RegularSupportInter₀ S.seed
+
+theorem RegularSupportBasis₀.val_def (S : RegularSupportBasis₀ α) : S.val = RegularSupportInter₀ S.seed := rfl
+
+@[simp]
+theorem RegularSupportBasis₀.nonempty (S : RegularSupportBasis₀ α) : Set.Nonempty S.val := S.val_nonempty
+
+@[simp]
+theorem RegularSupportBasis₀.regular (S : RegularSupportBasis₀ α) : Regular S.val := by
+  rw [S.val_def]
+  rw [RegularSupportInter₀.eq_sInter]
+
+  apply regular_sInter
+  · have set_decidable : DecidableEq (Set α) := Classical.typeDecidableEq (Set α)
+    let fin : Finset (Set α) := S.seed.image ((fun g => RegularSupport α g))
+
+    apply Set.Finite.ofFinset fin
+    simp
+  · intro S S_in_set
+    simp at S_in_set
+    let ⟨g, ⟨_, Heq⟩⟩ := S_in_set
+    rw [<-Heq]
+    exact regularSupport_regular α g
+
+lemma RegularSupportInter₀.mul_seed (seed : Finset (HomeoGroup α)) [DecidableEq (HomeoGroup α)] (f : HomeoGroup α):
+  RegularSupportInter₀ (Finset.image (fun g => f * g * f⁻¹) seed) = f •'' RegularSupportInter₀ seed :=
+by
+  unfold RegularSupportInter₀
+  simp
+  conv => {
+    rhs
+    ext; lhs; ext x; ext; lhs
+    ext
+    rw [regularSupport_smulImage]
+  }
+
+variable [DecidableEq (HomeoGroup α)]
+
+/--
+A `HomeoGroup α` group element `f` acts on an `RegularSupportBasis₀ α` set `S`,
+by mapping each element `g` of `S.seed` to `f * g * f⁻¹`
+--/
+instance homeoGroup_smul₂ : SMul (HomeoGroup α) (RegularSupportBasis₀ α) where
+  smul := fun f S => ⟨
+    (Finset.image (fun g => f * g * f⁻¹) S.seed),
+    by
+      rw [RegularSupportInter₀.mul_seed]
+      simp
+      exact S.val_nonempty
+  ⟩
+
+theorem RegularSupportBasis₀.smul_seed (f : HomeoGroup α) (S : RegularSupportBasis₀ α) :
+  (f • S).seed = (Finset.image (fun g => f * g * f⁻¹) S.seed) := rfl
+
+theorem RegularSupportBasis₀.smul_val (f : HomeoGroup α) (S : RegularSupportBasis₀ α) :
+  (f • S).val = RegularSupportInter₀ (Finset.image (fun g => f * g * f⁻¹) S.seed) := rfl
+
+theorem RegularSupportBasis₀.smul_val' (f : HomeoGroup α) (S : RegularSupportBasis₀ α) :
+  (f • S).val = f •'' S.val :=
+by
+  unfold val
+  rw [<-RegularSupportInter₀.mul_seed]
+  rw [RegularSupportBasis₀.smul_seed]
+
+-- We define a "preliminary" group action from `HomeoGroup α` to `RegularSupportBasis₀`
+instance homeoGroup_mulAction₂ : MulAction (HomeoGroup α) (RegularSupportBasis₀ α) where
+  one_smul := by
+    intro S
+    rw [RegularSupportBasis₀.eq_iff_seed_eq]
+    rw [RegularSupportBasis₀.smul_seed]
+    simp
+  mul_smul := by
+    intro f g S
+    rw [RegularSupportBasis₀.eq_iff_seed_eq]
+    repeat rw [RegularSupportBasis₀.smul_seed]
+    rw [Finset.image_image]
+    ext x
+    simp
+    group
+
+end RegularSupportBasis.Prelude
+
+
+/--
+A partially-ordered set, associated to Rubin's proof.
+Any element in that set is made up of a `seed`,
+such that `val = RegularSupportInter₀ seed` and `Set.Nonempty val`.
+
+Actions on this set are first defined in terms of `RegularSupportBasis₀`,
+as the proofs otherwise get hairy with a bunch of `Exists.choose` appearing.
+--/
+structure RegularSupportBasis (α : Type _) [TopologicalSpace α] where
+  val : Set α
+  val_has_seed : ∃ po_seed : RegularSupportBasis₀ α, po_seed.val = val
+
+namespace RegularSupportBasis
+
+variable {α : Type _}
+variable [TopologicalSpace α]
+variable [DecidableEq α]
+
+theorem eq_iff_val_eq (S T : RegularSupportBasis α) : S = T ↔ S.val = T.val := by
+  rw [mk.injEq]
+
+def fromSeed (seed : RegularSupportBasis₀ α) : RegularSupportBasis α := ⟨
+  seed.val,
+  ⟨seed, seed.val_def⟩
+⟩
+
+noncomputable def full_seed (S : RegularSupportBasis α) : RegularSupportBasis₀ α :=
+  (Exists.choose S.val_has_seed)
+
+noncomputable def seed (S : RegularSupportBasis α) : Finset (HomeoGroup α) :=
+  S.full_seed.seed
+
+@[simp]
+theorem full_seed_seed (S : RegularSupportBasis α) : S.full_seed.seed = S.seed := rfl
+
+@[simp]
+theorem fromSeed_val (seed : RegularSupportBasis₀ α) :
+  (fromSeed seed).val = seed.val :=
+by
+  unfold fromSeed
+  simp
+
+@[simp]
+theorem val_from_seed (S : RegularSupportBasis α) : RegularSupportInter₀ S.seed = S.val := by
+  unfold seed full_seed
+  rw [<-RegularSupportBasis₀.val_def]
+  rw [Exists.choose_spec S.val_has_seed]
+
+@[simp]
+theorem val_from_seed₂ (S : RegularSupportBasis α) : S.full_seed.val = S.val := by
+  unfold full_seed
+  rw [RegularSupportBasis₀.val_def]
+  nth_rw 2 [<-val_from_seed]
+  unfold seed full_seed
+  rfl
+
+-- Allows one to prove properties of RegularSupportBasis without jumping through `Exists.choose`-shaped hoops
+theorem prop_from_val {p : Set α → Prop}
+  (any_seed : ∀ po_seed : RegularSupportBasis₀ α, p po_seed.val) :
+  ∀ (S : RegularSupportBasis α), p S.val :=
+by
+  intro S
+  rw [<-val_from_seed]
+  have res := any_seed S.full_seed
+  rw [val_from_seed₂] at res
+  rw [val_from_seed]
+  exact res
+
+@[simp]
+theorem nonempty : ∀ (S : RegularSupportBasis α), Set.Nonempty S.val :=
+  prop_from_val RegularSupportBasis₀.nonempty
+
+@[simp]
+theorem regular : ∀ (S : RegularSupportBasis α), Regular S.val :=
+  prop_from_val RegularSupportBasis₀.regular
+
+variable [DecidableEq (HomeoGroup α)]
+
+instance homeoGroup_smul₃ : SMul (HomeoGroup α) (RegularSupportBasis α) where
+  smul := fun f S => ⟨
+    f •'' S.val,
+    by
+      use f • S.full_seed
+      rw [RegularSupportBasis₀.smul_val']
+      simp
+  ⟩
+
+theorem smul_val (f : HomeoGroup α) (S : RegularSupportBasis α) :
+  (f • S).val = f •'' S.val := rfl
+
+theorem smul_seed' (f : HomeoGroup α) (S : RegularSupportBasis α) (seed : Finset (HomeoGroup α)) :
+  S.val = RegularSupportInter₀ seed →
+  (f • S).val = RegularSupportInter₀ (Finset.image (fun g => f * g * f⁻¹) seed) :=
+by
+  intro S_val_eq
+  rw [smul_val]
+  rw [RegularSupportInter₀.mul_seed]
+  rw [S_val_eq]
+
+theorem smul_seed (f : HomeoGroup α) (S : RegularSupportBasis α) :
+  (f • S).val = RegularSupportInter₀ (Finset.image (fun g => f * g * f⁻¹) S.seed) :=
+by
+  apply smul_seed'
+  symm
+  exact val_from_seed S
+
+-- Note: we could potentially implement MulActionHom
+instance homeoGroup_mulAction₃ : MulAction (HomeoGroup α) (RegularSupportBasis α) where
+  one_smul := by
+    intro S
+    rw [eq_iff_val_eq]
+    repeat rw [smul_val]
+    rw [one_smulImage]
+  mul_smul := by
+    intro S f g
+    rw [eq_iff_val_eq]
+    repeat rw [smul_val]
+    rw [smulImage_mul]
+
+instance associatedPoset_le : LE (RegularSupportBasis α) where
+  le := fun S T => S.val ⊆ T.val
+
+theorem le_def (S T : RegularSupportBasis α) : S ≤ T ↔ S.val ⊆ T.val := by
+  rw [iff_eq_eq]
+  rfl
+
+instance associatedPoset_partialOrder : PartialOrder (RegularSupportBasis α) where
+  le_refl := fun S => (le_def S S).mpr (le_refl S.val)
+  le_trans := fun S T U S_le_T S_le_U => (le_def S U).mpr (le_trans
+    ((le_def _ _).mp S_le_T)
+    ((le_def _ _).mp S_le_U)
+  )
+  le_antisymm := by
+    intro S T S_le_T T_le_S
+    rw [le_def] at S_le_T
+    rw [le_def] at T_le_S
+    rw [eq_iff_val_eq]
+    apply le_antisymm <;> assumption
+
+theorem smul_mono {S T : RegularSupportBasis α} (f : HomeoGroup α) (S_le_T : S ≤ T) :
+  f • S ≤ f • T :=
+by
+  rw [le_def]
+  repeat rw [smul_val]
+  apply smulImage_mono
+  assumption
+
+instance associatedPoset_coeSet : Coe (RegularSupportBasis α) (Set α) where
+  coe := RegularSupportBasis.val
+
+def asSet (α : Type _) [TopologicalSpace α]: Set (Set α) :=
+  { S : Set α | ∃ T : RegularSupportBasis α, T.val = S }
+
+theorem asSet_def :
+  RegularSupportBasis.asSet α = { S : Set α | ∃ T : RegularSupportBasis α, T.val = S } := rfl
+
+theorem mem_asSet (S : Set α) :
+  S ∈ RegularSupportBasis.asSet α ↔ ∃ T : RegularSupportBasis α, T.val = S :=
+by
+  rw [asSet_def]
+  simp
+
+theorem mem_asSet' (S : Set α) :
+  S ∈ RegularSupportBasis.asSet α ↔ Set.Nonempty S ∧ ∃ seed : Finset (HomeoGroup α), S = RegularSupportInter₀ seed :=
+by
+  rw [asSet_def]
+  simp
+  constructor
+  · intro ⟨T, T_eq⟩
+    rw [<-T_eq]
+    constructor
+    simp
+
+    let ⟨⟨seed, _⟩, eq⟩ := T.val_has_seed
+    rw [RegularSupportBasis₀.val_def] at eq
+    simp at eq
+    use seed
+    exact eq.symm
+  · intro ⟨S_nonempty, ⟨seed, val_from_seed⟩⟩
+    rw [val_from_seed] at S_nonempty
+    use fromSeed ⟨seed, S_nonempty⟩
+    rw [val_from_seed]
+    simp
+    rw [RegularSupportBasis₀.val_def]
+
+instance membership : Membership α (RegularSupportBasis α) where
+  mem := fun x S => x ∈ S.val
+
+theorem mem_iff (x : α) (S : RegularSupportBasis α) : x ∈ S ↔ x ∈ (S : Set α) := iff_eq_eq ▸ rfl
+
+section Basis
+open Topology
+
+-- TODO: clean this lemma to not mention W anymore?
+lemma proposition_3_2_subset (G : Type _) {α : Type _} [Group G] [TopologicalSpace α] [MulAction G α]
+  [T2Space α] [LocallyCompactSpace α] [h_ld : LocallyDense G α] [HasNoIsolatedPoints α]
+  [ContinuousMulAction G α]
+  {U : Set α} (U_open : IsOpen U) {p : α} (p_in_U : p ∈ U) :
+  ∃ (W : Set α), W ∈ 𝓝 p ∧ closure W ⊆ U ∧
+  ∃ (g : G), g ∈ RigidStabilizer G W ∧ p ∈ RegularSupport α g ∧ RegularSupport α g ⊆ closure W :=
+by
+  have U_in_nhds : U ∈ 𝓝 p := by
+    rw [mem_nhds_iff]
+    use U
+
+  let ⟨W', W'_in_nhds, W'_ss_U, W'_compact⟩ := local_compact_nhds U_in_nhds
+
+  -- This feels like black magic, but okay
+  let ⟨W, _W_compact, W_closed, W'_ss_int_W, W_ss_U⟩ := exists_compact_closed_between W'_compact U_open W'_ss_U
+  have W_cl_eq_W : closure W = W := IsClosed.closure_eq W_closed
+
+  have W_in_nhds : W ∈ 𝓝 p := by
+    rw [mem_nhds_iff]
+    use interior W
+    repeat' apply And.intro
+    · exact interior_subset
+    · simp
+    · exact W'_ss_int_W (mem_of_mem_nhds W'_in_nhds)
+
+  use W
+
+  repeat' apply And.intro
+  exact W_in_nhds
+  {
+    rw [W_cl_eq_W]
+    exact W_ss_U
+  }
+
+  have p_in_int_W : p ∈ interior W := W'_ss_int_W (mem_of_mem_nhds W'_in_nhds)
+
+  let ⟨g, g_in_rist, g_moves_p⟩ := get_moving_elem_in_rigidStabilizer G isOpen_interior p_in_int_W
+
+  use g
+  repeat' apply And.intro
+  · apply rigidStabilizer_mono interior_subset
+    simp
+    exact g_in_rist
+  · rw [<-mem_support] at g_moves_p
+    apply support_subset_regularSupport
+    exact g_moves_p
+  · rw [rigidStabilizer_support] at g_in_rist
+    apply subset_trans
+    exact regularSupport_subset_closure_support
+    apply closure_mono
+    apply subset_trans
+    exact g_in_rist
+    exact interior_subset
+
+/--
+## Proposition 3.2 : RegularSupportBasis is a topological basis of `α`
+-/
+theorem isBasis (G α : Type _) [Group G] [TopologicalSpace α] [MulAction G α]
+  [T2Space α] [LocallyCompactSpace α] [h_ld : LocallyDense G α] [HasNoIsolatedPoints α]
+  [hc : ContinuousMulAction G α] :
+  TopologicalSpace.IsTopologicalBasis (RegularSupportBasis.asSet α) :=
+by
+  apply TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds
+  {
+    intro U U_in_poset
+    rw [RegularSupportBasis.mem_asSet] at U_in_poset
+    let ⟨T, T_val⟩ := U_in_poset
+    rw [<-T_val]
+    exact T.regular.isOpen
+  }
+  intro p U p_in_U U_open
+
+  let ⟨W, _, clW_ss_U, ⟨g, _, p_in_rsupp, rsupp_ss_clW⟩⟩ := proposition_3_2_subset G U_open p_in_U
+  use RegularSupport α g
+  repeat' apply And.intro
+  · rw [RegularSupportBasis.mem_asSet']
+    constructor
+    exact ⟨p, p_in_rsupp⟩
+    use {(ContinuousMulAction.toHomeomorph α g : HomeoGroup α)}
+    unfold RegularSupportInter₀
+    simp
+    unfold RegularSupport
+    rw [<-homeoGroup_support_eq_support_toHomeomorph g]
+  · exact p_in_rsupp
+  · apply subset_trans
+    exact rsupp_ss_clW
+    exact clW_ss_U
+
+end Basis
+end RegularSupportBasis
+end Rubin