diff --git a/Rubin.lean b/Rubin.lean
index 47cd6c4..af7a6d3 100644
--- a/Rubin.lean
+++ b/Rubin.lean
@@ -22,6 +22,7 @@ import Rubin.SmulImage
 import Rubin.Support
 import Rubin.Topological
 import Rubin.RigidStabilizer
+import Rubin.Period
 
 #align_import rubin
 
@@ -42,55 +43,11 @@ section Rubin
 
 variable {G α β : Type _} [Group G]
 
-----------------------------------------------------------------
-section Groups
-
-def is_algebraically_disjoint (f g : G) :=
-  ∀ h : G,
-    ¬Commute f h →
-      ∃ f₁ f₂ : G, Commute f₁ g ∧ Commute f₂ g ∧ Commute ⁅f₁, ⁅f₂, h⁆⁆ g ∧ ⁅f₁, ⁅f₂, h⁆⁆ ≠ 1
-#align is_algebraically_disjoint Rubin.is_algebraically_disjoint
-
-end Groups
-
-----------------------------------------------------------------
-section Actions
-
-variable [MulAction G α]
-
-@[simp]
-theorem orbit_bot (G : Type _) [Group G] [MulAction G α] (p : α) :
-    MulAction.orbit (⊥ : Subgroup G) p = {p} :=
-  by
-  ext1
-  rw [MulAction.mem_orbit_iff]
-  constructor
-  · rintro ⟨⟨_, g_bot⟩, g_to_x⟩
-    rw [← g_to_x, Set.mem_singleton_iff, Subgroup.mk_smul]
-    exact (Subgroup.mem_bot.mp g_bot).symm ▸ one_smul _ _
-  exact fun h => ⟨1, Eq.trans (one_smul _ p) (Set.mem_singleton_iff.mp h).symm⟩
-#align orbit_bot Rubin.orbit_bot
-
-end Actions
-
 ----------------------------------------------------------------
 section RubinActions
-open Topology
 
 variable [TopologicalSpace α] [TopologicalSpace β]
 
--- Note: `𝓝[≠] x` is notation for `nhdsWithin x {[x]}ᶜ`, ie. the neighborhood of x not containing itself
--- TODO: make this a class?
-def has_no_isolated_points (α : Type _) [TopologicalSpace α] :=
-  ∀ x : α, 𝓝[≠] x ≠ ⊥
-#align has_no_isolated_points Rubin.has_no_isolated_points
-
-def is_locally_dense (G α : Type _) [Group G] [TopologicalSpace α] [MulAction G α] :=
-  ∀ U : Set α,
-  ∀ p ∈ U,
-  p ∈ interior (closure (MulAction.orbit (RigidStabilizer G U) p))
-#align is_locally_dense Rubin.is_locally_dense
-
 structure RubinAction (G α : Type _) extends
   Group G,
   TopologicalSpace α,
@@ -100,413 +57,15 @@ where
   locally_compact : LocallyCompactSpace α
   hausdorff : T2Space α
   no_isolated_points : Rubin.has_no_isolated_points α
-  locallyDense : Rubin.is_locally_dense G α
+  locallyDense : LocallyDense G α
 #align rubin_action Rubin.RubinAction
 
 end RubinActions
 
-----------------------------------------------------------------
-section Rubin.Period.period
-
-variable [MulAction G α]
-
-noncomputable def Period.period (p : α) (g : G) : ℕ :=
-  sInf {n : ℕ | n > 0 ∧ g ^ n • p = p}
-#align period Rubin.Period.period
-
-theorem Period.period_le_fix {p : α} {g : G} {m : ℕ} (m_pos : m > 0)
-    (gmp_eq_p : g ^ m • p = p) : 0 < Rubin.Period.period p g ∧ Rubin.Period.period p g ≤ m :=
-  by
-  constructor
-  · by_contra h'; have period_zero : Rubin.Period.period p g = 0; linarith;
-    rcases Nat.sInf_eq_zero.1 period_zero with ⟨cont, h_1⟩ | h; linarith;
-    exact Set.eq_empty_iff_forall_not_mem.mp h ↑m ⟨m_pos, gmp_eq_p⟩
-  exact Nat.sInf_le ⟨m_pos, gmp_eq_p⟩
-#align period_le_fix Rubin.Period.period_le_fix
-
-theorem Period.notfix_le_period {p : α} {g : G} {n : ℕ} (n_pos : n > 0)
-    (period_pos : Rubin.Period.period p g > 0) (pmoves : ∀ i : ℕ, 0 < i → i < n → g ^ i • p ≠ p) :
-    n ≤ Rubin.Period.period p g := by
-  by_contra period_le
-  exact
-    (pmoves (Rubin.Period.period p g) period_pos (not_le.mp period_le))
-      (Nat.sInf_mem (Nat.nonempty_of_pos_sInf period_pos)).2
-#align notfix_le_period Rubin.Period.notfix_le_period
-
-theorem Period.notfix_le_period' {p : α} {g : G} {n : ℕ} (n_pos : n > 0)
-    (period_pos : Rubin.Period.period p g > 0)
-    (pmoves : ∀ i : Fin n, 0 < (i : ℕ) → g ^ (i : ℕ) • p ≠ p) : n ≤ Rubin.Period.period p g :=
-  Rubin.Period.notfix_le_period n_pos period_pos fun (i : ℕ) (i_pos : 0 < i) (i_lt_n : i < n) =>
-    pmoves (⟨i, i_lt_n⟩ : Fin n) i_pos
-#align notfix_le_period' Rubin.Period.notfix_le_period'
-
-theorem Period.period_neutral_eq_one (p : α) : Rubin.Period.period p (1 : G) = 1 :=
-  by
-  have : 0 < Rubin.Period.period p (1 : G) ∧ Rubin.Period.period p (1 : G) ≤ 1 :=
-    Rubin.Period.period_le_fix (by norm_num : 1 > 0)
-      (by group_action :
-        (1 : G) ^ 1 • p = p)
-  linarith
-#align period_neutral_eq_one Rubin.Period.period_neutral_eq_one
-
-def Period.periods (U : Set α) (H : Subgroup G) : Set ℕ :=
-  {n : ℕ | ∃ (p : α) (g : H), p ∈ U ∧ Rubin.Period.period (p : α) (g : G) = n}
-#align periods Rubin.Period.periods
-
--- TODO: split into multiple lemmas
-theorem Period.periods_lemmas {U : Set α} (U_nonempty : Set.Nonempty U) {H : Subgroup G}
-    (exp_ne_zero : Monoid.exponent H ≠ 0) :
-    (Rubin.Period.periods U H).Nonempty ∧
-      BddAbove (Rubin.Period.periods U H) ∧
-        ∃ (m : ℕ) (m_pos : m > 0), ∀ (p : α) (g : H), g ^ m • p = p :=
-  by
-  rcases Monoid.exponentExists_iff_ne_zero.2 exp_ne_zero with ⟨m, m_pos, gm_eq_one⟩
-  have gmp_eq_p : ∀ (p : α) (g : H), g ^ m • p = p := by
-    intro p g; rw [gm_eq_one g];
-    group_action
-  have periods_nonempty : (Rubin.Period.periods U H).Nonempty := by
-    use 1
-    let p := Set.Nonempty.some U_nonempty; use p
-    use 1
-    constructor
-    · exact Set.Nonempty.some_mem U_nonempty
-    · exact Rubin.Period.period_neutral_eq_one p
-
-  have periods_bounded : BddAbove (Rubin.Period.periods U H) := by
-    use m; intro some_period hperiod;
-    rcases hperiod with ⟨p, g, hperiod⟩
-    rw [← hperiod.2]
-    exact (Rubin.Period.period_le_fix m_pos (gmp_eq_p p g)).2
-  exact ⟨periods_nonempty, periods_bounded, m, m_pos, gmp_eq_p⟩
-#align period_lemma Rubin.Period.periods_lemmas
-
-theorem Period.period_from_exponent (U : Set α) (U_nonempty : U.Nonempty) {H : Subgroup G}
-    (exp_ne_zero : Monoid.exponent H ≠ 0) :
-    ∃ (p : α) (g : H) (n : ℕ),
-      p ∈ U ∧ n > 0 ∧ Rubin.Period.period (p : α) (g : G) = n ∧ n = sSup (Rubin.Period.periods U H) :=
-  by
-  rcases Rubin.Period.periods_lemmas U_nonempty exp_ne_zero with
-    ⟨periods_nonempty, periods_bounded, m, m_pos, gmp_eq_p⟩
-  rcases Nat.sSup_mem periods_nonempty periods_bounded with ⟨p, g, hperiod⟩
-  use p
-  use g
-  use sSup (Rubin.Period.periods U H)
-  -- TODO: cleanup?
-  exact ⟨
-    hperiod.1,
-    hperiod.2 ▸ (Rubin.Period.period_le_fix m_pos (gmp_eq_p p g)).1,
-    hperiod.2,
-    rfl
-  ⟩
-#align period_from_exponent Rubin.Period.period_from_exponent
-
-theorem Period.zero_lt_period_le_Sup_periods {U : Set α} (U_nonempty : U.Nonempty)
-    {H : Subgroup G} (exp_ne_zero : Monoid.exponent H ≠ 0) :
-    ∀ (p : U) (g : H),
-      0 < Rubin.Period.period (p : α) (g : G) ∧
-        Rubin.Period.period (p : α) (g : G) ≤ sSup (Rubin.Period.periods U H) :=
-  by
-  rcases Rubin.Period.periods_lemmas U_nonempty exp_ne_zero with
-    ⟨periods_nonempty, periods_bounded, m, m_pos, gmp_eq_p⟩
-  intro p g
-  have period_in_periods : Rubin.Period.period (p : α) (g : G) ∈ Rubin.Period.periods U H := by
-    use p; use g
-    simp
-  exact
-    ⟨(Rubin.Period.period_le_fix m_pos (gmp_eq_p p g)).1,
-      le_csSup periods_bounded period_in_periods⟩
-#align zero_lt_period_le_Sup_periods Rubin.Period.zero_lt_period_le_Sup_periods
-
-theorem Period.pow_period_fix (p : α) (g : G) : g ^ Rubin.Period.period p g • p = p :=
-  by
-  cases eq_zero_or_neZero (Rubin.Period.period p g) with
-  | inl h => rw [h]; simp
-  | inr h =>
-    exact
-      (Nat.sInf_mem
-          (Nat.nonempty_of_pos_sInf
-            (Nat.pos_of_ne_zero (@NeZero.ne _ _ (Rubin.Period.period p g) h)))).2
-#align pow_period_fix Rubin.Period.pow_period_fix
-
-end Rubin.Period.period
-
-----------------------------------------------------------------
-section AlgebraicDisjointness
-
-variable [TopologicalSpace α] [Rubin.Topological.ContinuousMulAction G α] [FaithfulSMul G α]
-
-def Disjointness.IsLocallyMoving (G α : Type _) [Group G] [TopologicalSpace α]
-    [MulAction G α] :=
-  ∀ U : Set α, IsOpen U → Set.Nonempty U → RigidStabilizer G U ≠ ⊥
-#align is_locally_moving Rubin.Disjointness.IsLocallyMoving
-
--- lemma dense_locally_moving : t2_space α ∧ has_no_isolated_points α ∧ is_locally_dense G α → is_locally_moving G α := begin
---   rintros ⟨t2α,nipα,ildGα⟩ U ioU neU,
---   by_contra,
---   have some_in_U := ildGα U neU.some neU.some_mem,
---   rw [h,orbit_bot G neU.some,@closure_singleton α _ (@t2_space.t1_space α _ t2α) neU.some,@interior_singleton α _ neU.some (nipα neU.some)] at some_in_U,
---   tauto
--- end
--- lemma disjoint_nbhd {g : G} {x : α} [t2_space α] : g • x ≠ x → ∃U : set α, is_open U ∧ x ∈ U ∧ disjoint U (g •'' U) := begin
---   intro xmoved,
---   rcases t2_space.t2 (g • x) x xmoved with ⟨V,W,open_V,open_W,gx_in_V,x_in_W,disjoint_V_W⟩,
---   let U := (g⁻¹ •'' V) ∩ W,
---   use U,
---   split,
---   exact is_open.inter (img_open_open g⁻¹ V open_V) open_W,
---   split,
---   exact ⟨mem_inv_smul''.mpr gx_in_V,x_in_W⟩,
---   exact Set.disjoint_of_subset
---     (Set.inter_subset_right (g⁻¹ •'' V) W)
---     (λ y hy, smul_inv_smul g y ▸ mem_inv_smul''.mp (Set.mem_of_mem_inter_left (mem_smulImage.mp hy)) : g •'' U ⊆ V)
---     disjoint_V_W.symm
--- end
--- lemma disjoint_nbhd_in {g : G} {x : α} [t2_space α] {V : set α} : is_open V → x ∈ V → g • x ≠ x → ∃U : set α, is_open U ∧ x ∈ U ∧ U ⊆ V ∧ disjoint U (g •'' U) := begin
---   intros open_V x_in_V xmoved,
---   rcases disjoint_nbhd xmoved with ⟨W,open_W,x_in_W,disjoint_W⟩,
---   let U := W ∩ V,
---   use U,
---   split,
---   exact is_open.inter open_W open_V,
---   split,
---   exact ⟨x_in_W,x_in_V⟩,
---   split,
---   exact Set.inter_subset_right W V,
---   exact Set.disjoint_of_subset
---     (Set.inter_subset_left W V)
---     ((@smul''_inter _ _ _ _ g W V).symm ▸ Set.inter_subset_left (g •'' W) (g •'' V) : g •'' U ⊆ g •'' W)
---     disjoint_W
--- end
--- lemma rewrite_Union (f : fin 2 × fin 2 → set α) : (⋃(i : fin 2 × fin 2), f i) = (f (0,0) ∪ f (0,1)) ∪ (f (1,0) ∪ f (1,1)) := begin
---   ext,
---   simp only [Set.mem_Union, Set.mem_union],
---   split,
---   { simp only [forall_exists_index],
---     intro i,
---     fin_cases i; simp {contextual := tt}, },
---   { rintro ((h|h)|(h|h)); exact ⟨_, h⟩, },
--- end
--- lemma proposition_1_1_1 (f g : G) (locally_moving : is_locally_moving G α) [t2_space α] : disjoint (support α f) (support α g) → is_algebraically_disjoint f g := begin
---   intros disjoint_f_g h hfh,
---   let support_f := support α f,
--- -- h is not the identity on support α f
---   cases Set.not_disjoint_iff.mp (mt (@disjoint_commute G α _ _ _ _ _) hfh) with x hx,
---   let x_in_support_f := hx.1,
---   let hx_ne_x := mem_support.mp hx.2,
--- -- so since α is Hausdoff there is V nonempty ⊆ support α f with h •'' V disjoint from V
---   rcases disjoint_nbhd_in (support_open f) x_in_support_f hx_ne_x with ⟨V,open_V,x_in_V,V_in_support,disjoint_img_V⟩,
---   let ristV_ne_bot := locally_moving V open_V (Set.nonempty_of_mem x_in_V),
--- -- let f₂ be a nontrivial element of rigid_stabilizer G V
---   rcases (or_iff_right ristV_ne_bot).mp (Subgroup.bot_or_exists_ne_one _) with ⟨f₂,f₂_in_ristV,f₂_ne_one⟩,
--- -- again since α is Hausdorff there is W nonempty ⊆ V with f₂ •'' W disjoint from W
---   rcases faithful_moves_point' α f₂_ne_one with ⟨y,ymoved⟩,
---   let y_in_V : y ∈ V := (rist_supported_in_set f₂_in_ristV) (mem_support.mpr ymoved),
---   rcases disjoint_nbhd_in open_V y_in_V ymoved with ⟨W,open_W,y_in_W,W_in_V,disjoint_img_W⟩,
--- -- let f₁ be a nontrivial element of rigid_stabilizer G W
---   let ristW_ne_bot := locally_moving W open_W (Set.nonempty_of_mem y_in_W),
---   rcases (or_iff_right ristW_ne_bot).mp (Subgroup.bot_or_exists_ne_one _) with ⟨f₁,f₁_in_ristW,f₁_ne_one⟩,
---   use f₁, use f₂,
--- -- note that f₁,f₂ commute with g since their support is in support α f
---   split,
---   exact disjoint_commute (Set.disjoint_of_subset_left (Set.subset.trans (Set.subset.trans (rist_supported_in_set f₁_in_ristW) W_in_V) V_in_support) disjoint_f_g),
---   split,
---   exact disjoint_commute (Set.disjoint_of_subset_left (Set.subset.trans (rist_supported_in_set f₂_in_ristV) V_in_support) disjoint_f_g),
--- -- we claim that [f₁,[f₂,h]] is a nontrivial element of centralizer G g
---   let k := ⁅f₂,h⁆,
--- -- first, h*f₂⁻¹*h⁻¹ is supported on h V, so k := [f₂,h] agrees with f₂ on V
---   have h2 : ∀z ∈ W, f₂•z = k•z := λ z z_in_W,
---     (disjoint_support_comm f₂ h (rist_supported_in_set f₂_in_ristV) disjoint_img_V z (W_in_V z_in_W)).symm,
--- -- then k*f₁⁻¹*k⁻¹ is supported on k W = f₂ W, so [f₁,k] is supported on W ∪ f₂ W ⊆ V ⊆ support f, so commutes with g.
---   have h3 : support α ⁅f₁,k⁆ ⊆ support α f := begin
---     let := (support_comm α k f₁).trans (Set.union_subset_union (rist_supported_in_set f₁_in_ristW) (smul''_subset k $ rist_supported_in_set f₁_in_ristW)),
---     rw [← commutator_element_inv,support_inv,(smul''_eq_of_smul_eq h2).symm] at this,
---     exact (this.trans $ (Set.union_subset_union W_in_V (moves_subset_within_support f₂ W V W_in_V $ rist_supported_in_set f₂_in_ristV)).trans $ eq.subset V.union_self).trans V_in_support
--- end,
---   split,
---   exact disjoint_commute (Set.disjoint_of_subset_left h3 disjoint_f_g),
--- -- finally, [f₁,k] agrees with f₁ on W, so is not the identity.
---   have h4 : ∀z ∈ W, ⁅f₁,k⁆•z = f₁•z :=
---     disjoint_support_comm f₁ k (rist_supported_in_set f₁_in_ristW) (smul''_eq_of_smul_eq h2 ▸ disjoint_img_W),
---   rcases faithful_rist_moves_point f₁_in_ristW f₁_ne_one with ⟨z,z_in_W,z_moved⟩,
---   by_contra h5,
---   exact ((h4 z z_in_W).symm ▸ z_moved : ⁅f₁, k⁆ • z ≠ z) ((congr_arg (λg : G, g•z) h5).trans (one_smul G z)),
--- end
--- @[simp] lemma smul''_mul {g h : G} {U : set α} : g •'' (h •'' U) = (g*h) •'' U :=
---   (mul_smul'' g h U).symm
--- lemma disjoint_nbhd_fin {ι : Type*} [fintype ι] {f : ι → G} {x : α} [t2_space α] : (λi : ι, f i • x).injective → ∃U : set α, is_open U ∧ x ∈ U ∧ (∀i j : ι, i ≠ j → disjoint (f i •'' U) (f j •'' U)) := begin
---   intro f_injective,
---   let disjoint_hyp := λi j (i_ne_j : i≠j), let x_moved : ((f j)⁻¹ * f i) • x ≠ x := begin
---     by_contra,
---     let := smul_congr (f j) h,
---     rw [mul_smul, ← mul_smul,mul_right_inv,one_smul] at this,
---     from i_ne_j (f_injective this),
---   end in disjoint_nbhd x_moved,
---   let ι2 := { p : ι×ι // p.1 ≠ p.2 },
---   let U := ⋂(p : ι2), (disjoint_hyp p.1.1 p.1.2 p.2).some,
---   use U,
---   split,
---   exact is_open_Inter (λp : ι2, (disjoint_hyp p.1.1 p.1.2 p.2).some_spec.1),
---   split,
---   exact Set.mem_Inter.mpr (λp : ι2, (disjoint_hyp p.1.1 p.1.2 p.2).some_spec.2.1),
---   intros i j i_ne_j,
---   let U_inc := Set.Inter_subset (λ p : ι2, (disjoint_hyp p.1.1 p.1.2 p.2).some) ⟨⟨i,j⟩,i_ne_j⟩,
---   let := (disjoint_smul'' (f j) (Set.disjoint_of_subset U_inc (smul''_subset ((f j)⁻¹ * (f i)) U_inc) (disjoint_hyp i j i_ne_j).some_spec.2.2)).symm,
---   simp only [subtype.val_eq_coe, smul''_mul, mul_inv_cancel_left] at this,
---   from this
--- end
--- lemma moves_inj {g : G} {x : α} {n : ℕ} (period_ge_n : ∀ (k : ℤ), 1 ≤ k → k < n → g ^ k • x ≠ x) : function.injective (λ (i : fin n), g ^ (i : ℤ) • x) := begin
---     intros i j same_img,
---     by_contra i_ne_j,
---     let same_img' := congr_arg ((•) (g ^ (-(j : ℤ)))) same_img,
---     simp only [inv_smul_smul] at same_img',
---     rw [← mul_smul,← mul_smul,← zpow_add,← zpow_add,add_comm] at same_img',
---     simp only [add_left_neg, zpow_zero, one_smul] at same_img',
---     let ij := |(i:ℤ) - (j:ℤ)|,
---     rw ← sub_eq_add_neg at same_img',
---     have xfixed : g^ij • x = x := begin
---       cases abs_cases ((i:ℤ) - (j:ℤ)),
---       { rw ← h.1 at same_img', exact same_img' },
---       { rw [smul_eq_iff_inv_smul_eq,← zpow_neg,← h.1] at same_img', exact same_img' }
---     end,
---     have ij_ge_1 : 1 ≤ ij := int.add_one_le_iff.mpr (abs_pos.mpr $ sub_ne_zero.mpr $ norm_num.nat_cast_ne i j ↑i ↑j rfl rfl (fin.vne_of_ne i_ne_j)),
---     let neg_le := int.sub_lt_sub_of_le_of_lt (nat.cast_nonneg i) (nat.cast_lt.mpr (fin.prop _)),
---     rw zero_sub at neg_le,
---     let le_pos := int.sub_lt_sub_of_lt_of_le (nat.cast_lt.mpr (fin.prop _)) (nat.cast_nonneg j),
---     rw sub_zero at le_pos,
---     have ij_lt_n : ij < n := abs_lt.mpr ⟨ neg_le, le_pos ⟩,
---     exact period_ge_n ij ij_ge_1 ij_lt_n xfixed,
--- end
--- lemma int_to_nat (k : ℤ) (k_pos : k ≥ 1) : k = k.nat_abs := begin
---   cases (int.nat_abs_eq k),
---   { exact h },
---   { have : -(k.nat_abs : ℤ) ≤ 0 := neg_nonpos.mpr (int.nat_abs k).cast_nonneg,
---     rw ← h at this, by_contra, linarith }
--- end
--- lemma moves_inj_N {g : G} {x : α} {n : ℕ} (period_ge_n' : ∀ (k : ℕ), 1 ≤ k → k < n → g ^ k • x ≠ x) : function.injective (λ (i : fin n), g ^ (i : ℕ) • x) := begin
---   have period_ge_n : ∀ (k : ℤ), 1 ≤ k → k < n → g ^ k • x ≠ x,
---   { intros k one_le_k k_lt_n,
---     have one_le_k_nat : 1 ≤ k.nat_abs := ((int.coe_nat_le_coe_nat_iff 1 k.nat_abs).1 ((int_to_nat k one_le_k) ▸ one_le_k)),
---     have k_nat_lt_n : k.nat_abs < n := ((int.coe_nat_lt_coe_nat_iff k.nat_abs n).1 ((int_to_nat k one_le_k) ▸ k_lt_n)),
---     have := period_ge_n' k.nat_abs one_le_k_nat k_nat_lt_n,
---     rw [(zpow_coe_nat g k.nat_abs).symm, (int_to_nat k one_le_k).symm] at this,
---     exact this },
---   have := moves_inj period_ge_n,
---   done
--- end
--- lemma moves_1234_of_moves_12 {g : G} {x : α} (xmoves : g^12 • x ≠ x) : function.injective (λi : fin 5, g^(i:ℤ) • x) := begin
---     apply moves_inj,
---     intros k k_ge_1 k_lt_5,
---     by_contra xfixed,
---     have k_div_12 : k * (12 / k) = 12 := begin
---       interval_cases using k_ge_1 k_lt_5; norm_num
---     end,
---     have veryfixed : g^12 • x = x := begin
---       let := smul_zpow_eq_of_smul_eq (12/k) xfixed,
---       rw [← zpow_mul,k_div_12] at this,
---       norm_cast at this
---     end,
---     exact xmoves veryfixed
--- end
--- lemma proposition_1_1_2 (f g : G) [t2_space α] : is_locally_moving G α → is_algebraically_disjoint f g → disjoint (support α f) (support α (g^12)) := begin
---   intros locally_moving alg_disjoint,
--- -- suppose to the contrary that the set U = supp(f) ∩ supp(g^12) is nonempty
---   by_contra not_disjoint,
---   let U := support α f ∩ support α (g^12),
---   have U_nonempty : U.nonempty := Set.not_disjoint_iff_nonempty_inter.mp not_disjoint,
--- -- since X is Hausdorff, we can find a nonempty open set V ⊆ U such that f(V) is disjoint from V and the sets {g^i(V): i=0..4} are pairwise disjoint
---   let x := U_nonempty.some,
---   have five_points : function.injective (λi : fin 5, g^(i:ℤ) • x) := moves_1234_of_moves_12 (mem_support.mp $ (Set.inter_subset_right _ _) U_nonempty.some_mem),
---   rcases disjoint_nbhd_in (is_open.inter (support_open f) (support_open $ g^12)) U_nonempty.some_mem ((Set.inter_subset_left _ _) U_nonempty.some_mem) with ⟨V₀,open_V₀,x_in_V₀,V₀_in_support,disjoint_img_V₀⟩,
---   rcases disjoint_nbhd_fin five_points with ⟨V₁,open_V₁,x_in_V₁,disjoint_img_V₁⟩,
---   simp only at disjoint_img_V₁,
---   let V := V₀ ∩ V₁,
--- -- let h be a nontrivial element of rigid_stabilizer G V, and note that [f,h]≠1 since f(V) is disjoint from V
---   let ristV_ne_bot := locally_moving V (is_open.inter open_V₀ open_V₁) (Set.nonempty_of_mem ⟨x_in_V₀,x_in_V₁⟩),
---   rcases (or_iff_right ristV_ne_bot).mp (Subgroup.bot_or_exists_ne_one _) with ⟨h,h_in_ristV,h_ne_one⟩,
---   have comm_non_trivial : ¬commute f h := begin
---     by_contra comm_trivial,
---     rcases faithful_rist_moves_point h_in_ristV h_ne_one with ⟨z,z_in_V,z_moved⟩,
---     let act_comm := disjoint_support_comm h f (rist_supported_in_set h_in_ristV) (Set.disjoint_of_subset (Set.inter_subset_left V₀ V₁) (smul''_subset f (Set.inter_subset_left V₀ V₁)) disjoint_img_V₀) z z_in_V,
---     rw [commutator_element_eq_one_iff_commute.mpr comm_trivial.symm,one_smul] at act_comm,
---     exact z_moved act_comm.symm,
---   end,
--- -- since g is algebraically disjoint from f, there exist f₁,f₂ ∈ C_G(g) so that the commutator h' = [f1,[f2,h]] is a nontrivial element of C_G(g)
---   rcases alg_disjoint h comm_non_trivial with ⟨f₁,f₂,f₁_commutes,f₂_commutes,h'_commutes,h'_non_trivial⟩,
---   let h' := ⁅f₁,⁅f₂,h⁆⁆,
--- -- now observe that supp([f₂, h]) ⊆ V ∪ f₂(V), and by the same reasoning supp(h')⊆V∪f₁(V)∪f₂(V)∪f₁f₂(V)
---   have support_f₂h : support α ⁅f₂,h⁆ ⊆ V ∪ (f₂ •'' V) := (support_comm α f₂ h).trans (Set.union_subset_union (rist_supported_in_set h_in_ristV) $ smul''_subset f₂ $ rist_supported_in_set h_in_ristV),
---   have support_h' : support α h' ⊆ ⋃(i : fin 2 × fin 2), (f₁^i.1.val*f₂^i.2.val) •'' V := begin
---     let this := (support_comm α f₁ ⁅f₂,h⁆).trans (Set.union_subset_union support_f₂h (smul''_subset f₁ support_f₂h)),
---     rw [smul''_union,← one_smul'' V,← mul_smul'',← mul_smul'',← mul_smul'',mul_one,mul_one] at this,
---     let rw_u := rewrite_Union (λi : fin 2 × fin 2, (f₁^i.1.val*f₂^i.2.val) •'' V),
---     simp only [fin.val_eq_coe, fin.val_zero', pow_zero, mul_one, fin.val_one, pow_one, one_mul] at rw_u,
---     exact rw_u.symm ▸ this,
---   end,
--- -- since h' is nontrivial, it has at least one point p in its support
---   cases faithful_moves_point' α h'_non_trivial with p p_moves,
--- -- since g commutes with h', all five of the points {gi(p):i=0..4} lie in supp(h')
---   have gi_in_support : ∀i : fin 5, g^i.val • p ∈ support α h' := begin
---     intro i,
---     rw mem_support,
---     by_contra p_fixed,
---     rw [← mul_smul,(h'_commutes.pow_right i.val).eq,mul_smul,smul_left_cancel_iff] at p_fixed,
---     exact p_moves p_fixed,
---   end,
--- -- by the pigeonhole principle, one of the four sets V, f₁(V), f₂(V), f₁f₂(V) must contain two of these points, say g^i(p),g^j(p) ∈ k(V) for some 0 ≤ i < j ≤ 4 and k ∈ {1,f₁,f₂,f₁f₂}
---   let pigeonhole : fintype.card (fin 5) > fintype.card (fin 2 × fin 2) := dec_trivial,
---   let choice := λi : fin 5, (Set.mem_Union.mp $ support_h' $ gi_in_support i).some,
---   rcases finset.exists_ne_map_eq_of_card_lt_of_maps_to pigeonhole (λ(i : fin 5) _, finset.mem_univ (choice i)) with ⟨i,_,j,_,i_ne_j,same_choice⟩,
---   clear h_1_w h_1_h_h_w pigeonhole,
---   let k := f₁^(choice i).1.val*f₂^(choice i).2.val,
---   have same_k : f₁^(choice j).1.val*f₂^(choice j).2.val = k := by { simp only at same_choice,
--- rw ← same_choice },
---   have g_i : g^i.val • p ∈ k •'' V := (Set.mem_Union.mp $ support_h' $ gi_in_support i).some_spec,
---   have g_j : g^j.val • p ∈ k •'' V := same_k ▸ (Set.mem_Union.mp $ support_h' $ gi_in_support j).some_spec,
--- -- but since g^(j−i)(V) is disjoint from V and k commutes with g, we know that g^(j−i)k(V) is disjoint from k(V), a contradiction since g^i(p) and g^j(p) both lie in k(V).
---   have g_disjoint : disjoint ((g^i.val)⁻¹ •'' V) ((g^j.val)⁻¹ •'' V) := begin
---     let := (disjoint_smul'' (g^(-(i.val+j.val : ℤ))) (disjoint_img_V₁ i j i_ne_j)).symm,
---     rw [← mul_smul'',← mul_smul'',← zpow_add,← zpow_add] at this,
---     simp only [fin.val_eq_coe, neg_add_rev, coe_coe, neg_add_cancel_right, zpow_neg, zpow_coe_nat, neg_add_cancel_comm] at this,
---     from Set.disjoint_of_subset (smul''_subset _ (Set.inter_subset_right V₀ V₁)) (smul''_subset _ (Set.inter_subset_right V₀ V₁)) this
---   end,
---   have k_commutes : commute k g := commute.mul_left (f₁_commutes.pow_left (choice i).1.val) (f₂_commutes.pow_left (choice i).2.val),
---   have g_k_disjoint : disjoint ((g^i.val)⁻¹ •'' (k •'' V)) ((g^j.val)⁻¹ •'' (k •'' V)) := begin
---     let this := disjoint_smul'' k g_disjoint,
---     rw [← mul_smul'',← mul_smul'',← inv_pow g i.val,← inv_pow g j.val,
---         ← (k_commutes.symm.inv_left.pow_left i.val).eq,
---         ← (k_commutes.symm.inv_left.pow_left j.val).eq,
---        mul_smul'',inv_pow g i.val,mul_smul'' (g⁻¹^j.val) k V,inv_pow g j.val] at this,
---     from this
---   end,
---   exact Set.disjoint_left.mp g_k_disjoint (mem_inv_smul''.mpr g_i) (mem_inv_smul''.mpr g_j)
--- end
--- lemma remark_1_2 (f g : G) : is_algebraically_disjoint f g → commute f g := begin
---   intro alg_disjoint,
---   by_contra non_commute,
---   rcases alg_disjoint g non_commute with ⟨_,_,_,b,_,d⟩,
---   rw [commutator_element_eq_one_iff_commute.mpr b,commutator_element_one_right] at d,
---   tauto
--- end
--- section remark_1_3
--- def G := equiv.perm (fin 2)
--- def σ := equiv.swap (0 : fin 2) (1 : fin 2)
--- example : is_algebraically_disjoint σ σ := begin
---   intro h,
---   fin_cases h,
---   intro hyp1,
---   exfalso,
---   swap, intro hyp2, exfalso,
--- -- is commute decidable? cc,
--- sorry -- dec_trivial
--- sorry -- second sorry needed
--- end
--- end remark_1_3
-end AlgebraicDisjointness
-
 ----------------------------------------------------------------
 section Rubin.RegularSupport.RegularSupport
 
-variable [TopologicalSpace α] [Rubin.Topological.ContinuousMulAction G α]
+variable [TopologicalSpace α] [Rubin.ContinuousMulAction G α]
 
 def RegularSupport.InteriorClosure (U : Set α) :=
   interior (closure U)
@@ -563,7 +122,7 @@ theorem RegularSupport.regularSupport_regular {g : G} :
 
 theorem RegularSupport.support_subset_regularSupport [T2Space α] (g : G) :
     Support α g ⊆ Rubin.RegularSupport.RegularSupport α g :=
-  Rubin.RegularSupport.IsOpen.interiorClosure_subset (Rubin.Topological.support_open g)
+  Rubin.RegularSupport.IsOpen.interiorClosure_subset (Rubin.support_open g)
 #align support_in_regular_support Rubin.RegularSupport.support_subset_regularSupport
 
 theorem RegularSupport.mem_regularSupport (g : G) (U : Set α) :
@@ -575,7 +134,7 @@ theorem RegularSupport.mem_regularSupport (g : G) (U : Set α) :
 
 -- FIXME: Weird naming?
 def RegularSupport.AlgebraicCentralizer (f : G) : Set G :=
-  {h | ∃ g, h = g ^ 12 ∧ Rubin.is_algebraically_disjoint f g}
+  {h | ∃ g, h = g ^ 12 ∧ AlgebraicallyDisjoint f g}
 #align algebraic_centralizer Rubin.RegularSupport.AlgebraicCentralizer
 
 end Rubin.RegularSupport.RegularSupport
diff --git a/Rubin/AlgebraicDisjointness.lean b/Rubin/AlgebraicDisjointness.lean
new file mode 100644
index 0000000..13cd696
--- /dev/null
+++ b/Rubin/AlgebraicDisjointness.lean
@@ -0,0 +1,399 @@
+import Mathlib.GroupTheory.GroupAction.Basic
+import Mathlib.GroupTheory.Subgroup.Basic
+import Mathlib.GroupTheory.Subgroup.Actions
+import Mathlib.Topology.Basic
+import Mathlib.Tactic.FinCases
+
+import Rubin.RigidStabilizer
+import Rubin.SmulImage
+import Rubin.Topological
+import Rubin.FaithfulAction
+
+namespace Rubin
+
+class LocallyMoving (G α : Type _) [Group G] [TopologicalSpace α] [MulAction G α] :=
+  locally_moving: ∀ U : Set α, IsOpen U → Set.Nonempty U → RigidStabilizer G U ≠ ⊥
+#align is_locally_moving Rubin.LocallyMoving
+
+namespace LocallyMoving
+
+theorem get_nontrivial_rist_elem {G α : Type _}
+  [Group G]
+  [TopologicalSpace α]
+  [MulAction G α]
+  [h_lm : LocallyMoving G α]
+  {U: Set α}
+  (U_open : IsOpen U)
+  (U_nonempty : U.Nonempty) :
+  ∃ x : G, x ∈ RigidStabilizer G U ∧ x ≠ 1 :=
+by
+  have rist_ne_bot := h_lm.locally_moving U U_open U_nonempty
+  exact (or_iff_right rist_ne_bot).mp (Subgroup.bot_or_exists_ne_one _)
+
+end LocallyMoving
+
+def AlgebraicallyDisjoint {G : Type _} [Group G] (f g : G) :=
+  ∀ h : G,
+    ¬Commute f h →
+      ∃ f₁ f₂ : G, Commute f₁ g ∧ Commute f₂ g ∧ Commute ⁅f₁, ⁅f₂, h⁆⁆ g ∧ ⁅f₁, ⁅f₂, h⁆⁆ ≠ 1
+#align is_algebraically_disjoint Rubin.AlgebraicallyDisjoint
+
+@[simp]
+theorem orbit_bot (G : Type _) [Group G] [MulAction G α] (p : α) :
+    MulAction.orbit (⊥ : Subgroup G) p = {p} :=
+  by
+  ext1
+  rw [MulAction.mem_orbit_iff]
+  constructor
+  · rintro ⟨⟨_, g_bot⟩, g_to_x⟩
+    rw [← g_to_x, Set.mem_singleton_iff, Subgroup.mk_smul]
+    exact (Subgroup.mem_bot.mp g_bot).symm ▸ one_smul _ _
+  exact fun h => ⟨1, Eq.trans (one_smul _ p) (Set.mem_singleton_iff.mp h).symm⟩
+#align orbit_bot Rubin.orbit_bot
+
+variable {G α : Type _}
+variable [Group G]
+variable [TopologicalSpace α]
+variable [ContinuousMulAction G α]
+variable [FaithfulSMul G α]
+
+instance dense_locally_moving [T2Space α]
+  (H_nip : has_no_isolated_points α)
+  (H_ld : LocallyDense G α) :
+  LocallyMoving G α
+where
+  locally_moving := by
+    intros U _ H_nonempty
+    by_contra h_rs
+    have ⟨elem, ⟨_, some_in_orbit⟩⟩ := H_ld.nonEmpty H_nonempty
+    have H_nebot := has_no_isolated_points_neBot H_nip elem
+    rw [h_rs] at some_in_orbit
+    simp at some_in_orbit
+
+lemma disjoint_nbhd [T2Space α] {g : G} {x : α} (x_moved: g • x ≠ x) :
+  ∃ U: Set α, IsOpen U ∧ x ∈ U ∧ Disjoint U (g •'' U) :=
+by
+  have ⟨V, W, V_open, W_open, gx_in_V, x_in_W, disjoint_V_W⟩ := T2Space.t2 (g • x) x x_moved
+  let U := (g⁻¹ •'' V) ∩ W
+  use U
+  constructor
+  {
+    -- NOTE: if this is common, then we should make a tactic for solving IsOpen goals
+    exact IsOpen.inter (img_open_open g⁻¹ V V_open) W_open
+  }
+  constructor
+  {
+    simp
+    rw [mem_inv_smulImage]
+    trivial
+  }
+  {
+    apply Set.disjoint_of_subset
+    · apply Set.inter_subset_right
+    · intro y hy; show y ∈ V
+
+      rw [<-smul_inv_smul g y]
+      rw [<-mem_inv_smulImage]
+
+      rw [mem_smulImage] at hy
+      simp at hy
+
+      exact hy.left
+    · exact disjoint_V_W.symm
+  }
+
+lemma disjoint_nbhd_in [T2Space α] {g : G} {x : α} {V : Set α}
+  (V_open : IsOpen V) (x_in_V : x ∈ V) (x_moved : g • x ≠ x) :
+  ∃ U : Set α, IsOpen U ∧ x ∈ U ∧ U ⊆ V ∧ Disjoint U (g •'' U) :=
+by
+  have ⟨W, W_open, x_in_W, disjoint_W_img⟩ := disjoint_nbhd x_moved
+  use W ∩ V
+  simp
+  constructor
+  {
+    apply IsOpen.inter <;> assumption
+  }
+  constructor
+  {
+    constructor <;> assumption
+  }
+  show Disjoint (W ∩ V) (g •'' W ∩ V)
+  apply Set.disjoint_of_subset
+  · exact Set.inter_subset_left W V
+  · show g •'' W ∩ V ⊆ g •'' W
+    rewrite [smulImage_inter]
+    exact Set.inter_subset_left _ _
+  · exact disjoint_W_img
+
+-- Kind of a boring lemma but okay
+lemma rewrite_Union (f : Fin 2 × Fin 2 → Set α) :
+  (⋃(i : Fin 2 × Fin 2), f i) = (f (0,0) ∪ f (0,1)) ∪ (f (1,0) ∪ f (1,1)) :=
+by
+  ext x
+  simp only [Set.mem_iUnion, Set.mem_union]
+  constructor
+  · rewrite [forall_exists_index]
+    intro i
+    fin_cases i
+      <;> simp only [Fin.zero_eta, Fin.mk_one]
+      <;> intro h
+      <;> simp only [h, true_or, or_true]
+  · rintro ((h|h)|(h|h)) <;> exact ⟨_, h⟩
+
+-- TODO: modify the proof to be less "let everything"-y, especially the first half
+lemma proposition_1_1_1 [h_lm : LocallyMoving G α] [T2Space α] (f g : G) (supp_disjoint : Disjoint (Support α f) (Support α g)) : AlgebraicallyDisjoint f g := by
+  intros h h_not_commute
+  -- h is not the identity on `Support α f`
+  have f_h_not_disjoint := (mt (disjoint_commute (G := G) (α := α)) h_not_commute)
+  have ⟨x, ⟨x_in_supp_f, x_in_supp_h⟩⟩ := Set.not_disjoint_iff.mp f_h_not_disjoint
+  have hx_ne_x := mem_support.mp x_in_supp_h
+
+  -- Since α is Hausdoff, there is a nonempty V ⊆ Support α f, with h •'' V disjoint from V
+  have ⟨V, V_open, x_in_V, V_in_support, disjoint_img_V⟩ := disjoint_nbhd_in (support_open f) x_in_supp_f hx_ne_x
+
+  -- let f₂ be a nontrivial element of the RigidStabilizer G V
+  let ⟨f₂, f₂_in_rist_V, f₂_ne_one⟩ := h_lm.get_nontrivial_rist_elem V_open (Set.nonempty_of_mem x_in_V)
+
+  -- Re-use the Hausdoff property of α again, this time yielding W ⊆ V
+  let ⟨y, y_moved⟩ := faithful_moves_point' α f₂_ne_one
+  have y_in_V := (rist_supported_in_set f₂_in_rist_V) (mem_support.mpr y_moved)
+  let ⟨W, W_open, y_in_W, W_in_V, disjoint_img_W⟩ := disjoint_nbhd_in V_open y_in_V y_moved
+
+  -- Let f₁ be a nontrivial element of RigidStabilizer G W
+  let ⟨f₁, f₁_in_rist_W, f₁_ne_one⟩ := h_lm.get_nontrivial_rist_elem W_open (Set.nonempty_of_mem y_in_W)
+
+  use f₁
+  use f₂
+  constructor <;> try constructor
+  · apply disjoint_commute (α := α)
+    apply Set.disjoint_of_subset_left _ supp_disjoint
+    calc
+      Support α f₁ ⊆ W := rist_supported_in_set f₁_in_rist_W
+      W ⊆ V := W_in_V
+      V ⊆ Support α f := V_in_support
+  · apply disjoint_commute (α := α)
+    apply Set.disjoint_of_subset_left _ supp_disjoint
+    calc
+      Support α f₂ ⊆ V := rist_supported_in_set f₂_in_rist_V
+      V ⊆ Support α f := V_in_support
+
+  -- We claim that [f₁, [f₂, h]] is a nontrivial elelement of Centralizer G g
+  let k := ⁅f₂, h⁆
+  have h₂ : ∀ z ∈ W, f₂ • z = k • z := by
+    intro z z_in_W
+    simp
+    symm
+    apply disjoint_support_comm f₂ h _ disjoint_img_V
+    · exact W_in_V z_in_W
+    · exact rist_supported_in_set f₂_in_rist_V
+
+  constructor
+  · -- then `k*f₁⁻¹*k⁻¹` is supported on k W = f₂ W,
+    -- so [f₁,k] is supported on W ∪ f₂ W ⊆ V ⊆ support f, so commutes with g.
+    apply disjoint_commute (α := α)
+    apply Set.disjoint_of_subset_left _ supp_disjoint
+    have supp_f₁_subset_W := (rist_supported_in_set f₁_in_rist_W)
+
+    show Support α ⁅f₁, ⁅f₂, h⁆⁆ ⊆ Support α f
+    calc
+      Support α ⁅f₁, k⁆ = Support α ⁅k, f₁⁆ := by rw [<-commutatorElement_inv, support_inv]
+      _ ⊆ Support α f₁ ∪ (k •'' Support α f₁) := support_comm α k f₁
+      _ ⊆ W ∪ (k •'' Support α f₁) := Set.union_subset_union_left _ supp_f₁_subset_W
+      _ ⊆ W ∪ (k •'' W) := by
+        apply Set.union_subset_union_right
+        exact (smulImage_subset k supp_f₁_subset_W)
+      _ = W ∪ (f₂ •'' W) := by rw [<-smulImage_eq_of_smul_eq h₂]
+      _ ⊆ V ∪ (f₂ •'' W) := Set.union_subset_union_left _ W_in_V
+      _ ⊆ V ∪ V := by
+        apply Set.union_subset_union_right
+        apply smulImage_subset_in_support f₂ W V W_in_V
+        exact rist_supported_in_set f₂_in_rist_V
+      _ ⊆ V := by rw [Set.union_self]
+      _ ⊆ Support α f := V_in_support
+
+  · -- finally, [f₁,k] agrees with f₁ on W, so is not the identity.
+    have h₄: ∀ z ∈ W, ⁅f₁, k⁆ • z = f₁ • z := by
+      apply disjoint_support_comm f₁ k
+      exact rist_supported_in_set f₁_in_rist_W
+      rw [<-smulImage_eq_of_smul_eq h₂]
+      exact disjoint_img_W
+    let ⟨z, z_in_W, z_moved⟩ := faithful_rigid_stabilizer_moves_point f₁_in_rist_W f₁_ne_one
+
+    by_contra h₅
+    rw [<-h₄ z z_in_W] at z_moved
+    have h₆ : ⁅f₁, ⁅f₂, h⁆⁆ • z = z := by rw [h₅, one_smul]
+    exact z_moved h₆
+#align proposition_1_1_1 Rubin.proposition_1_1_1
+
+-- @[simp] lemma smul''_mul {g h : G} {U : set α} : g •'' (h •'' U) = (g*h) •'' U :=
+--   (mul_smul'' g h U).symm
+-- lemma disjoint_nbhd_fin {ι : Type*} [fintype ι] {f : ι → G} {x : α} [t2_space α] : (λi : ι, f i • x).injective → ∃U : set α, is_open U ∧ x ∈ U ∧ (∀i j : ι, i ≠ j → disjoint (f i •'' U) (f j •'' U)) := begin
+--   intro f_injective,
+--   let disjoint_hyp := λi j (i_ne_j : i≠j), let x_moved : ((f j)⁻¹ * f i) • x ≠ x := begin
+--     by_contra,
+--     let := smul_congr (f j) h,
+--     rw [mul_smul, ← mul_smul,mul_right_inv,one_smul] at this,
+--     from i_ne_j (f_injective this),
+--   end in disjoint_nbhd x_moved,
+--   let ι2 := { p : ι×ι // p.1 ≠ p.2 },
+--   let U := ⋂(p : ι2), (disjoint_hyp p.1.1 p.1.2 p.2).some,
+--   use U,
+--   split,
+--   exact is_open_Inter (λp : ι2, (disjoint_hyp p.1.1 p.1.2 p.2).some_spec.1),
+--   split,
+--   exact Set.mem_Inter.mpr (λp : ι2, (disjoint_hyp p.1.1 p.1.2 p.2).some_spec.2.1),
+--   intros i j i_ne_j,
+--   let U_inc := Set.Inter_subset (λ p : ι2, (disjoint_hyp p.1.1 p.1.2 p.2).some) ⟨⟨i,j⟩,i_ne_j⟩,
+--   let := (disjoint_smul'' (f j) (Set.disjoint_of_subset U_inc (smul''_subset ((f j)⁻¹ * (f i)) U_inc) (disjoint_hyp i j i_ne_j).some_spec.2.2)).symm,
+--   simp only [subtype.val_eq_coe, smul''_mul, mul_inv_cancel_left] at this,
+--   from this
+-- end
+-- lemma moves_inj {g : G} {x : α} {n : ℕ} (period_ge_n : ∀ (k : ℤ), 1 ≤ k → k < n → g ^ k • x ≠ x) : function.injective (λ (i : fin n), g ^ (i : ℤ) • x) := begin
+--     intros i j same_img,
+--     by_contra i_ne_j,
+--     let same_img' := congr_arg ((•) (g ^ (-(j : ℤ)))) same_img,
+--     simp only [inv_smul_smul] at same_img',
+--     rw [← mul_smul,← mul_smul,← zpow_add,← zpow_add,add_comm] at same_img',
+--     simp only [add_left_neg, zpow_zero, one_smul] at same_img',
+--     let ij := |(i:ℤ) - (j:ℤ)|,
+--     rw ← sub_eq_add_neg at same_img',
+--     have xfixed : g^ij • x = x := begin
+--       cases abs_cases ((i:ℤ) - (j:ℤ)),
+--       { rw ← h.1 at same_img', exact same_img' },
+--       { rw [smul_eq_iff_inv_smul_eq,← zpow_neg,← h.1] at same_img', exact same_img' }
+--     end,
+--     have ij_ge_1 : 1 ≤ ij := int.add_one_le_iff.mpr (abs_pos.mpr $ sub_ne_zero.mpr $ norm_num.nat_cast_ne i j ↑i ↑j rfl rfl (fin.vne_of_ne i_ne_j)),
+--     let neg_le := int.sub_lt_sub_of_le_of_lt (nat.cast_nonneg i) (nat.cast_lt.mpr (fin.prop _)),
+--     rw zero_sub at neg_le,
+--     let le_pos := int.sub_lt_sub_of_lt_of_le (nat.cast_lt.mpr (fin.prop _)) (nat.cast_nonneg j),
+--     rw sub_zero at le_pos,
+--     have ij_lt_n : ij < n := abs_lt.mpr ⟨ neg_le, le_pos ⟩,
+--     exact period_ge_n ij ij_ge_1 ij_lt_n xfixed,
+-- end
+-- lemma int_to_nat (k : ℤ) (k_pos : k ≥ 1) : k = k.nat_abs := begin
+--   cases (int.nat_abs_eq k),
+--   { exact h },
+--   { have : -(k.nat_abs : ℤ) ≤ 0 := neg_nonpos.mpr (int.nat_abs k).cast_nonneg,
+--     rw ← h at this, by_contra, linarith }
+-- end
+-- lemma moves_inj_N {g : G} {x : α} {n : ℕ} (period_ge_n' : ∀ (k : ℕ), 1 ≤ k → k < n → g ^ k • x ≠ x) : function.injective (λ (i : fin n), g ^ (i : ℕ) • x) := begin
+--   have period_ge_n : ∀ (k : ℤ), 1 ≤ k → k < n → g ^ k • x ≠ x,
+--   { intros k one_le_k k_lt_n,
+--     have one_le_k_nat : 1 ≤ k.nat_abs := ((int.coe_nat_le_coe_nat_iff 1 k.nat_abs).1 ((int_to_nat k one_le_k) ▸ one_le_k)),
+--     have k_nat_lt_n : k.nat_abs < n := ((int.coe_nat_lt_coe_nat_iff k.nat_abs n).1 ((int_to_nat k one_le_k) ▸ k_lt_n)),
+--     have := period_ge_n' k.nat_abs one_le_k_nat k_nat_lt_n,
+--     rw [(zpow_coe_nat g k.nat_abs).symm, (int_to_nat k one_le_k).symm] at this,
+--     exact this },
+--   have := moves_inj period_ge_n,
+--   done
+-- end
+-- lemma moves_1234_of_moves_12 {g : G} {x : α} (xmoves : g^12 • x ≠ x) : function.injective (λi : fin 5, g^(i:ℤ) • x) := begin
+--     apply moves_inj,
+--     intros k k_ge_1 k_lt_5,
+--     by_contra xfixed,
+--     have k_div_12 : k * (12 / k) = 12 := begin
+--       interval_cases using k_ge_1 k_lt_5; norm_num
+--     end,
+--     have veryfixed : g^12 • x = x := begin
+--       let := smul_zpow_eq_of_smul_eq (12/k) xfixed,
+--       rw [← zpow_mul,k_div_12] at this,
+--       norm_cast at this
+--     end,
+--     exact xmoves veryfixed
+-- end
+-- lemma proposition_1_1_2 (f g : G) [t2_space α] : is_locally_moving G α → is_algebraically_disjoint f g → disjoint (support α f) (support α (g^12)) := begin
+--   intros locally_moving alg_disjoint,
+-- -- suppose to the contrary that the set U = supp(f) ∩ supp(g^12) is nonempty
+--   by_contra not_disjoint,
+--   let U := support α f ∩ support α (g^12),
+--   have U_nonempty : U.nonempty := Set.not_disjoint_iff_nonempty_inter.mp not_disjoint,
+-- -- since X is Hausdorff, we can find a nonempty open set V ⊆ U such that f(V) is disjoint from V and the sets {g^i(V): i=0..4} are pairwise disjoint
+--   let x := U_nonempty.some,
+--   have five_points : function.injective (λi : fin 5, g^(i:ℤ) • x) := moves_1234_of_moves_12 (mem_support.mp $ (Set.inter_subset_right _ _) U_nonempty.some_mem),
+--   rcases disjoint_nbhd_in (is_open.inter (support_open f) (support_open $ g^12)) U_nonempty.some_mem ((Set.inter_subset_left _ _) U_nonempty.some_mem) with ⟨V₀,open_V₀,x_in_V₀,V₀_in_support,disjoint_img_V₀⟩,
+--   rcases disjoint_nbhd_fin five_points with ⟨V₁,open_V₁,x_in_V₁,disjoint_img_V₁⟩,
+--   simp only at disjoint_img_V₁,
+--   let V := V₀ ∩ V₁,
+-- -- let h be a nontrivial element of rigid_stabilizer G V, and note that [f,h]≠1 since f(V) is disjoint from V
+--   let ristV_ne_bot := locally_moving V (is_open.inter open_V₀ open_V₁) (Set.nonempty_of_mem ⟨x_in_V₀,x_in_V₁⟩),
+--   rcases (or_iff_right ristV_ne_bot).mp (Subgroup.bot_or_exists_ne_one _) with ⟨h,h_in_ristV,h_ne_one⟩,
+--   have comm_non_trivial : ¬commute f h := begin
+--     by_contra comm_trivial,
+--     rcases faithful_rist_moves_point h_in_ristV h_ne_one with ⟨z,z_in_V,z_moved⟩,
+--     let act_comm := disjoint_support_comm h f (rist_supported_in_set h_in_ristV) (Set.disjoint_of_subset (Set.inter_subset_left V₀ V₁) (smul''_subset f (Set.inter_subset_left V₀ V₁)) disjoint_img_V₀) z z_in_V,
+--     rw [commutator_element_eq_one_iff_commute.mpr comm_trivial.symm,one_smul] at act_comm,
+--     exact z_moved act_comm.symm,
+--   end,
+-- -- since g is algebraically disjoint from f, there exist f₁,f₂ ∈ C_G(g) so that the commutator h' = [f1,[f2,h]] is a nontrivial element of C_G(g)
+--   rcases alg_disjoint h comm_non_trivial with ⟨f₁,f₂,f₁_commutes,f₂_commutes,h'_commutes,h'_non_trivial⟩,
+--   let h' := ⁅f₁,⁅f₂,h⁆⁆,
+-- -- now observe that supp([f₂, h]) ⊆ V ∪ f₂(V), and by the same reasoning supp(h')⊆V∪f₁(V)∪f₂(V)∪f₁f₂(V)
+--   have support_f₂h : support α ⁅f₂,h⁆ ⊆ V ∪ (f₂ •'' V) := (support_comm α f₂ h).trans (Set.union_subset_union (rist_supported_in_set h_in_ristV) $ smul''_subset f₂ $ rist_supported_in_set h_in_ristV),
+--   have support_h' : support α h' ⊆ ⋃(i : fin 2 × fin 2), (f₁^i.1.val*f₂^i.2.val) •'' V := begin
+--     let this := (support_comm α f₁ ⁅f₂,h⁆).trans (Set.union_subset_union support_f₂h (smul''_subset f₁ support_f₂h)),
+--     rw [smul''_union,← one_smul'' V,← mul_smul'',← mul_smul'',← mul_smul'',mul_one,mul_one] at this,
+--     let rw_u := rewrite_Union (λi : fin 2 × fin 2, (f₁^i.1.val*f₂^i.2.val) •'' V),
+--     simp only [fin.val_eq_coe, fin.val_zero', pow_zero, mul_one, fin.val_one, pow_one, one_mul] at rw_u,
+--     exact rw_u.symm ▸ this,
+--   end,
+-- -- since h' is nontrivial, it has at least one point p in its support
+--   cases faithful_moves_point' α h'_non_trivial with p p_moves,
+-- -- since g commutes with h', all five of the points {gi(p):i=0..4} lie in supp(h')
+--   have gi_in_support : ∀i : fin 5, g^i.val • p ∈ support α h' := begin
+--     intro i,
+--     rw mem_support,
+--     by_contra p_fixed,
+--     rw [← mul_smul,(h'_commutes.pow_right i.val).eq,mul_smul,smul_left_cancel_iff] at p_fixed,
+--     exact p_moves p_fixed,
+--   end,
+-- -- by the pigeonhole principle, one of the four sets V, f₁(V), f₂(V), f₁f₂(V) must contain two of these points, say g^i(p),g^j(p) ∈ k(V) for some 0 ≤ i < j ≤ 4 and k ∈ {1,f₁,f₂,f₁f₂}
+--   let pigeonhole : fintype.card (fin 5) > fintype.card (fin 2 × fin 2) := dec_trivial,
+--   let choice := λi : fin 5, (Set.mem_Union.mp $ support_h' $ gi_in_support i).some,
+--   rcases finset.exists_ne_map_eq_of_card_lt_of_maps_to pigeonhole (λ(i : fin 5) _, finset.mem_univ (choice i)) with ⟨i,_,j,_,i_ne_j,same_choice⟩,
+--   clear h_1_w h_1_h_h_w pigeonhole,
+--   let k := f₁^(choice i).1.val*f₂^(choice i).2.val,
+--   have same_k : f₁^(choice j).1.val*f₂^(choice j).2.val = k := by { simp only at same_choice,
+-- rw ← same_choice },
+--   have g_i : g^i.val • p ∈ k •'' V := (Set.mem_Union.mp $ support_h' $ gi_in_support i).some_spec,
+--   have g_j : g^j.val • p ∈ k •'' V := same_k ▸ (Set.mem_Union.mp $ support_h' $ gi_in_support j).some_spec,
+-- -- but since g^(j−i)(V) is disjoint from V and k commutes with g, we know that g^(j−i)k(V) is disjoint from k(V), a contradiction since g^i(p) and g^j(p) both lie in k(V).
+--   have g_disjoint : disjoint ((g^i.val)⁻¹ •'' V) ((g^j.val)⁻¹ •'' V) := begin
+--     let := (disjoint_smul'' (g^(-(i.val+j.val : ℤ))) (disjoint_img_V₁ i j i_ne_j)).symm,
+--     rw [← mul_smul'',← mul_smul'',← zpow_add,← zpow_add] at this,
+--     simp only [fin.val_eq_coe, neg_add_rev, coe_coe, neg_add_cancel_right, zpow_neg, zpow_coe_nat, neg_add_cancel_comm] at this,
+--     from Set.disjoint_of_subset (smul''_subset _ (Set.inter_subset_right V₀ V₁)) (smul''_subset _ (Set.inter_subset_right V₀ V₁)) this
+--   end,
+--   have k_commutes : commute k g := commute.mul_left (f₁_commutes.pow_left (choice i).1.val) (f₂_commutes.pow_left (choice i).2.val),
+--   have g_k_disjoint : disjoint ((g^i.val)⁻¹ •'' (k •'' V)) ((g^j.val)⁻¹ •'' (k •'' V)) := begin
+--     let this := disjoint_smul'' k g_disjoint,
+--     rw [← mul_smul'',← mul_smul'',← inv_pow g i.val,← inv_pow g j.val,
+--         ← (k_commutes.symm.inv_left.pow_left i.val).eq,
+--         ← (k_commutes.symm.inv_left.pow_left j.val).eq,
+--        mul_smul'',inv_pow g i.val,mul_smul'' (g⁻¹^j.val) k V,inv_pow g j.val] at this,
+--     from this
+--   end,
+--   exact Set.disjoint_left.mp g_k_disjoint (mem_inv_smul''.mpr g_i) (mem_inv_smul''.mpr g_j)
+-- end
+-- lemma remark_1_2 (f g : G) : is_algebraically_disjoint f g → commute f g := begin
+--   intro alg_disjoint,
+--   by_contra non_commute,
+--   rcases alg_disjoint g non_commute with ⟨_,_,_,b,_,d⟩,
+--   rw [commutator_element_eq_one_iff_commute.mpr b,commutator_element_one_right] at d,
+--   tauto
+-- end
+-- section remark_1_3
+-- def G := equiv.perm (fin 2)
+-- def σ := equiv.swap (0 : fin 2) (1 : fin 2)
+-- example : is_algebraically_disjoint σ σ := begin
+--   intro h,
+--   fin_cases h,
+--   intro hyp1,
+--   exfalso,
+--   swap, intro hyp2, exfalso,
+-- -- is commute decidable? cc,
+-- sorry -- dec_trivial
+-- sorry -- second sorry needed
+-- end
+-- end remark_1_3
+
+end Rubin
diff --git a/Rubin/FaithfulAction.lean b/Rubin/FaithfulAction.lean
index 16110e5..3bc5782 100644
--- a/Rubin/FaithfulAction.lean
+++ b/Rubin/FaithfulAction.lean
@@ -25,7 +25,7 @@ theorem faithful_moves_point' {g : G} (α : Type _) [MulAction G α] [FaithfulSM
 #align faithful_moves_point' Rubin.faithful_moves_point'
 
 theorem faithful_rigid_stabilizer_moves_point {g : G} {U : Set α} :
-    g ∈ rigidStabilizer G U → g ≠ 1 → ∃ x ∈ U, g • x ≠ x :=
+    g ∈ RigidStabilizer G U → g ≠ 1 → ∃ x ∈ U, g • x ≠ x :=
   by
   intro g_rigid g_ne_one
   let ⟨x, xmoved⟩ := Rubin.faithful_moves_point' α g_ne_one
diff --git a/Rubin/Period.lean b/Rubin/Period.lean
new file mode 100644
index 0000000..6b5bc60
--- /dev/null
+++ b/Rubin/Period.lean
@@ -0,0 +1,131 @@
+import Mathlib.Data.Finset.Basic
+import Mathlib.GroupTheory.GroupAction.Basic
+import Mathlib.GroupTheory.Exponent
+
+import Rubin.Tactic
+
+namespace Rubin.Period
+
+variable {G a : Type _}
+variable [Group G]
+variable [MulAction G α]
+
+noncomputable def period (p : α) (g : G) : ℕ :=
+  sInf {n : ℕ | n > 0 ∧ g ^ n • p = p}
+#align period Rubin.Period.period
+
+theorem period_le_fix {p : α} {g : G} {m : ℕ} (m_pos : m > 0)
+    (gmp_eq_p : g ^ m • p = p) : 0 < Rubin.Period.period p g ∧ Rubin.Period.period p g ≤ m :=
+  by
+  constructor
+  · by_contra h'; have period_zero : Rubin.Period.period p g = 0; linarith;
+    rcases Nat.sInf_eq_zero.1 period_zero with ⟨cont, h_1⟩ | h; linarith;
+    exact Set.eq_empty_iff_forall_not_mem.mp h ↑m ⟨m_pos, gmp_eq_p⟩
+  exact Nat.sInf_le ⟨m_pos, gmp_eq_p⟩
+#align period_le_fix Rubin.Period.period_le_fix
+
+theorem notfix_le_period {p : α} {g : G} {n : ℕ} (n_pos : n > 0)
+    (period_pos : Rubin.Period.period p g > 0) (pmoves : ∀ i : ℕ, 0 < i → i < n → g ^ i • p ≠ p) :
+    n ≤ Rubin.Period.period p g := by
+  by_contra period_le
+  exact
+    (pmoves (Rubin.Period.period p g) period_pos (not_le.mp period_le))
+      (Nat.sInf_mem (Nat.nonempty_of_pos_sInf period_pos)).2
+#align notfix_le_period Rubin.Period.notfix_le_period
+
+theorem notfix_le_period' {p : α} {g : G} {n : ℕ} (n_pos : n > 0)
+    (period_pos : Rubin.Period.period p g > 0)
+    (pmoves : ∀ i : Fin n, 0 < (i : ℕ) → g ^ (i : ℕ) • p ≠ p) : n ≤ Rubin.Period.period p g :=
+  Rubin.Period.notfix_le_period n_pos period_pos fun (i : ℕ) (i_pos : 0 < i) (i_lt_n : i < n) =>
+    pmoves (⟨i, i_lt_n⟩ : Fin n) i_pos
+#align notfix_le_period' Rubin.Period.notfix_le_period'
+
+theorem period_neutral_eq_one (p : α) : Rubin.Period.period p (1 : G) = 1 :=
+  by
+  have : 0 < Rubin.Period.period p (1 : G) ∧ Rubin.Period.period p (1 : G) ≤ 1 :=
+    Rubin.Period.period_le_fix (by norm_num : 1 > 0)
+      (by group_action :
+        (1 : G) ^ 1 • p = p)
+  linarith
+#align period_neutral_eq_one Rubin.Period.period_neutral_eq_one
+
+def periods (U : Set α) (H : Subgroup G) : Set ℕ :=
+  {n : ℕ | ∃ (p : α) (g : H), p ∈ U ∧ Rubin.Period.period (p : α) (g : G) = n}
+#align periods Rubin.Period.periods
+
+-- TODO: split into multiple lemmas
+theorem periods_lemmas {U : Set α} (U_nonempty : Set.Nonempty U) {H : Subgroup G}
+    (exp_ne_zero : Monoid.exponent H ≠ 0) :
+    (Rubin.Period.periods U H).Nonempty ∧
+      BddAbove (Rubin.Period.periods U H) ∧
+        ∃ (m : ℕ) (m_pos : m > 0), ∀ (p : α) (g : H), g ^ m • p = p :=
+  by
+  rcases Monoid.exponentExists_iff_ne_zero.2 exp_ne_zero with ⟨m, m_pos, gm_eq_one⟩
+  have gmp_eq_p : ∀ (p : α) (g : H), g ^ m • p = p := by
+    intro p g; rw [gm_eq_one g];
+    group_action
+  have periods_nonempty : (Rubin.Period.periods U H).Nonempty := by
+    use 1
+    let p := Set.Nonempty.some U_nonempty; use p
+    use 1
+    constructor
+    · exact Set.Nonempty.some_mem U_nonempty
+    · exact Rubin.Period.period_neutral_eq_one p
+
+  have periods_bounded : BddAbove (Rubin.Period.periods U H) := by
+    use m; intro some_period hperiod;
+    rcases hperiod with ⟨p, g, hperiod⟩
+    rw [← hperiod.2]
+    exact (Rubin.Period.period_le_fix m_pos (gmp_eq_p p g)).2
+  exact ⟨periods_nonempty, periods_bounded, m, m_pos, gmp_eq_p⟩
+#align period_lemma Rubin.Period.periods_lemmas
+
+theorem period_from_exponent (U : Set α) (U_nonempty : U.Nonempty) {H : Subgroup G}
+    (exp_ne_zero : Monoid.exponent H ≠ 0) :
+    ∃ (p : α) (g : H) (n : ℕ),
+      p ∈ U ∧ n > 0 ∧ Rubin.Period.period (p : α) (g : G) = n ∧ n = sSup (Rubin.Period.periods U H) :=
+  by
+  rcases Rubin.Period.periods_lemmas U_nonempty exp_ne_zero with
+    ⟨periods_nonempty, periods_bounded, m, m_pos, gmp_eq_p⟩
+  rcases Nat.sSup_mem periods_nonempty periods_bounded with ⟨p, g, hperiod⟩
+  use p
+  use g
+  use sSup (Rubin.Period.periods U H)
+  -- TODO: cleanup?
+  exact ⟨
+    hperiod.1,
+    hperiod.2 ▸ (Rubin.Period.period_le_fix m_pos (gmp_eq_p p g)).1,
+    hperiod.2,
+    rfl
+  ⟩
+#align period_from_exponent Rubin.Period.period_from_exponent
+
+theorem zero_lt_period_le_Sup_periods {U : Set α} (U_nonempty : U.Nonempty)
+    {H : Subgroup G} (exp_ne_zero : Monoid.exponent H ≠ 0) :
+    ∀ (p : U) (g : H),
+      0 < Rubin.Period.period (p : α) (g : G) ∧
+        Rubin.Period.period (p : α) (g : G) ≤ sSup (Rubin.Period.periods U H) :=
+  by
+  rcases Rubin.Period.periods_lemmas U_nonempty exp_ne_zero with
+    ⟨periods_nonempty, periods_bounded, m, m_pos, gmp_eq_p⟩
+  intro p g
+  have period_in_periods : Rubin.Period.period (p : α) (g : G) ∈ Rubin.Period.periods U H := by
+    use p; use g
+    simp
+  exact
+    ⟨(Rubin.Period.period_le_fix m_pos (gmp_eq_p p g)).1,
+      le_csSup periods_bounded period_in_periods⟩
+#align zero_lt_period_le_Sup_periods Rubin.Period.zero_lt_period_le_Sup_periods
+
+theorem pow_period_fix (p : α) (g : G) : g ^ Rubin.Period.period p g • p = p :=
+  by
+  cases eq_zero_or_neZero (Rubin.Period.period p g) with
+  | inl h => rw [h]; simp
+  | inr h =>
+    exact
+      (Nat.sInf_mem
+          (Nat.nonempty_of_pos_sInf
+            (Nat.pos_of_ne_zero (@NeZero.ne _ _ (Rubin.Period.period p g) h)))).2
+#align pow_period_fix Rubin.Period.pow_period_fix
+
+end Rubin.Period
diff --git a/Rubin/Topological.lean b/Rubin/Topological.lean
index 2cc59d8..c753d12 100644
--- a/Rubin/Topological.lean
+++ b/Rubin/Topological.lean
@@ -3,23 +3,25 @@ import Mathlib.GroupTheory.GroupAction.Basic
 import Mathlib.Topology.Basic
 import Mathlib.Topology.Homeomorph
 
+import Rubin.RigidStabilizer
 import Rubin.MulActionExt
 import Rubin.SmulImage
 import Rubin.Support
 
-namespace Rubin.Topological
+namespace Rubin
 
+section Continuity
 
 class ContinuousMulAction (G α : Type _) [Group G] [TopologicalSpace α] extends
     MulAction G α where
   continuous : ∀ g : G, Continuous (fun x: α => g • x)
-#align continuous_mul_action Rubin.Topological.ContinuousMulAction
+#align continuous_mul_action Rubin.ContinuousMulAction
 
 -- TODO: give this a notation?
 structure EquivariantHomeomorph (G α β : Type _) [Group G] [TopologicalSpace α]
     [TopologicalSpace β] [MulAction G α] [MulAction G β] extends Homeomorph α β where
   equivariant : is_equivariant G toFun
-#align equivariant_homeomorph Rubin.Topological.EquivariantHomeomorph
+#align equivariant_homeomorph Rubin.EquivariantHomeomorph
 
 variable {G α β : Type _}
 variable [Group G]
@@ -29,7 +31,7 @@ theorem equivariant_fun [MulAction G α] [MulAction G β]
     (h : EquivariantHomeomorph G α β) :
     is_equivariant G h.toFun :=
   h.equivariant
-#align equivariant_fun Rubin.Topological.equivariant_fun
+#align equivariant_fun Rubin.equivariant_fun
 
 theorem equivariant_inv [MulAction G α] [MulAction G β]
     (h : EquivariantHomeomorph G α β) :
@@ -40,19 +42,19 @@ theorem equivariant_inv [MulAction G α] [MulAction G β]
   let e := congr_arg h.invFun (h.equivariant g (h.invFun x))
   rw [h.left_inv _, h.right_inv _] at e
   exact e
-#align equivariant_inv Rubin.Topological.equivariant_inv
+#align equivariant_inv Rubin.equivariant_inv
 
-variable [Rubin.Topological.ContinuousMulAction G α]
+variable [Rubin.ContinuousMulAction G α]
 
 theorem img_open_open (g : G) (U : Set α) (h : IsOpen U): IsOpen (g •'' U) :=
   by
   rw [Rubin.smulImage_eq_inv_preimage]
-  exact Continuous.isOpen_preimage (Rubin.Topological.ContinuousMulAction.continuous g⁻¹) U h
+  exact Continuous.isOpen_preimage (Rubin.ContinuousMulAction.continuous g⁻¹) U h
 
-#align img_open_open Rubin.Topological.img_open_open
+#align img_open_open Rubin.img_open_open
 
 theorem support_open (g : G) [TopologicalSpace α] [T2Space α]
-    [Rubin.Topological.ContinuousMulAction G α] : IsOpen (Support α g) :=
+    [Rubin.ContinuousMulAction G α] : IsOpen (Support α g) :=
   by
   apply isOpen_iff_forall_mem_open.mpr
   intro x xmoved
@@ -63,9 +65,45 @@ theorem support_open (g : G) [TopologicalSpace α] [T2Space α]
         disjoint_U_V
         (mem_inv_smulImage.mp (Set.mem_of_mem_inter_right yW))
         (Set.mem_of_mem_inter_left yW),
-        IsOpen.inter open_V (Rubin.Topological.img_open_open g⁻¹ U open_U),
+        IsOpen.inter open_V (Rubin.img_open_open g⁻¹ U open_U),
         ⟨x_in_V, mem_inv_smulImage.mpr gx_in_U⟩
     ⟩
-#align support_open Rubin.Topological.support_open
+#align support_open Rubin.support_open
 
-end Rubin.Topological
+end Continuity
+
+-- TODO: come up with a name
+section Other
+open Topology
+
+-- Note: `𝓝[≠] x` is notation for `nhdsWithin x {[x]}ᶜ`, ie. the neighborhood of x not containing itself
+-- TODO: make this a class?
+def has_no_isolated_points (α : Type _) [TopologicalSpace α] :=
+  ∀ x : α, 𝓝[≠] x ≠ ⊥
+#align has_no_isolated_points Rubin.has_no_isolated_points
+
+instance has_no_isolated_points_neBot {α : Type _} [TopologicalSpace α] (h_nip: has_no_isolated_points α) (x: α): Filter.NeBot (𝓝[≠] x) where
+  ne' := h_nip x
+
+class LocallyDense (G α : Type _) [Group G] [TopologicalSpace α] extends MulAction G α :=
+  isLocallyDense:
+    ∀ U : Set α,
+    ∀ p ∈ U,
+    p ∈ interior (closure (MulAction.orbit (RigidStabilizer G U) p))
+#align is_locally_dense Rubin.LocallyDense
+
+namespace LocallyDense
+
+lemma nonEmpty {G α : Type _} [Group G] [TopologicalSpace α] [LocallyDense G α]:
+  ∀ {U : Set α},
+  Set.Nonempty U →
+  ∃ p ∈ U, p ∈ interior (closure (MulAction.orbit (RigidStabilizer G U) p)) := by
+  intros U H_ne
+  exact ⟨H_ne.some, H_ne.some_mem, LocallyDense.isLocallyDense U H_ne.some H_ne.some_mem⟩
+
+end LocallyDense
+
+
+end Other
+
+end Rubin