✨ Working equiv for RubinSpace

Rubin/AlgebraicDisjointness.lean

@@ -388,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
-    ext x
-    simp
-  rw [zpow_fix]
+  simp only [<-zpow_coe_nat]
   apply moves_inj
   intro k one_le_k k_lt_n
 
@@ -434,20 +431,16 @@ by
   · intro ⟨y, y_disj, x_eq⟩
     use g * y * g⁻¹
     rw [<-gxg12_eq]
-    refine ⟨?disj, x_eq⟩
-    exact y_disj.conj g
+    exact ⟨y_disj.conj g, x_eq⟩
   · intro ⟨y, y_disj, x_eq⟩
     use g⁻¹ * y * g
     constructor
-    · rw [(by group : f = g⁻¹ * (g * f * g⁻¹) * g⁻¹⁻¹)]
-      nth_rw 6 [<-inv_inv g]
-      exact y_disj.conj g⁻¹
+    · convert y_disj.conj g⁻¹ using 1
+      all_goals group
     · nth_rw 3 [<-inv_inv g]
       simp only [conj_pow]
+      rw [x_eq]
       group
-      group at x_eq
-      exact x_eq
-
 
 @[simp]
 theorem AlgebraicCentralizer.conj (f g : G) :

Rubin/Filter.lean

@@ -292,6 +292,21 @@ by
   any_goals apply B_ss_C
   all_goals assumption
 
+theorem Filter.InBasis.inf_eq_bot_iff {F G : Filter α} (F_in_basis : F.InBasis B) (G_in_basis : G.InBasis B) :
+  F ⊓ G = ⊥ ↔ ∃ U ∈ B, ∃ V ∈ B, U ∈ F ∧ V ∈ G ∧ U ∩ V = ∅ :=
+by
+  rw [Filter.inf_eq_bot_iff]
+  constructor
+  · intro ⟨U, U_in_F, V, V_in_G, UV_empty⟩
+    let ⟨U', U'_in_F, U'_in_B, U'_ss_U⟩ := F_in_basis U U_in_F
+    let ⟨V', V'_in_G, V'_in_B, V'_ss_V⟩ := G_in_basis V V_in_G
+    refine ⟨U', U'_in_B, V', V'_in_B, U'_in_F, V'_in_G, ?inter_empty⟩
+    apply Set.eq_empty_of_subset_empty
+    apply subset_trans _ (subset_of_eq UV_empty)
+    exact Set.inter_subset_inter U'_ss_U V'_ss_V
+  · intro ⟨U, _, V, _, U_in_F, V_in_G, UV_empty⟩
+    exact ⟨U, U_in_F, V, V_in_G, UV_empty⟩
+
 def Filter.InBasis.basis {α : Type _} (F : Filter α) (B : Set (Set α)): Set (Set α) :=
   { S : Set α | S ∈ F ∧ S ∈ B }
 
@@ -1129,6 +1144,23 @@ by
   apply U.ultra
   all_goals assumption
 
+theorem UltrafilterInBasis.eq_of_le (U U' : UltrafilterInBasis B) :
+  U.filter ≤ U'.filter → U = U' :=
+by
+  intro U_le_U'
+  symm
+  rw [mk.injEq]
+  exact unique _ U.in_basis U_le_U'
+
+theorem UltrafilterInBasis.le_of_basis_sets (U U' : UltrafilterInBasis B) :
+  (∀ S : Set α, S ∈ B → S ∈ U' → S ∈ U) → U.filter ≤ U'.filter :=
+by
+  intro h
+  intro S S_in_U'
+  let ⟨T, T_in_B, T_in_U', T_ss_S⟩ := U'.in_basis _ S_in_U'
+  apply Filter.mem_of_superset _ T_ss_S
+  apply h <;> assumption
+
 theorem UltrafilterInBasis.le_of_inf_neBot (U : UltrafilterInBasis B)
   (B_closed : ∀ (b1 b2 : Set α), b1 ∈ B → b2 ∈ B → Set.Nonempty (b1 ∩ b2) → b1 ∩ b2 ∈ B)
   {F : Filter α} (F_in_basis : F.InBasis B)

Rubin/RigidStabilizer.lean

@@ -147,6 +147,7 @@ by
   repeat rw [rigidStabilizer_support]
   rw [Set.subset_inter_iff]
 
+@[simp]
 theorem rigidStabilizer_empty (G α: Type _) [Group G] [MulAction G α] [FaithfulSMul G α]:
   G•[(∅ : Set α)] = ⊥ :=
 by
@@ -159,6 +160,7 @@ by
   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