Remove namespace that conflicted with #aligns

Rubin.lean

@@ -3,7 +3,6 @@ Copyright (c) 2023 Laurent Bartholdi. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author : Laurent Bartholdi
 -/
--- import Mathbin.Tactic.Default
 import Mathlib.Data.Finset.Basic
 import Mathlib.Data.Finset.Card
 import Mathlib.Data.Fintype.Perm
@@ -19,10 +18,11 @@ import Mathlib.Topology.Homeomorph
 
 #align_import rubin
 
+-- TODO: remove
 --@[simp]
 theorem Rubin.GroupActionExt.smul_smul' {G α : Type _} [Group G] [MulAction G α] {g h : G} {x : α} :
     g • h • x = (g * h) • x :=
-  (hMul_smul g h x).symm
+  smul_smul g h x
 #align smul_smul' Rubin.GroupActionExt.smul_smul'
 
 --@[simp]
@@ -116,29 +116,27 @@ add_tactic_doc
 
 end GroupActionTactic
 
-namespace Rubin
-
 /- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:73:14: unsupported tactic `group_action #[[]] -/
 example (G α : Type _) [Group G] (a b c : G) [MulAction G α] (x : α) :
     ⁅a * b, c⁆ • x = (a * ⁅b, c⁆ * a⁻¹ * ⁅a, c⁆) • x := by
   trace
     "./././Mathport/Syntax/Translate/Tactic/Builtin.lean:73:14: unsupported tactic `group_action #[[]]"
 
-theorem Equiv.congr_ne {ι ι' : Type _} (e : ι ≃ ι') {x y : ι} : x ≠ y → e x ≠ e y :=
+theorem Rubin.equiv_congr_ne {ι ι' : Type _} (e : ι ≃ ι') {x y : ι} : x ≠ y → e x ≠ e y :=
   by
   intro x_ne_y
   by_contra h
   apply x_ne_y
   convert congr_arg e.symm h <;> simp only [Equiv.symm_apply_apply]
-#align Rubin.equiv.congr_ne Rubin.Equiv.congr_ne
+#align equiv.congr_ne Rubin.equiv_congr_ne
 
 -- this definitely should be added to mathlib!
 @[simp, to_additive]
-theorem Subgroup.mk_smul {G α : Type _} [Group G] [MulAction G α] {S : Subgroup G} {g : G}
-    (hg : g ∈ S) (a : α) : (⟨g, hg⟩ : S) • a = g • a :=
+theorem Rubin.GroupActionExt.subgroup_mk_smul {G α : Type _} [Group G] [MulAction G α]
+    {S : Subgroup G} {g : G} (hg : g ∈ S) (a : α) : (⟨g, hg⟩ : S) • a = g • a :=
   rfl
-#align Rubin.subgroup.mk_smul Rubin.Subgroup.mk_smul
-#align Rubin.subgroup.mk_vadd Rubin.Subgroup.mk_vadd
+#align subgroup.mk_smul Rubin.GroupActionExt.subgroup_mk_smul
+#align add_subgroup.mk_vadd AddSubgroup.mk_vadd
 
 ----------------------------------------------------------------
 section Rubin
@@ -148,14 +146,14 @@ variable {G α β : Type _} [Group G]
 ----------------------------------------------------------------
 section Groups
 
-theorem bracket_hMul {f g : G} : ⁅f, g⁆ = f * g * f⁻¹ * g⁻¹ := by tauto
-#align Rubin.bracket_mul Rubin.bracket_hMul
+theorem Rubin.bracket_mul {f g : G} : ⁅f, g⁆ = f * g * f⁻¹ * g⁻¹ := by tauto
+#align bracket_mul Rubin.bracket_mul
 
-def IsAlgebraicallyDisjoint (f g : G) :=
+def Rubin.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 Rubin.is_algebraically_disjoint Rubin.IsAlgebraicallyDisjoint
+#align is_algebraically_disjoint Rubin.is_algebraically_disjoint
 
 end Groups
 
@@ -164,11 +162,8 @@ section Actions
 
 variable [MulAction G α]
 
-/- warning: Rubin.orbit_bot clashes with orbit_bot -> Rubin.orbit_bot
-Case conversion may be inaccurate. Consider using '#align Rubin.orbit_bot Rubin.orbit_botₓ'. -/
-#print Rubin.orbit_bot /-
 @[simp]
-theorem orbit_bot (G : Type _) [Group G] [MulAction G α] (p : α) :
+theorem Rubin.orbit_bot (G : Type _) [Group G] [MulAction G α] (p : α) :
     MulAction.orbit (⊥ : Subgroup G) p = {p} :=
   by
   ext1
@@ -178,32 +173,31 @@ theorem orbit_bot (G : Type _) [Group G] [MulAction G α] (p : α) :
     rw [← g_to_x, Set.mem_singleton_iff, Rubin.GroupActionExt.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 Rubin.orbit_bot Rubin.orbit_bot
--/
+#align orbit_bot Rubin.orbit_bot
 
 --------------------------------
 section Smul''
 
-theorem smul_congr (g : G) {x y : α} (h : x = y) : g • x = g • y :=
+theorem Rubin.GroupActionExt.smul_congr (g : G) {x y : α} (h : x = y) : g • x = g • y :=
   congr_arg ((· • ·) g) h
-#align Rubin.smul_congr Rubin.smul_congr
+#align smul_congr Rubin.GroupActionExt.smul_congr
 
-theorem smul_eq_iff_inv_smul_eq {x : α} {g : G} : g • x = x ↔ g⁻¹ • x = x :=
-  ⟨fun h => (smul_congr g⁻¹ h).symm.trans (inv_smul_smul g x), fun h =>
-    (smul_congr g h).symm.trans (smul_inv_smul g x)⟩
-#align Rubin.smul_eq_iff_inv_smul_eq Rubin.smul_eq_iff_inv_smul_eq
+theorem Rubin.GroupActionExt.smul_eq_iff_inv_smul_eq {x : α} {g : G} : g • x = x ↔ g⁻¹ • x = x :=
+  ⟨fun h => (Rubin.GroupActionExt.smul_congr g⁻¹ h).symm.trans (inv_smul_smul g x), fun h =>
+    (Rubin.GroupActionExt.smul_congr g h).symm.trans (smul_inv_smul g x)⟩
+#align smul_eq_iff_inv_smul_eq Rubin.GroupActionExt.smul_eq_iff_inv_smul_eq
 
-theorem smul_pow_eq_of_smul_eq {x : α} {g : G} (n : ℕ) : g • x = x → g ^ n • x = x :=
-  by
+theorem Rubin.GroupActionExt.smul_pow_eq_of_smul_eq {x : α} {g : G} (n : ℕ) :
+    g • x = x → g ^ n • x = x := by
   induction n
   simp only [pow_zero, one_smul, eq_self_iff_true, imp_true_iff]
   · intro h
     nth_rw 2 [← (Rubin.GroupActionExt.smul_congr g (n_ih h)).trans h]
     rw [← mul_smul, ← pow_succ]
-#align Rubin.smul_pow_eq_of_smul_eq Rubin.smul_pow_eq_of_smul_eq
+#align smul_pow_eq_of_smul_eq Rubin.GroupActionExt.smul_pow_eq_of_smul_eq
 
-theorem smul_zpow_eq_of_smul_eq {x : α} {g : G} (n : ℤ) : g • x = x → g ^ n • x = x :=
-  by
+theorem Rubin.GroupActionExt.smul_zpow_eq_of_smul_eq {x : α} {g : G} (n : ℤ) :
+    g • x = x → g ^ n • x = x := by
   intro h
   cases n
   · let this.1 := Rubin.GroupActionExt.smul_pow_eq_of_smul_eq n h; finish
@@ -211,31 +205,32 @@ theorem smul_zpow_eq_of_smul_eq {x : α} {g : G} (n : ℤ) : g • x = x → g ^
     let this.1 :=
       smul_eq_iff_inv_smul_eq.mp (Rubin.GroupActionExt.smul_pow_eq_of_smul_eq (1 + n) h);
     finish
-#align Rubin.smul_zpow_eq_of_smul_eq Rubin.smul_zpow_eq_of_smul_eq
+#align smul_zpow_eq_of_smul_eq Rubin.GroupActionExt.smul_zpow_eq_of_smul_eq
 
-def IsEquivariant (G : Type _) {β : Type _} [Group G] [MulAction G α] [MulAction G β] (f : α → β) :=
+def Rubin.GroupActionExt.is_equivariant (G : Type _) {β : Type _} [Group G] [MulAction G α]
+    [MulAction G β] (f : α → β) :=
   ∀ g : G, ∀ x : α, f (g • x) = g • f x
-#align Rubin.is_equivariant Rubin.IsEquivariant
+#align is_equivariant Rubin.GroupActionExt.is_equivariant
 
-def subsetImg' (g : G) (U : Set α) :=
+def Rubin.SmulImage.smulImage' (g : G) (U : Set α) :=
   {x | g⁻¹ • x ∈ U}
-#align Rubin.subset_img' Rubin.subsetImg'
+#align subset_img' Rubin.SmulImage.smulImage'
 
-def subsetPreimg' (g : G) (U : Set α) :=
+def Rubin.SmulImage.smul_preimage' (g : G) (U : Set α) :=
   {x | g • x ∈ U}
-#align Rubin.subset_preimg' Rubin.subsetPreimg'
+#align subset_preimg' Rubin.SmulImage.smul_preimage'
 
-def subsetImg (g : G) (U : Set α) :=
+def Rubin.SmulImage.SmulImage (g : G) (U : Set α) :=
   (· • ·) g '' U
-#align Rubin.subset_img Rubin.subsetImg
+#align subset_img Rubin.SmulImage.SmulImage
 
-infixl:60 "•''" => subsetImg
+infixl:60 "•''" => Rubin.SmulImage.SmulImage
 
-theorem subsetImg_def {g : G} {U : Set α} : g•''U = (· • ·) g '' U :=
+theorem Rubin.SmulImage.smulImage_def {g : G} {U : Set α} : g•''U = (· • ·) g '' U :=
   rfl
-#align Rubin.subset_img_def Rubin.subsetImg_def
+#align subset_img_def Rubin.SmulImage.smulImage_def
 
-theorem mem_smul'' {x : α} {g : G} {U : Set α} : x ∈ g•''U ↔ g⁻¹ • x ∈ U :=
+theorem Rubin.SmulImage.mem_smulImage {x : α} {g : G} {U : Set α} : x ∈ g•''U ↔ g⁻¹ • x ∈ U :=
   by
   rw [Rubin.SmulImage.smulImage_def, Set.mem_image ((· • ·) g) U x]
   constructor
@@ -244,35 +239,36 @@ theorem mem_smul'' {x : α} {g : G} {U : Set α} : x ∈ g•''U ↔ g⁻¹ •
     exact ygx ▸ yU
   · intro h
     use⟨g⁻¹ • x, set.mem_preimage.mp h, smul_inv_smul g x⟩
-#align Rubin.mem_smul'' Rubin.mem_smul''
+#align mem_smul'' Rubin.SmulImage.mem_smulImage
 
-theorem mem_inv_smul'' {x : α} {g : G} {U : Set α} : x ∈ g⁻¹•''U ↔ g • x ∈ U :=
+theorem Rubin.SmulImage.mem_inv_smulImage {x : α} {g : G} {U : Set α} : x ∈ g⁻¹•''U ↔ g • x ∈ U :=
   by
   let msi := @Rubin.SmulImage.mem_smulImage _ _ _ _ x g⁻¹ U
   rw [inv_inv] at msi
   exact msi
-#align Rubin.mem_inv_smul'' Rubin.mem_inv_smul''
+#align mem_inv_smul'' Rubin.SmulImage.mem_inv_smulImage
 
-theorem hMul_smul'' (g h : G) (U : Set α) : g * h•''U = g•''(h•''U) :=
+theorem Rubin.SmulImage.mul_smulImage (g h : G) (U : Set α) : g * h•''U = g•''(h•''U) :=
   by
   ext
   rw [Rubin.SmulImage.mem_smulImage, Rubin.SmulImage.mem_smulImage, Rubin.SmulImage.mem_smulImage, ←
     mul_smul, mul_inv_rev]
-#align Rubin.mul_smul'' Rubin.hMul_smul''
+#align mul_smul'' Rubin.SmulImage.mul_smulImage
 
 @[simp]
-theorem smul''_smul'' {g h : G} {U : Set α} : g•''(h•''U) = g * h•''U :=
-  (hMul_smul'' g h U).symm
-#align Rubin.smul''_smul'' Rubin.smul''_smul''
+theorem Rubin.SmulImage.smulImage_smulImage {g h : G} {U : Set α} : g•''(h•''U) = g * h•''U :=
+  (Rubin.SmulImage.mul_smulImage g h U).symm
+#align smul''_smul'' Rubin.SmulImage.smulImage_smulImage
 
 @[simp]
-theorem one_smul'' (U : Set α) : (1 : G)•''U = U :=
+theorem Rubin.SmulImage.one_smulImage (U : Set α) : (1 : G)•''U = U :=
   by
   ext
   rw [Rubin.SmulImage.mem_smulImage, inv_one, one_smul]
-#align Rubin.one_smul'' Rubin.one_smul''
+#align one_smul'' Rubin.SmulImage.one_smulImage
 
-theorem disjoint_smul'' (g : G) {U V : Set α} : Disjoint U V → Disjoint (g•''U) (g•''V) :=
+theorem Rubin.SmulImage.disjoint_smulImage (g : G) {U V : Set α} :
+    Disjoint U V → Disjoint (g•''U) (g•''V) :=
   by
   intro disjoint_U_V
   rw [Set.disjoint_left]
@@ -280,43 +276,44 @@ theorem disjoint_smul'' (g : G) {U V : Set α} : Disjoint U V → Disjoint (g•
   intro x x_in_gU
   by_contra h
   exact (disjoint_U_V (mem_smul''.mp x_in_gU)) (mem_smul''.mp h)
-#align Rubin.disjoint_smul'' Rubin.disjoint_smul''
+#align disjoint_smul'' Rubin.SmulImage.disjoint_smulImage
 
 -- TODO: check if this is actually needed
-theorem smul''_congr (g : G) {U V : Set α} : U = V → g•''U = g•''V :=
+theorem Rubin.SmulImage.smulImage_congr (g : G) {U V : Set α} : U = V → g•''U = g•''V :=
   congr_arg fun W : Set α => g•''W
-#align Rubin.smul''_congr Rubin.smul''_congr
+#align smul''_congr Rubin.SmulImage.smulImage_congr
 
-theorem smul''_subset (g : G) {U V : Set α} : U ⊆ V → g•''U ⊆ g•''V :=
+theorem Rubin.SmulImage.smulImage_subset (g : G) {U V : Set α} : U ⊆ V → g•''U ⊆ g•''V :=
   by
   intro h1 x
   rw [Rubin.SmulImage.mem_smulImage, Rubin.SmulImage.mem_smulImage]
   exact fun h2 => h1 h2
-#align Rubin.smul''_subset Rubin.smul''_subset
+#align smul''_subset Rubin.SmulImage.smulImage_subset
 
-theorem smul''_union (g : G) {U V : Set α} : g•''U ∪ V = (g•''U) ∪ (g•''V) :=
+theorem Rubin.SmulImage.smulImage_union (g : G) {U V : Set α} : g•''U ∪ V = (g•''U) ∪ (g•''V) :=
   by
   ext
   rw [Rubin.SmulImage.mem_smulImage, Set.mem_union, Set.mem_union, Rubin.SmulImage.mem_smulImage,
     Rubin.SmulImage.mem_smulImage]
-#align Rubin.smul''_union Rubin.smul''_union
+#align smul''_union Rubin.SmulImage.smulImage_union
 
-theorem smul''_inter (g : G) {U V : Set α} : g•''U ∩ V = (g•''U) ∩ (g•''V) :=
+theorem Rubin.SmulImage.smulImage_inter (g : G) {U V : Set α} : g•''U ∩ V = (g•''U) ∩ (g•''V) :=
   by
   ext
   rw [Set.mem_inter_iff, Rubin.SmulImage.mem_smulImage, Rubin.SmulImage.mem_smulImage,
     Rubin.SmulImage.mem_smulImage, Set.mem_inter_iff]
-#align Rubin.smul''_inter Rubin.smul''_inter
+#align smul''_inter Rubin.SmulImage.smulImage_inter
 
-theorem smul''_eq_inv_preimage {g : G} {U : Set α} : g•''U = (· • ·) g⁻¹ ⁻¹' U :=
+theorem Rubin.SmulImage.smulImage_eq_inv_preimage {g : G} {U : Set α} : g•''U = (· • ·) g⁻¹ ⁻¹' U :=
   by
   ext
   constructor
   · intro h; rw [Set.mem_preimage]; exact mem_smul''.mp h
   · intro h; rw [Rubin.SmulImage.mem_smulImage]; exact set.mem_preimage.mp h
-#align Rubin.smul''_eq_inv_preimage Rubin.smul''_eq_inv_preimage
+#align smul''_eq_inv_preimage Rubin.SmulImage.smulImage_eq_inv_preimage
 
-theorem smul''_eq_of_smul_eq {g h : G} {U : Set α} : (∀ x ∈ U, g • x = h • x) → g•''U = h•''U :=
+theorem Rubin.SmulImage.smulImage_eq_of_smul_eq {g h : G} {U : Set α} :
+    (∀ x ∈ U, g • x = h • x) → g•''U = h•''U :=
   by
   intro hU
   ext
@@ -326,41 +323,48 @@ theorem smul''_eq_of_smul_eq {g h : G} {U : Set α} : (∀ x ∈ U, g • x = h
     simp only [smul_inv_smul, inv_smul_smul] at a ; exact Set.mem_of_eq_of_mem a k
   · intro k; let a := congr_arg ((· • ·) g⁻¹) (hU (h⁻¹ • x) k);
     simp only [smul_inv_smul, inv_smul_smul] at a ; exact Set.mem_of_eq_of_mem a.symm k
-#align Rubin.smul''_eq_of_smul_eq Rubin.smul''_eq_of_smul_eq
+#align smul''_eq_of_smul_eq Rubin.SmulImage.smulImage_eq_of_smul_eq
 
 end Smul''
 
 --------------------------------
 section Rubin.SmulSupport.Support
 
-def support (α : Type _) [MulAction G α] (g : G) :=
+def Rubin.SmulSupport.Support (α : Type _) [MulAction G α] (g : G) :=
   {x : α | g • x ≠ x}
-#align Rubin.support Rubin.support
+#align support Rubin.SmulSupport.Support
 
-theorem support_eq_not_fixedBy {g : G} : support α g = MulAction.fixedBy G α gᶜ := by tauto
-#align Rubin.support_eq_not_fixed_by Rubin.support_eq_not_fixedBy
+theorem Rubin.SmulSupport.support_eq_not_fixed_by {g : G} :
+    Rubin.SmulSupport.Support α g = MulAction.fixedBy G α gᶜ := by tauto
+#align support_eq_not_fixed_by Rubin.SmulSupport.support_eq_not_fixed_by
 
-theorem mem_support {x : α} {g : G} : x ∈ support α g ↔ g • x ≠ x := by tauto
-#align Rubin.mem_support Rubin.mem_support
+theorem Rubin.SmulSupport.mem_support {x : α} {g : G} :
+    x ∈ Rubin.SmulSupport.Support α g ↔ g • x ≠ x := by tauto
+#align mem_support Rubin.SmulSupport.mem_support
 
-theorem mem_not_support {x : α} {g : G} : x ∉ support α g ↔ g • x = x := by
+theorem Rubin.SmulSupport.not_mem_support {x : α} {g : G} :
+    x ∉ Rubin.SmulSupport.Support α g ↔ g • x = x := by
   rw [Rubin.SmulSupport.mem_support, Classical.not_not]
-#align Rubin.mem_not_support Rubin.mem_not_support
+#align mem_not_support Rubin.SmulSupport.not_mem_support
 
-theorem smul_in_support {g : G} {x : α} : x ∈ support α g → g • x ∈ support α g := fun h =>
+theorem Rubin.SmulSupport.smul_mem_support {g : G} {x : α} :
+    x ∈ Rubin.SmulSupport.Support α g → g • x ∈ Rubin.SmulSupport.Support α g := fun h =>
   h ∘ smul_left_cancel g
-#align Rubin.smul_in_support Rubin.smul_in_support
+#align smul_in_support Rubin.SmulSupport.smul_mem_support
 
-theorem inv_smul_in_support {g : G} {x : α} : x ∈ support α g → g⁻¹ • x ∈ support α g := fun h k =>
-  h (smul_inv_smul g x ▸ smul_congr g k)
-#align Rubin.inv_smul_in_support Rubin.inv_smul_in_support
+theorem Rubin.SmulSupport.inv_smul_mem_support {g : G} {x : α} :
+    x ∈ Rubin.SmulSupport.Support α g → g⁻¹ • x ∈ Rubin.SmulSupport.Support α g := fun h k =>
+  h (smul_inv_smul g x ▸ Rubin.GroupActionExt.smul_congr g k)
+#align inv_smul_in_support Rubin.SmulSupport.inv_smul_mem_support
 
-theorem fixed_of_disjoint {g : G} {x : α} {U : Set α} :
-    x ∈ U → Disjoint U (support α g) → g • x = x := fun x_in_U disjoint_U_support =>
-  mem_not_support.mp (Set.disjoint_left.mp disjoint_U_support x_in_U)
-#align Rubin.fixed_of_disjoint Rubin.fixed_of_disjoint
+theorem Rubin.SmulSupport.fixed_of_disjoint {g : G} {x : α} {U : Set α} :
+    x ∈ U → Disjoint U (Rubin.SmulSupport.Support α g) → g • x = x :=
+  fun x_in_U disjoint_U_support =>
+  Rubin.SmulSupport.not_mem_support.mp (Set.disjoint_left.mp disjoint_U_support x_in_U)
+#align fixed_of_disjoint Rubin.SmulSupport.fixed_of_disjoint
 
-theorem fixes_subset_within_support (g : G) {U : Set α} : support α g ⊆ U → g•''U = U :=
+theorem Rubin.SmulSupport.fixed_smulImage_in_support (g : G) {U : Set α} :
+    Rubin.SmulSupport.Support α g ⊆ U → g•''U = U :=
   by
   intro support_in_U
   ext x
@@ -369,14 +373,17 @@ theorem fixes_subset_within_support (g : G) {U : Set α} : support α g ⊆ U
     ⟨fun _ => support_in_U xmoved, fun _ =>
       mem_smul''.mpr (support_in_U (Rubin.SmulSupport.inv_smul_mem_support xmoved))⟩
   rw [Rubin.SmulImage.mem_smulImage, smul_eq_iff_inv_smul_eq.mp (mem_not_support.mp xfixed)]
-#align Rubin.fixes_subset_within_support Rubin.fixes_subset_within_support
+#align fixes_subset_within_support Rubin.SmulSupport.fixed_smulImage_in_support
 
-theorem moves_subset_within_support (g : G) (U V : Set α) : U ⊆ V → support α g ⊆ V → g•''U ⊆ V :=
-  fun U_in_V support_in_V => fixes_subset_within_support g support_in_V ▸ smul''_subset g U_in_V
-#align Rubin.moves_subset_within_support Rubin.moves_subset_within_support
+theorem Rubin.SmulSupport.smulImage_subset_in_support (g : G) (U V : Set α) :
+    U ⊆ V → Rubin.SmulSupport.Support α g ⊆ V → g•''U ⊆ V := fun U_in_V support_in_V =>
+  Rubin.SmulSupport.fixed_smulImage_in_support g support_in_V ▸
+    Rubin.SmulImage.smulImage_subset g U_in_V
+#align moves_subset_within_support Rubin.SmulSupport.smulImage_subset_in_support
 
-theorem support_hMul (g h : G) (α : Type _) [MulAction G α] :
-    support α (g * h) ⊆ support α g ∪ support α h :=
+theorem Rubin.SmulSupport.support_mul (g h : G) (α : Type _) [MulAction G α] :
+    Rubin.SmulSupport.Support α (g * h) ⊆
+      Rubin.SmulSupport.Support α g ∪ Rubin.SmulSupport.Support α h :=
   by
   intro x x_in_support
   by_contra h_support
@@ -385,10 +392,10 @@ theorem support_hMul (g h : G) (α : Type _) [MulAction G α] :
     x_in_support
       ((mul_smul g h x).trans
         ((congr_arg ((· • ·) g) (mem_not_support.mp this.2)).trans <| mem_not_support.mp this.1))
-#align Rubin.support_mul Rubin.support_hMul
+#align support_mul Rubin.SmulSupport.support_mul
 
-theorem support_conjugate (α : Type _) [MulAction G α] (g h : G) :
-    support α (h * g * h⁻¹) = h•''support α g :=
+theorem Rubin.SmulSupport.support_conjugate (α : Type _) [MulAction G α] (g h : G) :
+    Rubin.SmulSupport.Support α (h * g * h⁻¹) = h•''Rubin.SmulSupport.Support α g :=
   by
   ext
   rw [Rubin.SmulSupport.mem_support, Rubin.SmulImage.mem_smulImage, Rubin.SmulSupport.mem_support,
@@ -396,19 +403,21 @@ theorem support_conjugate (α : Type _) [MulAction G α] (g h : G) :
   constructor
   · intro h1; by_contra h2; exact h1 ((congr_arg ((· • ·) h) h2).trans (smul_inv_smul _ _))
   · intro h1; by_contra h2; exact h1 (inv_smul_smul h (g • h⁻¹ • x) ▸ congr_arg ((· • ·) h⁻¹) h2)
-#align Rubin.support_conjugate Rubin.support_conjugate
+#align support_conjugate Rubin.SmulSupport.support_conjugate
 
-theorem support_inv (α : Type _) [MulAction G α] (g : G) : support α g⁻¹ = support α g :=
+theorem Rubin.SmulSupport.support_inv (α : Type _) [MulAction G α] (g : G) :
+    Rubin.SmulSupport.Support α g⁻¹ = Rubin.SmulSupport.Support α g :=
   by
   ext
   rw [Rubin.SmulSupport.mem_support, Rubin.SmulSupport.mem_support]
   constructor
   · intro h1; by_contra h2; exact h1 (smul_eq_iff_inv_smul_eq.mp h2)
   · intro h1; by_contra h2; exact h1 (smul_eq_iff_inv_smul_eq.mpr h2)
-#align Rubin.support_inv Rubin.support_inv
+#align support_inv Rubin.SmulSupport.support_inv
 
-theorem support_pow (α : Type _) [MulAction G α] (g : G) (j : ℕ) :
-    support α (g ^ j) ⊆ support α g := by
+theorem Rubin.SmulSupport.support_pow (α : Type _) [MulAction G α] (g : G) (j : ℕ) :
+    Rubin.SmulSupport.Support α (g ^ j) ⊆ Rubin.SmulSupport.Support α g :=
+  by
   intro x xmoved
   by_contra xfixed
   rw [Rubin.SmulSupport.mem_support] at xmoved
@@ -418,10 +427,11 @@ theorem support_pow (α : Type _) [MulAction G α] (g : G) (j : ℕ) :
     let j_ih := (congr_arg ((· • ·) g) (not_not.mp j_ih)).trans (mem_not_support.mp xfixed)
     rw [← mul_smul, ← pow_succ] at j_ih
     exact j_ih
-#align Rubin.support_pow Rubin.support_pow
+#align support_pow Rubin.SmulSupport.support_pow
 
-theorem support_comm (α : Type _) [MulAction G α] (g h : G) :
-    support α ⁅g, h⁆ ⊆ support α h ∪ (g•''support α h) :=
+theorem Rubin.SmulSupport.support_comm (α : Type _) [MulAction G α] (g h : G) :
+    Rubin.SmulSupport.Support α ⁅g, h⁆ ⊆
+      Rubin.SmulSupport.Support α h ∪ (g•''Rubin.SmulSupport.Support α h) :=
   by
   intro x x_in_support
   by_contra all_fixed
@@ -433,10 +443,10 @@ theorem support_comm (α : Type _) [MulAction G α] (g h : G) :
       ((Rubin.SmulSupport.support_conjugate α h g).symm ▸ (not_or_distrib.mp all_fixed).2)
         x_in_support
   · exact all_fixed (Or.inl xmoved)
-#align Rubin.support_comm Rubin.support_comm
+#align support_comm Rubin.SmulSupport.support_comm
 
-theorem disjoint_support_comm (f g : G) {U : Set α} :
-    support α f ⊆ U → Disjoint U (g•''U) → ∀ x ∈ U, ⁅f, g⁆ • x = f • x :=
+theorem Rubin.SmulSupport.disjoint_support_comm (f g : G) {U : Set α} :
+    Rubin.SmulSupport.Support α f ⊆ U → Disjoint U (g•''U) → ∀ x ∈ U, ⁅f, g⁆ • x = f • x :=
   by
   intro support_in_U disjoint_U x x_in_U
   have support_conj : Rubin.SmulSupport.Support α (g * f⁻¹ * g⁻¹) ⊆ g•''U :=
@@ -449,27 +459,28 @@ theorem disjoint_support_comm (f g : G) {U : Set α} :
           (Set.disjoint_of_subset_right support_conj disjoint_U))).symm
   rw [← mul_smul, ← mul_assoc, ← mul_assoc] at goal
   exact goal.symm
-#align Rubin.disjoint_support_comm Rubin.disjoint_support_comm
+#align disjoint_support_comm Rubin.SmulSupport.disjoint_support_comm
 
 end Rubin.SmulSupport.Support
 
 -- comment by Cedric: would be nicer to define just a subset, and then show it is a subgroup
 def rigidStabilizer' (G : Type _) [Group G] [MulAction G α] (U : Set α) : Set G :=
   {g : G | ∀ x : α, g • x = x ∨ x ∈ U}
-#align Rubin.rigid_stabilizer' Rubin.rigidStabilizer'
+#align rigid_stabilizer' rigidStabilizer'
 
 /- ./././Mathport/Syntax/Translate/Basic.lean:641:2: warning: expanding binder collection (x «expr ∉ » U) -/
 def rigidStabilizer (G : Type _) [Group G] [MulAction G α] (U : Set α) : Subgroup G
     where
   carrier := {g : G | ∀ (x) (_ : x ∉ U), g • x = x}
   hMul_mem' a b ha hb x x_notin_U := by rw [mul_smul a b x, hb x x_notin_U, ha x x_notin_U]
-  inv_mem' _ hg x x_notin_U := smul_eq_iff_inv_smul_eq.mp (hg x x_notin_U)
+  inv_mem' _ hg x x_notin_U := Rubin.GroupActionExt.smul_eq_iff_inv_smul_eq.mp (hg x x_notin_U)
   one_mem' x _ := one_smul G x
-#align Rubin.rigid_stabilizer Rubin.rigidStabilizer
+#align rigid_stabilizer rigidStabilizer
 
-theorem rist_supported_in_set {g : G} {U : Set α} : g ∈ rigidStabilizer G U → support α g ⊆ U :=
-  fun h x x_in_support => by_contradiction (x_in_support ∘ h x)
-#align Rubin.rist_supported_in_set Rubin.rist_supported_in_set
+theorem rist_supported_in_set {g : G} {U : Set α} :
+    g ∈ rigidStabilizer G U → Rubin.SmulSupport.Support α g ⊆ U := fun h x x_in_support =>
+  by_contradiction (x_in_support ∘ h x)
+#align rist_supported_in_set rist_supported_in_set
 
 theorem rist_ss_rist {U V : Set α} (V_ss_U : V ⊆ U) :
     (rigidStabilizer G V : Set G) ⊆ (rigidStabilizer G U : Set G) :=
@@ -477,7 +488,7 @@ theorem rist_ss_rist {U V : Set α} (V_ss_U : V ⊆ U) :
   intro g g_in_ristV x x_notin_U
   have x_notin_V : x ∉ V := by intro x_in_V; exact x_notin_U (V_ss_U x_in_V)
   exact g_in_ristV x x_notin_V
-#align Rubin.rist_ss_rist Rubin.rist_ss_rist
+#align rist_ss_rist rist_ss_rist
 
 end Actions
 
@@ -486,38 +497,44 @@ section TopologicalActions
 
 variable [TopologicalSpace α] [TopologicalSpace β]
 
-class ContinuousMulAction (G α : Type _) [Group G] [TopologicalSpace α] extends MulAction G α where
+class Rubin.Topological.ContinuousMulAction (G α : Type _) [Group G] [TopologicalSpace α] extends
+    MulAction G α where
   Continuous : ∀ g : G, Continuous (@SMul.smul G α _ g)
-#align Rubin.continuous_mul_action Rubin.ContinuousMulAction
+#align continuous_mul_action Rubin.Topological.ContinuousMulAction
 
-structure EquivariantHomeomorph (G α β : Type _) [Group G] [TopologicalSpace α] [TopologicalSpace β]
-    [MulAction G α] [MulAction G β] extends Homeomorph α β where
-  equivariant : IsEquivariant G to_fun
-#align Rubin.equivariant_homeomorph Rubin.EquivariantHomeomorph
+structure Rubin.Topological.equivariant_homeomorph (G α β : Type _) [Group G] [TopologicalSpace α]
+    [TopologicalSpace β] [MulAction G α] [MulAction G β] extends Homeomorph α β where
+  equivariant : Rubin.GroupActionExt.is_equivariant G to_fun
+#align equivariant_homeomorph Rubin.Topological.equivariant_homeomorph
 
-theorem equivariantFun [MulAction G α] [MulAction G β] (h : EquivariantHomeomorph G α β) :
-    IsEquivariant G h.toFun :=
+theorem Rubin.Topological.equivariant_fun [MulAction G α] [MulAction G β]
+    (h : Rubin.Topological.equivariant_homeomorph G α β) :
+    Rubin.GroupActionExt.is_equivariant G h.toFun :=
   h.equivariant
-#align Rubin.equivariant_fun Rubin.equivariantFun
+#align equivariant_fun Rubin.Topological.equivariant_fun
 
-theorem equivariantInv [MulAction G α] [MulAction G β] (h : EquivariantHomeomorph G α β) :
-    IsEquivariant G h.invFun := by
+theorem Rubin.Topological.equivariant_inv [MulAction G α] [MulAction G β]
+    (h : Rubin.Topological.equivariant_homeomorph G α β) :
+    Rubin.GroupActionExt.is_equivariant G h.invFun :=
+  by
   intro g x
   let e := congr_arg h.inv_fun (h.equivariant g (h.inv_fun x))
   rw [h.left_inv _, h.right_inv _] at e
   exact e.symm
-#align Rubin.equivariant_inv Rubin.equivariantInv
+#align equivariant_inv Rubin.Topological.equivariant_inv
 
-variable [ContinuousMulAction G α]
+variable [Rubin.Topological.ContinuousMulAction G α]
 
-theorem img_open_open (g : G) (U : Set α) (h : IsOpen U) [ContinuousMulAction G α] :
-    IsOpen (g•''U) := by
+theorem Rubin.Topological.img_open_open (g : G) (U : Set α) (h : IsOpen U)
+    [Rubin.Topological.ContinuousMulAction G α] : IsOpen (g•''U) :=
+  by
   rw [Rubin.SmulImage.smulImage_eq_inv_preimage]
-  exact Continuous.isOpen_preimage (continuous_mul_action.continuous g⁻¹) U h
-#align Rubin.img_open_open Rubin.img_open_open
+  exact Continuous.isOpen_preimage (Rubin.Topological.ContinuousMulAction.continuous g⁻¹) U h
+#align img_open_open Rubin.Topological.img_open_open
 
-theorem support_open (g : G) [TopologicalSpace α] [T2Space α] [ContinuousMulAction G α] :
-    IsOpen (support α g) := by
+theorem Rubin.Topological.support_open (g : G) [TopologicalSpace α] [T2Space α]
+    [Rubin.Topological.ContinuousMulAction G α] : IsOpen (Rubin.SmulSupport.Support α g) :=
+  by
   apply is_open_iff_forall_mem_open.mpr
   intro x xmoved
   rcases T2Space.t2 (g • x) x xmoved with ⟨U, V, open_U, open_V, gx_in_U, x_in_V, disjoint_U_V⟩
@@ -527,7 +544,7 @@ theorem support_open (g : G) [TopologicalSpace α] [T2Space α] [ContinuousMulAc
         (mem_inv_smul''.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),
       ⟨x_in_V, mem_inv_smul''.mpr gx_in_U⟩⟩
-#align Rubin.support_open Rubin.support_open
+#align support_open Rubin.Topological.support_open
 
 end TopologicalActions
 
@@ -536,33 +553,34 @@ section FaithfulActions
 
 variable [MulAction G α] [FaithfulSMul G α]
 
-theorem faithful_moves_point {g : G} (h2 : ∀ x : α, g • x = x) : g = 1 :=
+theorem Rubin.faithful_moves_point₁ {g : G} (h2 : ∀ x : α, g • x = x) : g = 1 :=
   haveI h3 : ∀ x : α, g • x = (1 : G) • x := fun x => (h2 x).symm ▸ (one_smul G x).symm
   eq_of_smul_eq_smul h3
-#align Rubin.faithful_moves_point Rubin.faithful_moves_point
+#align faithful_moves_point Rubin.faithful_moves_point₁
 
-theorem faithful_moves_point' {g : G} (α : Type _) [MulAction G α] [FaithfulSMul G α] :
+theorem Rubin.faithful_moves_point'₁ {g : G} (α : Type _) [MulAction G α] [FaithfulSMul G α] :
     g ≠ 1 → ∃ x : α, g • x ≠ x := fun k =>
-  by_contradiction fun h => k <| faithful_moves_point <| Classical.not_exists_not.mp h
-#align Rubin.faithful_moves_point' Rubin.faithful_moves_point'
+  by_contradiction fun h => k <| Rubin.faithful_moves_point₁ <| Classical.not_exists_not.mp h
+#align faithful_moves_point' Rubin.faithful_moves_point'₁
 
-theorem faithful_rist_moves_point {g : G} {U : Set α} :
+theorem Rubin.faithful_rigid_stabilizer_moves_point {g : G} {U : Set α} :
     g ∈ rigidStabilizer G U → g ≠ 1 → ∃ x ∈ U, g • x ≠ x :=
   by
   intro g_rigid g_ne_one
   rcases Rubin.faithful_moves_point'₁ α g_ne_one with ⟨x, xmoved⟩
   exact ⟨x, rist_supported_in_set g_rigid xmoved, xmoved⟩
-#align Rubin.faithful_rist_moves_point Rubin.faithful_rist_moves_point
+#align faithful_rist_moves_point Rubin.faithful_rigid_stabilizer_moves_point
 
-theorem ne_one_support_nempty {g : G} : g ≠ 1 → (support α g).Nonempty :=
+theorem Rubin.ne_one_support_nonempty {g : G} : g ≠ 1 → (Rubin.SmulSupport.Support α g).Nonempty :=
   by
   intro h1
   cases' Rubin.faithful_moves_point'₁ α h1 with x _
   use x
-#align Rubin.ne_one_support_nempty Rubin.ne_one_support_nempty
+#align ne_one_support_nempty Rubin.ne_one_support_nonempty
 
 -- FIXME: somehow clashes with another definition
-theorem disjoint_commute {f g : G} : Disjoint (support α f) (support α g) → Commute f g :=
+theorem Rubin.disjoint_commute₁ {f g : G} :
+    Disjoint (Rubin.SmulSupport.Support α f) (Rubin.SmulSupport.Support α g) → Commute f g :=
   by
   intro hdisjoint
   rw [← commutatorElement_eq_one_iff_commute]
@@ -585,7 +603,7 @@ theorem disjoint_commute {f g : G} : Disjoint (support α f) (support α g) →
     rw [smul_eq_iff_inv_smul_eq.mp (mem_not_support.mp hgfixed),
       smul_eq_iff_inv_smul_eq.mp (mem_not_support.mp hffixed), mem_not_support.mp hgfixed,
       mem_not_support.mp hffixed]
-#align Rubin.disjoint_commute Rubin.disjoint_commute
+#align disjoint_commute Rubin.disjoint_commute₁
 
 end FaithfulActions
 
@@ -594,21 +612,21 @@ section RubinActions
 
 variable [TopologicalSpace α] [TopologicalSpace β]
 
-def HasNoIsolatedPoints (α : Type _) [TopologicalSpace α] :=
+def Rubin.has_no_isolated_points (α : Type _) [TopologicalSpace α] :=
   ∀ x : α, (nhdsWithin x ({x}ᶜ)).ne_bot
-#align Rubin.has_no_isolated_points Rubin.HasNoIsolatedPoints
+#align has_no_isolated_points Rubin.has_no_isolated_points
 
-def IsLocallyDense (G α : Type _) [Group G] [TopologicalSpace α] [MulAction G α] :=
+def Rubin.is_locally_dense (G α : Type _) [Group G] [TopologicalSpace α] [MulAction G α] :=
   ∀ U : Set α, ∀ p ∈ U, p ∈ interior (closure (MulAction.orbit (rigidStabilizer G U) p))
-#align Rubin.is_locally_dense Rubin.IsLocallyDense
+#align is_locally_dense Rubin.is_locally_dense
 
-structure RubinActionCat (G α : Type _) extends Group G, TopologicalSpace α, MulAction G α,
+structure Rubin.RubinAction (G α : Type _) extends Group G, TopologicalSpace α, MulAction G α,
     FaithfulSMul G α where
   locally_compact : LocallyCompactSpace α
   hausdorff : T2Space α
-  no_isolated_points : HasNoIsolatedPoints α
-  locallyDense : IsLocallyDense G α
-#align Rubin.rubin_action Rubin.RubinActionCat
+  no_isolated_points : Rubin.has_no_isolated_points α
+  locallyDense : Rubin.is_locally_dense G α
+#align rubin_action Rubin.RubinAction
 
 end RubinActions
 
@@ -617,36 +635,38 @@ section Rubin.Period.period
 
 variable [MulAction G α]
 
-noncomputable def period (p : α) (g : G) : ℕ :=
+noncomputable def Rubin.Period.period (p : α) (g : G) : ℕ :=
   sInf {n : ℕ | n > 0 ∧ g ^ n • p = p}
-#align Rubin.period Rubin.period
+#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 < period p g ∧ period p g ≤ m := by
+theorem Rubin.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⟩; 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 Rubin.period_le_fix Rubin.period_le_fix
+#align period_le_fix Rubin.Period.period_le_fix
 
-theorem notfix_le_period {p : α} {g : G} {n : ℕ} (n_pos : n > 0) (period_pos : period p g > 0)
-    (pmoves : ∀ i : ℕ, 0 < i → i < n → g ^ i • p ≠ p) : n ≤ period p g :=
-  by
+theorem Rubin.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 Rubin.notfix_le_period Rubin.notfix_le_period
+#align notfix_le_period Rubin.Period.notfix_le_period
 
-theorem notfix_le_period' {p : α} {g : G} {n : ℕ} (n_pos : n > 0) (period_pos : period p g > 0)
-    (pmoves : ∀ i : Fin n, 0 < (i : ℕ) → g ^ (i : ℕ) • p ≠ p) : n ≤ period p g :=
-  notfix_le_period n_pos period_pos fun (i : ℕ) (i_pos : 0 < i) (i_lt_n : i < n) =>
+theorem Rubin.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 Rubin.notfix_le_period' Rubin.notfix_le_period'
+#align notfix_le_period' Rubin.Period.notfix_le_period'
 
 /- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:73:14: unsupported tactic `group_action #[[]] -/
-theorem period_neutral_eq_one (p : α) : period p (1 : G) = 1 :=
+theorem Rubin.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)
@@ -655,18 +675,19 @@ theorem period_neutral_eq_one (p : α) : period p (1 : G) = 1 :=
           "./././Mathport/Syntax/Translate/Tactic/Builtin.lean:73:14: unsupported tactic `group_action #[[]]" :
         (1 : G) ^ 1 • p = p)
   linarith
-#align Rubin.period_neutral_eq_one Rubin.period_neutral_eq_one
+#align period_neutral_eq_one Rubin.Period.period_neutral_eq_one
 
-def periods (U : Set α) (H : Subgroup G) : Set ℕ :=
-  {n : ℕ | ∃ (p : U) (g : H), period (p : α) (g : G) = n}
-#align Rubin.periods Rubin.periods
+def Rubin.Period.periods (U : Set α) (H : Subgroup G) : Set ℕ :=
+  {n : ℕ | ∃ (p : U) (g : H), Rubin.Period.period (p : α) (g : G) = n}
+#align periods Rubin.Period.periods
 
 /- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:73:14: unsupported tactic `group_action #[[]] -/
 -- TODO: split into multiple lemmas
-theorem period_lemma {U : Set α} (U_nonempty : U.Nonempty) {H : Subgroup G}
+theorem Rubin.Period.periods_lemmas {U : Set α} (U_nonempty : U.Nonempty) {H : Subgroup G}
     (exp_ne_zero : Monoid.exponent H ≠ 0) :
-    (periods U H).Nonempty ∧
-      BddAbove (periods U H) ∧ ∃ (m : ℕ) (m_pos : m > 0), ∀ (p : α) (g : H), g ^ m • p = p :=
+    (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];
@@ -678,11 +699,12 @@ theorem period_lemma {U : Set α} (U_nonempty : U.Nonempty) {H : Subgroup G}
     rcases hperiod with ⟨p, g, hperiod⟩; rw [← hperiod];
     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 Rubin.period_lemma Rubin.period_lemma
+#align period_lemma Rubin.Period.periods_lemmas
 
-theorem period_from_exponent (U : Set α) (U_nonempty : U.Nonempty) {H : Subgroup G}
+theorem Rubin.Period.period_from_exponent (U : Set α) (U_nonempty : U.Nonempty) {H : Subgroup G}
     (exp_ne_zero : Monoid.exponent H ≠ 0) :
-    ∃ (p : U) (g : H) (n : ℕ), n > 0 ∧ period (p : α) (g : G) = n ∧ n = sSup (periods U H) :=
+    ∃ (p : U) (g : H) (n : ℕ),
+      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⟩
@@ -690,11 +712,13 @@ theorem period_from_exponent (U : Set α) (U_nonempty : U.Nonempty) {H : Subgrou
   exact
     ⟨p, g, Sup (Rubin.Period.periods U H),
       hperiod ▸ (Rubin.Period.period_le_fix m_pos (gmp_eq_p p g)).1, hperiod, rfl⟩
-#align Rubin.period_from_exponent Rubin.period_from_exponent
+#align period_from_exponent Rubin.Period.period_from_exponent
 
-theorem zero_lt_period_le_sSup_periods {U : Set α} (U_nonempty : U.Nonempty) {H : Subgroup G}
-    (exp_ne_zero : Monoid.exponent H ≠ 0) :
-    ∀ (p : U) (g : H), 0 < period (p : α) (g : G) ∧ period (p : α) (g : G) ≤ sSup (periods U H) :=
+theorem Rubin.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⟩
@@ -704,9 +728,9 @@ theorem zero_lt_period_le_sSup_periods {U : Set α} (U_nonempty : U.Nonempty) {H
   exact
     ⟨(Rubin.Period.period_le_fix m_pos (gmp_eq_p p g)).1,
       le_csSup periods_bounded period_in_periods⟩
-#align Rubin.zero_lt_period_le_Sup_periods Rubin.zero_lt_period_le_sSup_periods
+#align zero_lt_period_le_Sup_periods Rubin.Period.zero_lt_period_le_Sup_periods
 
-theorem pow_period_fix (p : α) (g : G) : g ^ period p g • p = p :=
+theorem Rubin.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)
   · rw [h]; finish
@@ -715,18 +739,19 @@ theorem pow_period_fix (p : α) (g : G) : g ^ period p g • p = p :=
       (Nat.sInf_mem
           (Nat.nonempty_of_pos_sInf
             (Nat.pos_of_ne_zero (@NeZero.ne _ _ (Rubin.Period.period p g) h)))).2
-#align Rubin.pow_period_fix Rubin.pow_period_fix
+#align pow_period_fix Rubin.Period.pow_period_fix
 
 end Rubin.Period.period
 
 ----------------------------------------------------------------
 section AlgebraicDisjointness
 
-variable [TopologicalSpace α] [ContinuousMulAction G α] [FaithfulSMul G α]
+variable [TopologicalSpace α] [Rubin.Topological.ContinuousMulAction G α] [FaithfulSMul G α]
 
-def IsLocallyMoving (G α : Type _) [Group G] [TopologicalSpace α] [MulAction G α] :=
+def Rubin.Disjointness.IsLocallyMoving (G α : Type _) [Group G] [TopologicalSpace α]
+    [MulAction G α] :=
   ∀ U : Set α, IsOpen U → Set.Nonempty U → rigidStabilizer G U ≠ ⊥
-#align Rubin.is_locally_moving Rubin.IsLocallyMoving
+#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,
@@ -994,68 +1019,77 @@ end AlgebraicDisjointness
 ----------------------------------------------------------------
 section Rubin.RegularSupport.RegularSupport
 
-variable [TopologicalSpace α] [ContinuousMulAction G α]
+variable [TopologicalSpace α] [Rubin.Topological.ContinuousMulAction G α]
 
-def interiorClosure (U : Set α) :=
+def Rubin.RegularSupport.InteriorClosure (U : Set α) :=
   interior (closure U)
-#align Rubin.interior_closure Rubin.interiorClosure
+#align interior_closure Rubin.RegularSupport.InteriorClosure
 
-theorem isOpen_interiorClosure (U : Set α) : IsOpen (interiorClosure U) :=
+theorem Rubin.RegularSupport.is_open_interiorClosure (U : Set α) :
+    IsOpen (Rubin.RegularSupport.InteriorClosure U) :=
   isOpen_interior
-#align Rubin.is_open_interior_closure Rubin.isOpen_interiorClosure
+#align is_open_interior_closure Rubin.RegularSupport.is_open_interiorClosure
 
-theorem interiorClosure_mono {U V : Set α} : U ⊆ V → interiorClosure U ⊆ interiorClosure V :=
+theorem Rubin.RegularSupport.interiorClosure_mono {U V : Set α} :
+    U ⊆ V → Rubin.RegularSupport.InteriorClosure U ⊆ Rubin.RegularSupport.InteriorClosure V :=
   interior_mono ∘ closure_mono
-#align Rubin.interior_closure_mono Rubin.interiorClosure_mono
+#align interior_closure_mono Rubin.RegularSupport.interiorClosure_mono
 
-def Set.IsRegularOpen (U : Set α) :=
-  interiorClosure U = U
-#align Rubin.set.is_regular_open Rubin.Set.IsRegularOpen
+def Rubin.RegularSupport.Set.is_regular_open (U : Set α) :=
+  Rubin.RegularSupport.InteriorClosure U = U
+#align set.is_regular_open Rubin.RegularSupport.Set.is_regular_open
 
-theorem Set.is_regular_def (U : Set α) : U.IsRegularOpen ↔ interiorClosure U = U := by rfl
-#align Rubin.set.is_regular_def Rubin.Set.is_regular_def
+theorem Rubin.RegularSupport.Set.is_regular_def (U : Set α) :
+    U.is_regular_open ↔ Rubin.RegularSupport.InteriorClosure U = U := by rfl
+#align set.is_regular_def Rubin.RegularSupport.Set.is_regular_def
 
-theorem IsOpen.in_closure {U : Set α} : IsOpen U → U ⊆ interior (closure U) :=
+theorem Rubin.RegularSupport.IsOpen.in_closure {U : Set α} : IsOpen U → U ⊆ interior (closure U) :=
   by
   intro U_open x x_in_U
   apply interior_mono subset_closure
   rw [U_open.interior_eq]
   exact x_in_U
-#align Rubin.is_open.in_closure Rubin.IsOpen.in_closure
+#align is_open.in_closure Rubin.RegularSupport.IsOpen.in_closure
 
-theorem IsOpen.interiorClosure_subset {U : Set α} : IsOpen U → U ⊆ interiorClosure U := fun h =>
+theorem Rubin.RegularSupport.IsOpen.interiorClosure_subset {U : Set α} :
+    IsOpen U → U ⊆ Rubin.RegularSupport.InteriorClosure U := fun h =>
   (subset_interior_iff_isOpen.mpr h).trans (interior_mono subset_closure)
-#align Rubin.is_open.interior_closure_subset Rubin.IsOpen.interiorClosure_subset
+#align is_open.interior_closure_subset Rubin.RegularSupport.IsOpen.interiorClosure_subset
 
-theorem regular_interiorClosure (U : Set α) : (interiorClosure U).IsRegularOpen :=
+theorem Rubin.RegularSupport.regular_interior_closure (U : Set α) :
+    (Rubin.RegularSupport.InteriorClosure U).is_regular_open :=
   by
   rw [Rubin.RegularSupport.Set.is_regular_def]
   apply Set.Subset.antisymm
   exact interior_mono ((closure_mono interior_subset).trans (subset_of_eq closure_closure))
   exact (subset_of_eq interior_interior.symm).trans (interior_mono subset_closure)
-#align Rubin.regular_interior_closure Rubin.regular_interiorClosure
+#align regular_interior_closure Rubin.RegularSupport.regular_interior_closure
 
-def regularSupport (α : Type _) [TopologicalSpace α] [MulAction G α] (g : G) :=
-  interiorClosure (support α g)
-#align Rubin.regular_support Rubin.regularSupport
+def Rubin.RegularSupport.RegularSupport (α : Type _) [TopologicalSpace α] [MulAction G α] (g : G) :=
+  Rubin.RegularSupport.InteriorClosure (Rubin.SmulSupport.Support α g)
+#align regular_support Rubin.RegularSupport.RegularSupport
 
-theorem regular_regularSupport {g : G} : (regularSupport α g).IsRegularOpen :=
-  regular_interiorClosure _
-#align Rubin.regular_regular_support Rubin.regular_regularSupport
+theorem Rubin.RegularSupport.regularSupport_regular {g : G} :
+    (Rubin.RegularSupport.RegularSupport α g).is_regular_open :=
+  Rubin.RegularSupport.regular_interior_closure _
+#align regular_regular_support Rubin.RegularSupport.regularSupport_regular
 
-theorem support_in_regularSupport [T2Space α] (g : G) : support α g ⊆ regularSupport α g :=
-  IsOpen.interiorClosure_subset (support_open g)
-#align Rubin.support_in_regular_support Rubin.support_in_regularSupport
+theorem Rubin.RegularSupport.support_subset_regularSupport [T2Space α] (g : G) :
+    Rubin.SmulSupport.Support α g ⊆ Rubin.RegularSupport.RegularSupport α g :=
+  Rubin.RegularSupport.IsOpen.interiorClosure_subset (Rubin.Topological.support_open g)
+#align support_in_regular_support Rubin.RegularSupport.support_subset_regularSupport
 
-theorem mem_regularSupport (g : G) (U : Set α) :
-    U.IsRegularOpen → g ∈ rigidStabilizer G U → regularSupport α g ⊆ U := fun U_ro g_moves =>
-  (Set.is_regular_def _).mp U_ro ▸ interiorClosure_mono (rist_supported_in_set g_moves)
-#align Rubin.mem_regular_support Rubin.mem_regularSupport
+theorem Rubin.RegularSupport.mem_regularSupport (g : G) (U : Set α) :
+    U.is_regular_open → g ∈ rigidStabilizer G U → Rubin.RegularSupport.RegularSupport α g ⊆ U :=
+  fun U_ro g_moves =>
+  (Rubin.RegularSupport.Set.is_regular_def _).mp U_ro ▸
+    Rubin.RegularSupport.interiorClosure_mono (rist_supported_in_set g_moves)
+#align mem_regular_support Rubin.RegularSupport.mem_regularSupport
 
 -- FIXME: Weird naming?
-def algebraicCentralizer (f : G) : Set G :=
-  {h | ∃ g, h = g ^ 12 ∧ IsAlgebraicallyDisjoint f g}
-#align Rubin.algebraic_centralizer Rubin.algebraicCentralizer
+def Rubin.RegularSupport.AlgebraicCentralizer (f : G) : Set G :=
+  {h | ∃ g, h = g ^ 12 ∧ Rubin.is_algebraically_disjoint f g}
+#align algebraic_centralizer Rubin.RegularSupport.AlgebraicCentralizer
 
 end Rubin.RegularSupport.RegularSupport
 
@@ -1146,5 +1180,3 @@ end Rubin.RegularSupport.RegularSupport
 -- variables [topological_space α] [topological_space β] [continuous_mul_action G α] [continuous_mul_action G β]
 -- noncomputable theorem rubin (hα : rubin_action G α) (hβ : rubin_action G β) : equivariant_homeomorph G α β := sorry
 end Rubin
-
-end Rubin

old/rubin.lean

@@ -156,7 +156,6 @@ add_tactic_doc
 
 end group_action_tactic
 
-namespace Rubin
 example (G α : Type*) [group G] (a b c : G) [mul_action G α] (x : α) : ⁅a*b,c⁆ • x = (a*⁅b,c⁆*a⁻¹*⁅a,c⁆) • x := begin
   group_action,
 end
@@ -1053,5 +1052,3 @@ end regular_support
 -- noncomputable theorem rubin (hα : rubin_action G α) (hβ : rubin_action G β) : equivariant_homeomorph G α β := sorry
 
 end rubin
-
-end Rubin