diff --git a/Rubin.lean b/Rubin.lean
index 2d95869..4f7c01f 100644
--- a/Rubin.lean
+++ b/Rubin.lean
@@ -24,12 +24,10 @@ import Rubin.SmulImage
 import Rubin.Support
 import Rubin.Topology
 import Rubin.RigidStabilizer
--- import Rubin.RigidStabilizerBasis
 import Rubin.Period
 import Rubin.AlgebraicDisjointness
 import Rubin.RegularSupport
 import Rubin.RegularSupportBasis
-import Rubin.HomeoGroup
 import Rubin.Filter
 
 #align_import rubin
@@ -37,33 +35,54 @@ import Rubin.Filter
 namespace Rubin
 open Rubin.Tactic
 
--- TODO: find a home
-theorem 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 equiv.congr_ne Rubin.equiv_congr_ne
-
 ----------------------------------------------------------------
 section Rubin
 
 ----------------------------------------------------------------
 section RubinActions
 
-structure RubinAction (G α : Type _) extends
-  Group G,
-  TopologicalSpace α,
-  MulAction G α,
-  FaithfulSMul G α
-where
+-- TODO: debate whether having this structure is relevant or not,
+-- since the instance inference engine doesn't play well with it.
+-- One alternative would be to lay out all of the properties as-is (without their class wrappers),
+-- then provide ways to reconstruct them in instances.
+structure RubinAction (G α : Type _) where
+  group : Group G
+  action : MulAction G α
+  topology : TopologicalSpace α
+  faithful : FaithfulSMul G α
   locally_compact : LocallyCompactSpace α
   hausdorff : T2Space α
   no_isolated_points : HasNoIsolatedPoints α
-  locallyDense : LocallyDense G α
+  locally_dense : LocallyDense G α
 #align rubin_action Rubin.RubinAction
 
+/--
+Constructs a RubinAction from ambient instances.
+If needed, missing instances can be passed as named parameters.
+--/
+def RubinAction.mk' (G α : Type _)
+  [group : Group G] [topology : TopologicalSpace α] [hausdorff : T2Space α] [action : MulAction G α]
+  [faithful : FaithfulSMul G α] [locally_compact : LocallyCompactSpace α]
+  [no_isolated_points : HasNoIsolatedPoints α] [locally_dense : LocallyDense G α] :
+  RubinAction G α := ⟨
+    group,
+    action,
+    topology,
+    faithful,
+    locally_compact,
+    hausdorff,
+    no_isolated_points,
+    locally_dense
+  ⟩
+
+variable {G α : Type _}
+
+instance RubinAction.instGroup (act : RubinAction G α) : Group G := act.group
+
+instance RubinAction.instFaithful (act : RubinAction G α) : @FaithfulSMul G α (@MulAction.toSMul G α act.group.toMonoid act.action) := act.faithful
+
+instance RubinAction.topologicalSpace (act : RubinAction G α) : TopologicalSpace α := act.topology
+
 end RubinActions
 
 section AlgebraicDisjointness
@@ -2317,6 +2336,7 @@ theorem RubinFilter.mul_smul (g h : G) (F : RubinFilter G) : (F.smul g).smul h =
   rw [Filter.map_map, <-MulAut.coe_mul]
   rw [Filter.InBasis.map_basis_toOrderIsoSet _ F.filter.in_basis]
 
+-- Note: awfully slow to compile (since it isn't noncomputable, it gets compiled down to IR)
 def RubinSpace.smul (Q : RubinSpace G) (g : G) : RubinSpace G :=
   Quotient.map (fun F => F.smul g) (fun _ _ F_eqv => RubinFilter.smul_eqv_of_eqv g F_eqv) Q
 
@@ -2344,9 +2364,9 @@ instance : MulAction G (RubinSpace G) where
 
 theorem RubinSpace.smul_def (g : G) (Q : RubinSpace G) : g • Q = Q.smul g := rfl
 
-noncomputable def rubin' : EquivariantHomeomorph G (RubinSpace G) α where
+noncomputable def RubinSpace.equivariantHomeomorph : EquivariantHomeomorph G (RubinSpace G) α where
   toHomeomorph := RubinSpace.homeomorph (G := G) α
-  equivariant := by
+  toFun_equivariant' := by
     intro g Q
     simp [RubinSpace.homeomorph]
     rw [RubinSpace.smul_def]
@@ -2356,20 +2376,18 @@ noncomputable def rubin' : EquivariantHomeomorph G (RubinSpace G) α where
 
 end Equivariant
 
--- theorem rubin' (hα : RubinAction G α) : EquivariantHomeomorph G α (RubinSpace G) where
---   toFun := fun x => ⟦⟧
---   invFun := fun S => sorry
-
-
-
-/-
-variable {β : Type _}
-variable [TopologicalSpace β] [MulAction G β] [ContinuousConstSMul G β]
-
-theorem rubin (hα : RubinAction G α) (hβ : RubinAction G β) : EquivariantHomeomorph G α β := by
-  -- by composing rubin' hα
-  sorry
--/
+variable (G : Type _)
+variable [Group G] [Nontrivial G]
+variable (α : Type _) [TopologicalSpace α] [T2Space α] [LocallyCompactSpace α] [HasNoIsolatedPoints α]
+variable [MulAction G α] [FaithfulSMul G α] [ContinuousConstSMul G α] [LocallyDense G α]
+variable (β : Type _) [TopologicalSpace β] [T2Space β] [LocallyCompactSpace β] [HasNoIsolatedPoints β]
+variable [MulAction G β] [FaithfulSMul G β] [ContinuousConstSMul G β] [LocallyDense G β]
+
+noncomputable def rubin : EquivariantHomeomorph G α β :=
+  let α_nonempty : Nonempty α := by rwa [LocallyMoving.nonempty_iff_nontrivial G]
+  let β_nonempty : Nonempty β := by rwa [LocallyMoving.nonempty_iff_nontrivial G]
+  (RubinSpace.equivariantHomeomorph (G := G) (α := α)).inv.trans
+    (RubinSpace.equivariantHomeomorph (G := G) (α := β))
 
 end Rubin
 
diff --git a/Rubin/HomeoGroup.lean b/Rubin/HomeoGroup.lean
deleted file mode 100644
index 6d16930..0000000
--- a/Rubin/HomeoGroup.lean
+++ /dev/null
@@ -1,257 +0,0 @@
-import Mathlib.Logic.Equiv.Defs
-import Mathlib.Topology.Basic
-import Mathlib.Topology.Homeomorph
-import Mathlib.Topology.Algebra.ConstMulAction
-
-import Rubin.LocallyDense
-import Rubin.Topology
-import Rubin.Support
-import Rubin.RegularSupport
-
-structure HomeoGroup (α : Type _) [TopologicalSpace α] extends Homeomorph α α
-
-variable {α : Type _}
-variable [TopologicalSpace α]
-
-def HomeoGroup.coe : HomeoGroup α -> Homeomorph α α := HomeoGroup.toHomeomorph
-
-def HomeoGroup.from : Homeomorph α α -> HomeoGroup α := HomeoGroup.mk
-
-instance homeoGroup_coe : Coe (HomeoGroup α) (Homeomorph α α) where
-  coe := HomeoGroup.coe
-
-instance homeoGroup_coe₂ : Coe (Homeomorph α α) (HomeoGroup α) where
-  coe := HomeoGroup.from
-
-def HomeoGroup.toPerm : HomeoGroup α → Equiv.Perm α := fun g => g.coe.toEquiv
-
-instance homeoGroup_coe_perm : Coe (HomeoGroup α) (Equiv.Perm α) where
-  coe := HomeoGroup.toPerm
-
-@[simp]
-theorem HomeoGroup.toPerm_def (g : HomeoGroup α) : g.coe.toEquiv = (g : Equiv.Perm α) := rfl
-
-@[simp]
-theorem HomeoGroup.mk_coe (g : HomeoGroup α) : HomeoGroup.mk (g.coe) = g := rfl
-
-@[simp]
-theorem HomeoGroup.eq_iff_coe_eq {f g : HomeoGroup α} : f.coe = g.coe ↔ f = g := by
-  constructor
-  {
-    intro f_eq_g
-    rw [<-HomeoGroup.mk_coe f]
-    rw [f_eq_g]
-    simp
-  }
-  {
-    intro f_eq_g
-    unfold HomeoGroup.coe
-    rw [f_eq_g]
-  }
-
-@[simp]
-theorem HomeoGroup.from_toHomeomorph (m : Homeomorph α α) : (HomeoGroup.from m).toHomeomorph = m := rfl
-
-instance homeoGroup_one : One (HomeoGroup α) where
-  one := HomeoGroup.from (Homeomorph.refl α)
-
-theorem HomeoGroup.one_def : (1 : HomeoGroup α) = (Homeomorph.refl α : HomeoGroup α) := rfl
-
-instance homeoGroup_inv : Inv (HomeoGroup α) where
-  inv := fun g => HomeoGroup.from (g.coe.symm)
-
-@[simp]
-theorem HomeoGroup.inv_def (g : HomeoGroup α) : (Homeomorph.symm g.coe : HomeoGroup α) = g⁻¹ := rfl
-
-theorem HomeoGroup.coe_inv {g : HomeoGroup α} : HomeoGroup.coe (g⁻¹) = (HomeoGroup.coe g).symm := rfl
-
-instance homeoGroup_mul : Mul (HomeoGroup α) where
-  mul := fun a b => ⟨b.toHomeomorph.trans a.toHomeomorph⟩
-
-theorem HomeoGroup.coe_mul {f g : HomeoGroup α} : HomeoGroup.coe (f * g) = (HomeoGroup.coe g).trans (HomeoGroup.coe f) := rfl
-
-@[simp]
-theorem HomeoGroup.mul_def (f g : HomeoGroup α) : HomeoGroup.from ((HomeoGroup.coe g).trans (HomeoGroup.coe f)) = f * g := rfl
-
-instance homeoGroup_group : Group (HomeoGroup α) where
-  mul_assoc := by
-    intro a b c
-    rw [<-HomeoGroup.eq_iff_coe_eq]
-    repeat rw [HomeoGroup_coe_mul]
-    rfl
-  mul_one := by
-    intro a
-    rw [<-HomeoGroup.eq_iff_coe_eq]
-    rw [HomeoGroup.coe_mul]
-    rfl
-  one_mul := by
-    intro a
-    rw [<-HomeoGroup.eq_iff_coe_eq]
-    rw [HomeoGroup.coe_mul]
-    rfl
-  mul_left_inv := by
-    intro a
-    rw [<-HomeoGroup.eq_iff_coe_eq]
-    rw [HomeoGroup.coe_mul]
-    rw [HomeoGroup.coe_inv]
-    simp
-    rfl
-
-/--
-The HomeoGroup trivially has a continuous and faithful `MulAction` on the underlying topology `α`.
---/
-instance homeoGroup_smul₁ : SMul (HomeoGroup α) α where
-  smul := fun g x => g.toFun x
-
-@[simp]
-theorem HomeoGroup.smul₁_def (f : HomeoGroup α) (x : α) : f.toFun x = f • x := rfl
-
-@[simp]
-theorem HomeoGroup.smul₁_def' (f : HomeoGroup α) (x : α) : f.toHomeomorph x = f • x := rfl
-
-@[simp]
-theorem HomeoGroup.coe_toFun_eq_smul₁ (f : HomeoGroup α) (x : α) : FunLike.coe (HomeoGroup.coe f) x = f • x := rfl
-
-instance homeoGroup_mulAction₁ : MulAction (HomeoGroup α) α where
-  one_smul := by
-    intro x
-    rfl
-  mul_smul := by
-    intro f g x
-    rfl
-
-instance homeoGroup_mulAction₁_continuous : ContinuousConstSMul (HomeoGroup α) α where
-  continuous_const_smul := by
-    intro h
-    constructor
-    intro S S_open
-    conv => {
-      congr; ext
-      congr; ext
-      rw [<-HomeoGroup.smul₁_def']
-    }
-    simp only [Homeomorph.isOpen_preimage]
-    exact S_open
-
-instance homeoGroup_mulAction₁_faithful : FaithfulSMul (HomeoGroup α) α where
-  eq_of_smul_eq_smul := by
-    intro f g hyp
-    rw [<-HomeoGroup.eq_iff_coe_eq]
-    ext x
-    simp
-    exact hyp x
-
-theorem HomeoGroup.smulImage_eq_image (g : HomeoGroup α) (S : Set α) :
-  g •'' S = ⇑g.toHomeomorph '' S := rfl
-
-section FromContinuousConstSMul
-
-variable {G : Type _} [Group G]
-variable [MulAction G α] [ContinuousConstSMul G α]
-
-/--
-`fromContinuous` is a structure-preserving transformation from a continuous `MulAction` to a `HomeoGroup`
---/
-def HomeoGroup.fromContinuous (α : Type _) [TopologicalSpace α] [MulAction G α] [ContinuousConstSMul G α]
-  (g : G) : HomeoGroup α :=
-  HomeoGroup.from (Homeomorph.smul g)
-
-@[simp]
-theorem HomeoGroup.fromContinuous_def (g : G) :
-  HomeoGroup.from (Homeomorph.smul g) = HomeoGroup.fromContinuous α g := rfl
-
-@[simp]
-theorem HomeoGroup.fromContinuous_smul (g : G) :
-  ∀ x : α, (HomeoGroup.fromContinuous α g) • x = g • x :=
-by
-  intro x
-  unfold fromContinuous
-  rw [<-HomeoGroup.smul₁_def', HomeoGroup.from_toHomeomorph]
-  unfold Homeomorph.smul
-  simp
-
-theorem HomeoGroup.fromContinuous_one :
-  HomeoGroup.fromContinuous α (1 : G) = (1 : HomeoGroup α) :=
-by
-  apply FaithfulSMul.eq_of_smul_eq_smul (α := α)
-  simp
-
-theorem HomeoGroup.fromContinuous_mul (g h : G):
-  (HomeoGroup.fromContinuous α g) * (HomeoGroup.fromContinuous α h) = (HomeoGroup.fromContinuous α (g * h)) :=
-by
-  apply FaithfulSMul.eq_of_smul_eq_smul (α := α)
-  intro x
-  rw [mul_smul]
-  simp
-  rw [mul_smul]
-
-theorem HomeoGroup.fromContinuous_inv (g : G):
-  HomeoGroup.fromContinuous α g⁻¹ = (HomeoGroup.fromContinuous α g)⁻¹ :=
-by
-  apply FaithfulSMul.eq_of_smul_eq_smul (α := α)
-  intro x
-  group_action
-  rw [mul_smul]
-  simp
-
-theorem HomeoGroup.fromContinuous_eq_iff [FaithfulSMul G α] (g h : G):
-  (HomeoGroup.fromContinuous α g) = (HomeoGroup.fromContinuous α h) ↔ g = h :=
-by
-  constructor
-  · intro cont_eq
-    apply FaithfulSMul.eq_of_smul_eq_smul (α := α)
-    intro x
-    rw [<-HomeoGroup.fromContinuous_smul g]
-    rw [cont_eq]
-    simp
-  · tauto
-
-@[simp]
-theorem HomeoGroup.fromContinuous_support (g : G) :
-  Rubin.Support α (HomeoGroup.fromContinuous α g) = Rubin.Support α g :=
-by
-  ext x
-  repeat rw [Rubin.mem_support]
-  rw [<-HomeoGroup.smul₁_def, <-HomeoGroup.fromContinuous_def]
-  rw [HomeoGroup.from_toHomeomorph]
-  rw [Homeomorph.smul]
-  simp only [Equiv.toFun_as_coe, MulAction.toPerm_apply]
-
-@[simp]
-theorem HomeoGroup.fromContinuous_regularSupport (g : G) :
-  Rubin.RegularSupport α (HomeoGroup.fromContinuous α g) = Rubin.RegularSupport α g :=
-by
-  unfold Rubin.RegularSupport
-  rw [HomeoGroup.fromContinuous_support]
-
-@[simp]
-theorem HomeoGroup.fromContinuous_smulImage (g : G) (V : Set α) :
-  (HomeoGroup.fromContinuous α g) •'' V = g •'' V :=
-by
-  repeat rw [Rubin.smulImage_def]
-  simp
-
-def HomeoGroup.fromContinuous_embedding (α : Type _) [TopologicalSpace α] [MulAction G α] [ContinuousConstSMul G α] [FaithfulSMul G α]: G ↪ (HomeoGroup α) where
-  toFun := fun (g : G) => HomeoGroup.fromContinuous α g
-  inj' := by
-    intro g h fromCont_eq
-    simp at fromCont_eq
-    apply FaithfulSMul.eq_of_smul_eq_smul (α := α)
-    intro x
-    rw [<-fromContinuous_smul, fromCont_eq, fromContinuous_smul]
-
-@[simp]
-theorem HomeoGroup.fromContinuous_embedding_toFun [FaithfulSMul G α] (g : G):
-  HomeoGroup.fromContinuous_embedding α g = HomeoGroup.fromContinuous α g := rfl
-
-def HomeoGroup.fromContinuous_monoidHom (α : Type _) [TopologicalSpace α] [MulAction G α] [ContinuousConstSMul G α] [FaithfulSMul G α]: G →* (HomeoGroup α) where
-  toFun := fun (g : G) => HomeoGroup.fromContinuous α g
-  map_one' := by
-    simp
-    rw [fromContinuous_one]
-  map_mul' := by
-    simp
-    intros
-    rw [fromContinuous_mul]
-
-end FromContinuousConstSMul
diff --git a/Rubin/LocallyDense.lean b/Rubin/LocallyDense.lean
index be947e5..4f0eeb1 100644
--- a/Rubin/LocallyDense.lean
+++ b/Rubin/LocallyDense.lean
@@ -126,13 +126,29 @@ by
   let ⟨g, _, g_ne_one⟩ := (get_nontrivial_rist_elem (G := G) (α := α) isOpen_univ Set.univ_nonempty)
   use g
 
-theorem LocallyMoving.nontrivial {G α : Type _} [Group G] [TopologicalSpace α]
+theorem LocallyMoving.nontrivial (G α : Type _) [Group G] [TopologicalSpace α]
   [MulAction G α] [LocallyMoving G α] [Nonempty α] : Nontrivial G where
   exists_pair_ne := by
     use 1
     simp only [ne_comm]
     exact nontrivial_elem G α
 
+theorem LocallyMoving.nonempty_iff_nontrivial (G α : Type _) [Group G] [TopologicalSpace α]
+  [MulAction G α] [FaithfulSMul G α] [LocallyMoving G α] : Nonempty α ↔ Nontrivial G :=
+by
+  constructor
+  · intro; exact LocallyMoving.nontrivial G α
+  · intro nontrivial
+    by_contra α_empty
+    rw [not_nonempty_iff] at α_empty
+    let ⟨g, h, g_ne_h⟩ := nontrivial.exists_pair_ne
+    apply g_ne_h
+    apply FaithfulSMul.eq_of_smul_eq_smul (α := α)
+    intro a
+    exfalso
+    exact α_empty.false a
+
+
 variable {G α : Type _}
 variable [Group G]
 variable [TopologicalSpace α]
diff --git a/Rubin/MulActionExt.lean b/Rubin/MulActionExt.lean
index 86be76b..3cf04d6 100644
--- a/Rubin/MulActionExt.lean
+++ b/Rubin/MulActionExt.lean
@@ -37,12 +37,6 @@ theorem smul_zpow_eq_of_smul_eq {x : α} {g : G} (n : ℤ) :
     exact res
 #align smul_zpow_eq_of_smul_eq Rubin.smul_zpow_eq_of_smul_eq
 
--- TODO: turn this into a structure?
-def is_equivariant (G : Type _) {β : Type _} [Group G] [MulAction G α]
-    [MulAction G β] (f : α → β) :=
-  ∀ g : G, ∀ x : α, f (g • x) = g • f x
-#align is_equivariant Rubin.is_equivariant
-
 lemma disjoint_not_mem {α : Type _} {U V : Set α} (disj: Disjoint U V) :
   ∀ {x : α}, x ∈ U → x ∉ V :=
 by
diff --git a/Rubin/RegularSupportBasis.lean b/Rubin/RegularSupportBasis.lean
index d9fd0aa..34d1031 100644
--- a/Rubin/RegularSupportBasis.lean
+++ b/Rubin/RegularSupportBasis.lean
@@ -11,7 +11,6 @@ import Rubin.LocallyDense
 import Rubin.Topology
 import Rubin.Support
 import Rubin.RegularSupport
-import Rubin.HomeoGroup
 
 namespace Rubin
 
diff --git a/Rubin/RigidStabilizerBasis.lean b/Rubin/RigidStabilizerBasis.lean
deleted file mode 100644
index 6b41dea..0000000
--- a/Rubin/RigidStabilizerBasis.lean
+++ /dev/null
@@ -1,268 +0,0 @@
-/-
-This file describes [`RigidStabilizerBasis`], which are all non-trivial subgroups of `G` constructed
-by finite intersections of `RigidStabilizer G (RegularSupport α g)`.
--/
-
-import Mathlib.Topology.Basic
-import Mathlib.Topology.Homeomorph
-
-import Rubin.RegularSupport
-import Rubin.RigidStabilizer
-
-namespace Rubin
-
-variable {G α : Type _}
-variable [Group G]
-variable [MulAction G α]
-variable [TopologicalSpace α]
-
-/--
-Finite intersections of rigid stabilizers of regular supports
-(which are equivalent to the rigid stabilizers of finite intersections of regular supports).
--/
-def RigidStabilizerInter₀ {G: Type _} (α : Type _) [Group G] [MulAction G α] [TopologicalSpace α]
-  (S : Finset G) : Subgroup G :=
-  ⨅ (g ∈ S), RigidStabilizer G (RegularSupport α g)
-
-theorem RigidStabilizerInter₀.eq_sInter (S : Finset G) :
-  RigidStabilizerInter₀ α S = RigidStabilizer G (⋂ g ∈ S, (RegularSupport α g)) :=
-by
-  have img_eq : ⋂ g ∈ S, RegularSupport α g = ⋂₀ ((fun g : G => RegularSupport α g) '' S) :=
-    by simp only [Set.sInter_image, Finset.mem_coe]
-
-  rw [img_eq]
-  rw [rigidStabilizer_sInter]
-  unfold RigidStabilizerInter₀
-
-  ext x
-  repeat rw [Subgroup.mem_iInf]
-  constructor
-  · intro H T
-    rw [Subgroup.mem_iInf]
-    intro T_in_img
-    simp at T_in_img
-    let ⟨g, ⟨g_in_S, T_eq⟩⟩ := T_in_img
-    specialize H g
-    rw [Subgroup.mem_iInf] at H
-    rw [<-T_eq]
-    apply H; assumption
-  · intro H g
-    rw [Subgroup.mem_iInf]
-    intro g_in_S
-    specialize H (RegularSupport α g)
-    rw [Subgroup.mem_iInf] at H
-    simp at H
-    apply H g <;> tauto
-
-/--
-A predecessor structure to [`RigidStabilizerBasis`], where equality is defined on the choice of
-group elements who regular support's rigid stabilizer get intersected upon.
---/
-structure RigidStabilizerBasis₀ (G α : Type _) [Group G] [MulAction G α] [TopologicalSpace α] where
-  seed : Finset G
-  val_ne_bot : RigidStabilizerInter₀ α seed ≠ ⊥
-
-def RigidStabilizerBasis₀.val (B : RigidStabilizerBasis₀ G α) : Subgroup G :=
-  RigidStabilizerInter₀ α B.seed
-
-theorem RigidStabilizerBasis₀.val_def (B : RigidStabilizerBasis₀ G α) : B.val = RigidStabilizerInter₀ α B.seed := rfl
-
-/--
-The set of all non-trivial subgroups of `G` constructed
-by finite intersections of `RigidStabilizer G (RegularSupport α g)`.
---/
-def RigidStabilizerBasis (G α : Type _) [Group G] [MulAction G α] [TopologicalSpace α] : Set (Subgroup G) :=
-  { H.val | H : RigidStabilizerBasis₀ G α }
-
-theorem RigidStabilizerBasis.mem_iff (H : Subgroup G) :
-  H ∈ RigidStabilizerBasis G α ↔ ∃ B : RigidStabilizerBasis₀ G α, B.val = H := by rfl
-
-theorem RigidStabilizerBasis.mem_iff' (H : Subgroup G)
-  (H_ne_bot : H ≠ ⊥) :
-  H ∈ RigidStabilizerBasis G α ↔ ∃ seed : Finset G, RigidStabilizerInter₀ α seed = H :=
-by
-  rw [mem_iff]
-  constructor
-  · intro ⟨B, B_eq⟩
-    use B.seed
-    rw [RigidStabilizerBasis₀.val_def] at B_eq
-    exact B_eq
-  · intro ⟨seed, seed_eq⟩
-    let B := RigidStabilizerInter₀ α seed
-    have val_ne_bot : B ≠ ⊥ := by
-      unfold_let
-      rw [seed_eq]
-      exact H_ne_bot
-    use ⟨seed, val_ne_bot⟩
-    rw [<-seed_eq]
-    rfl
-
-def RigidStabilizerBasis.asSets (G α : Type _) [Group G] [MulAction G α] [TopologicalSpace α] : Set (Set G) :=
-  { (H.val : Set G) | H : RigidStabilizerBasis₀ G α }
-
-theorem RigidStabilizerBasis.mem_asSets_iff (S : Set G) :
-  S ∈ RigidStabilizerBasis.asSets G α ↔ ∃ H ∈ RigidStabilizerBasis G α, H.carrier = S :=
-by
-  unfold asSets RigidStabilizerBasis
-  simp
-  rfl
-
-theorem RigidStabilizerBasis.mem_iff_asSets (H : Subgroup G) :
-  H ∈ RigidStabilizerBasis G α ↔ (H : Set G) ∈ RigidStabilizerBasis.asSets G α :=
-by
-  unfold asSets RigidStabilizerBasis
-  simp
-
-variable [ContinuousConstSMul G α]
-
-lemma RigidStabilizerBasis.smulImage_mem₀ {H : Subgroup G} (H_in_ristBasis : H ∈ RigidStabilizerBasis G α)
-  (f : G) : ((fun g => f * g * f⁻¹) '' H.carrier) ∈ RigidStabilizerBasis.asSets G α :=
-by
-  have G_decidable : DecidableEq G := Classical.decEq _
-  rw [mem_iff] at H_in_ristBasis
-  let ⟨seed, H_eq⟩ := H_in_ristBasis
-  rw [mem_asSets_iff]
-
-  let new_seed := Finset.image (fun g => f * g * f⁻¹) seed.seed
-  have new_seed_ne_bot : RigidStabilizerInter₀ α new_seed ≠ ⊥ := by
-    rw [RigidStabilizerInter₀.eq_sInter]
-    unfold_let
-    simp [<-regularSupport_smulImage]
-    rw [<-ne_eq]
-    rw [<-smulImage_iInter_fin]
-
-    have val_ne_bot := seed.val_ne_bot
-    rw [Subgroup.ne_bot_iff_exists_ne_one] at val_ne_bot
-    let ⟨⟨g, g_in_ristInter⟩, g_ne_one⟩ := val_ne_bot
-    simp at g_ne_one
-
-    have fgf_in_ristInter₂ : f * g * f⁻¹ ∈ RigidStabilizer G (f •'' ⋂ x ∈ seed.seed, RegularSupport α x) := by
-      rw [rigidStabilizer_smulImage]
-      group
-      rw [RigidStabilizerInter₀.eq_sInter] at g_in_ristInter
-      exact g_in_ristInter
-
-    have fgf_ne_one : f * g * f⁻¹ ≠ 1 := by
-      intro h₁
-      have h₂ := congr_arg (fun x => x * f) h₁
-      group at h₂
-      have h₃ := congr_arg (fun x => f⁻¹ * x) h₂
-      group at h₃
-      exact g_ne_one h₃
-
-
-    rw [Subgroup.ne_bot_iff_exists_ne_one]
-    use ⟨f * g * f⁻¹, fgf_in_ristInter₂⟩
-    simp
-    rw [<-ne_eq]
-    exact fgf_ne_one
-
-  use RigidStabilizerInter₀ α new_seed
-  apply And.intro
-  exact ⟨⟨new_seed, new_seed_ne_bot⟩, rfl⟩
-  rw [RigidStabilizerInter₀.eq_sInter]
-  unfold_let
-  simp [<-regularSupport_smulImage]
-  rw [<-smulImage_iInter_fin]
-
-  ext x
-  simp only [Subsemigroup.mem_carrier, Submonoid.mem_toSubsemigroup,
-    Subgroup.mem_toSubmonoid, Set.mem_image]
-  rw [rigidStabilizer_smulImage]
-  rw [<-H_eq, RigidStabilizerBasis₀.val_def, RigidStabilizerInter₀.eq_sInter]
-
-  constructor
-  · intro fxf_mem
-    use f⁻¹ * x * f
-    constructor
-    · exact fxf_mem
-    · group
-  · intro ⟨y, ⟨y_in_H, y_conj⟩⟩
-    rw [<-y_conj]
-    group
-    exact y_in_H
-
-def RigidStabilizerBasisMul (G α : Type _) [Group G] [MulAction G α] [TopologicalSpace α]
-  [ContinuousConstSMul G α] (f : G) (H : Subgroup G) : Subgroup G
-where
-  carrier := (fun g => f * g * f⁻¹) '' H.carrier
-  mul_mem' := by
-    intro a b a_mem b_mem
-    simp at a_mem
-    simp at b_mem
-    let ⟨a', a'_in_H, a'_eq⟩ := a_mem
-    let ⟨b', b'_in_H, b'_eq⟩ := b_mem
-    use a' * b'
-    constructor
-    · apply Subsemigroup.mul_mem' <;> simp <;> assumption
-    · simp
-      rw [<-a'_eq, <-b'_eq]
-      group
-  one_mem' := by
-    simp
-    use 1
-    constructor
-    exact Subgroup.one_mem H
-    group
-  inv_mem' := by
-    simp
-    intro g g_in_H
-    use g⁻¹
-    constructor
-    exact Subgroup.inv_mem H g_in_H
-    rw [mul_assoc]
-
-theorem RigidStabilizerBasisMul_mem (f : G) {H : Subgroup G} (H_in_basis : H ∈ RigidStabilizerBasis G α)
-  : RigidStabilizerBasisMul G α f H ∈ RigidStabilizerBasis G α :=
-by
-  rw [RigidStabilizerBasis.mem_iff_asSets]
-  unfold RigidStabilizerBasisMul
-  simp
-
-  apply RigidStabilizerBasis.smulImage_mem₀
-  assumption
-
-instance rigidStabilizerBasis_smul : SMul G (RigidStabilizerBasis G α) where
-  smul := fun g H => ⟨
-    RigidStabilizerBasisMul G α g H.val,
-    RigidStabilizerBasisMul_mem g H.prop
-  ⟩
-
-theorem RigidStabilizerBasis.smul_eq (g : G) {H: Subgroup G} (H_in_basis : H ∈ RigidStabilizerBasis G α) :
-  g • (⟨H, H_in_basis⟩ : RigidStabilizerBasis G α) = ⟨
-    RigidStabilizerBasisMul G α g H,
-    RigidStabilizerBasisMul_mem g H_in_basis
-  ⟩ := rfl
-
-theorem RigidStabilizerBasis.mem_smul (f g : G) {H: Subgroup G} (H_in_basis : H ∈ RigidStabilizerBasis G α):
-  f ∈ (g • (⟨H, H_in_basis⟩ : RigidStabilizerBasis G α)).val ↔ g⁻¹ * f * g ∈ H :=
-by
-  rw [RigidStabilizerBasis.smul_eq]
-  simp
-  rw [<-Subgroup.mem_carrier]
-  unfold RigidStabilizerBasisMul
-  simp
-  constructor
-  · intro ⟨x, x_in_H, f_eq⟩
-    rw [<-f_eq]
-    group
-    exact x_in_H
-  · intro gfg_in_H
-    use g⁻¹ * f * g
-    constructor
-    assumption
-    group
-
-instance rigidStabilizerBasis_mulAction : MulAction G (RigidStabilizerBasis G α) where
-  one_smul := by
-    intro ⟨H, H_in_ristBasis⟩
-    ext x
-    rw [RigidStabilizerBasis.mem_smul]
-    group
-  mul_smul := by
-    intro f g ⟨B, B_in_ristBasis⟩
-    ext x
-    repeat rw [RigidStabilizerBasis.mem_smul]
-    group
-
-end Rubin
diff --git a/Rubin/Topology.lean b/Rubin/Topology.lean
index ee1990f..fd94dfc 100644
--- a/Rubin/Topology.lean
+++ b/Rubin/Topology.lean
@@ -1,5 +1,6 @@
 import Mathlib.GroupTheory.Subgroup.Basic
 import Mathlib.GroupTheory.GroupAction.Basic
+import Mathlib.GroupTheory.GroupAction.Hom
 import Mathlib.Topology.Basic
 import Mathlib.Topology.Homeomorph
 import Mathlib.Topology.Algebra.ConstMulAction
@@ -9,33 +10,88 @@ import Rubin.MulActionExt
 
 namespace Rubin
 
--- TODO: give this a notation?
--- TODO: coe to / extend MulActionHom
+section Equivariant
+
+-- TODO: rename or remove?
+def IsEquivariant (G : Type _) {β : Type _} [Group G] [MulAction G α]
+    [MulAction G β] (f : α → β) :=
+  ∀ g : G, ∀ x : α, f (g • x) = g • f x
+
+-- TODO: rename to MulActionHomeomorph
 structure EquivariantHomeomorph (G α β : Type _) [Group G] [TopologicalSpace α]
     [TopologicalSpace β] [MulAction G α] [MulAction G β] extends Homeomorph α β where
-  equivariant : is_equivariant G toFun
-#align equivariant_homeomorph Rubin.EquivariantHomeomorph
+  toFun_equivariant' : IsEquivariant G toFun
 
-variable {G α β : Type _}
+variable {G α β γ: Type*}
 variable [Group G]
-variable [TopologicalSpace α] [TopologicalSpace β]
-
-theorem equivariant_fun [MulAction G α] [MulAction G β]
-    (h : EquivariantHomeomorph G α β) :
-    is_equivariant G h.toFun :=
-  h.equivariant
-#align equivariant_fun Rubin.equivariant_fun
-
-theorem equivariant_inv [MulAction G α] [MulAction G β]
-    (h : EquivariantHomeomorph G α β) :
-    is_equivariant G h.invFun :=
-  by
+variable [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ]
+variable [MulAction G α] [MulAction G β] [MulAction G γ]
+
+theorem EquivariantHomeomorph.toFun_equivariant (f : EquivariantHomeomorph G α β) :
+  IsEquivariant G f.toHomeomorph :=
+by
+  show IsEquivariant G f.toFun
+  exact f.toFun_equivariant'
+
+instance EquivariantHomeomorph.smulHomClass : SMulHomClass (EquivariantHomeomorph G α β) G α β where
+  coe := fun f => f.toFun
+  coe_injective' := by
+    show Function.Injective (fun f => f.toHomeomorph)
+    refine Function.Injective.comp FunLike.coe_injective ?mk_inj
+    intro f g
+    rw [mk.injEq]
+    tauto
+  map_smul := fun f => f.toFun_equivariant
+
+theorem EquivariantHomeomorph.invFun_equivariant
+  (h : EquivariantHomeomorph G α β) :
+  IsEquivariant G h.invFun :=
+by
   intro g x
   symm
-  let e := congr_arg h.invFun (h.equivariant g (h.invFun x))
+  let e := congr_arg h.invFun (h.toFun_equivariant' g (h.invFun x))
   rw [h.left_inv _, h.right_inv _] at e
   exact e
-#align equivariant_inv Rubin.equivariant_inv
+
+def EquivariantHomeomorph.trans (f₁ : EquivariantHomeomorph G α β) (f₂ : EquivariantHomeomorph G β γ) :
+  EquivariantHomeomorph G α γ
+where
+  toHomeomorph := Homeomorph.trans f₁.toHomeomorph f₂.toHomeomorph
+  toFun_equivariant' := by
+    intro g x
+    simp
+    rw [f₁.toFun_equivariant]
+    rw [f₂.toFun_equivariant]
+
+@[simp]
+theorem EquivariantHomeomorph.trans_toFun (f₁ : EquivariantHomeomorph G α β) (f₂ : EquivariantHomeomorph G β γ) :
+  (f₁.trans f₂).toFun = f₂.toFun ∘ f₁.toFun :=
+by
+  simp [trans]
+  rfl
+
+@[simp]
+theorem EquivariantHomeomorph.trans_invFun (f₁ : EquivariantHomeomorph G α β) (f₂ : EquivariantHomeomorph G β γ) :
+  (f₁.trans f₂).invFun = f₁.invFun ∘ f₂.invFun :=
+by
+  simp [trans]
+  rfl
+
+def EquivariantHomeomorph.inv (f : EquivariantHomeomorph G α β) :
+  EquivariantHomeomorph G β α
+where
+  toHomeomorph := f.symm
+  toFun_equivariant' := f.invFun_equivariant
+
+@[simp]
+theorem EquivariantHomeomorph.inv_toFun (f : EquivariantHomeomorph G α β) :
+  f.inv.toFun = f.invFun := rfl
+
+@[simp]
+theorem EquivariantHomeomorph.inv_invFun (f : EquivariantHomeomorph G α β) :
+  f.inv.invFun = f.toFun := rfl
+
+end Equivariant
 
 open Topology