:up_arrow: Upgrade mathlib

All that remains is to define the conjugation action on RubinSpace,
and prove that the canonical homeomorph (lim/fromPoint) preserves that action.

The tools should be in place to prove most of this, and I don't have to deal with open sets ever again.

README.md

@@ -1 +1,32 @@
 # Lean4 port of the proof of Rubin's Theorem
+
+THis repository contains a (WIP) computer proof of Rubin's Theorem,
+which states that if a group acts on two topological spaces while satisfying enough conditions,
+then there exists a homeomorphism between those two topological spaces,
+such that the homeomorphism preserves the group structure of the group action.
+
+It is based on ["A short proof of Rubin's Theorem"](https://arxiv.org/abs/2203.05930) (James Belk, Luke Elliott and Franceso Matucci),
+and a good part of the computer proof was written in Lean 3 by [Laurent Bartholdi](https://www.math.uni-sb.de/ag/bartholdi/).
+
+The eventual goal of this computer proof is to have it land into [Mathlib](https://github.com/leanprover-community/mathlib4).
+
+## Installation and running
+
+You will need an installation of [`elan`](https://github.com/leanprover/elan) and `git`.
+
+Then, simply run the following:
+
+```sh
+# Clone this repository
+git clone https://github.com/adri326/rubin-lean4
+
+# Navigate to the folder created by git
+cd rubin-lean4
+
+# This will download mathlib, and try to download a set of pre-compiled .olean files,
+# so you won't have to re-compile the entirety of mathlib again (which takes a good hour or two)
+lake exe cache get
+
+# Build the code (if no errors are printed then Lean was happy)
+lake build
+```

Rubin/AlgebraicDisjointness.lean

@@ -3,40 +3,52 @@ import Mathlib.GroupTheory.Subgroup.Basic
 import Mathlib.GroupTheory.Subgroup.Actions
 import Mathlib.GroupTheory.Commutator
 import Mathlib.Topology.Basic
+import Mathlib.Topology.Algebra.ConstMulAction
 import Mathlib.Data.Fintype.Perm
 import Mathlib.Tactic.FinCases
 import Mathlib.Tactic.IntervalCases
 
 import Rubin.RigidStabilizer
 import Rubin.SmulImage
-import Rubin.Topological
+import Rubin.Topology
 import Rubin.FaithfulAction
 import Rubin.Period
+import Rubin.LocallyDense
 
 namespace Rubin
 
-class LocallyMoving (G α : Type _) [Group G] [TopologicalSpace α] [MulAction G α] :=
+variable {G : Type _} [Group G]
-  locally_moving: ∀ U : Set α, IsOpen U → Set.Nonempty U → RigidStabilizer G U ≠ ⊥
+
-#align is_locally_moving Rubin.LocallyMoving
+theorem Commute.conj (f g h : G) : Commute (f * g * f⁻¹) h ↔ Commute g (f⁻¹ * h * f) := by
-
+  suffices ∀ (f g h : G), Commute (f * g * f⁻¹) h → Commute g (f⁻¹ * h * f) by
-namespace LocallyMoving
+    constructor
-
+    · apply this
-theorem get_nontrivial_rist_elem {G α : Type _}
+    · intro cg
-  [Group G]
+      symm
-  [TopologicalSpace α]
+      nth_rw 1 [<-inv_inv f]
-  [MulAction G α]
+      apply this
-  [h_lm : LocallyMoving G α]
+      symm
-  {U: Set α}
+      rw [inv_inv]
-  (U_open : IsOpen U)
+      exact cg
-  (U_nonempty : U.Nonempty) :
+
-  ∃ x : G, x ∈ RigidStabilizer G U ∧ x ≠ 1 :=
+  intro f g h fgf_h_comm
-by
+  unfold Commute SemiconjBy at *
-  have rist_ne_bot := h_lm.locally_moving U U_open U_nonempty
+  rw [<-mul_assoc, <-mul_assoc]
-  exact (or_iff_right rist_ne_bot).mp (Subgroup.bot_or_exists_ne_one _)
+  rw [<-mul_assoc, <-mul_assoc] at fgf_h_comm
+  have gfh_eq : g * f⁻¹ * h = f⁻¹ * h * f * g * f⁻¹ := by
+    repeat rw [mul_assoc f⁻¹]
+    rw [<-fgf_h_comm]
+    group
+  rw [gfh_eq]
+  group
+
+theorem Commute.conj' (f g h : G) : Commute (f⁻¹ * g * f) h ↔ Commute g (f * h * f⁻¹) := by
+  nth_rw 2 [<-inv_inv f]
+  nth_rw 3 [<-inv_inv f]
+  apply Commute.conj
 
-end LocallyMoving
 
-structure AlgebraicallyDisjointElem {G : Type _} [Group G] (f g h : G) :=
+structure AlgebraicallyDisjointElem (f g h : G) :=
   non_commute: ¬Commute f h
   fst : G
   snd : G
@@ -47,18 +59,51 @@ structure AlgebraicallyDisjointElem {G : Type _} [Group G] (f g h : G) :=
 
 namespace AlgebraicallyDisjointElem
 
-def comm_elem {G : Type _} [Group G] {f g h : G} (disj_elem : AlgebraicallyDisjointElem f g h) : G :=
+def comm_elem {f g h : G} (disj_elem : AlgebraicallyDisjointElem f g h) : G :=
   ⁅disj_elem.fst, ⁅disj_elem.snd, h⁆⁆
 
 @[simp]
-theorem comm_elem_eq {G : Type _} [Group G] {f g h : G} (disj_elem : AlgebraicallyDisjointElem f g h) :
+theorem comm_elem_eq {f g h : G} (disj_elem : AlgebraicallyDisjointElem f g h) :
   disj_elem.comm_elem = ⁅disj_elem.fst, ⁅disj_elem.snd, h⁆⁆ :=
 by
   unfold comm_elem
   simp
 
+lemma comm_elem_conj (f g h i : G) :
+  ⁅i * f * i⁻¹, ⁅i * g * i⁻¹, i * h * i⁻¹⁆⁆ = i * ⁅f, ⁅g, h⁆⁆ * i⁻¹ := by group
+
+theorem conj {f g h : G} (disj_elem : AlgebraicallyDisjointElem f g h) (i : G): AlgebraicallyDisjointElem (i * f * i⁻¹) (i * g * i⁻¹) (i * h * i⁻¹) where
+  non_commute := by
+    rw [Commute.conj]
+    group
+    exact disj_elem.non_commute
+  fst := i * disj_elem.fst * i⁻¹
+  snd := i * disj_elem.snd * i⁻¹
+  fst_commute := by
+    rw [Commute.conj]
+    group
+    exact disj_elem.fst_commute
+  snd_commute := by
+    rw [Commute.conj]
+    group
+    exact disj_elem.snd_commute
+  comm_elem_nontrivial := by
+    intro eq_one
+    apply disj_elem.comm_elem_nontrivial
+    rw [comm_elem_conj, <-mul_right_inv i] at eq_one
+    apply mul_right_cancel at eq_one
+    nth_rw 2 [<-mul_one i] at eq_one
+    apply mul_left_cancel at eq_one
+    exact eq_one
+  comm_elem_commute := by
+    rw [comm_elem_conj, Commute.conj]
+    rw [(by group : i⁻¹ * (i * g * i⁻¹) * i = g)]
+    exact disj_elem.comm_elem_commute
+
 end AlgebraicallyDisjointElem
 
+-- Also known as `η_G(f)`.
+
 /--
 A pair (f, g) is said to be "algebraically disjoint" if it can produce an instance of
 [`AlgebraicallyDisjointElem`] for any element `h ∈ G` such that `f` and `h` don't commute.
@@ -69,7 +114,8 @@ so that `⁅f₁, ⁅f₂, h⁆⁆` is a nontrivial element of `Centralizer(g, G
 
 Here the definition of `k ∈ Centralizer(g, G)` is directly unrolled as `Commute k g`.
 
-This is a slightly stronger proposition that plain disjointness, a
+This is a slightly weaker proposition than plain disjointness,
+but it is easier to derive from the hypothesis of Rubin's theorem.
 -/
 def AlgebraicallyDisjoint {G : Type _} [Group G] (f g : G) :=
   ∀ (h : G), ¬Commute f h → AlgebraicallyDisjointElem f g h
@@ -89,7 +135,18 @@ fun (h : G) (nc : ¬Commute f h) => {
     exact (mk_thm h nc).choose_spec.choose_spec.right.right.right
 }
 
--- This is an idea of having a Prop version of AlgebraicallyDisjoint, but it sounds painful to work with
+/--
+This definition simply wraps `AlgebraicallyDisjoint` as a `Prop`.
+It is equivalent to it, although since `AlgebraicallyDisjoint` isn't a `Prop`,
+an `↔` (iff) statement joining the two cannot be written.
+
+You should consider using it when proving `↔`/`∧` kinds of theorems, or when tools like `cases` are needed,
+as the base `AlgebraicallyDisjoint` isn't a `Prop` and won't work with those.
+
+The two `Coe` and `CoeFn` instances provided around this type make it essentially transparent —
+you can use an instance of `AlgebraicallyDisjoint` in place of a `IsAlgebraicallyDisjoint` and vice-versa.
+You might need to add the odd `↑` (coe) operator to make Lean happy.
+--/
 def IsAlgebraicallyDisjoint {G : Type _} [Group G] (f g : G): Prop :=
   ∀ (h : G), ¬Commute f h → ∃ (f₁ f₂ : G), ∃ (elem : AlgebraicallyDisjointElem f g h), elem.fst = f₁ ∧ elem.snd = f₂
 
@@ -122,95 +179,26 @@ noncomputable instance coeFnAlgebraicallyDisjoint : CoeFun
 instance coeAlgebraicallyDisjoint : Coe (AlgebraicallyDisjoint f g) (IsAlgebraicallyDisjoint f g) where
   coe := mk
 
-end IsAlgebraicallyDisjoint
+theorem conj (is_alg_disj : IsAlgebraicallyDisjoint f g) (h : G) :
-
+  IsAlgebraicallyDisjoint (h * f * h⁻¹) (h * g * h⁻¹) :=
-@[simp]
-theorem orbit_bot (G : Type _) [Group G] [MulAction G α] (p : α) :
-    MulAction.orbit (⊥ : Subgroup G) p = {p} :=
 by
-  ext1
+  apply elim at is_alg_disj
-  rw [MulAction.mem_orbit_iff]
+  apply mk
-  constructor
+  intro i nc
-  · rintro ⟨⟨_, g_bot⟩, g_to_x⟩
+  rw [Commute.conj] at nc
-    rw [← g_to_x, Set.mem_singleton_iff, Subgroup.mk_smul]
+  rw [(by group : i = h * (h⁻¹ * i * h) * h⁻¹)]
-    exact (Subgroup.mem_bot.mp g_bot).symm ▸ one_smul _ _
+  exact (is_alg_disj (h⁻¹ * i * h) nc).conj h
-  exact fun h => ⟨1, Eq.trans (one_smul _ p) (Set.mem_singleton_iff.mp h).symm⟩
-#align orbit_bot Rubin.orbit_bot
 
+end IsAlgebraicallyDisjoint
+
+-- TODO: find a better home for these lemmas
 variable {G α : Type _}
 variable [Group G]
 variable [TopologicalSpace α]
-variable [ContinuousMulAction G α]
+variable [MulAction G α]
+variable [ContinuousConstSMul 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)) :=
@@ -226,97 +214,6 @@ by
       <;> simp only [h, true_or, or_true]
   · rintro ((h|h)|(h|h)) <;> exact ⟨_, h⟩
 
--- TODO: move to Rubin.lean
--- TODO: modify the proof to be less "let everything"-y, especially the first half
--- TODO: use the new class thingy to write a cleaner proof?
-lemma proposition_1_1_1 [h_lm : LocallyMoving G α] [T2Space α] (f g : G) (supp_disjoint : Disjoint (Support α f) (Support α g)) : AlgebraicallyDisjoint f g := by
-  apply AlgebraicallyDisjoint_mk
-  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 := (rigidStabilizer_support.mp 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 := rigidStabilizer_support.mp 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 := rigidStabilizer_support.mp 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 rigidStabilizer_support.mp 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 := (rigidStabilizer_support.mp 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 rigidStabilizer_support.mp 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 rigidStabilizer_support.mp 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 smulImage_mul {g h : G} {U : Set α} : g •'' (h •'' U) = (g*h) •'' U :=
-  (mul_smulImage g h U)
-
 lemma smul_inj_moves {ι : Type*} [Fintype ι] [T2Space α]
   {f : ι → G} {x : α} {i j : ι} (i_ne_j : i ≠ j)
   (f_smul_inj : Function.Injective (fun i : ι => (f i) • x)) :
@@ -325,7 +222,7 @@ lemma smul_inj_moves {ι : Type*} [Fintype ι] [T2Space α]
     apply i_ne_j
     apply f_smul_inj
     group_action
-    group_action at h
+    group at h
     exact h
 
 def smul_inj_nbhd {ι : Type*} [Fintype ι] [T2Space α]
@@ -367,11 +264,7 @@ by
   let U := ⋂(p : ι₂), smul_inj_nbhd p.prop f_smul_inj
   use U
 
-  -- The notations provided afterwards tend to be quite ugly because we used `Exists.choose`,
+  repeat' apply And.intro
-  -- but the idea is that this all boils down to applying `Exists.choose_spec`, except in the disjointness case,
-  -- where we transform `Disjoint (f i •'' U) (f j •'' U)` into `Disjoint U ((f i)⁻¹ * f j •'' U)`
-  -- and transform both instances of `U` into `N`, the neighborhood of the chosen `(i, j) ∈ ι₂`
-  repeat' constructor
   · apply isOpen_iInter_of_finite
     intro ⟨⟨i, j⟩, i_ne_j⟩
     apply smul_inj_nbhd_open
@@ -379,6 +272,8 @@ by
     intro ⟨⟨i, j⟩, i_ne_j⟩
     apply smul_inj_nbhd_mem
   · intro i j i_ne_j
+
+    -- We transform `Disjoint (f i •'' U) (f j •'' U)` into `Disjoint N ((f i)⁻¹ * f j •'' N)`
     let N := smul_inj_nbhd i_ne_j f_smul_inj
     have U_subset_N : U ⊆ N := Set.iInter_subset
       (fun (⟨⟨i, j⟩, i_ne_j⟩ : ι₂) => (smul_inj_nbhd i_ne_j f_smul_inj))
@@ -387,7 +282,7 @@ by
     rw [disjoint_comm, smulImage_disjoint_mul]
 
     apply Set.disjoint_of_subset U_subset_N
-    · apply smulImage_subset
+    · apply smulImage_mono
       exact U_subset_N
     · exact smul_inj_nbhd_disjoint i_ne_j f_smul_inj
 
@@ -435,7 +330,7 @@ by
       unfold_let
       rw [h.1]
       rw [smul_eq_iff_eq_inv_smul]
-      group_action
+      group
       symm
       exact same_img
   }
@@ -493,10 +388,7 @@ theorem smul_injective_within_period {g : G} {p : α} {n : ℕ}
   (period_eq_n : Period.period p g = n) :
   Function.Injective (fun (i : Fin n) => g ^ (i : ℕ) • p) :=
 by
-  have zpow_fix : (fun (i : Fin n) => g ^ (i : ℕ) • p) = (fun (i : Fin n) => g ^ (i : ℤ) • p) := by
+  simp only [<-zpow_coe_nat]
-    ext x
-    simp
-  rw [zpow_fix]
   apply moves_inj
   intro k one_le_k k_lt_n
 
@@ -506,191 +398,235 @@ by
   exact k_lt_n
 #align moves_inj_period Rubin.smul_injective_within_period
 
--- TODO: move to Rubin.lean
+
-lemma moves_1234_of_moves_12 {g : G} {x : α} (g12_moves : g^12 • x ≠ x) :
+/-
-  Function.Injective (fun i : Fin 5 => g^(i : ℤ) • x) :=
+The algebraic centralizer (and its associated basis) allow for a purely group-theoretic construction of the
+`RegularSupport` sets.
+They are defined as the centralizers of the subgroups `{g^12 | g ∈ G ∧ AlgebraicallyDisjoint f g}`
+-/
+section AlgebraicCentralizer
+
+variable {G : Type _}
+variable [Group G]
+
+-- TODO: prove this is a subgroup?
+-- This is referred to as `ξ_G^12(f)`
+def AlgebraicSubgroup (f : G) : Set G :=
+  (fun g : G => g^12) '' { g : G | IsAlgebraicallyDisjoint f g }
+
+def AlgebraicCentralizer (f : G) : Subgroup G :=
+  Subgroup.centralizer (AlgebraicSubgroup f)
+
+theorem AlgebraicSubgroup.conj (f g : G) :
+  (fun h => g * h * g⁻¹) '' AlgebraicSubgroup f = AlgebraicSubgroup (g * f * g⁻¹) :=
 by
-  apply moves_inj
+  unfold AlgebraicSubgroup
-  intros k k_ge_1 k_lt_5
+  rw [Set.image_image]
-  simp at k_lt_5
+  have gxg12_eq : ∀ x : G, g * x^12 * g⁻¹ = (g * x * g⁻¹)^12 := by
-
-  by_contra x_fixed
-  have k_div_12 : k ∣ 12 := by
-    -- Note: norm_num does not support ℤ.dvd yet, nor ℤ.mod, nor Int.natAbs, nor Int.div, etc.
-    have h: (12 : ℤ) = (12 : ℕ) := by norm_num
-    rw [h, Int.ofNat_dvd_right]
-    apply Nat.dvd_of_mod_eq_zero
-
-    interval_cases k
-    all_goals unfold Int.natAbs
-    all_goals norm_num
-
-  have g12_fixed : g^12 • x = x := by
-    rw [<-zpow_ofNat]
     simp
-    rw [<-Int.mul_ediv_cancel' k_div_12]
+  simp only [gxg12_eq]
-    have res := smul_zpow_eq_of_smul_eq (12/k) x_fixed
+  ext x
-    group_action at res
+  simp
-    exact res
+  constructor
+  · intro ⟨y, y_disj, x_eq⟩
+    use g * y * g⁻¹
+    rw [<-gxg12_eq]
+    exact ⟨y_disj.conj g, x_eq⟩
+  · intro ⟨y, y_disj, x_eq⟩
+    use g⁻¹ * y * g
+    constructor
+    · convert y_disj.conj g⁻¹ using 1
+      all_goals group
+    · nth_rw 3 [<-inv_inv g]
+      simp only [conj_pow]
+      rw [x_eq]
+      group
 
-  exact g12_moves g12_fixed
+@[simp]
+theorem AlgebraicCentralizer.conj (f g : G) :
+  (fun h => g * h * g⁻¹) '' AlgebraicCentralizer f = AlgebraicCentralizer (g * f * g⁻¹) :=
+by
+  unfold AlgebraicCentralizer
 
-lemma proposition_1_1_2 [T2Space α] [h_lm : LocallyMoving G α]
+  ext x
-  (f g : G) (h_disj : AlgebraicallyDisjoint f g) : Disjoint (Support α f) (Support α (g^12)) :=
+  simp [Subgroup.mem_centralizer_iff]
+
+  constructor
+  · intro ⟨y, ⟨x_comm, x_eq⟩⟩
+    intro h h_in_alg
+    rw [<-AlgebraicSubgroup.conj] at h_in_alg
+    simp at h_in_alg
+    let ⟨i, i_in_alg, gig_eq_h⟩ := h_in_alg
+    specialize x_comm i i_in_alg
+    rw [<-gig_eq_h, <-x_eq]
+    group
+    rw [mul_assoc _ i, x_comm, <-mul_assoc]
+  · intro x_comm
+    use g⁻¹ * x * g
+    group
+    simp
+    intro h h_in_alg
+    simp [<-AlgebraicSubgroup.conj] at x_comm
+    specialize x_comm h h_in_alg
+    have h₁ : g⁻¹ * x * g * h = g⁻¹ * (g * h * g⁻¹ * x) * g := by
+      rw [x_comm]
+      group
+    rw [h₁]
+    group
+
+/--
+Finite intersections of [`AlgebraicCentralizer`].
+--/
+def AlgebraicCentralizerInter (S : Finset G) : Subgroup G :=
+  ⨅ (g ∈ S), AlgebraicCentralizer g
+
+def AlgebraicCentralizerBasis (G : Type _) [Group G] : Set (Set G) :=
+  { S : Set G | S ≠ {1} ∧ ∃ seed : Finset G,
+    S = AlgebraicCentralizerInter seed
+  }
+
+theorem AlgebraicCentralizerBasis.mem_iff (S : Set G) :
+  S ∈ AlgebraicCentralizerBasis G ↔
+    S ≠ {1} ∧ ∃ seed : Finset G, S = AlgebraicCentralizerInter seed
+:= by rfl
+
+theorem AlgebraicCentralizerBasis.subgroup_mem_iff (S : Subgroup G) :
+  (S : Set G) ∈ AlgebraicCentralizerBasis G ↔
+    S ≠ ⊥ ∧ ∃ seed : Finset G, S = AlgebraicCentralizerInter seed :=
 by
-  by_contra not_disjoint
+  rw [mem_iff, <-Subgroup.coe_bot, ne_eq, SetLike.coe_set_eq]
-  let U := Support α f ∩ Support α (g^12)
+  simp
-  have U_nonempty : U.Nonempty := by
+
-    apply Set.not_disjoint_iff_nonempty_inter.mp
+theorem AlgebraicCentralizerBasis.empty_not_mem : ∅ ∉ AlgebraicCentralizerBasis G := by
-    exact not_disjoint
+  simp [AlgebraicCentralizerBasis]
-
+  intro _ _
-  -- Since G is Hausdorff, we can find a nonempty set V ⊆ such that f(V) is disjoint from V and the sets {g^i(V): i=0..4} are pairwise disjoint
+  rw [<-ne_eq]
-  let x := U_nonempty.some
-  have x_in_U : x ∈ U := Set.Nonempty.some_mem U_nonempty
-  have fx_moves : f • x ≠ x := Set.inter_subset_left _ _ x_in_U
-
-  have five_points : Function.Injective (fun i : Fin 5 => g^(i : ℤ) • x) := by
-    apply moves_1234_of_moves_12
-    exact (Set.inter_subset_right _ _ x_in_U)
-  have U_open: IsOpen U := (IsOpen.inter (support_open f) (support_open (g^12)))
-
-  let ⟨V₀, V₀_open, x_in_V₀, V₀_in_support, disjoint_img_V₀⟩ := disjoint_nbhd_in U_open x_in_U fx_moves
-  let ⟨V₁, V₁_open, x_in_V₁, disjoint_img_V₁⟩ := disjoint_nbhd_fin five_points
-
-  let V := V₀ ∩ V₁
-  -- Let h be a nontrivial element of the RigidStabilizer G V
-  let ⟨h, ⟨h_in_ristV, h_ne_one⟩⟩ := h_lm.get_nontrivial_rist_elem (IsOpen.inter V₀_open V₁_open) (Set.nonempty_of_mem ⟨x_in_V₀, x_in_V₁⟩)
-
-  have V_disjoint_smulImage: Disjoint V (f •'' V) := by
-    apply Set.disjoint_of_subset
-    · exact Set.inter_subset_left _ _
-    · apply smulImage_subset
-      exact Set.inter_subset_left _ _
-    · exact disjoint_img_V₀
-
-  have comm_non_trivial : ¬Commute f h := by
-    by_contra comm_trivial
-    let ⟨z, z_in_V, z_moved⟩ := faithful_rigid_stabilizer_moves_point h_in_ristV h_ne_one
-    apply z_moved
-
-    nth_rewrite 2 [<-one_smul G z]
-    rw [<-commutatorElement_eq_one_iff_commute.mpr comm_trivial.symm]
   symm
+  rw [<-Set.nonempty_iff_ne_empty]
+  exact Subgroup.coe_nonempty _
 
-    apply disjoint_support_comm h f
+theorem AlgebraicCentralizerBasis.to_subgroup {S : Set G} (S_in_basis : S ∈ AlgebraicCentralizerBasis G):
-    · exact rigidStabilizer_support.mp h_in_ristV
+  ∃ S' : Subgroup G, S = S' :=
-    · exact V_disjoint_smulImage
+by
-    · exact z_in_V
+  rw [mem_iff] at S_in_basis
-
+  let ⟨_, ⟨seed, S_eq⟩⟩ := S_in_basis
-  -- 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)
+  use AlgebraicCentralizerInter seed
-  let alg_disj_elem := h_disj h comm_non_trivial
+
-  let f₁ := alg_disj_elem.fst
+theorem Set.image_equiv_eq {α β : Type _} (S : Set α) (T : Set β) (f : α ≃ β) :
-  let f₂ := alg_disj_elem.snd
+  f '' S = T ↔ S = f.symm '' T :=
-  let h' := alg_disj_elem.comm_elem
+by
-  have f₁_commutes : Commute f₁ g := alg_disj_elem.fst_commute
+  constructor
-  have f₂_commutes : Commute f₂ g := alg_disj_elem.snd_commute
+  · intro fS_eq_T
-  have h'_commutes : Commute h' g := alg_disj_elem.comm_elem_commute
+    ext x
-  have h'_nontrivial : h' ≠ 1 := alg_disj_elem.comm_elem_nontrivial
+    rw [<-fS_eq_T]
-
+    simp
-  have support_f₂_h : Support α ⁅f₂,h⁆ ⊆ V ∪ (f₂ •'' V) := by
+  · intro S_eq_fT
-    calc
+    ext x
-      Support α ⁅f₂, h⁆ ⊆ Support α h ∪ (f₂ •'' Support α h) := support_comm α f₂ h
+    rw [S_eq_fT]
-      _ ⊆ V ∪ (f₂ •'' Support α h) := by
+    simp
-        apply Set.union_subset_union_left
+
-        exact rigidStabilizer_support.mp h_in_ristV
+theorem AlgebraicCentralizerBasis.univ_mem (ex_non_trivial : ∃ g : G, g ≠ 1): Set.univ ∈ AlgebraicCentralizerBasis G := by
-      _ ⊆ V ∪ (f₂ •'' V) := by
+  rw [mem_iff]
-        apply Set.union_subset_union_right
+  constructor
-        apply smulImage_subset
+  symm
-        exact rigidStabilizer_support.mp h_in_ristV
+  exact Set.nonempty_compl.mp ex_non_trivial
-  have support_h' : Support α h' ⊆ ⋃(i : Fin 2 × Fin 2), (f₁^(i.1.val) * f₂^(i.2.val)) •'' V := by
+  use ∅
-    rw [rewrite_Union]
+  simp [AlgebraicCentralizerInter]
-    simp (config := {zeta := false})
+
-    rw [<-smulImage_mul, <-smulImage_union]
+theorem AlgebraicCentralizerBasis.conj_mem {S : Set G} (S_in_basis : S ∈ AlgebraicCentralizerBasis G)
-    calc
+  (h : G) : (fun g => h * g * h⁻¹) '' S ∈ AlgebraicCentralizerBasis G :=
-      Support α h' ⊆ Support α ⁅f₂,h⁆ ∪ (f₁ •'' Support α ⁅f₂, h⁆) := support_comm α f₁ ⁅f₂,h⁆
+by
-      _ ⊆ V ∪ (f₂ •'' V) ∪ (f₁ •'' Support α ⁅f₂, h⁆) := by
+  let ⟨S', S_eq⟩ := to_subgroup S_in_basis
-        apply Set.union_subset_union_left
+  rw [S_eq]
-        exact support_f₂_h
+  rw [S_eq, subgroup_mem_iff] at S_in_basis
-      _ ⊆ V ∪ (f₂ •'' V) ∪ (f₁ •'' V ∪ (f₂ •'' V)) := by
+  rw [mem_iff]
-        apply Set.union_subset_union_right
+
-        apply smulImage_subset f₁
+  have conj_eq : (fun g => h * g * h⁻¹) = (MulAut.conj h).toEquiv := by
-        exact support_f₂_h
+    ext x
-
+    simp
-  -- Since h' is nontrivial, it has at least one point p in its support
+
-  let ⟨p, p_moves⟩ := faithful_moves_point' α h'_nontrivial
+  constructor
-  -- Since g commutes with h', all five of the points {gi(p):i=0..4} lie in supp(h')
+  · rw [conj_eq]
-  have gi_in_support : ∀ (i: Fin 5), g^(i.val) • p ∈ Support α h' := by
+    rw [ne_eq, Set.image_equiv_eq]
-    intro i
+    simp
-    rw [mem_support]
+    rw [<-Subgroup.coe_bot, SetLike.coe_set_eq]
-    by_contra p_fixed
+    exact S_in_basis.left
-    rw [<-mul_smul, h'_commutes.pow_right, mul_smul] at p_fixed
+  · let ⟨seed, S'_eq⟩ := S_in_basis.right
-    group_action at p_fixed
+    have dec_eq : DecidableEq G := Classical.typeDecidableEq _
-    exact p_moves p_fixed
+    use Finset.image (fun g => h * g * h⁻¹) seed
-
+    rw [S'_eq]
-  -- The next section gets tricky, so let us clear away some stuff first :3
+    unfold AlgebraicCentralizerInter
-  clear h'_commutes h'_nontrivial
+    ext g
-  clear V₀_open x_in_V₀ V₀_in_support disjoint_img_V₀
+    rw [conj_eq]
-  clear V₁_open x_in_V₁
+    rw [Set.mem_image_equiv]
-  clear five_points h_in_ristV h_ne_one V_disjoint_smulImage
+    simp
-  clear support_f₂_h
+    conv => {
-
+      rhs
-  -- by the pigeonhole principle, one of the four sets V, f₁(V), f₂(V), f₁f₂(V) must contain two of these points,
+      intro
-  -- say g^i(p),g^j(p) ∈ k(V) for some 0 ≤ i < j ≤ 4 and k ∈ {1,f₁,f₂,f₁f₂}
+      intro
-  let pigeonhole : Fintype.card (Fin 5) > Fintype.card (Fin 2 × Fin 2) := by trivial
+      rw [<-SetLike.mem_coe, <-AlgebraicCentralizer.conj, conj_eq, Set.mem_image_equiv]
-  let choice_pred := fun (i : Fin 5) => (Set.mem_iUnion.mp (support_h' (gi_in_support i)))
+    }
-  let choice := fun (i : Fin 5) => (choice_pred i).choose
+
-  let ⟨i, _, j, _, i_ne_j, same_choice⟩ := Finset.exists_ne_map_eq_of_card_lt_of_maps_to
+theorem AlgebraicCentralizerBasis.inter_closed
-    pigeonhole
+  {S T : Set G} (S_in_basis : S ∈ AlgebraicCentralizerBasis G) (T_in_basis : T ∈ AlgebraicCentralizerBasis G)
-    (fun (i : Fin 5) _ => Finset.mem_univ (choice i))
+  (ST_ne_bot : S ∩ T ≠ {1}) :
-
+  S ∩ T ∈ AlgebraicCentralizerBasis G :=
-  let k := f₁^(choice i).1.val * f₂^(choice i).2.val
+by
-  have same_k : f₁^(choice j).1.val * f₂^(choice j).2.val = k := by rw [<-same_choice]
+  let ⟨S', S_eq⟩ := to_subgroup S_in_basis
-  have gi : g^i.val • p ∈ k •'' V := (choice_pred i).choose_spec
+  rw [S_eq]
-  have gk : g^j.val • p ∈ k •'' V := by
+  rw [S_eq, subgroup_mem_iff] at S_in_basis
-    have gk' := (choice_pred j).choose_spec
+  let ⟨S'_ne_bot, ⟨S'_seed, S'_eq⟩⟩ := S_in_basis
-    rw [same_k] at gk'
+
-    exact gk'
+  let ⟨T', T_eq⟩ := to_subgroup T_in_basis
-
+  rw [T_eq]
-  -- Since g^(j-i)(V) is disjoint from V and k commutes with g,
+  rw [T_eq, subgroup_mem_iff] at T_in_basis
-  -- we know that g^(j−i)k(V) is disjoint from k(V),
+  let ⟨T'_ne_bot, ⟨T'_seed, T'_eq⟩⟩ := T_in_basis
-  -- which leads to a contradiction since g^i(p) and g^j(p) both lie in k(V).
+
-
+  rw [<-Subgroup.coe_inf, subgroup_mem_iff]
-  have g_disjoint : Disjoint ((g^i.val)⁻¹ •'' V) ((g^j.val)⁻¹ •'' V) := by
+  rw [S_eq, T_eq, <-Subgroup.coe_inf, <-Subgroup.coe_bot, ne_eq, SetLike.coe_set_eq, <-ne_eq] at ST_ne_bot
-    apply smulImage_disjoint_subset (Set.inter_subset_right V₀ V₁)
+
-    group
+  have dec_eq : DecidableEq G := Classical.typeDecidableEq G
-    rw [smulImage_disjoint_inv_pow]
+
+  refine ⟨ST_ne_bot, ⟨S'_seed ∪ T'_seed, ?inter_eq⟩⟩
+
+  unfold AlgebraicCentralizerInter
+
+  simp only [<-Finset.mem_coe]
+  rw [Finset.coe_union, iInf_union]
+  rw [S'_eq, T'_eq]
+  rfl
+
+
+def MulAut.conj_order_iso (g : G) : Set G ≃o Set G := (MulAut.conj g).toEquiv.toOrderIsoSet
+
+theorem AlgebraicCentralizerBasis.eq_conj_self (g : G) :
+  (MulAut.conj_order_iso g) '' AlgebraicCentralizerBasis G = AlgebraicCentralizerBasis G :=
+by
+  ext S
+  simp [MulAut.conj_order_iso]
+  conv => {
+    lhs
+    congr; intro x
+    rw [Equiv.toOrderIsoSet_apply]
+  }
+  simp
+  constructor
+  · intro ⟨T, T_in_basis, T_eq⟩
+    rw [<-T_eq]
+    exact conj_mem T_in_basis g
+  · intro S_in_basis
+    use (fun h => g⁻¹ * h * g⁻¹⁻¹) '' S
+    refine ⟨conj_mem S_in_basis g⁻¹, ?S_eq⟩
+    rw [Set.image_image]
     group
-    apply disjoint_img_V₁
+    rw [Set.image_id']
-    symm; exact i_ne_j
+
-
+theorem AlgebraicCentralizerBasis.conj_mem' {S : Set G} (S_in_basis : S ∈ AlgebraicCentralizerBasis G) (g : G) :
-  have k_commutes: Commute k g := by
+  (MulAut.conj_order_iso g) S ∈ AlgebraicCentralizerBasis G :=
-    apply Commute.mul_left
+by
-    · exact f₁_commutes.pow_left _
+  show (fun i => g * i * g⁻¹) '' S ∈ AlgebraicCentralizerBasis G
-    · exact f₂_commutes.pow_left _
+  exact conj_mem S_in_basis g
-  clear f₁_commutes f₂_commutes
+
-
+end AlgebraicCentralizer
-  have g_k_disjoint : Disjoint ((g^i.val)⁻¹ •'' (k •'' V)) ((g^j.val)⁻¹ •'' (k •'' V)) := by
-    repeat rw [mul_smulImage]
-    repeat rw [<-inv_pow]
-    repeat rw [k_commutes.symm.inv_left.pow_left]
-    repeat rw [<-mul_smulImage k]
-    repeat rw [inv_pow]
-    exact disjoint_smulImage k g_disjoint
-
-  apply Set.disjoint_left.mp g_k_disjoint
-  · rw [mem_inv_smulImage]
-    exact gi
-  · rw [mem_inv_smulImage]
-    exact gk
-
-lemma remark_1_2 (f g : G) (h_disj : AlgebraicallyDisjoint f g): Commute f g := by
-  by_contra non_commute
-  let disj_elem := h_disj g non_commute
-  let nontrivial := disj_elem.comm_elem_nontrivial
-
-  rw [commutatorElement_eq_one_iff_commute.mpr disj_elem.snd_commute] at nontrivial
-  rw [commutatorElement_one_right] at nontrivial
-
-  tauto
 
 end Rubin

Rubin/InteriorClosure.lean

@@ -0,0 +1,260 @@
+import Mathlib.Topology.Basic
+import Mathlib.Topology.Separation
+
+import Rubin.SmulImage
+
+namespace Rubin
+
+variable {α : Type _}
+variable [TopologicalSpace α]
+
+/--
+Defines a kind of "regularization" transformation made to sets,
+by calling `closure` followed by `interior` on those sets.
+
+A set is then said to be [`Regular`] if the InteriorClosure does not modify it.
+--/
+def InteriorClosure (U : Set α) : Set α :=
+  interior (closure U)
+#align interior_closure Rubin.InteriorClosure
+
+@[simp]
+theorem InteriorClosure.def (U : Set α) : InteriorClosure U = interior (closure U) :=
+  by simp [InteriorClosure]
+
+@[simp]
+theorem InteriorClosure.fdef : InteriorClosure = (interior ∘ (closure (α := α))) := by ext; simp
+
+/--
+A set `U` is said to be regular if the interior of the closure of `U` is equal to `U`.
+Notably, a regular set is also open, and the interior of a regular set is equal to itself.
+--/
+def Regular (U : Set α) : Prop :=
+  InteriorClosure U = U
+
+@[simp]
+theorem Regular.def (U : Set α) : Regular U ↔ interior (closure U) = U :=
+  by simp [Regular]
+#align set.is_regular_def Rubin.Regular.def
+
+@[simp]
+theorem Regular.eq {U : Set α} (U_reg : Regular U) : interior (closure U) = U :=
+  (Regular.def U).mp U_reg
+
+instance Regular.instCoe {U : Set α} : Coe (Regular U) (interior (closure U) = U) where
+  coe := Regular.eq
+
+/-- From this, the set of regular sets is the set of regular *open* sets. --/
+theorem regular_open (U : Set α) : Regular U → IsOpen U :=
+by
+  intro h_reg
+  rw [<-h_reg]
+  simp
+
+theorem Regular.isOpen {U : Set α} (U_regular : Regular U): IsOpen U := regular_open _ U_regular
+
+theorem regular_interior {U : Set α} : Regular U → interior U = U :=
+by
+  intro h_reg
+  rw [<-h_reg]
+  simp
+
+theorem interiorClosure_open (U : Set α) : IsOpen (InteriorClosure U) := by simp
+#align is_open_interior_closure Rubin.interiorClosure_open
+
+theorem interiorClosure_subset {U : Set α} :
+  IsOpen U → U ⊆ InteriorClosure U :=
+by
+  intro h
+  apply subset_trans
+  exact subset_interior_iff_isOpen.mpr h
+  apply interior_mono
+  exact subset_closure
+#align is_open.interior_closure_subset Rubin.interiorClosure_subset
+
+theorem interiorClosure_regular (U : Set α) : Regular (InteriorClosure U) :=
+by
+  apply Set.eq_of_subset_of_subset <;> unfold InteriorClosure
+  {
+    apply interior_mono
+    nth_rw 2 [<-closure_closure (s := U)]
+    apply closure_mono
+    exact interior_subset
+  }
+  {
+    nth_rw 1 [<-interior_interior]
+    apply interior_mono
+    exact subset_closure
+  }
+#align regular_interior_closure Rubin.interiorClosure_regular
+
+theorem interiorClosure_mono (U V : Set α) :
+  U ⊆ V → InteriorClosure U ⊆ InteriorClosure V
+:= interior_mono ∘ closure_mono
+#align interior_closure_mono Rubin.interiorClosure_mono
+
+theorem monotone_interiorClosure : Monotone (InteriorClosure (α := α))
+:= fun a b =>
+  interiorClosure_mono a b
+
+theorem interiorClosure_subset_of_regular {U V : Set α} (U_ss_V : U ⊆ V) (V_regular : Regular V) :
+  InteriorClosure U ⊆ V :=
+by
+  rw [<-V_regular]
+  apply interiorClosure_mono
+  assumption
+
+theorem compl_closure_regular_of_open {S : Set α} (S_open : IsOpen S) : Regular (closure S)ᶜ := by
+  apply Set.eq_of_subset_of_subset
+  · simp
+    apply closure_mono
+    rw [IsOpen.subset_interior_iff S_open]
+    exact subset_closure
+  · apply interiorClosure_subset
+    simp
+
+@[simp]
+theorem interiorClosure_closure {S : Set α} (S_open : IsOpen S) : closure (InteriorClosure S) = closure S :=
+by
+  apply Set.eq_of_subset_of_subset
+  · simp
+    rw [<-Set.compl_subset_compl]
+    rw [<-(compl_closure_regular_of_open S_open)]
+    simp
+    rfl
+  · apply closure_mono
+    exact interiorClosure_subset S_open
+
+@[simp]
+theorem interiorClosure_interior {S : Set α} : interior (InteriorClosure S) = (InteriorClosure S) :=
+regular_interior (interiorClosure_regular S)
+
+theorem disjoint_interiorClosure_left {U V : Set α} (V_open : IsOpen V) :
+  Disjoint U V → Disjoint (InteriorClosure U) V :=
+by
+  intro disj
+  apply Set.disjoint_of_subset_left interior_subset
+  exact Disjoint.closure_left disj V_open
+
+theorem disjoint_interiorClosure_right {U V : Set α} (U_open : IsOpen U)
+  (disj : Disjoint U V) : Disjoint U (InteriorClosure V) :=
+  (disjoint_interiorClosure_left U_open (Disjoint.symm disj)).symm
+
+theorem disjoint_interiorClosure_left_iff {U V : Set α} (U_open : IsOpen U) (V_open : IsOpen V) :
+  Disjoint U V ↔ Disjoint (InteriorClosure U) V :=
+by
+  constructor
+  exact disjoint_interiorClosure_left V_open
+
+  intro disj
+  apply Set.disjoint_of_subset_left
+  · exact subset_closure
+  · rw [<-interiorClosure_closure U_open]
+    exact Disjoint.closure_left disj V_open
+
+theorem disjoint_interiorClosure_iff {U V : Set α} (U_open : IsOpen U) (V_open : IsOpen V) :
+  Disjoint U V ↔ Disjoint (InteriorClosure U) (InteriorClosure V) :=
+by
+  constructor
+  {
+    intro disj
+    apply disjoint_interiorClosure_left (interiorClosure_regular V).isOpen
+    apply disjoint_interiorClosure_right U_open
+    exact disj
+  }
+  {
+    intro disj
+    rw [disjoint_interiorClosure_left_iff U_open V_open]
+    symm
+    rw [disjoint_interiorClosure_left_iff V_open (interiorClosure_open _)]
+    symm
+    exact disj
+  }
+
+theorem subset_from_diff_closure_eq_empty {U V : Set α}
+  (U_regular : Regular U) (V_open : IsOpen V) (V_diff_cl_empty : V \ closure U = ∅) :
+  V ⊆ U :=
+by
+  have V_eq_interior : interior V = V := IsOpen.interior_eq V_open
+  rw [<-V_eq_interior]
+  rw [<-U_regular]
+  apply interior_mono
+  rw [<-Set.diff_eq_empty]
+  exact V_diff_cl_empty
+
+theorem regular_empty (α : Type _) [TopologicalSpace α]: Regular (∅ : Set α) :=
+by
+  simp
+
+theorem regular_univ (α : Type _) [TopologicalSpace α]: Regular (Set.univ : Set α) :=
+by
+  simp
+
+theorem regular_nbhd [T2Space α] {u v : α} (u_ne_v : u ≠ v):
+  ∃ (U V : Set α), Regular U ∧ Regular V ∧ Disjoint U V ∧ u ∈ U ∧ v ∈ V :=
+by
+  let ⟨U', V', U'_open, V'_open, u_in_U', v_in_V', disj⟩ := t2_separation u_ne_v
+  let U := InteriorClosure U'
+  let V := InteriorClosure V'
+  use U, V
+  repeat' apply And.intro
+  · apply interiorClosure_regular
+  · apply interiorClosure_regular
+  · apply disjoint_interiorClosure_left (interiorClosure_regular V').isOpen
+    apply disjoint_interiorClosure_right U'_open
+    exact disj
+  · exact (interiorClosure_subset U'_open) u_in_U'
+  · exact (interiorClosure_subset V'_open) v_in_V'
+
+theorem regular_inter {U V : Set α} : Regular U → Regular V → Regular (U ∩ V) :=
+by
+  intro U_reg V_reg
+  simp
+  have UV_open : IsOpen (U ∩ V) := IsOpen.inter U_reg.isOpen V_reg.isOpen
+
+  apply Set.eq_of_subset_of_subset
+  · simp
+    constructor
+    · nth_rw 2 [<-U_reg]
+      apply interiorClosure_mono
+      simp
+    · nth_rw 2 [<-V_reg]
+      apply interiorClosure_mono
+      simp
+  · apply interiorClosure_subset
+    exact UV_open
+
+theorem regular_sInter {S : Set (Set α)} (S_finite : Set.Finite S) (all_reg : ∀ U ∈ S, Regular U):
+  Regular (⋂₀ S) :=
+Set.Finite.induction_on' S_finite (by simp) (by
+  intro U S' U_in_S _ _ IH
+  rw [Set.sInter_insert]
+  apply regular_inter
+  · exact all_reg _ U_in_S
+  · exact IH
+)
+
+theorem interiorClosure_smulImage {G : Type _} [Group G] [MulAction G α] [ContinuousConstSMul G α]
+  (g : G) (U : Set α) :
+  InteriorClosure (g •'' U) = g •'' InteriorClosure U :=
+by
+  simp
+  rw [<-smulImage_interior]
+  rw [<-smulImage_closure]
+
+theorem smulImage_regular {G : Type _} [Group G] [MulAction G α] [ContinuousConstSMul G α]
+  (g : G) (U : Set α) :
+  Regular U ↔ Regular (g •'' U) :=
+by
+  suffices ∀ V : Set α, ∀ h : G, Regular V → Regular (h •'' V) by
+    constructor
+    apply this
+    have U_eq : g⁻¹ •'' (g •'' U) = U := by simp
+    nth_rw 2 [<-U_eq]
+    apply this
+  intro U g U_reg
+  unfold Regular
+  rw [interiorClosure_smulImage]
+  rw [U_reg]
+
+end Rubin

Rubin/LocallyDense.lean

@@ -0,0 +1,307 @@
+import Mathlib.GroupTheory.Subgroup.Basic
+import Mathlib.GroupTheory.GroupAction.Basic
+import Mathlib.Topology.Basic
+import Mathlib.Topology.Algebra.ConstMulAction
+
+import Rubin.RigidStabilizer
+import Rubin.InteriorClosure
+
+namespace Rubin
+
+open Topology
+
+/--
+A group action is said to be "locally dense" if for any open set `U` and `p ∈ U`,
+the closure of the orbit of `p` under the `RigidStabilizer G U` contains a neighborhood of `p`.
+
+The definition provided here is an equivalent one, that does not require using filters.
+See [`LocallyDense.from_rigidStabilizer_in_nhds`] and [`LocallyDense.rigidStabilizer_in_nhds`]
+to translate from/to the original definition.
+
+A weaker relationship, [`LocallyMoving`], is used whenever possible.
+The main difference between the two is that `LocallyMoving` does not allow us to find a group member
+`g ∈ G` such that `g • p ≠ p` — it only allows us to know that `∃ g ∈ RigidStabilizer G U, g ≠ 1`.
+--/
+class LocallyDense (G α : Type _) [Group G] [TopologicalSpace α] [MulAction G α] :=
+  isLocallyDense:
+    ∀ U : Set α,
+    IsOpen U →
+    ∀ p ∈ U,
+    p ∈ interior (closure (MulAction.orbit (RigidStabilizer G U) p))
+#align is_locally_dense Rubin.LocallyDense
+
+theorem LocallyDense.from_rigidStabilizer_in_nhds (G α : Type _) [Group G] [TopologicalSpace α] [MulAction G α] :
+  (∀ U : Set α, IsOpen U → ∀ p ∈ U, closure (MulAction.orbit G•[U] p) ∈ 𝓝 p) →
+  LocallyDense G α :=
+by
+  intro hyp
+  constructor
+  intro U U_open p p_in_U
+
+  have closure_in_nhds := hyp U U_open p p_in_U
+  rw [mem_nhds_iff] at closure_in_nhds
+
+  rw [mem_interior]
+  exact closure_in_nhds
+
+theorem LocallyDense.rigidStabilizer_in_nhds (G α : Type _) [Group G] [TopologicalSpace α]
+  [MulAction G α] [LocallyDense G α]
+  {U : Set α} (U_open : IsOpen U) {p : α} (p_in_U : p ∈ U)
+:
+  closure (MulAction.orbit G•[U] p) ∈ 𝓝 p :=
+by
+  rw [mem_nhds_iff]
+  rw [<-mem_interior]
+  apply LocallyDense.isLocallyDense <;> assumption
+
+lemma LocallyDense.elem_from_nonEmpty {G α : Type _} [Group G] [TopologicalSpace α] [MulAction G α] [LocallyDense G α]:
+  ∀ {U : Set α},
+  IsOpen U →
+  Set.Nonempty U →
+  ∃ p ∈ U, p ∈ interior (closure (MulAction.orbit G•[U] p)) :=
+by
+  intros U U_open H_ne
+  exact ⟨H_ne.some, H_ne.some_mem, LocallyDense.isLocallyDense U U_open H_ne.some H_ne.some_mem⟩
+
+/--
+This is a stronger statement than `LocallyMoving.get_nontrivial_rist_elem`,
+as here we are able to prove that the nontrivial element does move `p`.
+
+The condition that `Filer.NeBot (𝓝[≠] p)` is automatically satisfied by the `HasNoIsolatedPoints` class.
+--/
+theorem get_moving_elem_in_rigidStabilizer (G : Type _) {α : Type _}
+  [Group G] [TopologicalSpace α] [MulAction G α] [LocallyDense G α]
+  [T1Space α] {p : α} [Filter.NeBot (𝓝[≠] p)]
+  {U : Set α} (U_open : IsOpen U) (p_in_U : p ∈ U) :
+  ∃ g : G, g ∈ G•[U] ∧ g • p ≠ p :=
+by
+  by_contra g_not_exist
+  rw [<-Classical.not_forall_not] at g_not_exist
+  simp at g_not_exist
+
+  have orbit_singleton : MulAction.orbit (RigidStabilizer G U) p = {p} := by
+    ext x
+    rw [MulAction.mem_orbit_iff]
+    rw [Set.mem_singleton_iff]
+    simp
+    constructor
+    · intro ⟨g, g_in_rist, g_eq_p⟩
+      rw [g_not_exist g g_in_rist] at g_eq_p
+      exact g_eq_p.symm
+    · intro x_eq_p
+      use 1
+      rw [x_eq_p, one_smul]
+      exact ⟨Subgroup.one_mem _, rfl⟩
+
+  have regular_orbit_empty : interior (closure (MulAction.orbit (RigidStabilizer G U) p)) = ∅ := by
+    rw [orbit_singleton]
+    rw [closure_singleton]
+    rw [interior_singleton]
+
+  have p_in_regular_orbit := LocallyDense.isLocallyDense (G := G) U U_open p p_in_U
+  rw [regular_orbit_empty] at p_in_regular_orbit
+  exact p_in_regular_orbit
+
+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
+
+theorem LocallyMoving.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 ∈ 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 _)
+
+theorem LocallyMoving.nontrivial_elem (G α : Type _) [Group G] [TopologicalSpace α]
+  [MulAction G α] [LocallyMoving G α] [Nonempty α] :
+  ∃ g: G, g ≠ 1 :=
+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 α]
+  [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 α]
+variable [MulAction G α]
+variable [ContinuousConstSMul G α]
+variable [FaithfulSMul G α]
+
+instance dense_locally_moving [T2Space α]
+  [H_nip : HasNoIsolatedPoints α]
+  [H_ld : LocallyDense G α] :
+  LocallyMoving G α
+where
+  locally_moving := by
+    intros U U_open H_nonempty
+    by_contra h_rs
+    have ⟨elem, ⟨_, some_in_orbit⟩⟩ := H_ld.elem_from_nonEmpty U_open H_nonempty
+    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 x_moved
+  let U := (g⁻¹ •'' V) ∩ W
+  use U
+  constructor
+  exact IsOpen.inter (smulImage_isOpen g⁻¹ 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
+      simp
+
+      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
+
+/--
+## Proposition 3.1:
+
+If a group action is faithful, continuous and "locally moving",
+then `U ⊆ V` if and only if `G•[U] ≤ G•[V]` when `U` and `V` are regular.
+--/
+theorem rigidStabilizer_subset_iff (G : Type _) {α : Type _} [Group G] [TopologicalSpace α]
+  [MulAction G α] [ContinuousConstSMul G α] [FaithfulSMul G α]
+  [h_lm : LocallyMoving G α]
+  {U V : Set α} (U_reg : Regular U) (V_reg : Regular V):
+  U ⊆ V ↔ G•[U] ≤ G•[V] :=
+by
+  constructor
+  exact rigidStabilizer_mono
+  intro rist_ss
+
+  by_contra U_not_ss_V
+
+  let W := U \ closure V
+  have W_nonempty : Set.Nonempty W := by
+    by_contra W_empty
+    apply U_not_ss_V
+    apply subset_from_diff_closure_eq_empty
+    · assumption
+    · exact U_reg.isOpen
+    · rw [Set.not_nonempty_iff_eq_empty] at W_empty
+      exact W_empty
+  have W_ss_U : W ⊆ U := by
+    simp
+    exact Set.diff_subset _ _
+  have W_open : IsOpen W := by
+    unfold_let
+    rw [Set.diff_eq_compl_inter]
+    apply IsOpen.inter
+    simp
+    exact U_reg.isOpen
+
+  have ⟨f, f_in_ristW, f_ne_one⟩ := h_lm.get_nontrivial_rist_elem W_open W_nonempty
+
+  have f_in_ristU : f ∈ RigidStabilizer G U := by
+    exact rigidStabilizer_mono W_ss_U f_in_ristW
+
+  have f_notin_ristV : f ∉ RigidStabilizer G V := by
+    apply rigidStabilizer_compl f_ne_one
+    apply rigidStabilizer_mono _ f_in_ristW
+    calc
+      W = U ∩ (closure V)ᶜ := by unfold_let; rw [Set.diff_eq_compl_inter, Set.inter_comm]
+      _ ⊆ (closure V)ᶜ := Set.inter_subset_right _ _
+      _ ⊆ Vᶜ := by
+        rw [Set.compl_subset_compl]
+        exact subset_closure
+
+  exact f_notin_ristV (rist_ss f_in_ristU)
+
+/--
+A corollary of the previous theorem is that the rigid stabilizers of two regular sets `U` and `V`
+are equal if and only if `U = V`.
+--/
+theorem rigidStabilizer_eq_iff (G : Type _) [Group G] {α : Type _} [TopologicalSpace α]
+  [MulAction G α] [ContinuousConstSMul G α] [FaithfulSMul G α] [LocallyMoving G α]
+  {U V : Set α} (U_reg : Regular U) (V_reg : Regular V):
+  G•[U] = G•[V] ↔ U = V :=
+by
+  constructor
+  · intro rist_eq
+    apply le_antisymm <;> simp only [Set.le_eq_subset]
+    all_goals {
+      rw [rigidStabilizer_subset_iff G] <;> try assumption
+      rewrite [rist_eq]
+      rfl
+    }
+  · intro H_eq
+    rw [H_eq]
+
+theorem rigidStabilizer_empty_iff (G : Type _) [Group G] {α : Type _} [TopologicalSpace α]
+  [MulAction G α] [ContinuousConstSMul G α] [FaithfulSMul G α] [LocallyMoving G α]
+  {U : Set α} (U_reg : Regular U) :
+  G•[U] = ⊥ ↔ U = ∅ :=
+by
+  rw [<-rigidStabilizer_empty (α := α) (G := G)]
+  exact rigidStabilizer_eq_iff G U_reg (regular_empty α)
+
+end Rubin

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
@@ -71,4 +65,37 @@ by
     rw [<-mul_smul, mul_right_inv, one_smul]
   }
 
+lemma exists_smul_ne {G : Type _} (α : Type _) [Group G] [MulAction G α] [h_f : FaithfulSMul G α]
+  {f g : G} (f_ne_g : f ≠ g) : ∃ (x : α), f • x ≠ g • x :=
+by
+  by_contra h
+  rw [Classical.not_exists_not] at h
+  apply f_ne_g
+  apply h_f.eq_of_smul_eq_smul
+  exact h
+
+@[simp]
+theorem orbit_bot {G : Type _} [Group G] {H : Subgroup G} (H_eq_bot : H = ⊥):
+  ∀ (g : G), MulAction.orbit H g = {g} :=
+by
+  intro g
+  ext x
+  rw [MulAction.mem_orbit_iff]
+  simp
+  rw [H_eq_bot]
+  simp
+  constructor <;> tauto
+
+@[simp]
+theorem orbit_bot₂ {G : Type _} [Group G] {α : Type _} [MulAction G α] (H : Subgroup G) (H_eq_bot : H = ⊥):
+  ∀ (x : α), MulAction.orbit H x = {x} :=
+by
+  intro g
+  ext x
+  rw [MulAction.mem_orbit_iff]
+  simp
+  rw [H_eq_bot]
+  simp
+  constructor <;> tauto
+
 end Rubin

Rubin/Period.lean

@@ -19,13 +19,15 @@ 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;
+  · by_contra h'
-    rcases Nat.sInf_eq_zero.1 period_zero with ⟨cont, h_1⟩ | h; linarith;
+    have period_zero : Rubin.Period.period p g = 0 := by linarith
-    exact Set.eq_empty_iff_forall_not_mem.mp h ↑m ⟨m_pos, gmp_eq_p⟩
+    rcases Nat.sInf_eq_zero.1 period_zero with ⟨cont, _⟩ | 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)
+theorem notfix_le_period {p : α} {g : G} {n : ℕ}
     (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
@@ -34,10 +36,10 @@ theorem notfix_le_period {p : α} {g : G} {n : ℕ} (n_pos : n > 0)
       (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)
+theorem notfix_le_period' {p : α} {g : G} {n : ℕ}
     (period_pos : 0 < Rubin.Period.period p g)
     (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) =>
+  Rubin.Period.notfix_le_period 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'
 
@@ -65,7 +67,7 @@ theorem moves_within_period' {z : ℤ} (g : G) (x : α) :
   0 < z → z < period x g → g^z • x ≠ x :=
 by
   intro n_pos n_lt_period
-  rw [<-Int.ofNat_natAbs_eq_of_nonneg _ (Int.le_of_lt n_pos)]
+  rw [<-Int.natAbs_of_nonneg (Int.le_of_lt n_pos)]
   rw [zpow_ofNat]
   apply moves_within_period
   · rw [<-Int.natAbs_zero]
@@ -86,7 +88,7 @@ theorem periods_lemmas {U : Set α} (U_nonempty : Set.Nonempty U) {H : Subgroup
     (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 :=
+        ∃ (m : ℕ), 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
@@ -135,7 +137,7 @@ theorem zero_lt_period_le_Sup_periods {U : Set α} (U_nonempty : U.Nonempty)
         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⟩
+    ⟨_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

Rubin/RegularSupport.lean

@@ -6,90 +6,12 @@ import Mathlib.Topology.Separation
 
 import Rubin.Tactic
 import Rubin.Support
-import Rubin.Topological
+import Rubin.Topology
+import Rubin.InteriorClosure
+import Rubin.RigidStabilizer
 
 namespace Rubin
 
-section InteriorClosure
-
-variable {α : Type _}
-variable [TopologicalSpace α]
-
--- Defines a kind of "regularization" transformation made to sets,
--- by calling `closure` followed by `interior` on it.
---
--- A set is then said to be regular if the InteriorClosure does not modify it.
-def InteriorClosure (U : Set α) : Set α :=
-  interior (closure U)
-#align interior_closure Rubin.InteriorClosure
-
-@[simp]
-theorem InteriorClosure.def (U : Set α) : InteriorClosure U = interior (closure U) :=
-  by simp [InteriorClosure]
-
-@[simp]
-theorem InteriorClosure.fdef : InteriorClosure = (interior ∘ (closure (α := α))) := by ext; simp
-
-def Regular (U : Set α) : Prop :=
-  InteriorClosure U = U
-
-@[simp]
-theorem Regular.def (U : Set α) : Regular U ↔ interior (closure U) = U :=
-  by simp [Regular]
-#align set.is_regular_def Rubin.Regular.def
-
-theorem interiorClosure_open (U : Set α) : IsOpen (InteriorClosure U) := by simp
-#align is_open_interior_closure Rubin.interiorClosure_open
-
-theorem interiorClosure_subset {U : Set α} :
-  IsOpen U → U ⊆ InteriorClosure U :=
-by
-  intro h
-  apply subset_trans
-  exact subset_interior_iff_isOpen.mpr h
-  apply interior_mono
-  exact subset_closure
-#align is_open.interior_closure_subset Rubin.interiorClosure_subset
-
-theorem interiorClosure_regular (U : Set α) : Regular (InteriorClosure U) :=
-by
-  apply Set.eq_of_subset_of_subset <;> unfold InteriorClosure
-  {
-    apply interior_mono
-    nth_rw 2 [<-closure_closure (s := U)]
-    apply closure_mono
-    exact interior_subset
-  }
-  {
-    nth_rw 1 [<-interior_interior]
-    apply interior_mono
-    exact subset_closure
-  }
-#align regular_interior_closure Rubin.interiorClosure_regular
-
-theorem interiorClosure_mono (U V : Set α) :
-  U ⊆ V → InteriorClosure U ⊆ InteriorClosure V
-:= interior_mono ∘ closure_mono
-#align interior_closure_mono Rubin.interiorClosure_mono
-
-theorem monotone_interior_closure : Monotone (InteriorClosure (α := α))
-:= fun a b =>
-  interiorClosure_mono a b
-
-theorem regular_open (U : Set α) : Regular U → IsOpen U :=
-by
-  intro h_reg
-  rw [<-h_reg]
-  simp
-
-theorem regular_interior (U : Set α) : Regular U → interior U = U :=
-by
-  intro h_reg
-  rw [<-h_reg]
-  simp
-
-end InteriorClosure
-
 section RegularSupport_def
 
 variable {G : Type _}
@@ -125,13 +47,14 @@ section RegularSupport_continuous
 variable {G α : Type _}
 variable [Group G]
 variable [TopologicalSpace α]
-variable [ContinuousMulAction G α]
+variable [MulAction G α]
+variable [ContinuousConstSMul G α]
 
 theorem support_subset_regularSupport [T2Space α] {g : G} :
   Support α g ⊆ RegularSupport α g :=
 by
   apply interiorClosure_subset
-  apply support_open (α := α) (g := g)
+  apply support_isOpen (α := α) (g := g)
 #align support_in_regular_support Rubin.support_subset_regularSupport
 
 theorem regularSupport_subset {g : G} {U : Set α} :
@@ -142,6 +65,13 @@ by
   apply interiorClosure_mono
   exact h
 
+theorem regularSupport_subset_closure_support {g : G} :
+  RegularSupport α g ⊆ closure (Support α g) :=
+by
+  unfold RegularSupport
+  simp
+  exact interior_subset
+
 theorem regularSupport_subset_of_rigidStabilizer {g : G} {U : Set α} (U_reg : Regular U) :
   g ∈ RigidStabilizer G U → RegularSupport α g ⊆ U :=
 by
@@ -163,6 +93,38 @@ by
     exact rs_subset
 #align mem_regular_support Rubin.regularSupport_subset_of_rigidStabilizer
 
+theorem regularSupport_smulImage {f g : G} :
+  f •'' (RegularSupport α g) = RegularSupport α (f * g * f⁻¹) :=
+by
+  unfold RegularSupport
+  rw [support_conjugate]
+  rw [interiorClosure_smulImage]
+
+theorem rigidStabilizer_iInter_regularSupport (F : Set G) :
+  G•[⋂ (g ∈ F), RegularSupport α g] = (⨅ (g ∈ F), G•[RegularSupport α g]) :=
+by
+  let S := { RegularSupport α g | g ∈ F }
+  have h₁ : ⋂ (g ∈ F), RegularSupport α g = ⋂₀ S := by
+    ext x
+    simp
+  have h₂ : ⨅ (g ∈ F), G•[RegularSupport α g] = ⨅ (s ∈ S), G•[s] := by
+    ext x
+    rw [<-sInf_image]
+    simp
+    rw [Subgroup.mem_iInf]
+    simp only [Subgroup.mem_iInf, and_imp, forall_apply_eq_imp_iff₂]
+
+  rw [h₁, h₂]
+  rw [rigidStabilizer_sInter]
+
+theorem rigidStabilizer_iInter_regularSupport' (F : Finset G) :
+  G•[⋂ (g ∈ F), RegularSupport α g] = (⨅ (g ∈ F), G•[RegularSupport α g]) :=
+by
+  have h₁ : G•[⋂ (g ∈ F), RegularSupport α g] = G•[⋂ (g ∈ (F : Set G)), RegularSupport α g] := by simp
+  have h₂ : ⨅ (g ∈ F), G•[RegularSupport α g] = ⨅ (g ∈ (F : Set G)), G•[RegularSupport α g] := by simp
+
+  rw [h₁, h₂, rigidStabilizer_iInter_regularSupport]
+
 end RegularSupport_continuous
 
 end Rubin

Rubin/RegularSupportBasis.lean

@@ -0,0 +1,291 @@
+/-
+This files defines `RegularSupportBasis`, which is a basis of the topological space α,
+made up of finite intersections of `RegularSupport α g` for `g : G`.
+-/
+
+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
+
+namespace Rubin
+
+/--
+Maps a "seed" of homeorphisms in α to the intersection of their regular support in α.
+
+Note that the condition that the resulting set is non-empty is introduced later in `RegularSupportBasis₀`
+--/
+def RegularSupport.FiniteInter {G : Type _} [Group G] (α : Type _) [TopologicalSpace α] [MulAction G α] (S : Finset G): Set α :=
+  ⋂ (g ∈ S), RegularSupport α g
+
+def RegularSupportBasis (G α : Type _) [Group G] [TopologicalSpace α] [MulAction G α] : Set (Set α) :=
+  { S : Set α | S.Nonempty ∧ ∃ (seed : Finset G), S = RegularSupport.FiniteInter α seed }
+
+variable {G : Type _}
+variable {α : Type _}
+variable [Group G]
+variable [TopologicalSpace α]
+variable [MulAction G α]
+
+theorem RegularSupport.FiniteInter_sInter (S : Finset G) :
+  RegularSupport.FiniteInter α S = ⋂₀ ((fun (g : G) => RegularSupport α g) '' S) :=
+by
+  rw [Set.sInter_image]
+  rfl
+
+theorem RegularSupportBasis.mem_iff (S : Set α) :
+  S ∈ RegularSupportBasis G α ↔ S.Nonempty ∧ ∃ (seed : Finset G), S = RegularSupport.FiniteInter α seed :=
+by
+  simp only [RegularSupportBasis, Set.mem_setOf_eq]
+
+@[simp]
+
+theorem RegularSupport.FiniteInter_regular (F : Finset G) :
+  Regular (RegularSupport.FiniteInter α F) :=
+by
+  rw [RegularSupport.FiniteInter_sInter]
+  apply regular_sInter
+  · have set_decidable : DecidableEq (Set α) := Classical.typeDecidableEq (Set α)
+    let fin : Finset (Set α) := F.image ((fun g => RegularSupport α g))
+
+    apply Set.Finite.ofFinset fin
+    simp
+  · intro S S_in_set
+    simp at S_in_set
+    let ⟨g, ⟨_, Heq⟩⟩ := S_in_set
+    rw [<-Heq]
+    exact regularSupport_regular α g
+
+@[simp]
+theorem RegularSupportBasis.regular {S : Set α} (S_mem_basis : S ∈ RegularSupportBasis G α) : Regular S := by
+  let ⟨_, ⟨seed, S_eq_inter⟩⟩ := (RegularSupportBasis.mem_iff S).mp S_mem_basis
+  rw [S_eq_inter]
+  apply RegularSupport.FiniteInter_regular
+
+variable [ContinuousConstSMul G α] [DecidableEq G]
+
+lemma RegularSupport.FiniteInter_conj (seed : Finset G) (f : G):
+  RegularSupport.FiniteInter α (Finset.image (fun g => f * g * f⁻¹) seed) = f •'' RegularSupport.FiniteInter α seed :=
+by
+  unfold RegularSupport.FiniteInter
+  simp
+  conv => {
+    rhs
+    ext; lhs; ext x; ext; lhs
+    ext
+    rw [regularSupport_smulImage]
+  }
+
+/--
+A group element `f` acts on sets of `RegularSupportBasis G α`,
+by mapping each element `g` of `S.seed` to `f * g * f⁻¹`
+--/
+noncomputable instance RegularSupportBasis.instSmul : SMul G (RegularSupportBasis G α) where
+  smul := fun f S =>
+    let new_seed := (Finset.image (fun g => f * g * f⁻¹) S.prop.right.choose)
+    ⟨
+      RegularSupport.FiniteInter α new_seed,
+      by
+        rw [RegularSupportBasis.mem_iff]
+        nth_rw 1 [RegularSupport.FiniteInter_conj, smulImage_nonempty]
+        rw [<-S.prop.right.choose_spec]
+
+        constructor
+        · exact S.prop.left
+        · use new_seed
+    ⟩
+
+theorem RegularSupportBasis.smul_eq' (f : G) (S : RegularSupportBasis G α) :
+  (f • S).val
+    = RegularSupport.FiniteInter α (Finset.image (fun g => f * g * f⁻¹) S.prop.right.choose) := rfl
+
+theorem RegularSupportBasis.smul_eq (f : G) (S : RegularSupportBasis G α) :
+  (f • S).val = f •'' S.val :=
+by
+  rw [RegularSupportBasis.smul_eq']
+  rw [RegularSupport.FiniteInter_conj]
+  rw [<-S.prop.right.choose_spec]
+
+theorem RegularSupportBasis.smulImage_in_basis {U : Set α} (U_in_basis : U ∈ RegularSupportBasis G α)
+  (f : G) : f •'' U ∈ RegularSupportBasis G α :=
+by
+  have eq := smul_eq f ⟨U, U_in_basis⟩
+  simp only at eq
+  rw [<-eq]
+  exact Subtype.coe_prop _
+
+def RegularSupportBasis.fromSingleton [T2Space α] [FaithfulSMul G α] (g : G) (g_ne_one : g ≠ 1) : { S : Set α // S ∈ RegularSupportBasis G α } :=
+  let seed : Finset G := {g}
+  ⟨
+    RegularSupport.FiniteInter α seed,
+    by
+      rw [RegularSupportBasis.mem_iff]
+      constructor
+      swap
+      use seed
+
+      rw [Set.nonempty_iff_ne_empty]
+      intro rsupp_empty
+      apply g_ne_one
+      apply FaithfulSMul.eq_of_smul_eq_smul (α := α)
+      intro x
+      simp
+      rw [<-not_mem_support]
+      apply Set.not_mem_subset
+      · apply support_subset_regularSupport
+      · simp [RegularSupport.FiniteInter] at rsupp_empty
+        rw [rsupp_empty]
+        exact Set.not_mem_empty x
+  ⟩
+
+theorem RegularSupportBasis.fromSingleton_val [T2Space α] [FaithfulSMul G α] (g : G) (g_ne_one : g ≠ 1) :
+  (fromSingleton g g_ne_one).val = RegularSupport α g := by simp [fromSingleton, RegularSupport.FiniteInter]
+
+-- Note: we could potentially implement MulActionHom
+noncomputable instance RegularSupportBasis.instMulAction : MulAction G (RegularSupportBasis G α) where
+  one_smul := by
+    intro S
+    apply Subtype.eq
+    rw [RegularSupportBasis.smul_eq]
+    rw [one_smulImage]
+  mul_smul := by
+    intro S f g
+    apply Subtype.eq
+    repeat rw [RegularSupportBasis.smul_eq]
+    rw [smulImage_mul]
+
+theorem RegularSupportBasis.smul_mono {S T : RegularSupportBasis G α} (f : G) (S_le_T : S.val ⊆ T.val) :
+  (f • S).val ⊆ (f • T).val :=
+by
+  repeat rw [RegularSupportBasis.smul_eq]
+  apply smulImage_mono
+  assumption
+
+section Basis
+open Topology
+
+variable (G α : Type _)
+variable [Group G]
+variable [TopologicalSpace α] [T2Space α] [LocallyCompactSpace α] [HasNoIsolatedPoints α]
+variable [MulAction G α] [LocallyDense G α] [ContinuousConstSMul G α]
+
+-- TODO: clean this lemma to not mention W anymore?
+lemma proposition_3_2_subset
+  {U : Set α} (U_open : IsOpen U) {p : α} (p_in_U : p ∈ U) :
+  ∃ (W : Set α), W ∈ 𝓝 p ∧ closure W ⊆ U ∧
+  ∃ (g : G), g ∈ RigidStabilizer G W ∧ p ∈ RegularSupport α g ∧ RegularSupport α g ⊆ closure W :=
+by
+  have U_in_nhds : U ∈ 𝓝 p := by
+    rw [mem_nhds_iff]
+    use U
+
+  let ⟨W', W'_in_nhds, W'_ss_U, W'_compact⟩ := local_compact_nhds U_in_nhds
+
+  -- This feels like black magic, but okay
+  let ⟨W, _W_compact, W_closed, W'_ss_int_W, W_ss_U⟩ := exists_compact_closed_between W'_compact U_open W'_ss_U
+  have W_cl_eq_W : closure W = W := IsClosed.closure_eq W_closed
+
+  have W_in_nhds : W ∈ 𝓝 p := by
+    rw [mem_nhds_iff]
+    use interior W
+    repeat' apply And.intro
+    · exact interior_subset
+    · simp
+    · exact W'_ss_int_W (mem_of_mem_nhds W'_in_nhds)
+
+  use W
+
+  repeat' apply And.intro
+  exact W_in_nhds
+  {
+    rw [W_cl_eq_W]
+    exact W_ss_U
+  }
+
+  have p_in_int_W : p ∈ interior W := W'_ss_int_W (mem_of_mem_nhds W'_in_nhds)
+
+  let ⟨g, g_in_rist, g_moves_p⟩ := get_moving_elem_in_rigidStabilizer G isOpen_interior p_in_int_W
+
+  use g
+  repeat' apply And.intro
+  · apply rigidStabilizer_mono interior_subset
+    simp
+    exact g_in_rist
+  · rw [<-mem_support] at g_moves_p
+    apply support_subset_regularSupport
+    exact g_moves_p
+  · rw [rigidStabilizer_support] at g_in_rist
+    apply subset_trans
+    exact regularSupport_subset_closure_support
+    apply closure_mono
+    apply subset_trans
+    exact g_in_rist
+    exact interior_subset
+
+/--
+## Proposition 3.2 : RegularSupportBasis is a topological basis of `α`
+-/
+theorem RegularSupportBasis.isBasis :
+  TopologicalSpace.IsTopologicalBasis (RegularSupportBasis G α) :=
+by
+  apply TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds
+  {
+    intro U U_in_poset
+    exact (RegularSupportBasis.regular U_in_poset).isOpen
+  }
+  intro p U p_in_U U_open
+
+  let ⟨W, _, clW_ss_U, ⟨g, _, p_in_rsupp, rsupp_ss_clW⟩⟩ := proposition_3_2_subset G α U_open p_in_U
+  use RegularSupport α g
+  repeat' apply And.intro
+  · exact ⟨p, p_in_rsupp⟩
+  · use {g}
+    simp [RegularSupport.FiniteInter]
+  · assumption
+  · apply subset_trans
+    exact rsupp_ss_clW
+    exact clW_ss_U
+
+theorem RegularSupportBasis.closed_inter (b1 b2 : Set α)
+  (b1_in_basis : b1 ∈ RegularSupportBasis G α)
+  (b2_in_basis : b2 ∈ RegularSupportBasis G α)
+  (inter_nonempty : Set.Nonempty (b1 ∩ b2)) :
+  (b1 ∩ b2) ∈ RegularSupportBasis G α :=
+by
+  unfold RegularSupportBasis
+  simp
+  constructor
+  assumption
+
+  let ⟨_, ⟨s1, b1_eq⟩⟩ := b1_in_basis
+  let ⟨_, ⟨s2, b2_eq⟩⟩ := b2_in_basis
+
+  have dec_eq : DecidableEq G := Classical.typeDecidableEq G
+  use s1 ∪ s2
+  rw [RegularSupport.FiniteInter_sInter]
+  rw [Finset.coe_union, Set.image_union, Set.sInter_union]
+  repeat rw [<-RegularSupport.FiniteInter_sInter]
+  rw [b2_eq, b1_eq]
+
+theorem RegularSupportBasis.empty_not_mem :
+  ∅ ∉ RegularSupportBasis G α :=
+by
+  intro empty_mem
+  rw [RegularSupportBasis.mem_iff] at empty_mem
+  exact Set.not_nonempty_empty empty_mem.left
+
+theorem RegularSupportBasis.univ_mem [Nonempty α]:
+  Set.univ ∈ RegularSupportBasis G α :=
+by
+  rw [RegularSupportBasis.mem_iff]
+  constructor
+  exact Set.univ_nonempty
+  use ∅
+  simp [RegularSupport.FiniteInter]
+
+end Basis
+end Rubin

Rubin/RigidStabilizer.lean

@@ -1,5 +1,6 @@
 import Mathlib.Data.Finset.Basic
 import Mathlib.GroupTheory.GroupAction.Basic
+import Mathlib.GroupTheory.GroupAction.FixingSubgroup
 
 import Rubin.Support
 import Rubin.MulActionExt
@@ -11,7 +12,15 @@ def rigidStabilizer' (G : Type _) [Group G] [MulAction G α] (U : Set α) : Set
   {g : G | ∀ x : α, g • x = x ∨ x ∈ U}
 #align rigid_stabilizer' Rubin.rigidStabilizer'
 
--- A subgroup of G for which `Support α g ⊆ U`, or in other words, all elements of `G` that don't move points outside of `U`.
+-- TODO: rename to something else? Also check the literature on what this is called
+/--
+A "rigid stabilizer" is a subgroup of `G` associated with a set `U` for which `Support α g ⊆ U` is true for all of its elements.
+
+In other words, a rigid stabilizer for a set `U` contains all elements of `G` that don't move points outside of `U`.
+
+The notation for this subgroup is `G•[U]`.
+You might sometimes find an expression written as `↑G•[U]` when `G•[U]` is used as a set.
+--/
 def RigidStabilizer (G : Type _) [Group G] [MulAction G α] (U : Set α) : Subgroup G
     where
   carrier := {g : G | ∀ (x) (_ : x ∉ U), g • x = x}
@@ -20,10 +29,20 @@ def RigidStabilizer (G : Type _) [Group G] [MulAction G α] (U : Set α) : Subgr
   one_mem' x _ := one_smul G x
 #align rigid_stabilizer Rubin.RigidStabilizer
 
+notation:max G "•[" U "]" => RigidStabilizer G U
+
 variable {G α: Type _}
 variable [Group G]
 variable [MulAction G α]
 
+theorem rigidStabilizer_eq_fixingSubgroup_compl (U : Set α) :
+  G•[U] = fixingSubgroup G Uᶜ :=
+by
+  ext g
+  rw [mem_fixingSubgroup_iff, <-Subgroup.mem_carrier]
+  unfold RigidStabilizer
+  simp
+
 theorem rigidStabilizer_support {g : G} {U : Set α} :
   g ∈ RigidStabilizer G U ↔ Support α g ⊆ U :=
 ⟨
@@ -49,16 +68,16 @@ by
 
 theorem monotone_rigidStabilizer : Monotone (RigidStabilizer (α := α) G) := fun _ _ => rigidStabilizer_mono
 
-theorem rigidStabilizer_to_subgroup_closure {g : G} {U : Set α} :
+theorem rigidStabilizer_compl [FaithfulSMul G α] {U : Set α} {f : G} (f_ne_one : f ≠ 1) :
-  g ∈ RigidStabilizer G U → g ∈ Subgroup.closure { g : G | Support α g ⊆ U } :=
+  f ∈ G•[Uᶜ] → f ∉ G•[U] :=
 by
-  rw [rigidStabilizer_support]
+  intro f_in_rist_compl
-  intro h
+  intro f_in_rist
-  rw [Subgroup.mem_closure]
+  rw [rigidStabilizer_support] at f_in_rist_compl
-  intro V orbit_subset_V
+  rw [rigidStabilizer_support] at f_in_rist
-  apply orbit_subset_V
+  rw [Set.subset_compl_iff_disjoint_left] at f_in_rist_compl
-  simp
+  have supp_empty : Support α f = ∅ := empty_of_subset_disjoint f_in_rist_compl.symm f_in_rist
-  exact h
+  exact f_ne_one ((support_empty_iff f).mp supp_empty)
 
 theorem commute_if_rigidStabilizer_and_disjoint {g h : G} {U : Set α} [FaithfulSMul G α] :
   g ∈ RigidStabilizer G U → Disjoint U (Support α h) → Commute g h :=
@@ -95,6 +114,7 @@ by
       symm at gx_notin_support
       rw [fixes_inv] at gx_notin_support
       rw [<-gx_notin_support]
+      symm
       group_action
       rw [not_mem_support.mp x_notin_support]
     }
@@ -109,8 +129,9 @@ by
       have hx_notin_support := disjoint_not_mem U_disj hx_in_U?
       rw [<-support_inv] at hx_notin_support
       rw [not_mem_support] at hx_notin_support
+      symm at hx_notin_support
       group_action at hx_notin_support
-      rw [<-hx_notin_support]
+      rw [hx_notin_support]
       exact x_fixed
     }
     {
@@ -118,4 +139,99 @@ by
     }
   }
 
+theorem rigidStabilizer_inter (U V : Set α) :
+  G•[U ∩ V] = G•[U] ⊓ G•[V] :=
+by
+  ext x
+  simp
+  repeat rw [rigidStabilizer_support]
+  rw [Set.subset_inter_iff]
+
+@[simp]
+theorem rigidStabilizer_empty (G α: Type _) [Group G] [MulAction G α] [FaithfulSMul G α]:
+  G•[(∅ : Set α)] = ⊥ :=
+by
+  rw [Subgroup.eq_bot_iff_forall]
+  intro f f_in_rist
+  rw [<-Subgroup.mem_carrier] at f_in_rist
+  apply eq_of_smul_eq_smul (α := α)
+
+  intro x
+  rw [f_in_rist x (Set.not_mem_empty x)]
+  simp
+
+@[simp]
+theorem rigidStabilizer_univ (G α: Type _) [Group G] [MulAction G α]:
+  G•[(Set.univ : Set α)] = ⊤ :=
+by
+  ext g
+  rw [rigidStabilizer_support]
+  simp
+
+theorem rigidStabilizer_sInter (S : Set (Set α)) :
+  G•[⋂₀ S] = ⨅ T ∈ S, G•[T] :=
+by
+  ext x
+  rw [rigidStabilizer_support]
+  constructor
+  · intro supp_ss_sInter
+    rw [Subgroup.mem_iInf]
+    intro T
+    rw [Subgroup.mem_iInf]
+    intro T_in_S
+    rw [rigidStabilizer_support]
+    rw [Set.subset_sInter_iff] at supp_ss_sInter
+    exact supp_ss_sInter T T_in_S
+  · intro x_in_rist
+    rw [Set.subset_sInter_iff]
+    intro T T_in_S
+    rw [<-rigidStabilizer_support]
+    rw [Subgroup.mem_iInf] at x_in_rist
+    specialize x_in_rist T
+    rw [Subgroup.mem_iInf] at x_in_rist
+    exact x_in_rist T_in_S
+
+theorem rigidStabilizer_smulImage (f g : G) (S : Set α) :
+  g ∈ G•[f •'' S] ↔ f⁻¹ * g * f ∈ G•[S] :=
+by
+  repeat rw [rigidStabilizer_support]
+  nth_rw 3 [<-inv_inv f]
+  rw [support_conjugate]
+  rw [smulImage_subset_inv]
+  simp
+
+theorem rigidStabilizer_conj_image_eq (S : Set α) (f : G) :
+  (fun g => f * g * f⁻¹) '' G•[S] = G•[f •'' S] :=
+by
+  ext x
+  have f_eq : (fun g => f * g * f⁻¹) = (MulAut.conj f).toEquiv := by
+    ext x
+    simp
+
+  rw [f_eq, Set.mem_image_equiv]
+  rw [MulEquiv.toEquiv_eq_coe, MulEquiv.coe_toEquiv_symm, MulAut.conj_symm_apply]
+  simp [rigidStabilizer_smulImage]
+
+theorem orbit_rigidStabilizer_subset {p : α} {U : Set α} (p_in_U : p ∈ U):
+  MulAction.orbit G•[U] p ⊆ U :=
+by
+  intro q q_in_orbit
+  have ⟨⟨h, h_in_rist⟩, hp_eq_q⟩ := MulAction.mem_orbit_iff.mp q_in_orbit
+  simp at hp_eq_q
+  rw [<-hp_eq_q]
+  rw [rigidStabilizer_support] at h_in_rist
+  rw [<-elem_moved_in_support' p h_in_rist]
+  assumption
+
+-- TODO: remov ethe need for FaithfulSMul?
+theorem rigidStabilizer_neBot [FaithfulSMul G α] {U : Set α}:
+  G•[U] ≠ ⊥ → Set.Nonempty U :=
+by
+  intro ne_bot
+  by_contra empty
+  apply ne_bot
+  rw [Set.not_nonempty_iff_eq_empty] at empty
+  rw [empty]
+  exact rigidStabilizer_empty G α
+
 end Rubin

Rubin/SmulImage.lean

@@ -1,8 +1,10 @@
 import Mathlib.Data.Finset.Basic
 import Mathlib.GroupTheory.Subgroup.Basic
 import Mathlib.GroupTheory.GroupAction.Basic
+import Mathlib.Topology.Basic
 
 import Rubin.MulActionExt
+import Rubin.Topology
 
 namespace Rubin
 
@@ -54,6 +56,12 @@ theorem mem_smulImage {x : α} {g : G} {U : Set α} : x ∈ g •'' U ↔ g⁻¹
 -- this is simply [`mem_smulImage`] paired with set extensionality.
 theorem smulImage_set {g: G} {U: Set α} : g •'' U = {x | g⁻¹ • x ∈ U} := Set.ext (fun _x => mem_smulImage)
 
+@[simp]
+theorem smulImage_preImage (g: G) (U: Set α) : (fun p => g • p) ⁻¹' U = g⁻¹ •'' U := by
+  ext x
+  simp
+  rw [mem_smulImage, inv_inv]
+
 theorem mem_inv_smulImage {x : α} {g : G} {U : Set α} : x ∈ g⁻¹ •'' U ↔ g • x ∈ U :=
   by
   let msi := @Rubin.mem_smulImage _ _ _ _ x g⁻¹ U
@@ -61,19 +69,19 @@ theorem mem_inv_smulImage {x : α} {g : G} {U : Set α} : x ∈ g⁻¹ •'' U
   exact msi
 #align mem_inv_smul'' Rubin.mem_inv_smulImage
 
-theorem mem_smulImage' {x : α} (g : G) {U : Set α} : x ∈ U ↔ g • x ∈ g •'' U :=
+@[simp]
+theorem mem_smulImage' {x : α} (g : G) {U : Set α} : g • x ∈ g •'' U ↔ x ∈ U :=
 by
   rw [mem_smulImage]
   rw [<-mul_smul, mul_left_inv, one_smul]
 
--- TODO: rename to smulImage_mul
 @[simp]
-theorem mul_smulImage (g h : G) (U : Set α) : g •'' (h •'' U) = (g * h) •'' U :=
+theorem smulImage_mul (g h : G) (U : Set α) : g •'' (h •'' U) = (g * h) •'' U :=
   by
   ext
   rw [Rubin.mem_smulImage, Rubin.mem_smulImage, Rubin.mem_smulImage, ←
     mul_smul, mul_inv_rev]
-#align mul_smul'' Rubin.mul_smulImage
+#align mul_smul'' Rubin.smulImage_mul
 
 @[simp]
 theorem one_smulImage (U : Set α) : (1 : G) •'' U = U :=
@@ -82,7 +90,7 @@ theorem one_smulImage (U : Set α) : (1 : G) •'' U = U :=
   rw [Rubin.mem_smulImage, inv_one, one_smul]
 #align one_smul'' Rubin.one_smulImage
 
-theorem disjoint_smulImage (g : G) {U V : Set α} :
+theorem smulImage_disjoint (g : G) {U V : Set α} :
     Disjoint U V → Disjoint (g •'' U) (g •'' V) :=
   by
   intro disjoint_U_V
@@ -91,20 +99,37 @@ theorem disjoint_smulImage (g : G) {U V : Set α} :
   intro x x_in_gU
   by_contra h
   exact (disjoint_U_V (mem_smulImage.mp x_in_gU)) (mem_smulImage.mp h)
-#align disjoint_smul'' Rubin.disjoint_smulImage
+#align disjoint_smul'' Rubin.smulImage_disjoint
 
-namespace SmulImage
+theorem SmulImage.congr (g : G) {U V : Set α} : U = V → g •'' U = g •'' V :=
-theorem congr (g : G) {U V : Set α} : U = V → g •'' U = g •'' V :=
   congr_arg fun W : Set α => g •'' W
 #align smul''_congr Rubin.SmulImage.congr
-end SmulImage
 
-theorem smulImage_subset (g : G) {U V : Set α} : U ⊆ V → g •'' U ⊆ g •'' V :=
+theorem SmulImage.inv_congr (g: G) {U V : Set α} : g •'' U = g •'' V → U = V :=
 by
+  intro h
+  rw [<-one_smulImage (G := G) U]
+  rw [<-one_smulImage (G := G) V]
+  rw [<-mul_left_inv g]
+  repeat rw [<-smulImage_mul]
+  exact SmulImage.congr g⁻¹ h
+
+theorem smulImage_inv (g: G) (U V : Set α) : g •'' U = V ↔ U = g⁻¹ •'' V := by
+  nth_rw 2 [<-one_smulImage (G := G) U]
+  rw [<-mul_left_inv g, <-smulImage_mul]
+  constructor
+  · intro h
+    rw [SmulImage.congr]
+    exact h
+  · intro h
+    apply SmulImage.inv_congr at h
+    exact h
+
+theorem smulImage_mono (g : G) {U V : Set α} : U ⊆ V → g •'' U ⊆ g •'' V := by
   intro h1 x
   rw [Rubin.mem_smulImage, Rubin.mem_smulImage]
   exact fun h2 => h1 h2
-#align smul''_subset Rubin.smulImage_subset
+#align smul''_subset Rubin.smulImage_mono
 
 theorem smulImage_union (g : G) {U V : Set α} : g •'' U ∪ V = (g •'' U) ∪ (g •'' V) :=
   by
@@ -120,6 +145,105 @@ theorem smulImage_inter (g : G) {U V : Set α} : g •'' U ∩ V = (g •'' U)
     Rubin.mem_smulImage, Set.mem_inter_iff]
 #align smul''_inter Rubin.smulImage_inter
 
+@[simp]
+theorem smulImage_sUnion (g : G) {S : Set (Set α)} : g •'' (⋃₀ S) = ⋃₀ {g •'' T | T ∈ S} :=
+by
+  ext x
+  constructor
+  · intro h
+    rw [mem_smulImage, Set.mem_sUnion] at h
+    rw [Set.mem_sUnion]
+    let ⟨T, ⟨T_in_S, ginv_x_in_T⟩⟩ := h
+    simp
+    use T
+    constructor; trivial
+    rw [mem_smulImage]
+    exact ginv_x_in_T
+  · intro h
+    rw [Set.mem_sUnion] at h
+    rw [mem_smulImage, Set.mem_sUnion]
+    simp at h
+    let ⟨T, ⟨T_in_S, x_in_gT⟩⟩ := h
+    use T
+    constructor; trivial
+    rw [<-mem_smulImage]
+    exact x_in_gT
+
+@[simp]
+theorem smulImage_sInter (g : G) {S : Set (Set α)} : g •'' (⋂₀ S) = ⋂₀ {g •'' T | T ∈ S} := by
+  ext x
+  constructor
+  · intro h
+    rw [mem_smulImage, Set.mem_sInter] at h
+    rw [Set.mem_sInter]
+    simp
+    intro T T_in_S
+    rw [mem_smulImage]
+    exact h T T_in_S
+  · intro h
+    rw [Set.mem_sInter] at h
+    rw [mem_smulImage, Set.mem_sInter]
+    intro T T_in_S
+    rw [<-mem_smulImage]
+    simp at h
+    exact h T T_in_S
+
+@[simp]
+theorem smulImage_iInter {β : Type _} (g : G) (S : Set β) (f : β → Set α) :
+  g •'' (⋂ x ∈ S, f x) = ⋂ x ∈ S, g •'' (f x) :=
+by
+  ext x
+  constructor
+  · intro h
+    rw [mem_smulImage] at h
+    simp
+    simp at h
+    intro i i_in_S
+    rw [mem_smulImage]
+    exact h i i_in_S
+  · intro h
+    simp at h
+    rw [mem_smulImage]
+    simp
+    intro i i_in_S
+    rw [<-mem_smulImage]
+    exact h i i_in_S
+
+@[simp]
+theorem smulImage_iInter_fin {β : Type _} (g : G) (S : Finset β) (f : β → Set α) :
+  g •'' (⋂ x ∈ S, f x) = ⋂ x ∈ S, g •'' (f x) :=
+by
+  -- For some strange reason I can't use the above theorem
+  ext x
+  rw [mem_smulImage, Set.mem_iInter, Set.mem_iInter]
+  simp
+  conv => {
+    rhs
+    ext; ext
+    rw [mem_smulImage]
+  }
+
+@[simp]
+theorem smulImage_compl (g : G) (U : Set α) : (g •'' U)ᶜ = g •'' Uᶜ :=
+by
+  ext x
+  rw [Set.mem_compl_iff]
+  repeat rw [mem_smulImage]
+  rw [Set.mem_compl_iff]
+
+@[simp]
+theorem smulImage_nonempty (g: G) {U : Set α} : Set.Nonempty (g •'' U) ↔ Set.Nonempty U :=
+by
+  constructor
+  · intro ⟨x, x_in_gU⟩
+    use g⁻¹•x
+    rw [<-mem_smulImage]
+    assumption
+  · intro ⟨x, x_in_U⟩
+    use g•x
+    simp
+    assumption
+
 theorem smulImage_eq_inv_preimage {g : G} {U : Set α} : g •'' U = (g⁻¹ • ·) ⁻¹' U :=
   by
   ext
@@ -148,13 +272,13 @@ theorem smulImage_subset_inv {G α : Type _} [Group G] [MulAction G α]
 by
   constructor
   · intro h
-    apply smulImage_subset f⁻¹ at h
+    apply smulImage_mono f⁻¹ at h
-    rw [mul_smulImage] at h
+    rw [smulImage_mul] at h
     rw [mul_left_inv, one_smulImage] at h
     exact h
   · intro h
-    apply smulImage_subset f at h
+    apply smulImage_mono f at h
-    rw [mul_smulImage] at h
+    rw [smulImage_mul] at h
     rw [mul_right_inv, one_smulImage] at h
     exact h
 
@@ -170,14 +294,14 @@ theorem smulImage_disjoint_mul {G α : Type _} [Group G] [MulAction G α]
   Disjoint (f •'' U) (g •'' V) ↔ Disjoint U ((f⁻¹ * g) •'' V) := by
   constructor
   · intro h
-    apply disjoint_smulImage f⁻¹ at h
+    apply smulImage_disjoint f⁻¹ at h
-    repeat rw [mul_smulImage] at h
+    repeat rw [smulImage_mul] at h
     rw [mul_left_inv, one_smulImage] at h
     exact h
 
   · intro h
-    apply disjoint_smulImage f at h
+    apply smulImage_disjoint f at h
-    rw [mul_smulImage] at h
+    rw [smulImage_mul] at h
     rw [<-mul_assoc] at h
     rw [mul_right_inv, one_mul] at h
     exact h
@@ -195,12 +319,11 @@ by
 theorem smulImage_disjoint_subset {G α : Type _} [Group G] [MulAction G α]
   {f g : G} {U V : Set α} (h_sub: U ⊆ V):
   Disjoint (f •'' V) (g •'' V) → Disjoint (f •'' U) (g •'' U) :=
-by
+Set.disjoint_of_subset (smulImage_mono _ h_sub) (smulImage_mono _ h_sub)
-  apply Set.disjoint_of_subset (smulImage_subset _ h_sub) (smulImage_subset _ h_sub)
 
 -- States that if `g^i •'' V` and `g^j •'' V` are disjoint for any `i ≠ j` and `x ∈ V`
--- then `g^i • x` will always lie outside of `V`.
+-- then `g^i • x` will always lie outside of `V` if `x ∈ V`.
-lemma smulImage_distinct_of_disjoint_exp {G α : Type _} [Group G] [MulAction G α] {g : G} {V : Set α} {n : ℕ}
+lemma smulImage_distinct_of_disjoint_pow {G α : Type _} [Group G] [MulAction G α] {g : G} {V : Set α} {n : ℕ}
   (n_pos : 0 < n)
   (h_disj : ∀ (i j : Fin n), i ≠ j → Disjoint (g ^ (i : ℕ) •'' V) (g ^ (j : ℕ) •'' V)) :
   ∀ (x : α) (_hx : x ∈ V) (i : Fin n), 0 < (i : ℕ) → g ^ (i : ℕ) • (x : α) ∉ V :=
@@ -216,6 +339,223 @@ by
   have h_notin_V := Set.disjoint_left.mp (h_disj i (⟨0, n_pos⟩ : Fin n) i_ne_zero) h_contra
   simp only [pow_zero, one_smulImage] at h_notin_V
   exact h_notin_V
-#align distinct_images_from_disjoint Rubin.smulImage_distinct_of_disjoint_exp
+#align distinct_images_from_disjoint Rubin.smulImage_distinct_of_disjoint_pow
+
+theorem smulImage_isOpen {G α : Type _}
+  [Group G] [TopologicalSpace α] [MulAction G α] [ContinuousConstSMul G α] (g : G)
+  {S : Set α} (S_open : IsOpen S) : IsOpen (g •'' S) :=
+by
+  rw [smulImage_eq_inv_preimage]
+  exact (continuous_id.const_smul g⁻¹).isOpen_preimage S S_open
+
+theorem smulImage_isClosed {G α : Type _}
+  [Group G] [TopologicalSpace α] [MulAction G α] [ContinuousConstSMul G α] (g : G)
+  {S : Set α} (S_open : IsClosed S) : IsClosed (g •'' S) :=
+by
+  rw [<-isOpen_compl_iff]
+  rw [<-isOpen_compl_iff] at S_open
+  rw [smulImage_compl]
+  apply smulImage_isOpen
+  assumption
+
+theorem smulImage_interior {G α : Type _} [Group G] [TopologicalSpace α] [MulAction G α]
+  [hc : ContinuousConstSMul G α] (g : G) (U : Set α) :
+  interior (g •'' U) = g •'' interior U :=
+by
+  unfold interior
+  rw [smulImage_sUnion]
+  simp
+  ext x
+  simp
+  constructor
+  · intro ⟨T, ⟨T_open, T_sub⟩, x_in_T⟩
+    use g⁻¹ •'' T
+    repeat' apply And.intro
+    · exact smulImage_isOpen g⁻¹ T_open
+    · rw [smulImage_subset_inv]
+      rw [inv_inv]
+      exact T_sub
+    · rw [smulImage_mul, mul_right_inv, one_smulImage]
+      exact x_in_T
+  · intro ⟨T, ⟨T_open, T_sub⟩, x_in_T⟩
+    use g •'' T
+    repeat' apply And.intro
+    ·  exact smulImage_isOpen g T_open
+    · apply smulImage_mono
+      exact T_sub
+    · exact x_in_T
+
+theorem smulImage_closure {G α : Type _} [Group G] [TopologicalSpace α] [MulAction G α]
+  [ContinuousConstSMul G α] (g : G) (U : Set α) :
+  closure (g •'' U) = g •'' closure U :=
+by
+  unfold closure
+  rw [smulImage_sInter]
+  simp
+  ext x
+  simp
+  constructor
+  · intro IH T' T T_closed U_ss_T T'_eq
+    rw [<-T'_eq]
+    clear T' T'_eq
+    apply IH
+    · exact smulImage_isClosed g T_closed
+    · apply smulImage_mono
+      exact U_ss_T
+  · intro IH T T_closed gU_ss_T
+    apply IH
+    · exact smulImage_isClosed g⁻¹ T_closed
+    · rw [<-smulImage_subset_inv]
+      exact gU_ss_T
+    · simp
+
+section Filters
+
+open Topology
+
+variable {G α : Type _}
+variable [Group G] [MulAction G α]
+
+/--
+An SMul can be extended to filters, while preserving the properties of `MulAction`.
+
+To avoid polluting the `SMul` instances for filters, those properties are made separate,
+instead of implementing `MulAction G (Filter α)`.
+--/
+def SmulFilter {G α : Type _} [SMul G α] (g : G) (F : Filter α) : Filter α :=
+  Filter.map (fun p => g • p) F
+
+infixl:60 " •ᶠ " => Rubin.SmulFilter
+
+theorem smulFilter_def {G α : Type _} [SMul G α] (g : G) (F : Filter α) :
+  Filter.map (fun p => g • p) F = g •ᶠ F := rfl
+
+theorem smulFilter_neBot {G α : Type _} [SMul G α] (g : G) {F : Filter α} (F_neBot : Filter.NeBot F) :
+  Filter.NeBot (g •ᶠ F) :=
+by
+  rw [<-smulFilter_def]
+  exact Filter.map_neBot
+
+instance smulFilter_neBot' {G α : Type _} [SMul G α] {g : G} {F : Filter α} [F_neBot : Filter.NeBot F] :
+  Filter.NeBot (g •ᶠ F) := smulFilter_neBot g F_neBot
+
+theorem smulFilter_principal (g : G) (S : Set α) :
+  g •ᶠ Filter.principal S = Filter.principal (g •'' S) :=
+by
+  rw [<-smulFilter_def]
+  rw [Filter.map_principal]
+  rfl
+
+theorem mul_smulFilter (g h: G) (F : Filter α) :
+  (g * h) •ᶠ F = g •ᶠ (h •ᶠ F) :=
+by
+  repeat rw [<-smulFilter_def]
+  simp only [mul_smul]
+  rw [Filter.map_map]
+  rfl
+
+theorem one_smulFilter (G : Type _) [Group G] [MulAction G α] (F : Filter α) :
+  (1 : G) •ᶠ F = F :=
+by
+  rw [<-smulFilter_def]
+  simp only [one_smul]
+  exact Filter.map_id
+
+theorem mem_smulFilter_iff (g : G) (F : Filter α) (U : Set α) :
+  U ∈ g •ᶠ F ↔ g⁻¹ •'' U ∈ F :=
+by
+  rw [<-smulFilter_def, Filter.mem_map, smulImage_eq_inv_preimage, inv_inv]
+
+theorem smulFilter_mono (g : G) (F F' : Filter α) :
+  F ≤ F' ↔ g •ᶠ F ≤ g •ᶠ F' :=
+by
+  suffices ∀ (g : G) (F F' : Filter α), F ≤ F' → g •ᶠ F ≤ g •ᶠ F' by
+    constructor
+    apply this
+    intro H
+    specialize this g⁻¹ _ _ H
+    repeat rw [<-mul_smulFilter] at this
+    rw [mul_left_inv] at this
+    repeat rw [one_smulFilter] at this
+    exact this
+  intro g F F' F_le_F'
+  intro U U_in_gF
+  rw [mem_smulFilter_iff] at U_in_gF
+  rw [mem_smulFilter_iff]
+  apply F_le_F'
+  assumption
+
+theorem smulFilter_le_iff_le_inv (g : G) (F F' : Filter α) :
+  F ≤ g •ᶠ F' ↔ g⁻¹ •ᶠ F ≤ F' :=
+by
+  nth_rw 2 [<-one_smulFilter G F']
+  rw [<-mul_left_inv g, mul_smulFilter]
+  exact smulFilter_mono g⁻¹ _ _
+
+variable [TopologicalSpace α]
+
+theorem smulFilter_nhds (g : G) (p : α) [ContinuousConstSMul G α]:
+  g •ᶠ 𝓝 p = 𝓝 (g • p) :=
+by
+  ext S
+  rw [<-smulFilter_def, Filter.mem_map, mem_nhds_iff, mem_nhds_iff]
+  simp
+  constructor
+  · intro ⟨T, T_ss_smulImage, T_open, p_in_T⟩
+    use g •'' T
+    repeat' apply And.intro
+    · rw [smulImage_subset_inv]
+      assumption
+    · exact smulImage_isOpen g T_open
+    · simp
+      assumption
+  · intro ⟨T, T_ss_S, T_open, gp_in_T⟩
+    use g⁻¹ •'' T
+    repeat' apply And.intro
+    · apply smulImage_mono
+      assumption
+    · exact smulImage_isOpen g⁻¹ T_open
+    · rw [mem_smulImage, inv_inv]
+      assumption
+
+theorem smulFilter_clusterPt (g : G) (F : Filter α) (x : α) [ContinuousConstSMul G α] :
+  ClusterPt x (g •ᶠ F) ↔ ClusterPt (g⁻¹ • x) F :=
+by
+  suffices ∀ (g : G) (F : Filter α) (x : α), ClusterPt x (g •ᶠ F) → ClusterPt (g⁻¹ • x) F by
+    constructor
+    apply this
+    intro gx_clusterPt_F
+
+    rw [<-one_smul G x, <-mul_right_inv g, mul_smul]
+    nth_rw 1 [<-inv_inv g]
+    apply this
+    rw [<-mul_smulFilter, mul_left_inv, one_smulFilter]
+    assumption
+  intro g F x x_cp_gF
+  rw [clusterPt_iff_forall_mem_closure]
+  rw [clusterPt_iff_forall_mem_closure] at x_cp_gF
+  simp only [mem_smulFilter_iff] at x_cp_gF
+  intro S S_in_F
+
+  rw [<-mem_inv_smulImage]
+  rw [<-smulImage_closure]
+
+  apply x_cp_gF
+  rw [inv_inv, smulImage_mul, mul_left_inv, one_smulImage]
+  assumption
+
+theorem smulImage_compact [ContinuousConstSMul G α] (g : G) {U : Set α} (U_compact : IsCompact U) :
+  IsCompact (g •'' U) :=
+by
+  intro F F_neBot F_le_principal
+  rw [<-smulFilter_principal, smulFilter_le_iff_le_inv] at F_le_principal
+  let ⟨x, x_in_U, x_clusterPt⟩ := U_compact F_le_principal
+  use g • x
+  constructor
+  · rw [mem_smulImage']
+    assumption
+  · rw [smulFilter_clusterPt, inv_inv] at x_clusterPt
+    assumption
 
+end Filters
 end Rubin

Rubin/Support.lean

@@ -2,6 +2,8 @@ import Mathlib.Data.Finset.Basic
 import Mathlib.GroupTheory.Commutator
 import Mathlib.GroupTheory.Subgroup.Basic
 import Mathlib.GroupTheory.GroupAction.Basic
+import Mathlib.Topology.Basic
+import Mathlib.Topology.Algebra.ConstMulAction
 
 import Rubin.MulActionExt
 import Rubin.SmulImage
@@ -14,27 +16,25 @@ The support of a group action of `g: G` on `α` (here generalized to `SMul G α`
 is the set of values `x` in `α` for which `g • x ≠ x`.
 
 This can also be thought of as the complement of the fixpoints of `(g •)`,
-which [`support_eq_not_fixed_by`] provides.
+which [`support_eq_compl_fixedBy`] provides.
 --/
+-- TODO: rename to MulAction.support
 def Support {G : Type _} (α : Type _) [SMul G α] (g : G) :=
   {x : α | g • x ≠ x}
 #align support Rubin.Support
 
-theorem SmulSupport_def {G : Type _} (α : Type _) [SMul G α] {g : G} :
-  Support α g = {x : α | g • x ≠ x} := by tauto
-
 variable {G α: Type _}
 variable [Group G]
 variable [MulAction G α]
 variable {f g : G}
 variable {x : α}
 
-theorem support_eq_not_fixed_by : Support α g = (MulAction.fixedBy α g)ᶜ := by tauto
+theorem support_eq_compl_fixedBy : Support α g = (MulAction.fixedBy α g)ᶜ := by tauto
-#align support_eq_not_fixed_by Rubin.support_eq_not_fixed_by
+#align support_eq_not_fixed_by Rubin.support_eq_compl_fixedBy
 
-theorem support_compl_eq_fixed_by : (Support α g)ᶜ = MulAction.fixedBy α g := by
+theorem fixedBy_eq_compl_support : MulAction.fixedBy α g = (Support α g)ᶜ := by
   rw [<-compl_compl (MulAction.fixedBy _ _)]
-  exact congr_arg (·ᶜ) support_eq_not_fixed_by
+  exact congr_arg (·ᶜ) support_eq_compl_fixedBy
 
 theorem mem_support :
     x ∈ Support α g ↔ g • x ≠ x := by tauto
@@ -45,6 +45,12 @@ theorem not_mem_support :
   rw [Rubin.mem_support, Classical.not_not]
 #align mem_not_support Rubin.not_mem_support
 
+theorem support_one : Support α (1 : G) = ∅ := by
+  rw [Set.eq_empty_iff_forall_not_mem]
+  intro x
+  rw [not_mem_support]
+  simp
+
 theorem smul_mem_support :
     x ∈ Support α g → g • x ∈ Support α g := fun h =>
   h ∘ smul_left_cancel g
@@ -61,24 +67,6 @@ theorem fixed_of_disjoint {U : Set α} :
   not_mem_support.mp (Set.disjoint_left.mp disjoint_U_support x_in_U)
 #align fixed_of_disjoint Rubin.fixed_of_disjoint
 
-theorem fixed_smulImage_in_support (g : G) {U : Set α} :
-    Support α g ⊆ U → g •'' U = U :=
-  by
-  intro support_in_U
-  ext x
-  cases' @or_not (x ∈ Support α g) with xmoved xfixed
-  exact
-    ⟨fun _ => support_in_U xmoved, fun _ =>
-      mem_smulImage.mpr (support_in_U (Rubin.inv_smul_mem_support xmoved))⟩
-  rw [Rubin.mem_smulImage, smul_eq_iff_inv_smul_eq.mp (not_mem_support.mp xfixed)]
-#align fixes_subset_within_support Rubin.fixed_smulImage_in_support
-
-theorem smulImage_subset_in_support (g : G) (U V : Set α) :
-    U ⊆ V → Support α g ⊆ V → g •'' U ⊆ V := fun U_in_V support_in_V =>
-  Rubin.fixed_smulImage_in_support g support_in_V ▸
-    Rubin.smulImage_subset g U_in_V
-#align moves_subset_within_support Rubin.smulImage_subset_in_support
-
 theorem support_mul (g h : G) (α : Type _) [MulAction G α] :
     Support α (g * h) ⊆
       Support α g ∪ Support α h :=
@@ -135,6 +123,19 @@ theorem support_pow (α : Type _) [MulAction G α] (g : G) (j : ℕ) :
     -- exact j_ih
 #align support_pow Rubin.support_pow
 
+theorem support_zpow (α : Type _) [MulAction G α] (g : G) (j : ℤ) :
+    Support α (g ^ j) ⊆ Support α g :=
+by
+  cases j with
+  | ofNat n =>
+    rw [Int.ofNat_eq_coe, zpow_coe_nat]
+    exact support_pow α g n
+  | negSucc n =>
+    rw [Int.negSucc_eq, zpow_neg, support_inv, zpow_add, zpow_coe_nat, zpow_one]
+    nth_rw 2 [<-pow_one g]
+    rw [<-pow_add]
+    exact support_pow α g (n+1)
+
 theorem support_comm (α : Type _) [MulAction G α] (g h : G) :
     Support α ⁅g, h⁆ ⊆
       Support α h ∪ (g •'' Support α h) :=
@@ -155,10 +156,11 @@ theorem disjoint_support_comm (f g : G) {U : Set α} :
     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 : Support α (g * f⁻¹ * g⁻¹) ⊆ g •'' U :=
+  have support_conj : Support α (g * f⁻¹ * g⁻¹) ⊆ g •'' U := by
-    ((Rubin.support_conjugate α f⁻¹ g).trans
+    rw [support_conjugate]
-          (Rubin.SmulImage.congr g (Rubin.support_inv α f))).symm ▸
+    apply smulImage_mono
-      Rubin.smulImage_subset g support_in_U
+    rw [support_inv]
+    exact support_in_U
   have goal :=
     (congr_arg (f • ·)
         (Rubin.fixed_of_disjoint x_in_U
@@ -192,7 +194,7 @@ by
   have h₀ : ∀ x ∈ U, x ∉ Support α f := by
     intro x x_in_U
     unfold Commute SemiconjBy at h_comm
-    have gx_in_img := (mem_smulImage' g).mp x_in_U
+    have gx_in_img := (mem_smulImage' g).mpr x_in_U
     have h₁ : g • f • x = g • x := by
       have res := disjoint_not_mem₂ disj gx_in_img
       rw [not_mem_support] at res
@@ -229,4 +231,175 @@ by
   apply Set.eq_empty_iff_forall_not_mem.mp support_empty
   exact h
 
+theorem support_eq: Support α f = Support α g ↔ ∀ (x : α), (f • x = x ∧ g • x = x) ∨ (f • x ≠ x ∧ g • x ≠ x) := by
+  constructor
+  · intro h
+    intro x
+    by_cases x_in? : x ∈ Support α f
+    · right
+      have gx_ne_x := by rw [h] at x_in?; exact x_in?
+      exact ⟨x_in?, gx_ne_x⟩
+    · left
+      have fx_eq_x : f • x = x := by rw [<-not_mem_support]; exact x_in?
+      have gx_eq_x : g • x = x := by rw [<-not_mem_support, <-h]; exact x_in?
+      exact ⟨fx_eq_x, gx_eq_x⟩
+  · intro h
+    ext x
+    constructor
+    · intro fx_ne_x
+      rw [mem_support] at fx_ne_x
+      rw [mem_support]
+      cases h x with
+      | inl h₁ => exfalso; exact fx_ne_x h₁.left
+      | inr h₁ => exact h₁.right
+    · intro gx_ne_x
+      rw [mem_support] at gx_ne_x
+      rw [mem_support]
+      cases h x with
+      | inl h₁ => exfalso; exact gx_ne_x h₁.right
+      | inr h₁ => exact h₁.left
+
+theorem support_empty_iff (g : G) [h_f : FaithfulSMul G α] :
+  Support α g = ∅ ↔ g = 1 :=
+by
+  constructor
+  · intro supp_empty
+    rw [Set.eq_empty_iff_forall_not_mem] at supp_empty
+    apply h_f.eq_of_smul_eq_smul
+    intro x
+    specialize supp_empty x
+    rw [not_mem_support] at supp_empty
+    simp
+    exact supp_empty
+  · intro g_eq_1
+    rw [g_eq_1]
+    exact support_one
+
+theorem support_nonempty_iff (g : G) [h_f : FaithfulSMul G α] :
+  Set.Nonempty (Support α g) ↔ g ≠ 1 :=
+by
+  constructor
+  · intro ⟨x, x_in_supp⟩
+    by_contra g_eq_1
+    rw [g_eq_1, support_one] at x_in_supp
+    exact x_in_supp
+  · intro g_ne_one
+    by_contra supp_empty
+    rw [Set.not_nonempty_iff_eq_empty] at supp_empty
+    exact g_ne_one ((support_empty_iff _).mp supp_empty)
+
+theorem elem_moved_in_support (g : G) (p : α) :
+  p ∈ Support α g ↔ g • p ∈ Support α g :=
+by
+  suffices ∀ (g : G) (p : α), p ∈ Support α g → g • p ∈ Support α g by
+    constructor
+    exact this g p
+    rw [<-support_inv]
+    intro H
+    rw [<-one_smul G p, <-mul_left_inv g, mul_smul]
+    exact this _ _ H
+  intro g p p_in_supp
+  by_contra gp_notin_supp
+  rw [<-support_inv, not_mem_support] at gp_notin_supp
+  rw [mem_support] at p_in_supp
+  apply p_in_supp
+  symm at gp_notin_supp
+  group_action at gp_notin_supp
+  exact gp_notin_supp
+
+theorem elem_moved_in_support' {g : G} (p : α) {U : Set α} (support_in_U : Support α g ⊆ U):
+  p ∈ U ↔ g • p ∈ U :=
+by
+  by_cases p_in_supp? : p ∈ Support α g
+  · constructor
+    rw [elem_moved_in_support] at p_in_supp?
+    all_goals intro; exact support_in_U p_in_supp?
+  · rw [not_mem_support] at p_in_supp?
+    rw [p_in_supp?]
+
+theorem elem_moved_in_support_zpow {g : G} (p : α) (j : ℤ) {U : Set α} (support_in_U : Support α g ⊆ U):
+  p ∈ U ↔ g^j • p ∈ U :=
+by
+  by_cases p_in_supp? : p ∈ Support α g
+  · constructor
+    all_goals intro; apply support_in_U
+    swap; exact p_in_supp?
+    rw [<-elem_moved_in_support' p (support_zpow α g j)]
+    assumption
+  · rw [not_mem_support] at p_in_supp?
+    rw [smul_zpow_eq_of_smul_eq j p_in_supp?]
+
+theorem orbit_subset_support (g : G) (p : α) :
+  MulAction.orbit (Subgroup.closure {g}) p ⊆ Support α g ∪ {p} :=
+by
+  intro q q_in_orbit
+  rw [MulAction.mem_orbit_iff] at q_in_orbit
+  let ⟨⟨h, h_in_closure⟩, hp_eq_q⟩ := q_in_orbit
+  simp at hp_eq_q
+  rw [Subgroup.mem_closure_singleton] at h_in_closure
+  let ⟨n, g_pow_n_eq_h⟩ := h_in_closure
+  rw [<-hp_eq_q, <-g_pow_n_eq_h]
+  clear hp_eq_q g_pow_n_eq_h h_in_closure
+
+  have union_superset : Support α g ⊆ Support α g ∪ {p} := by
+    simp only [Set.union_singleton, Set.subset_insert]
+  rw [<-elem_moved_in_support_zpow _ _ union_superset]
+  simp only [Set.union_singleton, Set.mem_insert_iff, true_or]
+
+theorem orbit_subset_of_support_subset (g : G) {p : α} {U : Set α} (p_in_U : p ∈ U)
+  (supp_ss_U : Support α g ⊆ U) :
+  MulAction.orbit (Subgroup.closure {g}) p ⊆ U :=
+by
+  apply subset_trans
+  exact orbit_subset_support g p
+  apply Set.union_subset
+  assumption
+  rw [Set.singleton_subset_iff]
+  assumption
+
+theorem fixed_smulImage_in_support (g : G) {U : Set α} :
+  Support α g ⊆ U → g •'' U = U :=
+by
+  intro support_in_U
+  ext x
+  rw [mem_smulImage]
+  symm
+  apply elem_moved_in_support'
+  rw [support_inv]
+  assumption
+#align fixes_subset_within_support Rubin.fixed_smulImage_in_support
+
+theorem smulImage_subset_in_support (g : G) (U V : Set α) :
+    U ⊆ V → Support α g ⊆ V → g •'' U ⊆ V := fun U_in_V support_in_V =>
+  Rubin.fixed_smulImage_in_support g support_in_V ▸
+    smulImage_mono g U_in_V
+#align moves_subset_within_support Rubin.smulImage_subset_in_support
+
+
+section Continuous
+
+variable {G α : Type _}
+variable [Group G]
+variable [TopologicalSpace α]
+variable [MulAction G α]
+variable [ContinuousConstSMul G α]
+
+theorem support_isOpen (g : G) [T2Space α]: IsOpen (Support α g) := by
+  apply isOpen_iff_forall_mem_open.mpr
+  intro x xmoved
+  let ⟨U, V, open_U, open_V, gx_in_U, x_in_V, disjoint_U_V⟩ := T2Space.t2 xmoved
+
+  refine ⟨
+    V ∩ (g⁻¹ •'' U),
+    ?subset,
+    IsOpen.inter open_V (smulImage_isOpen g⁻¹ open_U),
+    ⟨x_in_V, mem_inv_smulImage.mpr gx_in_U⟩
+  ⟩
+  intro y ⟨yV, yU⟩
+  apply Disjoint.ne_of_mem disjoint_U_V _ yV
+  rw [mem_inv_smulImage] at yU
+  exact yU
+
+end Continuous
+
 end Rubin

Rubin/Tactic.lean

@@ -54,18 +54,18 @@ macro_rules
     tsub_self,
     <-mul_assoc,
 
-    one_pow,
+    -- one_pow,
-    one_zpow,
+    -- one_zpow,
-    <-mul_zpow_neg_one,
+    -- <-mul_zpow_neg_one,
-    zpow_zero,
+    -- zpow_zero,
-    mul_zpow,
+    -- mul_zpow,
-    zpow_sub,
+    -- zpow_sub,
-    <-zpow_ofNat,
+    -- <-zpow_ofNat,
-    <-zpow_neg_one,
+    -- <-zpow_neg_one,
-    <-zpow_mul,
+    -- <-zpow_mul,
-    <-zpow_add_one,
+    -- <-zpow_add_one,
-    <-zpow_one_add,
+    -- <-zpow_one_add,
-    <-zpow_add,
+    -- <-zpow_add,
 
     Int.ofNat_add,
     Int.ofNat_mul,

Rubin/Topological.lean

@@ -1,105 +0,0 @@
-import Mathlib.GroupTheory.Subgroup.Basic
-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
-
-section Continuity
-
--- TODO: don't have this extend MulAction
-class ContinuousMulAction (G α : Type _) [Group G] [TopologicalSpace α] extends
-    MulAction G α where
-  continuous : ∀ g : G, Continuous (fun x: α => g • x)
-#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.EquivariantHomeomorph
-
-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
-  intro g x
-  symm
-  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.equivariant_inv
-
-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.ContinuousMulAction.continuous g⁻¹) U h
-
-#align img_open_open Rubin.img_open_open
-
-theorem support_open (g : G) [TopologicalSpace α] [T2Space α]
-    [Rubin.ContinuousMulAction G α] : IsOpen (Support α g) :=
-  by
-  apply isOpen_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⟩
-  exact
-    ⟨V ∩ (g⁻¹ •'' U), fun y yW =>
-      Disjoint.ne_of_mem
-        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.img_open_open g⁻¹ U open_U),
-        ⟨x_in_V, mem_inv_smulImage.mpr gx_in_U⟩
-    ⟩
-#align support_open Rubin.support_open
-
-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
-
-lemma LocallyDense.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 Other
-
-end Rubin

Rubin/Topology.lean

@@ -0,0 +1,229 @@
+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
+import Mathlib.Data.Set.Basic
+
+import Rubin.MulActionExt
+
+namespace Rubin
+
+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
+  toFun_equivariant' : IsEquivariant G toFun
+
+variable {G α β γ: Type*}
+variable [Group G]
+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.toFun_equivariant' g (h.invFun x))
+  rw [h.left_inv _, h.right_inv _] at e
+  exact e
+
+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
+
+-- Note: this sounds like a general enough theorem that it should already be in mathlib
+lemma inter_of_open_subset_of_closure {α : Type _} [TopologicalSpace α] {U V : Set α}
+  (U_open : IsOpen U) (U_nonempty : Set.Nonempty U) (V_nonempty : Set.Nonempty V)
+  (U_ss_clV : U ⊆ closure V) : Set.Nonempty (U ∩ V) :=
+by
+  by_contra empty
+  rw [Set.not_nonempty_iff_eq_empty] at empty
+  rw [Set.nonempty_iff_ne_empty] at U_nonempty
+  apply U_nonempty
+
+  have clV_diff_U_ss_V : V ⊆ closure V \ U := by
+    rw [Set.subset_diff]
+    constructor
+    exact subset_closure
+    symm
+    rw [Set.disjoint_iff_inter_eq_empty]
+    exact empty
+  have clV_diff_U_closed : IsClosed (closure V \ U) := by
+    apply IsClosed.sdiff
+    exact isClosed_closure
+    assumption
+  unfold closure at U_ss_clV
+  simp at U_ss_clV
+  specialize U_ss_clV (closure V \ U) clV_diff_U_closed clV_diff_U_ss_V
+
+  rw [Set.subset_diff] at U_ss_clV
+  rw [Set.disjoint_iff_inter_eq_empty] at U_ss_clV
+  simp at U_ss_clV
+  exact U_ss_clV.right
+
+/--
+Note: `𝓝[≠] x` is notation for `nhdsWithin x {[x]}ᶜ`, ie. the neighborhood of x not containing itself.
+--/
+class HasNoIsolatedPoints (α : Type _) [TopologicalSpace α] :=
+  -- TODO: rename to nhdsWithin_ne_bot
+  nhbd_ne_bot : ∀ x : α, 𝓝[≠] x ≠ ⊥
+#align has_no_isolated_points Rubin.HasNoIsolatedPoints
+
+instance has_no_isolated_points_neBot₁ {α : Type _} [TopologicalSpace α] [h_nip: HasNoIsolatedPoints α]
+  (x: α) : Filter.NeBot (𝓝[≠] x) where
+  ne' := h_nip.nhbd_ne_bot x
+
+theorem Filter.NeBot.choose {α : Type _} (F : Filter α) [Filter.NeBot F] :
+  ∃ S : Set α, S ∈ F :=
+by
+  have res := (Filter.inhabitedMem (α := α) (f := F)).default
+  exact ⟨res.val, res.prop⟩
+
+
+theorem TopologicalSpace.IsTopologicalBasis.contains_point {α : Type _} [TopologicalSpace α]
+  {B : Set (Set α)} (B_basis : TopologicalSpace.IsTopologicalBasis B) (p : α) :
+  ∃ S : Set α, S ∈ B ∧ p ∈ S :=
+by
+  have nhds_basis := B_basis.nhds_hasBasis (a := p)
+
+  rw [Filter.hasBasis_iff] at nhds_basis
+  let ⟨S₁, S₁_in_nhds⟩ := Filter.NeBot.choose (𝓝 p)
+  let ⟨S, ⟨⟨S_in_B, p_in_S⟩, _⟩⟩ := (nhds_basis S₁).mp S₁_in_nhds
+  exact ⟨S, S_in_B, p_in_S⟩
+
+-- The collection of all the sets in `B` (a topological basis of `α`), such that `p` is in them.
+def TopologicalBasisContaining {α : Type _} [TopologicalSpace α]
+  {B : Set (Set α)} (B_basis : TopologicalSpace.IsTopologicalBasis B) (p : α) : FilterBasis α
+where
+  sets := {b ∈ B | p ∈ b}
+  nonempty := by
+    let ⟨S, S_in_B, p_in_S⟩ := TopologicalSpace.IsTopologicalBasis.contains_point B_basis p
+    use S
+    simp
+    tauto
+  inter_sets := by
+    intro S T ⟨S_in_B, p_in_S⟩ ⟨T_in_B, p_in_T⟩
+
+    have S_in_nhds := B_basis.mem_nhds_iff.mpr ⟨S, S_in_B, ⟨p_in_S, Eq.subset rfl⟩⟩
+    have T_in_nhds := B_basis.mem_nhds_iff.mpr ⟨T, T_in_B, ⟨p_in_T, Eq.subset rfl⟩⟩
+
+    have ST_in_nhds : S ∩ T ∈ 𝓝 p := Filter.inter_mem S_in_nhds T_in_nhds
+    rw [B_basis.mem_nhds_iff] at ST_in_nhds
+    let ⟨U, props⟩ := ST_in_nhds
+    use U
+    simp
+    simp at props
+    tauto
+
+theorem TopologicalBasisContaining.mem_iff {α : Type _} [TopologicalSpace α]
+  {B : Set (Set α)} (B_basis : TopologicalSpace.IsTopologicalBasis B) (p : α) (S : Set α) :
+  S ∈ TopologicalBasisContaining B_basis p ↔ S ∈ B ∧ p ∈ S :=
+by
+  rw [<-FilterBasis.mem_sets]
+  rfl
+
+theorem TopologicalBasisContaining.mem_nhds {α : Type _} [TopologicalSpace α]
+  {B : Set (Set α)} (B_basis : TopologicalSpace.IsTopologicalBasis B) (p : α) (S : Set α) :
+  S ∈ TopologicalBasisContaining B_basis p → S ∈ 𝓝 p :=
+by
+  rw [TopologicalBasisContaining.mem_iff]
+  rw [B_basis.mem_nhds_iff]
+  intro ⟨S_in_B, p_in_S⟩
+  use S
+
+instance TopologicalBasisContaining.neBot {α : Type _} [TopologicalSpace α]
+  {B : Set (Set α)} (B_basis : TopologicalSpace.IsTopologicalBasis B) (p : α) :
+  Filter.NeBot (TopologicalBasisContaining B_basis p).filter where
+  ne' := by
+    intro empty_in
+    rw [<-Filter.empty_mem_iff_bot, FilterBasis.mem_filter_iff] at empty_in
+    let ⟨S, ⟨S_in_basis, S_ss_empty⟩⟩ := empty_in
+    rw [TopologicalBasisContaining.mem_iff] at S_in_basis
+    exact S_ss_empty S_in_basis.right
+
+-- Note: the definition of "convergence" in the article doesn't quite match with the definition of ClusterPt
+-- Instead, `F ≤ nhds p` should be used.
+
+-- Note: Filter.HasBasis is a stronger statement than just FilterBasis - it defines a two-way relationship between a filter and a property; if the property is true for a set, then any superset of it is part of the filter, and vice-versa.
+-- With this, it's impossible for there to be a finer filter satisfying the property,
+-- as is evidenced by `filter_eq`: stripping away the `Filter` allows us to uniquely reconstruct it from the property itself.
+
+-- Proposition 3.3.1 trivially follows from `TopologicalSpace.IsTopologicalBasis.nhds_hasBasis` and `disjoint_nhds_nhds`: if `F.HasBasis (S → S ∈ B ∧ p ∈ S)` and `F.HasBasis (S → S ∈ B ∧ q ∈ S)`,
+-- then one can prove that `F ≤ nhds x` and `F ≤ nhds y` ~> `F = ⊥`
+-- Proposition 3.3.2 becomes simply `TopologicalSpace.IsTopologicalBasis.nhds_hasBasis`
+-- Proposition 3.3.3 is a consequence of the structure of `HasBasis`
+
+-- Proposition 3.4.1 can maybe be proven with `TopologicalSpace.IsTopologicalBasis.mem_closure_iff`?
+
+-- The tricky part here though is that "F is an ultra(pre)filter on B" can't easily be expressed.
+-- I should maybe define a Prop for it, and show that "F is an ultrafilter on B" + "F tends to a point p"
+-- is equivalent to `TopologicalSpace.IsTopologicalBasis.nhds_hasBasis`.
+
+-- The alternative is to only work with `Filter`, and state conditions with `Filter.HasBasis`,
+-- since that will force the filter to be an ultraprefilter on B.
+
+end Rubin

lake-manifest.json

@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "d3049643f6dded69eb7ce8124796cb1ec8df8840",
+   "rev": "d8610e1bcb91c013c3d868821c0ef28bf693be07",
    "name": "std",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -13,7 +13,7 @@
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
-   "rev": "d3a1d25f3eba0d93a58d5d3d027ffa78ece07755",
+   "rev": "1c88406514a636d241903e2e288d21dc6d861e01",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -22,34 +22,34 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "bf5ab42a58e71de7ebad399ce3f90d29aae7fca9",
+   "rev": "69404390bdc1de946bf0a2e51b1a69f308e56d7a",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
    "inherited": true,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover/lean4-cli",
+  {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
-   "rev": "a751d21d4b68c999accb6fc5d960538af26ad5ec",
+   "rev": "31d41415d5782a196999d4fd8eeaef3cae386a5f",
-   "name": "Cli",
+   "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v0.0.24",
    "inherited": true,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/ProofWidgets4",
+  {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
-   "rev": "c3b9f0d4ebedc43635d3f7e764e277b1010844b7",
+   "rev": "a751d21d4b68c999accb6fc5d960538af26ad5ec",
-   "name": "proofwidgets",
+   "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.22",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "c6979569edc545f999b82d8a833b190c918aec2e",
+   "rev": "95f91f8e66f14c0eecde8da6dbfeff39d44cbd81",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.3.0-rc2
+leanprover/lean4:v4.5.0-rc1