refactor(topology/*): Use disjoint (#14950)

Replace uses of `s ∩ t = ∅` by `disjoint s t` in the topology library. This shortens proofs.

src/data/set/basic.lean

@@ -955,10 +955,6 @@ theorem subset_union_compl_iff_inter_subset {s t u : set α} : s ⊆ t ∪ uᶜ
 theorem compl_subset_iff_union {s t : set α} : sᶜ ⊆ t ↔ s ∪ t = univ :=
 iff.symm $ eq_univ_iff_forall.trans $ forall_congr $ λ a, or_iff_not_imp_left
 
--- TODO@Yaël: This duplicates `subset_compl_iff_disjoint_right`
-theorem subset_compl_iff_disjoint {s t : set α} : s ⊆ tᶜ ↔ s ∩ t = ∅ :=
-iff.trans (forall_congr $ λ a, and_imp.symm) subset_empty_iff
-
 @[simp] lemma subset_compl_singleton_iff {a : α} {s : set α} : s ⊆ {a}ᶜ ↔ a ∉ s :=
 subset_compl_comm.trans singleton_subset_iff
 

src/field_theory/krull_topology.lean

@@ -244,12 +244,8 @@ lemma krull_topology_t2 {K L : Type*} [field K] [field L] [algebra K L]
     rcases h_nhd with ⟨W, hWH, hW_open, hW_1⟩,
     refine ⟨left_coset f W, left_coset g W,
       ⟨hW_open.left_coset f, hW_open.left_coset g, ⟨1, hW_1, mul_one _⟩, ⟨1, hW_1, mul_one _⟩, _⟩⟩,
-    by_contra h_nonempty,
-    change left_coset f W ∩ left_coset g W ≠ ∅ at h_nonempty,
-    rw set.ne_empty_iff_nonempty at h_nonempty,
-    rcases h_nonempty with ⟨σ, ⟨⟨w1, hw1, hfw1⟩, ⟨w2, hw2, hgw2⟩⟩⟩,
-    rw ← hgw2 at hfw1,
-    rename hfw1 h,
+    rintro σ ⟨⟨w1, hw1, h⟩, w2, hw2, hgw2⟩,
+    rw ← hgw2 at h,
     rw [eq_inv_mul_iff_mul_eq.symm, ← mul_assoc, mul_inv_eq_iff_eq_mul.symm] at h,
     have h_in_H : w1 * w2⁻¹ ∈ H := H.mul_mem (hWH hw1) (H.inv_mem (hWH hw2)),
     rw h at h_in_H,

src/group_theory/group_action/basic.lean

@@ -211,24 +211,22 @@ begin
     simp only [inv_smul_smul], },
 end
 
-@[to_additive]
-lemma image_inter_image_iff (U V : set β) :
-  (quotient.mk '' U) ∩ (quotient.mk '' V) = ∅ ↔ ∀ x ∈ U, ∀ a : α, a • x ∉ V :=
+@[to_additive] lemma disjoint_image_image_iff {U V : set β} :
+  disjoint (quotient.mk '' U) (quotient.mk '' V) ↔ ∀ x ∈ U, ∀ a : α, a • x ∉ V :=
 begin
   set f : β → quotient (mul_action.orbit_rel α β) := quotient.mk,
-  rw set.eq_empty_iff_forall_not_mem,
-  split,
-  { intros h x x_in_U a a_in_V,
-    refine h (f (a • x)) ⟨⟨x, x_in_U, _⟩, ⟨a • x, a_in_V, rfl⟩⟩,
-    rw quotient.eq,
-    use a⁻¹,
-    simp, },
-  { rintros h x ⟨⟨y, hy₁, hy₂⟩, ⟨z, hz₁, hz₂⟩⟩,
-    obtain ⟨a, ha⟩ := quotient.exact (hz₂.trans hy₂.symm),
-    apply h y hy₁ a,
-    convert hz₁, },
+  refine ⟨λ h x x_in_U a a_in_V, h ⟨⟨x, x_in_U, quotient.sound ⟨a⁻¹, _⟩⟩, ⟨a • x, a_in_V, rfl⟩⟩, _⟩,
+  { simp },
+  { rintro h x ⟨⟨y, hy₁, hy₂⟩, ⟨z, hz₁, hz₂⟩⟩,
+    obtain ⟨a, rfl⟩ := quotient.exact (hz₂.trans hy₂.symm),
+    exact h y hy₁ a hz₁ }
 end
 
+@[to_additive]
+lemma image_inter_image_iff (U V : set β) :
+  (quotient.mk '' U) ∩ (quotient.mk '' V) = ∅ ↔ ∀ x ∈ U, ∀ a : α, a • x ∉ V :=
+set.disjoint_iff_inter_eq_empty.symm.trans disjoint_image_image_iff
+
 variables (α) (β)
 local notation `Ω` := (quotient $ orbit_rel α β)
 

src/measure_theory/constructions/polish.lean

@@ -372,7 +372,7 @@ begin
       exact (Iy i n hi).symm } },
   -- consider two open sets separating `f x` and `g y`.
   obtain ⟨u, v, u_open, v_open, xu, yv, huv⟩ :
-    ∃ u v : set α, is_open u ∧ is_open v ∧ f x ∈ u ∧ g y ∈ v ∧ u ∩ v = ∅,
+    ∃ u v : set α, is_open u ∧ is_open v ∧ f x ∈ u ∧ g y ∈ v ∧ disjoint u v,
   { apply t2_separation,
     exact disjoint_iff_forall_ne.1 h _ (mem_range_self _) _ (mem_range_self _) },
   letI : metric_space (ℕ → ℕ) := metric_space_nat_nat,
@@ -392,8 +392,7 @@ begin
       assume z hz,
       rw mem_cylinder_iff_dist_le at hz,
       exact hz.trans_lt (hn.trans_le (min_le_left _ _)) },
-    { have D : disjoint v u, by rwa [disjoint_iff_inter_eq_empty, inter_comm],
-      apply disjoint.mono_left _ D,
+    { refine disjoint.mono_left _ huv.symm,
       change g '' cylinder y n ⊆ v,
       rw image_subset_iff,
       apply subset.trans _ hεy,
@@ -545,9 +544,7 @@ begin
     -- assume for a contradiction that `f z ≠ x`.
     by_contra' hne,
     -- introduce disjoint open sets `v` and `w` separating `f z` from `x`.
-    obtain ⟨v, w, v_open, w_open, fzv, xw, hvw⟩ :
-      ∃ v w : set β, is_open v ∧ is_open w ∧ f z ∈ v ∧ x ∈ w ∧ v ∩ w = ∅ :=
-        t2_separation hne,
+    obtain ⟨v, w, v_open, w_open, fzv, xw, hvw⟩ := t2_separation hne,
     obtain ⟨δ, δpos, hδ⟩ : ∃ δ > (0 : ℝ), ball z δ ⊆ f ⁻¹' v,
     { apply metric.mem_nhds_iff.1,
       exact f_cont.continuous_at.preimage_mem_nhds (v_open.mem_nhds fzv) },
@@ -568,7 +565,7 @@ begin
     have : x ∈ closure v := closure_mono fsnv (hxs n).1,
     -- this is a contradiction, as `x` is supposed to belong to `w`, which is disjoint from
     -- the closure of `v`.
-    exact disjoint_left.1 ((disjoint_iff_inter_eq_empty.2 hvw).closure_left w_open) this xw }
+    exact disjoint_left.1 (hvw.closure_left w_open) this xw }
 end
 
 theorem _root_.is_closed.measurable_set_image_of_continuous_on_inj_on

src/measure_theory/function/continuous_map_dense.lean

@@ -101,9 +101,7 @@ begin
     simpa using ennreal.add_lt_add_left hsμ.ne hη_pos' },
   obtain ⟨F, Fs, F_closed, μF⟩ : ∃ F ⊆ s, is_closed F ∧ μ s < μ F + ↑η :=
     hs.exists_is_closed_lt_add hsμ.ne hη_pos'.ne',
-  have : disjoint uᶜ F,
-  { rw [set.disjoint_iff_inter_eq_empty, set.inter_comm, ← set.subset_compl_iff_disjoint],
-    simpa using Fs.trans su },
+  have : disjoint uᶜ F := (Fs.trans su).disjoint_compl_left,
   have h_μ_sdiff : μ (u \ F) ≤ 2 * η,
   { have hFμ : μ F < ⊤ := (measure_mono Fs).trans_lt hsμ,
     refine ennreal.le_of_add_le_add_left hFμ.ne _,

src/measure_theory/measure/haar.lean

@@ -414,9 +414,7 @@ end
 lemma chaar_sup_eq [t2_space G] {K₀ : positive_compacts G} {K₁ K₂ : compacts G}
   (h : disjoint K₁.1 K₂.1) : chaar K₀ (K₁ ⊔ K₂) = chaar K₀ K₁ + chaar K₀ K₂ :=
 begin
-  rcases compact_compact_separated K₁.2 K₂.2 (disjoint_iff.mp h) with
-    ⟨U₁, U₂, h1U₁, h1U₂, h2U₁, h2U₂, hU⟩,
-  rw [← disjoint_iff_inter_eq_empty] at hU,
+  rcases compact_compact_separated K₁.2 K₂.2 h with ⟨U₁, U₂, h1U₁, h1U₂, h2U₁, h2U₂, hU⟩,
   rcases compact_open_separated_mul_right K₁.2 h1U₁ h2U₁ with ⟨L₁, h1L₁, h2L₁⟩,
   rcases mem_nhds_iff.mp h1L₁ with ⟨V₁, h1V₁, h2V₁, h3V₁⟩,
   replace h2L₁ := subset.trans (mul_subset_mul_left h1V₁) h2L₁,

src/topology/alexandroff.lean

@@ -375,19 +375,17 @@ Hausdorff and regular) topological space. -/
 instance [locally_compact_space X] [t2_space X] : normal_space (alexandroff X) :=
 begin
   have key : ∀ z : X,
-    ∃ u v : set (alexandroff X), is_open u ∧ is_open v ∧ ↑z ∈ u ∧ ∞ ∈ v ∧ u ∩ v = ∅,
+    ∃ u v : set (alexandroff X), is_open u ∧ is_open v ∧ ↑z ∈ u ∧ ∞ ∈ v ∧ disjoint u v,
   { intro z,
     rcases exists_open_with_compact_closure z with ⟨u, hu, huy', Hu⟩,
-    refine ⟨coe '' u, (coe '' closure u)ᶜ, is_open_image_coe.2 hu,
+    exact ⟨coe '' u, (coe '' closure u)ᶜ, is_open_image_coe.2 hu,
       is_open_compl_image_coe.2 ⟨is_closed_closure, Hu⟩, mem_image_of_mem _ huy',
-      mem_compl infty_not_mem_image_coe, _⟩,
-    rw [← subset_compl_iff_disjoint, compl_compl],
-    exact image_subset _ subset_closure },
+      mem_compl infty_not_mem_image_coe, (image_subset _ subset_closure).disjoint_compl_right⟩ },
   refine @normal_of_compact_t2 _ _ _ ⟨λ x y hxy, _⟩,
   induction x using alexandroff.rec; induction y using alexandroff.rec,
   { exact (hxy rfl).elim },
   { rcases key y with ⟨u, v, hu, hv, hxu, hyv, huv⟩,
-    exact ⟨v, u, hv, hu, hyv, hxu, (inter_comm u v) ▸ huv⟩ },
+    exact ⟨v, u, hv, hu, hyv, hxu, huv.symm⟩ },
   { exact key x },
   { exact separated_by_open_embedding open_embedding_coe (mt coe_eq_coe.mpr hxy) }
 end

src/topology/algebra/const_mul_action.lean

@@ -369,7 +369,7 @@ begin
   let f : T → Q := quotient.mk,
   have f_op : is_open_map f := is_open_map_quotient_mk_mul,
   rintros ⟨x₀⟩ ⟨y₀⟩ (hxy : f x₀ ≠ f y₀),
-  show ∃ (U ∈ 𝓝 (f x₀)) (V ∈ 𝓝 (f y₀)), U ∩ V = ∅,
+  show ∃ (U ∈ 𝓝 (f x₀)) (V ∈ 𝓝 (f y₀)), _,
   have hx₀y₀ : x₀ ≠ y₀ := ne_of_apply_ne _ hxy,
   have hγx₀y₀ : ∀ γ : Γ, γ • x₀ ≠ y₀ := not_exists.mp (mt quotient.sound hxy.symm : _),
   obtain ⟨K₀, L₀, K₀_in, L₀_in, hK₀, hL₀, hK₀L₀⟩ := t2_separation_compact_nhds hx₀y₀,
@@ -385,13 +385,10 @@ begin
     exact (continuous_const_smul _).continuous_at (hu γ) },
   have V_nhds : f '' V₀ ∈ 𝓝 (f y₀),
     from f_op.image_mem_nhds (inter_mem ((bInter_mem bad_Γ_finite).mpr $ λ γ hγ, hv γ) L₀_in),
-  refine ⟨f '' U₀, U_nhds, f '' V₀, V_nhds, _⟩,
-  rw mul_action.image_inter_image_iff,
+  refine ⟨f '' U₀, U_nhds, f '' V₀, V_nhds, mul_action.disjoint_image_image_iff.2 _⟩,
   rintros x ⟨x_in_U₀₀, x_in_K₀⟩ γ,
   by_cases H : γ ∈ bad_Γ_set,
-  { rintros ⟨h, -⟩,
-    exact eq_empty_iff_forall_not_mem.mp (u_v_disjoint γ) (γ • x)
-      ⟨(mem_Inter₂.mp x_in_U₀₀ γ H : _), mem_Inter₂.mp h γ H⟩ },
+  { exact λ h, u_v_disjoint γ ⟨mem_Inter₂.mp x_in_U₀₀ γ H, mem_Inter₂.mp h.1 γ H⟩ },
   { rintros ⟨-, h'⟩,
     simp only [image_smul, not_not, mem_set_of_eq, ne.def] at H,
     exact eq_empty_iff_forall_not_mem.mp H (γ • x) ⟨mem_image_of_mem _ x_in_K₀, h'⟩ },

src/topology/algebra/continuous_monoid_hom.lean

@@ -226,7 +226,7 @@ lemma is_closed_embedding [has_continuous_mul B] [t2_space B] :
     obtain ⟨UV, W, hUV, hW, hfUV, hfW, h⟩ := t2_separation hf2.symm,
     have hB := @continuous_mul B _ _ _,
     obtain ⟨U, V, hU, hV, hfU, hfV, h'⟩ := is_open_prod_iff.mp (hUV.preimage hB) (f x) (f y) hfUV,
-    refine ⟨x, y, U, V, W, hU, hV, hW, ((disjoint_iff.mpr h).mono_left _), ⟨hfU, hfV⟩, hfW⟩,
+    refine ⟨x, y, U, V, W, hU, hV, hW, h.mono_left _, ⟨hfU, hfV⟩, hfW⟩,
     rintros _ ⟨x, y, hx : (x, y).1 ∈ U, hy : (x, y).2 ∈ V, rfl⟩,
     exact h' ⟨hx, hy⟩ },
 end⟩⟩

src/topology/algebra/order/basic.lean

@@ -249,20 +249,10 @@ section partial_order
 variables [topological_space α] [partial_order α] [t : order_closed_topology α]
 include t
 
-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} := 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,
-    set.eq_empty_iff_forall_not_mem.2 $ assume a ⟨h₁, h₂⟩,
-    have a ≠ a, from @h (a, a) ⟨h₁, h₂⟩,
-    this rfl⟩ }
+t2_iff_is_closed_diagonal.2 $ by simpa only [diagonal, le_antisymm_iff] using
+  t.is_closed_le'.inter (is_closed_le continuous_snd continuous_fst)
 
 end partial_order
 

src/topology/basic.lean

@@ -84,27 +84,26 @@ def topological_space.of_closed {α : Type u} (T : set (set α))
 
 section topological_space
 
-variables {α : Type u} {β : Type v} {ι : Sort w} {a : α} {s s₁ s₂ : set α} {p p₁ p₂ : α → Prop}
+variables {α : Type u} {β : Type v} {ι : Sort w} {a : α} {s s₁ s₂ t : set α} {p p₁ p₂ : α → Prop}
 
 @[ext]
 lemma topological_space_eq : ∀ {f g : topological_space α}, f.is_open = g.is_open → f = g
 | ⟨a, _, _, _⟩ ⟨b, _, _, _⟩ rfl := rfl
 
 section
-variables [t : topological_space α]
-include t
+variables [topological_space α]
 
 /-- `is_open s` means that `s` is open in the ambient topological space on `α` -/
-def is_open (s : set α) : Prop := topological_space.is_open t s
+def is_open (s : set α) : Prop := topological_space.is_open ‹_› s
 
 @[simp]
-lemma is_open_univ : is_open (univ : set α) := topological_space.is_open_univ t
+lemma is_open_univ : is_open (univ : set α) := topological_space.is_open_univ _
 
 lemma is_open.inter (h₁ : is_open s₁) (h₂ : is_open s₂) : is_open (s₁ ∩ s₂) :=
-topological_space.is_open_inter t s₁ s₂ h₁ h₂
+topological_space.is_open_inter _ s₁ s₂ h₁ h₂
 
 lemma is_open_sUnion {s : set (set α)} (h : ∀t ∈ s, is_open t) : is_open (⋃₀ s) :=
-topological_space.is_open_sUnion t s h
+topological_space.is_open_sUnion _ s h
 
 end
 
@@ -600,13 +599,12 @@ lemma closure_eq_interior_union_frontier (s : set α) : closure s = interior s 
 lemma closure_eq_self_union_frontier (s : set α) : closure s = s ∪ frontier s :=
 (union_diff_cancel' interior_subset subset_closure).symm
 
-lemma is_open.inter_frontier_eq_empty_of_disjoint {s t : set α} (ht : is_open t)
-  (hd : disjoint s t) :
-  t ∩ frontier s = ∅ :=
-begin
-  rw [inter_comm, ← subset_compl_iff_disjoint],
-  exact frontier_subset_closure.trans (closure_minimal (disjoint_left.1 hd) ht.is_closed_compl),
-end
+lemma disjoint.frontier_left (ht : is_open t) (hd : disjoint s t) : disjoint (frontier s) t :=
+subset_compl_iff_disjoint_right.1 $ frontier_subset_closure.trans $ closure_minimal
+  (disjoint_left.1 hd) $ is_closed_compl_iff.2 ht
+
+lemma disjoint.frontier_right (hs : is_open s) (hd : disjoint s t) : disjoint s (frontier t) :=
+(hd.symm.frontier_left hs).symm
 
 lemma frontier_eq_inter_compl_interior {s : set α} :
   frontier s = (interior s)ᶜ ∩ (interior (sᶜ))ᶜ :=

src/topology/compact_open.lean

@@ -59,6 +59,9 @@ set.ext (λ f, subset_inter_iff)
   compact_open.gen (s ∪ t) u = compact_open.gen s u ∩ compact_open.gen t u :=
 set.ext (λ f, (iff_of_eq (congr_arg (⊆ u) (image_union f s t))).trans union_subset_iff)
 
+lemma gen_empty_right {s : set α} (h : s.nonempty) : compact_open.gen s (∅ : set β) = ∅ :=
+eq_empty_of_forall_not_mem $ λ f, (h.image _).not_subset_empty
+
 -- The compact-open topology on the space of continuous maps α → β.
 instance compact_open : topological_space C(α, β) :=
 topological_space.generate_from
@@ -129,10 +132,8 @@ instance [t2_space β] : t2_space C(α, β) :=
       is_compact_singleton hu, continuous_map.is_open_gen is_compact_singleton hv, _, _, _⟩,
     { rwa [compact_open.gen, mem_set_of_eq, image_singleton, singleton_subset_iff] },
     { rwa [compact_open.gen, mem_set_of_eq, image_singleton, singleton_subset_iff] },
-    { rw [←continuous_map.gen_inter, huv],
-      refine subset_empty_iff.mp (λ f, _),
-      rw [compact_open.gen, mem_set_of_eq, image_singleton, singleton_subset_iff],
-      exact id },
+    { rw [disjoint_iff_inter_eq_empty, ←gen_inter, huv.inter_eq,
+        gen_empty_right (singleton_nonempty _)] }
   end ⟩
 
 end ev