refactor(topology): make is_closed a class (#6552)

In `lean-liquid`, it would be useful that `is_closed` would be a class, to be able to infer a normed space structure on `E/F` when `F` is a closed subspace of a normed space `E`. This is implemented in this PR. This is mostly straightforward: the only proofs that need fixing are those abusing defeqness, so the new version makes them clearer IMHO.

Co-authored-by: Johan Commelin <johan@commelin.net>

src/algebraic_geometry/prime_spectrum.lean

@@ -323,7 +323,7 @@ by simp only [@eq_comm _ Uᶜ]; refl
 
 lemma is_closed_iff_zero_locus (Z : set (prime_spectrum R)) :
   is_closed Z ↔ ∃ s, Z = zero_locus s :=
-by rw [is_closed, is_open_iff, compl_compl]
+by rw [← is_open_compl_iff, is_open_iff, compl_compl]
 
 lemma is_closed_zero_locus (s : set R) :
   is_closed (zero_locus s) :=

src/analysis/convex/integral.lean

@@ -50,7 +50,8 @@ private lemma convex.smul_integral_mem_of_measurable
   (hμ : μ ≠ 0) {f : α → E} (hfs : ∀ᵐ x ∂μ, f x ∈ s) (hfi : integrable f μ) (hfm : measurable f) :
   (μ univ).to_real⁻¹ • ∫ x, f x ∂μ ∈ s :=
 begin
-  rcases eq_empty_or_nonempty s with rfl|⟨y₀, h₀⟩, { refine (hμ _).elim, simpa using hfs },
+  unfreezingI { rcases eq_empty_or_nonempty s with rfl|⟨y₀, h₀⟩ },
+  { refine (hμ _).elim, simpa using hfs },
   rw ← hsc.closure_eq at hfs,
   have hc : integrable (λ _, y₀) μ := integrable_const _,
   set F : ℕ → simple_func α E := simple_func.approx_on f hfm s y₀ h₀,

src/data/analysis/topology.lean

@@ -92,7 +92,7 @@ is_open_iff_mem_nhds.trans $ ball_congr $ λ a h, F.mem_nhds
 
 theorem is_closed_iff [topological_space α] (F : realizer α) {s : set α} :
   is_closed s ↔ ∀ a, (∀ b, a ∈ F.F b → ∃ z, z ∈ F.F b ∩ s) → a ∈ s :=
-F.is_open_iff.trans $ forall_congr $ λ a,
+is_open_compl_iff.symm.trans $ F.is_open_iff.trans $ forall_congr $ λ a,
 show (a ∉ s → (∃ (b : F.σ), a ∈ F.F b ∧ ∀ z ∈ F.F b, z ∉ s)) ↔ _,
 by haveI := classical.prop_decidable; rw [not_imp_comm];
    simp [not_exists, not_and, not_forall, and_comm]

src/measure_theory/borel_space.lean

@@ -61,7 +61,7 @@ begin
   intros x hx,
   apply measurable_set.of_compl,
   apply generate_measurable.basic,
-  exact is_closed_singleton
+  exact is_closed_singleton.is_open_compl
 end
 
 lemma borel_eq_generate_from_of_subbasis {s : set (set α)}
@@ -190,7 +190,7 @@ lemma measurable_set_of_continuous_at {β} [emetric_space β] (f : α → β) :
 (is_Gδ_set_of_continuous_at f).measurable_set
 
 lemma is_closed.measurable_set (h : is_closed s) : measurable_set s :=
-h.measurable_set.of_compl
+h.is_open_compl.measurable_set.of_compl
 
 lemma is_compact.measurable_set [t2_space α] (h : is_compact s) : measurable_set s :=
 h.is_closed.measurable_set

src/topology/algebra/open_subgroup.lean

@@ -94,6 +94,7 @@ instance : inhabited (open_subgroup G) := ⟨⊤⟩
 @[to_additive]
 lemma is_closed [has_continuous_mul G] (U : open_subgroup G) : is_closed (U : set G) :=
 begin
+  apply is_open_compl_iff.1,
   refine is_open_iff_forall_mem_open.2 (λ x hx, ⟨(λ y, y * x⁻¹) ⁻¹' U, _, _, _⟩),
   { intros u hux,
     simp only [set.mem_preimage, set.mem_compl_iff, mem_coe] at hux hx ⊢,

src/topology/algebra/ordered.lean

@@ -234,14 +234,14 @@ section partial_order
 variables [topological_space α] [partial_order α] [t : order_closed_topology α]
 include t
 
-private lemma is_closed_eq : is_closed {p : α × α | p.1 = p.2} :=
+private lemma is_closed_eq_aux : is_closed {p : α × α | p.1 = p.2} :=
 by simp only [le_antisymm_iff];
    exact is_closed_inter t.is_closed_le' (is_closed_le continuous_snd continuous_fst)
 
 @[priority 90] -- see Note [lower instance priority]
 instance order_closed_topology.to_t2_space : t2_space α :=
 { t2 :=
-  have is_open {p : α × α | p.1 ≠ p.2}, from is_closed_eq,
+  have is_open {p : α × α | p.1 ≠ p.2} := is_closed_eq_aux.is_open_compl,
   assume a b h,
   let ⟨u, v, hu, hv, ha, hb, h⟩ := is_open_prod_iff.mp this a b h in
   ⟨u, v, hu, hv, ha, hb,
@@ -260,7 +260,7 @@ by { simp_rw [← is_closed_compl_iff, compl_set_of, not_lt],
 
 lemma is_open_lt [topological_space β] {f g : β → α} (hf : continuous f) (hg : continuous g) :
   is_open {b | f b < g b} :=
-by simp [lt_iff_not_ge, -not_le]; exact is_closed_le hg hf
+by simp [lt_iff_not_ge, -not_le]; exact (is_closed_le hg hf).is_open_compl
 
 variables {a b : α}
 
@@ -905,7 +905,7 @@ end
 @[priority 100] -- see Note [lower instance priority]
 instance order_topology.to_order_closed_topology : order_closed_topology α :=
 { is_closed_le' :=
-    is_open_prod_iff.mpr $ assume a₁ a₂ (h : ¬ a₁ ≤ a₂),
+    is_open_compl_iff.1 $ is_open_prod_iff.mpr $ assume a₁ a₂ (h : ¬ a₁ ≤ a₂),
       have h : a₂ < a₁, from lt_of_not_ge h,
       let ⟨u, v, hu, hv, ha₁, ha₂, h⟩ := order_separated h in
       ⟨v, u, hv, hu, ha₂, ha₁, assume ⟨b₁, b₂⟩ ⟨h₁, h₂⟩, not_le_of_gt $ h b₂ h₂ b₁ h₁⟩ }
@@ -915,7 +915,7 @@ lemma order_topology.t2_space : t2_space α := by apply_instance
 @[priority 100] -- see Note [lower instance priority]
 instance order_topology.regular_space : regular_space α :=
 { regular := assume s a hs ha,
-    have hs' : sᶜ ∈ 𝓝 a, from mem_nhds_sets hs ha,
+    have hs' : sᶜ ∈ 𝓝 a, from mem_nhds_sets hs.is_open_compl ha,
     have ∃t:set α, is_open t ∧ (∀l∈ s, l < a → l ∈ t) ∧ 𝓝[t] a = ⊥,
       from by_cases
         (assume h : ∃l, l < a,
@@ -2365,7 +2365,7 @@ begin
   have zt : z ∈ tᶜ, from λ zt, hst ⟨z, xyab $ Ico_subset_Icc_self hz, zs, zt⟩,
   have : tᶜ ∩ Ioc z y ∈ 𝓝[Ioi z] z,
   { rw [← nhds_within_Ioc_eq_nhds_within_Ioi hz.2],
-    exact mem_nhds_within.2 ⟨tᶜ, ht, zt, subset.refl _⟩},
+    exact mem_nhds_within.2 ⟨tᶜ, ht.is_open_compl, zt, subset.refl _⟩},
   apply mem_sets_of_superset this,
   have : Ioc z y ⊆ s ∪ t, from λ w hw, hab (xyab ⟨le_trans hz.1 (le_of_lt hw.1), hw.2⟩),
   exact λ w ⟨wt, wzy⟩, (this wzy).elim id (λ h, (wt h).elim)

src/topology/basic.lean

@@ -154,19 +154,23 @@ lemma is_open_and : is_open {a | p₁ a} → is_open {a | p₂ a} → is_open {a
 is_open_inter
 
 /-- A set is closed if its complement is open -/
-def is_closed (s : set α) : Prop := is_open sᶜ
+class is_closed (s : set α) : Prop :=
+(is_open_compl : is_open sᶜ)
+
+@[simp] lemma is_open_compl_iff {s : set α} : is_open sᶜ ↔ is_closed s :=
+⟨λ h, ⟨h⟩, λ h, h.is_open_compl⟩
 
 @[simp] lemma is_closed_empty : is_closed (∅ : set α) :=
-by unfold is_closed; rw compl_empty; exact is_open_univ
+by { rw [← is_open_compl_iff, compl_empty], exact is_open_univ }
 
 @[simp] lemma is_closed_univ : is_closed (univ : set α) :=
-by unfold is_closed; rw compl_univ; exact is_open_empty
+by { rw [← is_open_compl_iff, compl_univ], exact is_open_empty }
 
 lemma is_closed_union : is_closed s₁ → is_closed s₂ → is_closed (s₁ ∪ s₂) :=
-λ h₁ h₂, by unfold is_closed; rw compl_union; exact is_open_inter h₁ h₂
+λ h₁ h₂, by { rw [← is_open_compl_iff] at *, rw compl_union, exact is_open_inter h₁ h₂ }
 
 lemma is_closed_sInter {s : set (set α)} : (∀t ∈ s, is_closed t) → is_closed (⋂₀ s) :=
-by simpa only [is_closed, compl_sInter, sUnion_image] using is_open_bUnion
+by simpa only [← is_open_compl_iff, compl_sInter, sUnion_image] using is_open_bUnion
 
 lemma is_closed_Inter {f : ι → set α} (h : ∀i, is_closed (f i)) : is_closed (⋂i, f i ) :=
 is_closed_sInter $ assume t ⟨i, (heq : f i = t)⟩, heq ▸ h i
@@ -175,16 +179,17 @@ lemma is_closed_bInter {s : set β} {f : β → set α} (h : ∀ i ∈ s, is_clo
   is_closed (⋂ i ∈ s, f i) :=
 is_closed_Inter $ λ i, is_closed_Inter $ h i
 
-@[simp] lemma is_open_compl_iff {s : set α} : is_open sᶜ ↔ is_closed s := iff.rfl
-
 @[simp] lemma is_closed_compl_iff {s : set α} : is_closed sᶜ ↔ is_open s :=
 by rw [←is_open_compl_iff, compl_compl]
 
+lemma is_open.is_closed_compl {s : set α} (hs : is_open s) : is_closed sᶜ :=
+is_closed_compl_iff.2 hs
+
 lemma is_open_diff {s t : set α} (h₁ : is_open s) (h₂ : is_closed t) : is_open (s \ t) :=
 is_open_inter h₁ $ is_open_compl_iff.mpr h₂
 
 lemma is_closed_inter (h₁ : is_closed s₁) (h₂ : is_closed s₂) : is_closed (s₁ ∩ s₂) :=
-by rw [is_closed, compl_inter]; exact is_open_union h₁ h₂
+by { rw [← is_open_compl_iff] at *, rw compl_inter, exact is_open_union h₁ h₂ }
 
 lemma is_closed_bUnion {s : set β} {f : β → set α} (hs : finite s) :
   (∀i∈s, is_closed (f i)) → is_closed (⋃i∈s, f i) :=
@@ -359,9 +364,8 @@ subset.trans interior_subset subset_closure
 
 lemma closure_eq_compl_interior_compl {s : set α} : closure s = (interior sᶜ)ᶜ :=
 begin
-  unfold interior closure is_closed,
-  rw [compl_sUnion, compl_image_set_of],
-  simp only [compl_subset_compl]
+  rw [interior, closure, compl_sUnion, compl_image_set_of],
+  simp only [compl_subset_compl, is_open_compl_iff],
 end
 
 @[simp] lemma interior_compl {s : set α} : interior sᶜ = (closure s)ᶜ :=
@@ -376,7 +380,7 @@ theorem mem_closure_iff {s : set α} {a : α} :
   have s ⊆ oᶜ, from λ x xs xo, os ⟨x, xo, xs⟩,
   closure_minimal this (is_closed_compl_iff.2 oo) h ao,
 λ H c ⟨h₁, h₂⟩, classical.by_contradiction $ λ nc,
-  let ⟨x, hc, hs⟩ := (H _ h₁ nc) in hc (h₂ hs)⟩
+  let ⟨x, hc, hs⟩ := (H _ h₁.is_open_compl nc) in hc (h₂ hs)⟩
 
 /-- A set is dense in a topological space if every point belongs to its closure. -/
 def dense (s : set α) : Prop := ∀ x, x ∈ closure s
@@ -978,11 +982,12 @@ end
 
 lemma locally_finite.is_closed_Union {f : β → set α}
   (h₁ : locally_finite f) (h₂ : ∀i, is_closed (f i)) : is_closed (⋃i, f i) :=
-is_open_iff_nhds.mpr $ assume a, assume h : a ∉ (⋃i, f i),
+is_open_compl_iff.1 $ is_open_iff_nhds.mpr $ assume a, assume h : a ∉ (⋃i, f i),
   have ∀i, a ∈ (f i)ᶜ,
     from assume i hi, h $ mem_Union.2 ⟨i, hi⟩,
   have ∀i, (f i)ᶜ ∈ (𝓝 a),
-    by simp only [mem_nhds_sets_iff]; exact assume i, ⟨(f i)ᶜ, subset.refl _, h₂ i, this i⟩,
+    by simp only [mem_nhds_sets_iff]; exact assume i,
+      ⟨(f i)ᶜ, subset.refl _, (h₂ i).is_open_compl, this i⟩,
   let ⟨t, h_sets, (h_fin : finite {i | (f i ∩ t).nonempty })⟩ := h₁ a in
   calc 𝓝 a ≤ 𝓟 (t ∩ (⋂ i∈{i | (f i ∩ t).nonempty }, (f i)ᶜ)) : by simp *
   ... ≤ 𝓟 (⋃i, f i)ᶜ :
@@ -1111,7 +1116,7 @@ from continuous_at.comp (hx.symm ▸ ihn) hf
 
 lemma continuous_iff_is_closed {f : α → β} :
   continuous f ↔ (∀s, is_closed s → is_closed (f ⁻¹' s)) :=
-⟨assume hf s hs, continuous_def.1 hf sᶜ hs,
+⟨assume hf s hs, by simpa using (continuous_def.1 hf sᶜ hs.is_open_compl).is_closed_compl,
   assume hf, continuous_def.2 $ assume s,
     by rw [←is_closed_compl_iff, ←is_closed_compl_iff]; exact hf _⟩
 

src/topology/category/Compactum.lean

@@ -139,6 +139,7 @@ instance {X : Compactum} : topological_space X :=
 theorem is_closed_iff {X : Compactum} (S : set X) : is_closed S ↔
   (∀ F : ultrafilter X, S ∈ F → X.str F ∈ S) :=
 begin
+  rw ← is_open_compl_iff,
   split,
   { intros cond F h,
     by_contradiction c,
@@ -267,7 +268,7 @@ begin
   { intros A hA h,
     by_contradiction H,
     rw le_nhds_iff at cond,
-    specialize cond Aᶜ H hA,
+    specialize cond Aᶜ H hA.is_open_compl,
     rw [ultrafilter.mem_coe, ultrafilter.compl_mem_iff_not_mem] at cond,
     contradiction },
   -- If A ∈ F, then x ∈ cl A.

src/topology/connected.lean

@@ -294,7 +294,7 @@ theorem is_clopen_iff [preconnected_space α] {s : set α} : is_clopen s ↔ s =
 ⟨λ hs, classical.by_contradiction $ λ h,
   have h1 : s ≠ ∅ ∧ sᶜ ≠ ∅, from ⟨mt or.inl h,
     mt (λ h2, or.inr $ (by rw [← compl_compl s, h2, compl_empty] : s = univ)) h⟩,
-  let ⟨_, h2, h3⟩ := nonempty_inter hs.1 hs.2 (union_compl_self s)
+  let ⟨_, h2, h3⟩ := nonempty_inter hs.1 hs.2.is_open_compl (union_compl_self s)
     (ne_empty_iff_nonempty.1 h1.1) (ne_empty_iff_nonempty.1 h1.2) in
   h3 h2,
 by rintro (rfl | rfl); [exact is_clopen_empty, exact is_clopen_univ]⟩
@@ -874,7 +874,8 @@ begin
     rw ←connected_components_preimage_singleton,
     exact is_connected_connected_component },
   refine λ T, ⟨λ hT, hT.preimage continuous_quotient_mk, λ hT, _⟩,
-  rwa [←is_open_compl_iff, ←preimage_compl, quotient_map_quotient_mk.is_open_preimage] at hT,
+  rwa [← is_open_compl_iff, ← preimage_compl, quotient_map_quotient_mk.is_open_preimage,
+    is_open_compl_iff] at hT,
 end
 
 /-- Functoriality of `connected_components` -/

src/topology/constructions.lean

@@ -750,7 +750,7 @@ lemma is_open_sigma_iff {s : set (sigma σ)} : is_open s ↔ ∀ i, is_open (sig
 by simp only [is_open_supr_iff, is_open_coinduced]
 
 lemma is_closed_sigma_iff {s : set (sigma σ)} : is_closed s ↔ ∀ i, is_closed (sigma.mk i ⁻¹' s) :=
-is_open_sigma_iff
+by simp [← is_open_compl_iff, is_open_sigma_iff]
 
 lemma is_open_map_sigma_mk {i : ι} : is_open_map (@sigma.mk ι σ i) :=
 begin

src/topology/homeomorph.lean

@@ -141,7 +141,7 @@ h.quotient_map.is_open_preimage
 by rw [← preimage_symm, is_open_preimage]
 
 @[simp] lemma is_closed_preimage (h : α ≃ₜ β) {s : set β} : is_closed (h ⁻¹' s) ↔ is_closed s :=
-by simp only [is_closed, ← preimage_compl, is_open_preimage]
+by simp only [← is_open_compl_iff, ← preimage_compl, is_open_preimage]
 
 @[simp] lemma is_closed_image (h : α ≃ₜ β) {s : set α} : is_closed (h '' s) ↔ is_closed s :=
 by rw [← preimage_symm, is_closed_preimage]

src/topology/metric_space/basic.lean

@@ -1399,7 +1399,7 @@ ball with the same center and a strictly smaller radius that includes `s`. -/
 lemma exists_pos_lt_subset_ball (hr : 0 < r) (hs : is_closed s) (h : s ⊆ ball x r) :
   ∃ r' ∈ Ioo 0 r, s ⊆ ball x r' :=
 begin
-  rcases eq_empty_or_nonempty s with rfl|hne,
+  unfreezingI { rcases eq_empty_or_nonempty s with rfl|hne },
   { exact ⟨r / 2, ⟨half_pos hr, half_lt_self hr⟩, empty_subset _⟩ },
   have : is_compact s,
     from compact_of_is_closed_subset (proper_space.compact_ball x r) hs
@@ -1417,7 +1417,7 @@ lemma exists_lt_subset_ball (hs : is_closed s) (h : s ⊆ ball x r) :
   ∃ r' < r, s ⊆ ball x r' :=
 begin
   cases le_or_lt r 0 with hr hr,
-  { rw [ball_eq_empty_iff_nonpos.2 hr, subset_empty_iff] at h, subst s,
+  { rw [ball_eq_empty_iff_nonpos.2 hr, subset_empty_iff] at h, unfreezingI { subst s },
     exact (no_bot r).imp (λ r' hr', ⟨hr', empty_subset _⟩) },
   { exact (exists_pos_lt_subset_ball hr hs h).imp (λ r' hr', ⟨hr'.fst.2, hr'.snd⟩) }
 end

src/topology/metric_space/emetric_space.lean

@@ -589,7 +589,7 @@ theorem is_open_ball : is_open (ball x ε) :=
 is_open_iff.2 $ λ y, exists_ball_subset_ball
 
 theorem is_closed_ball_top : is_closed (ball x ⊤) :=
-is_open_iff.2 $ λ y hy, ⟨⊤, ennreal.coe_lt_top, subset_compl_iff_disjoint.2 $
+is_open_compl_iff.1 $ is_open_iff.2 $ λ y hy, ⟨⊤, ennreal.coe_lt_top, subset_compl_iff_disjoint.2 $
   ball_disjoint $ by { rw ennreal.top_add, exact le_of_not_lt hy }⟩
 
 theorem ball_mem_nhds (x : α) {ε : ℝ≥0∞} (ε0 : 0 < ε) : ball x ε ∈ 𝓝 x :=

src/topology/order.lean

@@ -204,7 +204,7 @@ instance discrete_topology_bot (α : Type*) : @discrete_topology α ⊥ :=
 
 @[simp] lemma is_closed_discrete [topological_space α] [discrete_topology α] (s : set α) :
   is_closed s :=
-(discrete_topology.eq_bot α).symm ▸ trivial
+is_open_compl_iff.1 $ (discrete_topology.eq_bot α).symm ▸ trivial
 
 lemma continuous_of_discrete_topology [topological_space α] [discrete_topology α]
   [topological_space β] {f : α → β} : continuous f :=
@@ -272,9 +272,11 @@ iff.rfl
 
 lemma is_closed_induced_iff [t : topological_space β] {s : set α} {f : α → β} :
   @is_closed α (t.induced f) s ↔ (∃t, is_closed t ∧ f ⁻¹' t = s) :=
-⟨assume ⟨t, ht, heq⟩, ⟨tᶜ, is_closed_compl_iff.2 ht,
-    by simp only [preimage_compl, heq, compl_compl]⟩,
-  assume ⟨t, ht, heq⟩, ⟨tᶜ, ht, by simp only [preimage_compl, heq.symm]⟩⟩
+begin
+  simp only [← is_open_compl_iff, is_open_induced_iff],
+  exact ⟨λ ⟨t, ht, heq⟩, ⟨tᶜ, by rwa compl_compl, by simp [preimage_compl, heq, compl_compl]⟩,
+         λ ⟨t, ht, heq⟩, ⟨tᶜ, ht, by simp only [preimage_compl, heq.symm]⟩⟩
+end
 
 /-- Given `f : α → β` and a topology on `α`, the coinduced topology on `β` is defined
   such that `s:set β` is open if the preimage of `s` is open. This is the finest topology that
@@ -648,6 +650,6 @@ begin
 end
 
 lemma is_closed_infi_iff {s : set α} : @is_closed _ (⨆ i, t i) s ↔ ∀ i, @is_closed _ (t i) s :=
-is_open_supr_iff
+by simp [← is_open_compl_iff, is_open_supr_iff]
 
 end infi

src/topology/paracompact.lean

@@ -160,7 +160,8 @@ begin
   -- Next we choose a finite covering `B (c n i) (r n i)` of each
   -- `Kdiff (n + 1) ∩ s` such that `B (c n i) (r n i) ∩ s` is disjoint with `K n`
   have : ∀ n (x : Kdiff (n + 1) ∩ s), (K n)ᶜ ∈ 𝓝 (x : X),
-    from λ n x, mem_nhds_sets (K.is_closed n) (λ hx', x.2.1.2 $ K.subset_interior_succ _ hx'),
+    from λ n x, mem_nhds_sets (K.is_closed n).is_open_compl
+      (λ hx', x.2.1.2 $ K.subset_interior_succ _ hx'),
   haveI : ∀ n (x : Kdiff n ∩ s), nonempty (ι x) := λ n x, (hB x x.2.2).nonempty,
   choose! r hrp hr using (λ n (x : Kdiff (n + 1) ∩ s), (hB x x.2.2).mem_iff.1 (this n x)),
   have hxr : ∀ n x (hx : x ∈ Kdiff (n + 1) ∩ s), B x (r n ⟨x, hx⟩) ∈ 𝓝 x,
@@ -245,8 +246,8 @@ begin
     intros s t hs ht H, choose u v hu hv hxu htv huv using set_coe.forall'.1 H,
     rcases precise_refinement_set hs u hu (λ x hx, mem_Union.2 ⟨⟨x, hx⟩, hxu _⟩)
       with ⟨u', hu'o, hcov', hu'fin, hsub⟩,
-    refine ⟨⋃ i, u' i, (closure (⋃ i, u' i))ᶜ, is_open_Union hu'o, is_closed_closure, hcov', _,
-      disjoint_compl_right.mono le_rfl (compl_le_compl subset_closure)⟩,
+    refine ⟨⋃ i, u' i, (closure (⋃ i, u' i))ᶜ, is_open_Union hu'o, is_closed_closure.is_open_compl,
+      hcov', _, disjoint_compl_right.mono le_rfl (compl_le_compl subset_closure)⟩,
     rw [hu'fin.closure_Union, compl_Union, subset_Inter_iff],
     refine λ i x hxt hxu, absurd (htv i hxt) (closure_minimal _ (is_closed_compl_iff.2 $ hv _) hxu),
     exact λ y hyu hyv, huv i ⟨hsub _ hyu, hyv⟩ },

src/topology/separation.lean

@@ -136,7 +136,7 @@ lemma is_closed_singleton [t1_space α] {x : α} : is_closed ({x} : set α) :=
 t1_space.t1 x
 
 lemma is_open_compl_singleton [t1_space α] {x : α} : is_open ({x}ᶜ : set α) :=
-is_closed_singleton
+is_closed_singleton.is_open_compl
 
 lemma is_open_ne [t1_space α] {x : α} : is_open {y | y ≠ x} :=
 is_open_compl_singleton
@@ -151,7 +151,7 @@ instance t1_space.t0_space [t1_space α] : t0_space α :=
 ⟨λ x y h, ⟨{z | z ≠ y}, is_open_ne, or.inl ⟨h, not_not_intro rfl⟩⟩⟩
 
 lemma compl_singleton_mem_nhds [t1_space α] {x y : α} (h : y ≠ x) : {x}ᶜ ∈ 𝓝 y :=
-mem_nhds_sets is_closed_singleton $ by rwa [mem_compl_eq, mem_singleton_iff]
+mem_nhds_sets is_open_compl_singleton $ by rwa [mem_compl_eq, mem_singleton_iff]
 
 @[simp] lemma closure_singleton [t1_space α] {a : α} :
   closure ({a} : set α) = {a} :=
@@ -280,7 +280,7 @@ t2_space.t2 x y h
 
 @[priority 100] -- see Note [lower instance priority]
 instance t2_space.t1_space [t2_space α] : t1_space α :=
-⟨λ x, is_open_iff_forall_mem_open.2 $ λ y hxy,
+⟨λ x, is_open_compl_iff.1 $ is_open_iff_forall_mem_open.2 $ λ y hxy,
 let ⟨u, v, hu, hv, hyu, hxv, huv⟩ := t2_separation (mt mem_singleton_of_eq hxy) in
 ⟨u, λ z hz1 hz2, (ext_iff.1 huv x).1 ⟨mem_singleton_iff.1 hz2 ▸ hz1, hxv⟩, hu, hyu⟩⟩
 
@@ -326,7 +326,7 @@ begin
     intros x y hxy,
     have : (x, y) ∈ (diagonal α)ᶜ, by rwa [mem_compl_iff],
     obtain ⟨t, t_sub, t_op, xyt⟩ : ∃ t ⊆ (diagonal α)ᶜ, is_open t ∧ (x, y) ∈ t :=
-      is_open_iff_forall_mem_open.mp h _ this,
+      is_open_iff_forall_mem_open.mp h.is_open_compl _ this,
     rcases is_open_prod_iff.mp t_op x y xyt with ⟨U, V, U_op, V_op, xU, yV, H⟩,
     use [U, V, U_op, V_op, xU, yV],
     have := subset.trans H t_sub,
@@ -560,11 +560,11 @@ lemma compact_compact_separated [t2_space α] {s t : set α}
   (hs : is_compact s) (ht : is_compact t) (hst : s ∩ t = ∅) :
   ∃u v : set α, is_open u ∧ is_open v ∧ s ⊆ u ∧ t ⊆ v ∧ u ∩ v = ∅ :=
 by simp only [prod_subset_compl_diagonal_iff_disjoint.symm] at ⊢ hst;
-   exact generalized_tube_lemma hs ht is_closed_diagonal hst
+   exact generalized_tube_lemma hs ht is_closed_diagonal.is_open_compl hst
 
 /-- In a `t2_space`, every compact set is closed. -/
 lemma is_compact.is_closed [t2_space α] {s : set α} (hs : is_compact s) : is_closed s :=
-is_open_compl_iff.mpr $ is_open_iff_forall_mem_open.mpr $ assume x hx,
+is_open_compl_iff.1 $ is_open_iff_forall_mem_open.mpr $ assume x hx,
   let ⟨u, v, uo, vo, su, xv, uv⟩ :=
     compact_compact_separated hs (compact_singleton : is_compact {x})
       (by rwa [inter_comm, ←subset_compl_iff_disjoint, singleton_subset_iff]) in