diff --git a/src/data/set/lattice.lean b/src/data/set/lattice.lean
index 371f38db50707..e131b1026bba4 100644
--- a/src/data/set/lattice.lean
+++ b/src/data/set/lattice.lean
@@ -1434,10 +1434,12 @@ disjoint_iff
 lemma not_disjoint_iff : ¬disjoint s t ↔ ∃ x, x ∈ s ∧ x ∈ t :=
 not_forall.trans $ exists_congr $ λ x, not_not
 
-lemma not_disjoint_iff_nonempty_inter {α : Type*} {s t : set α} :
-  ¬disjoint s t ↔ (s ∩ t).nonempty :=
+lemma not_disjoint_iff_nonempty_inter : ¬disjoint s t ↔ (s ∩ t).nonempty :=
 by simp [set.not_disjoint_iff, set.nonempty_def]
 
+lemma disjoint_or_nonempty_inter (s t : set α) : disjoint s t ∨ (s ∩ t).nonempty :=
+(em _).imp_right not_disjoint_iff_nonempty_inter.mp
+
 lemma disjoint_left : disjoint s t ↔ ∀ {a}, a ∈ s → a ∉ t :=
 show (∀ x, ¬(x ∈ s ∩ t)) ↔ _, from ⟨λ h a, not_and.1 $ h a, λ h a, not_and.2 $ h a⟩
 
diff --git a/src/topology/category/Profinite/default.lean b/src/topology/category/Profinite/default.lean
index 7d6f670dd4df5..33669f7141d69 100644
--- a/src/topology/category/Profinite/default.lean
+++ b/src/topology/category/Profinite/default.lean
@@ -96,7 +96,6 @@ def Profinite.to_Top : Profinite ⥤ Top := forget₂ _ _
 rfl
 
 section Profinite
-local attribute [instance] connected_component_setoid
 
 /--
 (Implementation) The object part of the connected_components functor from compact Hausdorff spaces
@@ -118,13 +117,11 @@ spaces in compact Hausdorff spaces.
 -/
 def Profinite.to_CompHaus_equivalence (X : CompHaus.{u}) (Y : Profinite.{u}) :
   (CompHaus.to_Profinite_obj X ⟶ Y) ≃ (X ⟶ Profinite_to_CompHaus.obj Y) :=
-{ to_fun := λ f,
-  { to_fun := f.1 ∘ quotient.mk,
-    continuous_to_fun := continuous.comp f.2 (continuous_quotient_mk) },
+{ to_fun := λ f, f.comp ⟨quotient.mk', continuous_quotient_mk⟩,
   inv_fun := λ g,
     { to_fun := continuous.connected_components_lift g.2,
       continuous_to_fun := continuous.connected_components_lift_continuous g.2},
-  left_inv := λ f, continuous_map.ext $ λ x, quotient.induction_on x $ λ a, rfl,
+  left_inv := λ f, continuous_map.ext $ connected_components.surjective_coe.forall.2 $ λ a, rfl,
   right_inv := λ f, continuous_map.ext $ λ x, rfl }
 
 /--
diff --git a/src/topology/connected.lean b/src/topology/connected.lean
index 0c6f419099fdf..ba9070c6cef57 100644
--- a/src/topology/connected.lean
+++ b/src/topology/connected.lean
@@ -694,27 +694,25 @@ begin
 end
 
 /-- Preconnected sets are either contained in or disjoint to any given clopen set. -/
-theorem subset_or_disjoint_of_clopen {α : Type*} [topological_space α] {s t : set α}
-  (h : is_preconnected t) (h1 : is_clopen s) : s ∩ t = ∅ ∨ t ⊆ s :=
+theorem is_preconnected.subset_clopen {s t : set α} (hs : is_preconnected s) (ht : is_clopen t)
+  (hne : (s ∩ t).nonempty) : s ⊆ t :=
 begin
-  by_contradiction h2,
-  have h3 : (s ∩ t).nonempty := ne_empty_iff_nonempty.mp (mt or.inl h2),
-  have h4 : (t ∩ sᶜ).nonempty,
-  { apply inter_compl_nonempty_iff.2,
-    push_neg at h2,
-    exact h2.2 },
-  rw [inter_comm] at h3,
-  apply ne_empty_iff_nonempty.2 (h s sᶜ h1.1 (is_open_compl_iff.2 h1.2) _ h3 h4),
-  { rw [inter_compl_self, inter_empty] },
-  { rw [union_compl_self],
-    exact subset_univ t },
+  by_contra h,
+  have : (s ∩ tᶜ).nonempty := inter_compl_nonempty_iff.2 h,
+  obtain ⟨x, -, hx, hx'⟩ : (s ∩ (t ∩ tᶜ)).nonempty,
+    from hs t tᶜ ht.is_open ht.compl.is_open (λ x hx, em _) hne this,
+  exact hx' hx
 end
 
+/-- Preconnected sets are either contained in or disjoint to any given clopen set. -/
+theorem disjoint_or_subset_of_clopen {s t : set α} (hs : is_preconnected s) (ht : is_clopen t) :
+  disjoint s t ∨ s ⊆ t :=
+(disjoint_or_nonempty_inter s t).imp_right $ hs.subset_clopen ht
+
 /-- A set `s` is preconnected if and only if
 for every cover by two closed sets that are disjoint on `s`,
 it is contained in one of the two covering sets. -/
-theorem is_preconnected_iff_subset_of_disjoint_closed {α : Type*} {s : set α}
-  [topological_space α] :
+theorem is_preconnected_iff_subset_of_disjoint_closed :
   is_preconnected s ↔
     ∀ (u v : set α) (hu : is_closed u) (hv : is_closed v) (hs : s ⊆ u ∪ v) (huv : s ∩ (u ∩ v) = ∅),
       s ⊆ u ∨ s ⊆ v :=
@@ -769,28 +767,21 @@ begin
         inter_comm, inter_assoc, inter_comm v u, huv] }
 end
 
+lemma is_clopen.connected_component_subset {x} (hs : is_clopen s) (hx : x ∈ s) :
+  connected_component x ⊆ s :=
+is_preconnected_connected_component.subset_clopen hs ⟨x, mem_connected_component, hx⟩
+
 /-- The connected component of a point is always a subset of the intersection of all its clopen
 neighbourhoods. -/
 lemma connected_component_subset_Inter_clopen {x : α} :
   connected_component x ⊆ ⋂ Z : {Z : set α // is_clopen Z ∧ x ∈ Z}, Z :=
-begin
-  apply subset_Inter (λ Z, _),
-  cases (subset_or_disjoint_of_clopen (@is_connected_connected_component _ _ x).2 Z.2.1),
-  { exfalso,
-    apply nonempty.ne_empty
-      (nonempty_of_mem (mem_inter (@mem_connected_component _ _ x) Z.2.2)),
-    rw inter_comm,
-    exact h },
-  exact h,
-end
+subset_Inter $ λ Z, Z.2.1.connected_component_subset Z.2.2
 
 /-- A clopen set is the union of its connected components. -/
-lemma is_clopen.eq_union_connected_components {Z : set α} (h : is_clopen Z) :
-  Z = (⋃ (x : α) (H : x ∈ Z), connected_component x) :=
-eq_of_subset_of_subset (λ x xZ, mem_Union.2 ⟨x, mem_Union.2 ⟨xZ, mem_connected_component⟩⟩)
-  (Union_subset $ λ x, Union_subset $ λ xZ,
-    (by { apply subset.trans connected_component_subset_Inter_clopen
-      (Inter_subset _ ⟨Z, ⟨h, xZ⟩⟩) }))
+lemma is_clopen.bUnion_connected_component_eq {Z : set α} (h : is_clopen Z) :
+  (⋃ x ∈ Z, connected_component x) = Z :=
+(bUnion_subset $ λ x, h.connected_component_subset).antisymm $
+  λ x hx, mem_bUnion hx mem_connected_component
 
 /-- The preimage of a connected component is preconnected if the function has connected fibers
 and a subset is closed iff the preimage is. -/
@@ -902,6 +893,18 @@ begin
   exact preimage_mono h,
 end
 
+lemma quotient_map.preimage_connected_component [topological_space β] {f : α → β}
+  (hf : quotient_map f) (h_fibers : ∀ y : β, is_connected (f ⁻¹' {y})) (a : α) :
+  f ⁻¹' connected_component (f a) = connected_component a :=
+((preimage_connected_component_connected h_fibers
+  (λ _, hf.is_closed_preimage.symm) _).subset_connected_component mem_connected_component).antisymm
+  (hf.continuous.maps_to_connected_component a)
+
+lemma quotient_map.image_connected_component [topological_space β] {f : α → β}
+  (hf : quotient_map f) (h_fibers : ∀ y : β, is_connected (f ⁻¹' {y})) (a : α) :
+  f '' connected_component a = connected_component (f a) :=
+by rw [← hf.preimage_connected_component h_fibers, image_preimage_eq _ hf.surjective]
+
 end preconnected
 
 section totally_disconnected
@@ -1081,27 +1084,47 @@ section connected_component_setoid
 def connected_component_setoid (α : Type*) [topological_space α] : setoid α :=
 ⟨λ x y, connected_component x = connected_component y,
   ⟨λ x, by trivial, λ x y h1, h1.symm, λ x y z h1 h2, h1.trans h2⟩⟩
--- see Note [lower instance priority]
-local attribute [instance, priority 100] connected_component_setoid
-
-lemma connected_component_rel_iff {x y : α} : ⟦x⟧ = ⟦y⟧ ↔
-  connected_component x = connected_component y :=
-⟨λ h, quotient.exact h, λ h, quotient.sound h⟩
-
-lemma connected_component_nrel_iff {x y : α} : ⟦x⟧ ≠ ⟦y⟧ ↔
-  connected_component x ≠ connected_component y :=
-by { rw not_iff_not, exact connected_component_rel_iff }
 
 /-- The quotient of a space by its connected components -/
 def connected_components (α : Type u) [topological_space α] :=
-  quotient (connected_component_setoid α)
+quotient (connected_component_setoid α)
+
+instance : has_coe_t α (connected_components α) := ⟨quotient.mk'⟩
+
+namespace connected_components
+
+@[simp] lemma coe_eq_coe {x y : α} :
+  (x : connected_components α) = y ↔ connected_component x = connected_component y :=
+quotient.eq'
+
+lemma coe_ne_coe {x y : α} :
+  (x : connected_components α) ≠ y ↔ connected_component x ≠ connected_component y :=
+not_congr coe_eq_coe
 
-instance [inhabited α] : inhabited (connected_components α) := ⟨quotient.mk default⟩
-instance connected_components.topological_space : topological_space (connected_components α) :=
-  quotient.topological_space
+lemma coe_eq_coe' {x y : α} :
+  (x : connected_components α) = y ↔ x ∈ connected_component y :=
+coe_eq_coe.trans ⟨λ h, h ▸ mem_connected_component, λ h, (connected_component_eq h).symm⟩
 
-lemma continuous.image_eq_of_equiv {β : Type*} [topological_space β] [totally_disconnected_space β]
-  {f : α → β} (h : continuous f) (a b : α) (hab : a ≈ b) : f a = f b :=
+instance [inhabited α] : inhabited (connected_components α) := ⟨↑(default : α)⟩
+
+instance : topological_space (connected_components α) :=
+quotient.topological_space
+
+lemma surjective_coe : surjective (coe : α → connected_components α) := surjective_quot_mk _
+lemma quotient_map_coe : quotient_map (coe : α → connected_components α) := quotient_map_quot_mk
+
+@[continuity]
+lemma continuous_coe : continuous (coe : α → connected_components α) := quotient_map_coe.continuous
+
+@[simp] lemma range_coe : range (coe : α → connected_components α)= univ :=
+surjective_coe.range_eq
+
+end connected_components
+
+variables [topological_space β] [totally_disconnected_space β] {f : α → β}
+
+lemma continuous.image_eq_of_connected_component_eq (h : continuous f) (a b : α)
+  (hab : connected_component a = connected_component b) : f a = f b :=
 singleton_eq_singleton_iff.1 $
   h.image_connected_component_eq_singleton a ▸
   h.image_connected_component_eq_singleton b ▸ hab ▸ rfl
@@ -1109,83 +1132,52 @@ singleton_eq_singleton_iff.1 $
 /--
 The lift to `connected_components α` of a continuous map from `α` to a totally disconnected space
 -/
-def continuous.connected_components_lift {β : Type*} [topological_space β]
-  [totally_disconnected_space β] {f : α → β} (h : continuous f) : connected_components α → β :=
-quotient.lift f h.image_eq_of_equiv
+def continuous.connected_components_lift (h : continuous f) :
+  connected_components α → β :=
+λ x, quotient.lift_on' x f h.image_eq_of_connected_component_eq
 
-@[continuity] lemma continuous.connected_components_lift_continuous {β : Type*}
-  [topological_space β] [totally_disconnected_space β] {f : α → β} (h : continuous f) :
+@[continuity] lemma continuous.connected_components_lift_continuous (h : continuous f) :
   continuous h.connected_components_lift :=
-continuous_quotient_lift h.image_eq_of_equiv h
+continuous_quotient_lift_on' h.image_eq_of_connected_component_eq h
 
-@[simp] lemma continuous.connected_components_lift_factors {β : Type*} [topological_space β]
-  [totally_disconnected_space β] {f : α → β} (h : continuous f) :
-  h.connected_components_lift ∘ quotient.mk = f := rfl
+@[simp] lemma continuous.connected_components_lift_apply_coe (h : continuous f) (x : α) :
+  h.connected_components_lift x = f x := rfl
 
-lemma continuous.connected_components_lift_unique {β : Type*} [topological_space β]
-  [totally_disconnected_space β] {f : α → β} (h : continuous f) (g : connected_components α → β)
-  (hg : g ∘ quotient.mk = f) : g = h.connected_components_lift :=
-by { subst hg, ext1 x, exact quotient.induction_on x (λ a, refl _) }
+@[simp] lemma continuous.connected_components_lift_comp_coe (h : continuous f) :
+  h.connected_components_lift ∘ coe = f := rfl
 
-lemma connected_components_lift_unique' {β : Type*} (g₁ : connected_components α → β)
-  (g₂ : connected_components α → β) (hg : g₁ ∘ quotient.mk = g₂ ∘ quotient.mk ) : g₁ = g₂ :=
-begin
-  ext1 x,
-  refine quotient.induction_on x (λ a, _),
-  change (g₁ ∘ quotient.mk) a = (g₂ ∘ quotient.mk) a,
-  rw hg,
-end
+lemma connected_components_lift_unique' {β : Sort*} {g₁ g₂ : connected_components α → β}
+  (hg : g₁ ∘ (coe : α → connected_components α) = g₂ ∘ coe) :
+  g₁ = g₂ :=
+connected_components.surjective_coe.injective_comp_right hg
+
+lemma continuous.connected_components_lift_unique (h : continuous f)
+  (g : connected_components α → β) (hg : g ∘ coe = f) : g = h.connected_components_lift :=
+connected_components_lift_unique' $ hg.trans h.connected_components_lift_comp_coe.symm
 
 /-- The preimage of a singleton in `connected_components` is the connected component
 of an element in the equivalence class. -/
-lemma connected_components_preimage_singleton {t : α} :
-  connected_component t = quotient.mk ⁻¹' {⟦t⟧} :=
-begin
-  apply set.eq_of_subset_of_subset; intros a ha,
-  { have H : ⟦a⟧ = ⟦t⟧ := quotient.sound (connected_component_eq ha).symm,
-    rw [mem_preimage, H],
-    exact mem_singleton ⟦t⟧ },
-  rw [mem_preimage, mem_singleton_iff] at ha,
-  have ha' : connected_component a = connected_component t := quotient.exact ha,
-  rw ←ha',
-  exact mem_connected_component,
-end
+lemma connected_components_preimage_singleton {x : α} :
+  coe ⁻¹' ({x} : set (connected_components α)) = connected_component x :=
+by { ext y, simp [connected_components.coe_eq_coe'] }
 
 /-- The preimage of the image of a set under the quotient map to `connected_components α`
 is the union of the connected components of the elements in it. -/
 lemma connected_components_preimage_image (U : set α) :
-  quotient.mk ⁻¹' (quotient.mk '' U) = ⋃ (x : α) (h : x ∈ U), connected_component x :=
-begin
-  apply set.eq_of_subset_of_subset,
-  { rintros a ⟨b, hb, hab⟩,
-    refine mem_Union.2 ⟨b, mem_Union.2 ⟨hb, _⟩⟩,
-    rw connected_component_rel_iff.1 hab,
-    exact mem_connected_component },
-  refine Union_subset (λ a, Union_subset (λ ha, _)),
-  rw [connected_components_preimage_singleton,
-    (surjective_quotient_mk _).preimage_subset_preimage_iff, singleton_subset_iff],
-  exact ⟨a, ha, refl _⟩,
-end
+  coe ⁻¹' (coe '' U : set (connected_components α)) = ⋃ x ∈ U, connected_component x :=
+by simp only [connected_components_preimage_singleton, preimage_bUnion, image_eq_Union]
 
 instance connected_components.totally_disconnected_space :
   totally_disconnected_space (connected_components α) :=
 begin
   rw totally_disconnected_space_iff_connected_component_singleton,
-  refine λ x, quotient.induction_on x (λ a, _),
-  apply eq_of_subset_of_subset _ (singleton_subset_iff.2 mem_connected_component),
-  rw subset_singleton_iff,
-  refine λ x, quotient.induction_on x (λ b hb, _),
-  rw [connected_component_rel_iff, connected_component_eq],
-  suffices : is_preconnected (quotient.mk ⁻¹' connected_component ⟦a⟧),
-  { apply mem_of_subset_of_mem (this.subset_connected_component hb),
-    exact mem_preimage.2 mem_connected_component },
-  apply (@preimage_connected_component_connected _ _ _ _ _ _ _ _).2,
-  { refine λ t, quotient.induction_on t (λ s, _),
-    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,
-    is_open_compl_iff] at hT,
+  refine connected_components.surjective_coe.forall.2 (λ x, _),
+  rw [← connected_components.quotient_map_coe.image_connected_component,
+    ← connected_components_preimage_singleton,
+    image_preimage_eq _ connected_components.surjective_coe],
+  refine connected_components.surjective_coe.forall.2 (λ y, _),
+  rw connected_components_preimage_singleton,
+  exact is_connected_connected_component
 end
 
 /-- Functoriality of `connected_components` -/
diff --git a/src/topology/constructions.lean b/src/topology/constructions.lean
index adcd6ff7975c3..5cb65246e65ca 100644
--- a/src/topology/constructions.lean
+++ b/src/topology/constructions.lean
@@ -751,6 +751,10 @@ lemma continuous_quotient_lift {f : α → β} (hs : ∀ a b, a ≈ b → f a =
   (h : continuous f) : continuous (quotient.lift f hs : quotient s → β) :=
 continuous_coinduced_dom h
 
+lemma continuous_quotient_lift_on' {f : α → β} (hs : ∀ a b, a ≈ b → f a = f b)
+  (h : continuous f) : continuous (λ x, quotient.lift_on' x f hs : quotient s → β) :=
+continuous_coinduced_dom h
+
 end quotient
 
 section pi
diff --git a/src/topology/separation.lean b/src/topology/separation.lean
index 748d68459686c..dd290846c87f9 100644
--- a/src/topology/separation.lean
+++ b/src/topology/separation.lean
@@ -1282,7 +1282,7 @@ end normality
 
 /-- In a compact t2 space, the connected component of a point equals the intersection of all
 its clopen neighbourhoods. -/
-lemma connected_component_eq_Inter_clopen [t2_space α] [compact_space α] {x : α} :
+lemma connected_component_eq_Inter_clopen [t2_space α] [compact_space α] (x : α) :
   connected_component x = ⋂ Z : {Z : set α // is_clopen Z ∧ x ∈ Z}, Z :=
 begin
   apply eq_of_subset_of_subset connected_component_subset_Inter_clopen,
@@ -1358,7 +1358,7 @@ variables [t2_space α]
 
 /-- A Hausdorff space with a clopen basis is totally separated. -/
 lemma tot_sep_of_zero_dim (h : is_topological_basis {s : set α | is_clopen s}) :
-    totally_separated_space α :=
+  totally_separated_space α :=
 begin
   constructor,
   rintros x - y - hxy,
@@ -1377,7 +1377,7 @@ variables [compact_space α]
 /-- A compact Hausdorff space is totally disconnected if and only if it is totally separated, this
   is also true for locally compact spaces. -/
 theorem compact_t2_tot_disc_iff_tot_sep :
-totally_disconnected_space α ↔ totally_separated_space α :=
+  totally_disconnected_space α ↔ totally_separated_space α :=
 begin
   split,
   { intro h, constructor,
@@ -1499,47 +1499,28 @@ end
 
 end locally_compact
 
-section connected_component_setoid
-local attribute [instance] connected_component_setoid
-
 /-- `connected_components α` is Hausdorff when `α` is Hausdorff and compact -/
 instance connected_components.t2 [t2_space α] [compact_space α] :
   t2_space (connected_components α) :=
 begin
   -- Proof follows that of: https://stacks.math.columbia.edu/tag/0900
   -- Fix 2 distinct connected components, with points a and b
-  refine ⟨λ x y, quotient.induction_on x (quotient.induction_on y (λ a b ne, _))⟩,
-  rw connected_component_nrel_iff at ne,
+  refine ⟨connected_components.surjective_coe.forall₂.2 $ λ a b ne, _⟩,
+  rw connected_components.coe_ne_coe at ne,
   have h := connected_component_disjoint ne,
-  -- write ⟦b⟧ as the intersection of all clopen subsets containing it
-  rw [connected_component_eq_Inter_clopen, disjoint_iff_inter_eq_empty, inter_comm] at h,
-  -- Now we show that this can be reduced to some clopen containing ⟦b⟧ being disjoint to ⟦a⟧
-  cases is_closed_connected_component.is_compact.elim_finite_subfamily_closed _ _ h
-    with fin_a ha,
-  swap, { exact λ Z, Z.2.1.2 },
-  set U : set α := (⋂ (i : {Z // is_clopen Z ∧ b ∈ Z}) (H : i ∈ fin_a), i) with hU,
-  rw ←hU at ha,
-  have hu_clopen : is_clopen U := is_clopen_bInter (λ i j, i.2.1),
-  -- This clopen and its complement will separate the points corresponding to ⟦a⟧ and ⟦b⟧
-  use [quotient.mk '' U, quotient.mk '' Uᶜ],
-  -- Using the fact that clopens are unions of connected components, we show that
-  -- U and Uᶜ is the preimage of a clopen set in the quotient
-  have hu : quotient.mk ⁻¹' (quotient.mk '' U) = U :=
-    (connected_components_preimage_image U ▸ eq.symm) hu_clopen.eq_union_connected_components,
-  have huc : quotient.mk ⁻¹' (quotient.mk '' Uᶜ) = Uᶜ :=
-    (connected_components_preimage_image Uᶜ ▸ eq.symm)
-      (is_clopen.compl hu_clopen).eq_union_connected_components,
-  -- showing that U and Uᶜ are open and separates ⟦a⟧ and ⟦b⟧
-  refine ⟨_,_,_,_,_⟩,
-  { rw [(quotient_map_iff.1 quotient_map_quotient_mk).2 _, hu],
-    exact hu_clopen.1 },
-  { rw [(quotient_map_iff.1 quotient_map_quotient_mk).2 _, huc],
-    exact is_open_compl_iff.2 hu_clopen.2 },
-  { exact mem_image_of_mem _ (mem_Inter.2 (λ Z, mem_Inter.2 (λ Zmem, Z.2.2))) },
-  { apply mem_image_of_mem,
-    exact mem_of_subset_of_mem (subset_compl_iff_disjoint.2 ha) (@mem_connected_component _ _ a) },
-  apply preimage_injective.2 (@surjective_quotient_mk _ _),
-  rw [preimage_inter, preimage_empty, hu, huc, inter_compl_self _],
+  -- write ↑b as the intersection of all clopen subsets containing it
+  rw [connected_component_eq_Inter_clopen b, disjoint_iff_inter_eq_empty] at h,
+  -- Now we show that this can be reduced to some clopen containing `↑b` being disjoint to `↑a`
+  obtain ⟨U, V, hU, ha, hb, rfl⟩ : ∃ (U : set α) (V : set (connected_components α)), is_clopen U ∧
+    connected_component a ∩ U = ∅ ∧ connected_component b ⊆ U ∧ coe ⁻¹' V = U,
+  { cases is_closed_connected_component.is_compact.elim_finite_subfamily_closed _ _ h with fin_a ha,
+    swap, { exact λ Z, Z.2.1.2 },
+    -- This clopen and its complement will separate the connected components of `a` and `b`
+    set U : set α := (⋂ (i : {Z // is_clopen Z ∧ b ∈ Z}) (H : i ∈ fin_a), i),
+    have hU : is_clopen U := is_clopen_bInter (λ i j, i.2.1),
+    exact ⟨U, coe '' U, hU, ha, subset_bInter (λ Z _, Z.2.1.connected_component_subset Z.2.2),
+      (connected_components_preimage_image U).symm ▸ hU.bUnion_connected_component_eq⟩ },
+  rw connected_components.quotient_map_coe.is_clopen_preimage at hU,
+  refine ⟨Vᶜ, V, hU.compl.is_open, hU.is_open, _, hb mem_connected_component, compl_inter_self _⟩,
+  exact λ h, flip set.nonempty.ne_empty ha ⟨a, mem_connected_component, h⟩,
 end
-
-end connected_component_setoid
diff --git a/src/topology/subset_properties.lean b/src/topology/subset_properties.lean
index de417f49939c3..3ac3d9756b6c3 100644
--- a/src/topology/subset_properties.lean
+++ b/src/topology/subset_properties.lean
@@ -1227,11 +1227,14 @@ section clopen
 def is_clopen (s : set α) : Prop :=
 is_open s ∧ is_closed s
 
+protected lemma is_clopen.is_open (hs : is_clopen s) : is_open s := hs.1
+protected lemma is_clopen.is_closed (hs : is_clopen s) : is_closed s := hs.2
+
 theorem is_clopen.union {s t : set α} (hs : is_clopen s) (ht : is_clopen t) : is_clopen (s ∪ t) :=
-⟨is_open.union hs.1 ht.1, is_closed.union hs.2 ht.2⟩
+⟨hs.1.union ht.1, hs.2.union ht.2⟩
 
 theorem is_clopen.inter {s t : set α} (hs : is_clopen s) (ht : is_clopen t) : is_clopen (s ∩ t) :=
-⟨is_open.inter hs.1 ht.1, is_closed.inter hs.2 ht.2⟩
+⟨hs.1.inter ht.1, hs.2.inter ht.2⟩
 
 @[simp] theorem is_clopen_empty : is_clopen (∅ : set α) :=
 ⟨is_open_empty, is_closed_empty⟩
@@ -1240,7 +1243,7 @@ theorem is_clopen.inter {s t : set α} (hs : is_clopen s) (ht : is_clopen t) : i
 ⟨is_open_univ, is_closed_univ⟩
 
 theorem is_clopen.compl {s : set α} (hs : is_clopen s) : is_clopen sᶜ :=
-⟨hs.2.is_open_compl, is_closed_compl_iff.2 hs.1⟩
+⟨hs.2.is_open_compl, hs.1.is_closed_compl⟩
 
 @[simp] theorem is_clopen_compl_iff {s : set α} : is_clopen sᶜ ↔ is_clopen s :=
 ⟨λ h, compl_compl s ▸ is_clopen.compl h, is_clopen.compl⟩
@@ -1297,6 +1300,10 @@ lemma clopen_range_sigma_mk {ι : Type*} {σ : ι → Type*} [Π i, topological_
   is_clopen (set.range (@sigma.mk ι σ i)) :=
 ⟨open_embedding_sigma_mk.open_range, closed_embedding_sigma_mk.closed_range⟩
 
+protected lemma quotient_map.is_clopen_preimage [topological_space β] {f : α → β}
+  (hf : quotient_map f) {s : set β} : is_clopen (f ⁻¹' s) ↔ is_clopen s :=
+and_congr hf.is_open_preimage hf.is_closed_preimage
+
 end clopen
 
 section preirreducible