Merge branch 'aliu/left-right-group' into aliu/krullTopology

Author: plp127

Mathlib/Topology/Algebra/IsUniformGroup/Basic.lean

@@ -86,23 +86,47 @@ variable {G : Type*} [Group G] [UniformSpace G] [IsRightUniformGroup G]
 /-- A locally compact right-uniform group is complete. -/
 @[to_additive
 /-- A locally compact right-uniform additive group is complete. -/]
+-- not an instance for performance reasons, see benchmark on PR #42117
 theorem completeSpace_of_weaklyLocallyCompactSpace
     [WeaklyLocallyCompactSpace G] : CompleteSpace G where
   complete {f} hf := by
     open scoped RightActions in
     have : f.NeBot := hf.1
     obtain ⟨K, K_compact, K_mem⟩ := WeaklyLocallyCompactSpace.exists_compact_mem_nhds (1 : G)
-    obtain ⟨x, hx⟩ : ∃ x, ∀ᶠ y in f, y / x ∈ K := by
-      rw [cauchy_iff_le, uniformity_eq_comap_nhds_one, ← tendsto_iff_comap] at hf
+    obtain ⟨x, hx⟩ : ∃ x, ∀ᶠ y in f, y * x⁻¹ ∈ K := by
+      rw [cauchy_iff_le, uniformity_eq_comap_mul_inv_nhds_one, ← tendsto_iff_comap] at hf
       exact hf.eventually_mem K_mem |>.curry.exists
-    simp_rw [div_eq_mul_inv, ← op_smul_eq_mul, MulOpposite.op_inv,
-      ← mem_smul_set_iff_inv_smul_mem] at hx
+    simp_rw [← op_smul_eq_mul, MulOpposite.op_inv, ← mem_smul_set_iff_inv_smul_mem] at hx
     have Kx_complete : IsComplete (K <• x) := K_compact.smul _ |>.isComplete
     obtain ⟨l, -, hl⟩ := Kx_complete f hf (by simpa using hx)
     exact ⟨l, hl⟩
 
 end IsRightUniformGroup
 
+namespace IsLeftUniformGroup
+
+variable {G : Type*} [Group G] [UniformSpace G] [IsLeftUniformGroup G]
+
+/-- A locally compact left-uniform group is complete. -/
+@[to_additive
+/-- A locally compact left-uniform additive group is complete. -/]
+-- not an instance for performance reasons, see benchmark on PR #42117
+theorem completeSpace_of_weaklyLocallyCompactSpace
+    [WeaklyLocallyCompactSpace G] : CompleteSpace G where
+  complete {f} hf := by
+    open scoped RightActions in
+    have : f.NeBot := hf.1
+    obtain ⟨K, K_compact, K_mem⟩ := WeaklyLocallyCompactSpace.exists_compact_mem_nhds (1 : G)
+    obtain ⟨x, hx⟩ : ∃ x, ∀ᶠ y in f, x⁻¹ * y ∈ K := by
+      rw [cauchy_iff_le, uniformity_eq_comap_inv_mul_nhds_one, ← tendsto_iff_comap] at hf
+      exact hf.eventually_mem K_mem |>.curry.exists
+    simp_rw [← smul_eq_mul, ← mem_smul_set_iff_inv_smul_mem] at hx
+    have Kx_complete : IsComplete (x •> K) := K_compact.smul _ |>.isComplete
+    obtain ⟨l, -, hl⟩ := Kx_complete f hf (by simpa using hx)
+    exact ⟨l, hl⟩
+
+end IsLeftUniformGroup
+
 namespace Subgroup
 
 @[to_additive]