feat(SeparationQuotient): add IsTopologicalGroup instance (#23225)

Also move `nhds_mk` and deprecate it in favor of `map_mk_nhds`.

Author: urkud

Mathlib/Topology/Algebra/SeparationQuotient/Basic.lean

@@ -92,7 +92,6 @@ instance instMul [Mul M] [ContinuousMul M] : Mul (SeparationQuotient M) where
 @[to_additive (attr := simp)]
 theorem mk_mul [Mul M] [ContinuousMul M] (a b : M) : mk (a * b) = mk a * mk b := rfl
 
-
 @[to_additive]
 instance instContinuousMul [Mul M] [ContinuousMul M] : ContinuousMul (SeparationQuotient M) where
   continuous_mul := isQuotientMap_prodMap_mk.continuous_iff.2 <| continuous_mk.comp continuous_mul
@@ -197,9 +196,9 @@ instance instGroup [Group G] [IsTopologicalGroup G] : Group (SeparationQuotient
 instance instCommGroup [CommGroup G] [IsTopologicalGroup G] : CommGroup (SeparationQuotient G) :=
   surjective_mk.commGroup mk mk_one mk_mul mk_inv mk_div mk_pow mk_zpow
 
-/-- Neighborhoods in the quotient are precisely the map of neighborhoods in the prequotient. -/
-theorem nhds_mk (x : G) : 𝓝 (mk x) = .map mk (𝓝 x) :=
-  le_antisymm ((SeparationQuotient.isOpenMap_mk).nhds_le x) continuous_quot_mk.continuousAt
+@[to_additive]
+instance instIsTopologicalGroup [Group G] [IsTopologicalGroup G] :
+    IsTopologicalGroup (SeparationQuotient G) where
 
 end Group
 

Mathlib/Topology/Inseparable.lean

@@ -605,9 +605,14 @@ theorem comap_mk_nhds_mk : comap mk (𝓝 (mk x)) = 𝓝 x :=
 theorem comap_mk_nhdsSet_image : comap mk (𝓝ˢ (mk '' s)) = 𝓝ˢ s :=
   (isInducing_mk.nhdsSet_eq_comap _).symm
 
+/-- Push-forward of the neighborhood of a point along the projection to the separation quotient
+is the neighborhood of its equivalence class. -/
 theorem map_mk_nhds : map mk (𝓝 x) = 𝓝 (mk x) := by
   rw [← comap_mk_nhds_mk, map_comap_of_surjective surjective_mk]
 
+@[deprecated map_mk_nhds (since := "2025-03-21")]
+theorem nhds_mk (x : X) : 𝓝 (mk x) = .map mk (𝓝 x) := .symm <| map_mk_nhds ..
+
 theorem map_mk_nhdsSet : map mk (𝓝ˢ s) = 𝓝ˢ (mk '' s) := by
   rw [← comap_mk_nhdsSet_image, map_comap_of_surjective surjective_mk]