feat(Topology/Basic): add TopologicalSpace.ext_isClosed (#9963)

Use it to golf `PrimeSpectrum.localization_comap_inducing`.

Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean

@@ -639,21 +639,14 @@ variable (S)
 
 theorem localization_comap_inducing [Algebra R S] (M : Submonoid R) [IsLocalization M S] :
     Inducing (comap (algebraMap R S)) := by
+  refine ⟨TopologicalSpace.ext_isClosed fun Z ↦ ?_⟩
+  simp_rw [isClosed_induced_iff, isClosed_iff_zeroLocus, @eq_comm _ _ (zeroLocus _),
+    exists_exists_eq_and, preimage_comap_zeroLocus]
   constructor
-  rw [TopologicalSpace.ext_iff]
-  intro U
-  rw [← isClosed_compl_iff, ← @isClosed_compl_iff (X := PrimeSpectrum S) (s := U)]
-  generalize Uᶜ = Z
-  simp_rw [isClosed_induced_iff, isClosed_iff_zeroLocus]
-  constructor
   · rintro ⟨s, rfl⟩
-    refine ⟨_, ⟨algebraMap R S ⁻¹' Ideal.span s, rfl⟩, ?_⟩
-    rw [preimage_comap_zeroLocus, ← zeroLocus_span, ← zeroLocus_span s]
-    congr 2
-    exact congr_arg (zeroLocus ·) <| Submodule.carrier_inj.mpr
-      (IsLocalization.map_comap M S (Ideal.span s))
-  · rintro ⟨_, ⟨t, rfl⟩, rfl⟩
-    rw [preimage_comap_zeroLocus]
+    refine ⟨(Ideal.span s).comap (algebraMap R S), ?_⟩
+    rw [← zeroLocus_span, ← zeroLocus_span s, ← Ideal.map, IsLocalization.map_comap M S]
+  · rintro ⟨s, rfl⟩
     exact ⟨_, rfl⟩
 #align prime_spectrum.localization_comap_inducing PrimeSpectrum.localization_comap_inducing
 

Mathlib/Topology/Basic.lean

@@ -210,6 +210,13 @@ scoped[Topology] notation (name := IsClosed_of) "IsClosed[" t "]" => @IsClosed _
   ⟨fun h => ⟨h⟩, fun h => h.isOpen_compl⟩
 #align is_open_compl_iff isOpen_compl_iff
 
+theorem TopologicalSpace.ext_iff_isClosed {t₁ t₂ : TopologicalSpace X} :
+    t₁ = t₂ ↔ ∀ s, IsClosed[t₁] s ↔ IsClosed[t₂] s := by
+  rw [TopologicalSpace.ext_iff, compl_surjective.forall]
+  simp only [@isOpen_compl_iff _ t₁, @isOpen_compl_iff _ t₂]
+
+alias ⟨_, TopologicalSpace.ext_isClosed⟩ := TopologicalSpace.ext_iff_isClosed
+
 -- porting note: new lemma
 theorem isClosed_const {p : Prop} : IsClosed { _a : X | p } := ⟨isOpen_const (p := ¬p)⟩