feat(Inseparable): Prod.map mk mk is a quotient map (#12327)

This is needed to prove continuity of binary arithmetic operations
on the separation quotient.

Author: urkud

Mathlib/Topology/Inseparable.lean

@@ -489,6 +489,16 @@ theorem map_mk_nhdsWithin_preimage (s : Set (SeparationQuotient X)) (x : X) :
   rw [nhdsWithin, ← comap_principal, Filter.push_pull, nhdsWithin, map_mk_nhds]
 #align separation_quotient.map_mk_nhds_within_preimage SeparationQuotient.map_mk_nhdsWithin_preimage
 
+/-- The map `(x, y) ↦ (mk x, mk y)` is a quotient map. -/
+theorem quotientMap_prodMap_mk : QuotientMap (Prod.map mk mk : X × Y → _) := by
+  have hsurj : Surjective (Prod.map mk mk : X × Y → _) := surjective_mk.Prod_map surjective_mk
+  refine quotientMap_iff.2 ⟨hsurj, fun s ↦ ?_⟩
+  refine ⟨fun hs ↦ hs.preimage (continuous_mk.prod_map continuous_mk), fun hs ↦ ?_⟩
+  refine isOpen_iff_mem_nhds.2 <| hsurj.forall.2 fun (x, y) h ↦ ?_
+  rw [Prod.map_mk, nhds_prod_eq, ← map_mk_nhds, ← map_mk_nhds, Filter.prod_map_map_eq',
+    ← nhds_prod_eq, Filter.mem_map]
+  exact hs.mem_nhds h
+
 /-- Lift a map `f : X → α` such that `Inseparable x y → f x = f y` to a map
 `SeparationQuotient X → α`. -/
 def lift (f : X → α) (hf : ∀ x y, (x ~ᵢ y) → f x = f y) : SeparationQuotient X → α := fun x =>