refactor(Topology/Clopen): order of open and closed (#9957)

Co-authored-by: Moritz Firsching <firsching@google.com>

Counterexamples/SorgenfreyLine.lean

@@ -166,7 +166,7 @@ instance : ContinuousAdd ℝₗ := by
   exact (continuous_add.tendsto _).inf (MapsTo.tendsto fun x hx => add_le_add hx.1 hx.2)
 
 theorem isClopen_Ici (a : ℝₗ) : IsClopen (Ici a) :=
-  ⟨isOpen_Ici a, isClosed_Ici⟩
+  ⟨isClosed_Ici, isOpen_Ici a⟩
 #align counterexample.sorgenfrey_line.is_clopen_Ici Counterexample.SorgenfreyLine.isClopen_Ici
 
 theorem isClopen_Iio (a : ℝₗ) : IsClopen (Iio a) := by
@@ -247,7 +247,7 @@ theorem isClosed_of_subset_antidiagonal {s : Set (ℝₗ × ℝₗ)} {c : ℝₗ
   obtain rfl : x + y = c := by
     change (x, y) ∈ {p : ℝₗ × ℝₗ | p.1 + p.2 = c}
     exact closure_minimal (hs : s ⊆ {x | x.1 + x.2 = c}) (isClosed_antidiagonal c) H
-  rcases mem_closure_iff.1 H (Ici (x, y)) (isClopen_Ici_prod _).1 left_mem_Ici with
+  rcases mem_closure_iff.1 H (Ici (x, y)) (isClopen_Ici_prod _).2 left_mem_Ici with
     ⟨⟨x', y'⟩, ⟨hx : x ≤ x', hy : y ≤ y'⟩, H⟩
   convert H
   · refine' hx.antisymm _

Mathlib/FieldTheory/KrullTopology.lean

@@ -267,7 +267,7 @@ theorem krullTopology_totallyDisconnected {K L : Type*} [Field K] [Field L] [Alg
   let E := IntermediateField.adjoin K ({x} : Set L)
   haveI := IntermediateField.adjoin.finiteDimensional (h_int x)
   refine' ⟨σ • E.fixingSubgroup,
-    ⟨E.fixingSubgroup_isOpen.leftCoset σ, E.fixingSubgroup_isClosed.leftCoset σ⟩,
+    ⟨E.fixingSubgroup_isClosed.leftCoset σ, E.fixingSubgroup_isOpen.leftCoset σ⟩,
     ⟨1, E.fixingSubgroup.one_mem', mul_one σ⟩, _⟩
   simp only [mem_leftCoset_iff, SetLike.mem_coe, IntermediateField.mem_fixingSubgroup_iff,
     not_forall]

Mathlib/Topology/AlexandrovDiscrete.lean

@@ -80,20 +80,20 @@ lemma isClosed_iUnion₂ {f : ∀ i, κ i → Set α} (hf : ∀ i j, IsClosed (f
   isClosed_iUnion fun _ ↦ isClosed_iUnion <| hf _
 
 lemma isClopen_sInter (hS : ∀ s ∈ S, IsClopen s) : IsClopen (⋂₀ S) :=
-  ⟨isOpen_sInter fun s hs ↦ (hS s hs).1, isClosed_sInter fun s hs ↦ (hS s hs).2⟩
+  ⟨isClosed_sInter fun s hs ↦ (hS s hs).1, isOpen_sInter fun s hs ↦ (hS s hs).2⟩
 
 lemma isClopen_iInter (hf : ∀ i, IsClopen (f i)) : IsClopen (⋂ i, f i) :=
-  ⟨isOpen_iInter fun i ↦ (hf i).1, isClosed_iInter fun i ↦ (hf i).2⟩
+  ⟨isClosed_iInter fun i ↦ (hf i).1, isOpen_iInter fun i ↦ (hf i).2⟩
 
 lemma isClopen_iInter₂ {f : ∀ i, κ i → Set α} (hf : ∀ i j, IsClopen (f i j)) :
     IsClopen (⋂ i, ⋂ j, f i j) :=
   isClopen_iInter fun _ ↦ isClopen_iInter <| hf _
 
 lemma isClopen_sUnion (hS : ∀ s ∈ S, IsClopen s) : IsClopen (⋃₀ S) :=
-  ⟨isOpen_sUnion fun s hs ↦ (hS s hs).1, isClosed_sUnion fun s hs ↦ (hS s hs).2⟩
+  ⟨isClosed_sUnion fun s hs ↦ (hS s hs).1, isOpen_sUnion fun s hs ↦ (hS s hs).2⟩
 
 lemma isClopen_iUnion (hf : ∀ i, IsClopen (f i)) : IsClopen (⋃ i, f i) :=
-  ⟨isOpen_iUnion fun i ↦ (hf i).1, isClosed_iUnion fun i ↦ (hf i).2⟩
+  ⟨isClosed_iUnion fun i ↦ (hf i).1, isOpen_iUnion fun i ↦ (hf i).2⟩
 
 lemma isClopen_iUnion₂ {f : ∀ i, κ i → Set α} (hf : ∀ i j, IsClopen (f i j)) :
     IsClopen (⋃ i, ⋃ j, f i j) :=

Mathlib/Topology/Algebra/OpenSubgroup.lean

@@ -179,7 +179,7 @@ theorem isClosed [ContinuousMul G] (U : OpenSubgroup G) : IsClosed (U : Set G) :
 
 @[to_additive]
 theorem isClopen [ContinuousMul G] (U : OpenSubgroup G) : IsClopen (U : Set G) :=
-  ⟨U.isOpen, U.isClosed⟩
+  ⟨U.isClosed, U.isOpen⟩
 #align open_subgroup.is_clopen OpenSubgroup.isClopen
 #align open_add_subgroup.is_clopen OpenAddSubgroup.isClopen
 

Mathlib/Topology/Category/Profinite/CofilteredLimit.lean

@@ -65,7 +65,7 @@ theorem exists_isClopen_of_cofiltered {U : Set C.pt} (hC : IsLimit C) (hU : IsCl
     -- Porting note: `<;> continuity` fails
   -- Using this, since `U` is open, we can write `U` as a union of clopen sets all of which
   -- are preimages of clopens from the factors in the limit.
-  obtain ⟨S, hS, h⟩ := hB.open_eq_sUnion hU.1
+  obtain ⟨S, hS, h⟩ := hB.open_eq_sUnion hU.2
   clear hB
   let j : S → J := fun s => (hS s.2).choose
   let V : ∀ s : S, Set (F.obj (j s)) := fun s => (hS s.2).choose_spec.choose
@@ -76,15 +76,15 @@ theorem exists_isClopen_of_cofiltered {U : Set C.pt} (hC : IsLimit C) (hU : IsCl
   -- clopens constructed in the previous step.
   have hUo : ∀ (i : ↑S), IsOpen ((fun s ↦ (forget Profinite).map (C.π.app (j s)) ⁻¹' V s) i)
   · intro s
-    exact (hV s).1.1.preimage (C.π.app (j s)).continuous
+    exact (hV s).1.2.preimage (C.π.app (j s)).continuous
   have hsU : U ⊆ ⋃ (i : ↑S), (fun s ↦ (forget Profinite).map (C.π.app (j s)) ⁻¹' V s) i
   · dsimp only
     rw [h]
     rintro x ⟨T, hT, hx⟩
     refine' ⟨_, ⟨⟨T, hT⟩, rfl⟩, _⟩
     dsimp only [forget_map_eq_coe]
     rwa [← (hV ⟨T, hT⟩).2]
-  have := hU.2.isCompact.elim_finite_subcover (fun s : S => C.π.app (j s) ⁻¹' V s) hUo hsU
+  have := hU.1.isCompact.elim_finite_subcover (fun s : S => C.π.app (j s) ⁻¹' V s) hUo hsU
   -- Porting note: same remark as after `hB`
   -- We thus obtain a finite set `G : Finset J` and a clopen set of `F.obj j` for each
   -- `j ∈ G` such that `U` is the union of the preimages of these clopen sets.

Mathlib/Topology/Category/Stonean/Limits.lean

@@ -182,14 +182,14 @@ def pullback : Stonean where
     dsimp at U
     have h : IsClopen (f ⁻¹' (Set.range i))
     · constructor
-      · exact IsOpen.preimage f.continuous hi.open_range
       · refine' IsClosed.preimage f.continuous _
         apply IsCompact.isClosed
         simp only [← Set.image_univ]
         exact IsCompact.image isCompact_univ i.continuous
-    have hU' : IsOpen (Subtype.val '' U) := h.1.openEmbedding_subtype_val.isOpenMap U hU
+      · exact IsOpen.preimage f.continuous hi.open_range
+    have hU' : IsOpen (Subtype.val '' U) := h.2.openEmbedding_subtype_val.isOpenMap U hU
     have := ExtremallyDisconnected.open_closure _ hU'
-    rw [h.2.closedEmbedding_subtype_val.closure_image_eq U] at this
+    rw [h.1.closedEmbedding_subtype_val.closure_image_eq U] at this
     suffices hhU : closure U = Subtype.val ⁻¹' (Subtype.val '' (closure U))
     · rw [hhU]
       exact isOpen_induced this

Mathlib/Topology/Clopen.lean

@@ -9,7 +9,7 @@ import Mathlib.Data.Set.BoolIndicator
 /-!
 # Clopen sets
 
-A clopen set is a set that is both open and closed.
+A clopen set is a set that is both closed and open.
 -/
 
 open Set Filter Topology TopologicalSpace Classical
@@ -22,23 +22,22 @@ variable [TopologicalSpace X] [TopologicalSpace Y] {s t : Set X}
 
 section Clopen
 
--- porting note: todo: redefine as `IsClosed s ∧ IsOpen s`
-/-- A set is clopen if it is both open and closed. -/
+/-- A set is clopen if it is both closed and open. -/
 def IsClopen (s : Set X) : Prop :=
-  IsOpen s ∧ IsClosed s
+  IsClosed s ∧ IsOpen s
 #align is_clopen IsClopen
 
-protected theorem IsClopen.isOpen (hs : IsClopen s) : IsOpen s := hs.1
+protected theorem IsClopen.isOpen (hs : IsClopen s) : IsOpen s := hs.2
 #align is_clopen.is_open IsClopen.isOpen
 
-protected theorem IsClopen.isClosed (hs : IsClopen s) : IsClosed s := hs.2
+protected theorem IsClopen.isClosed (hs : IsClopen s) : IsClosed s := hs.1
 #align is_clopen.is_closed IsClopen.isClosed
 
 theorem isClopen_iff_frontier_eq_empty : IsClopen s ↔ frontier s = ∅ := by
   rw [IsClopen, ← closure_eq_iff_isClosed, ← interior_eq_iff_isOpen, frontier, diff_eq_empty]
-  refine' ⟨fun h => (h.2.trans h.1.symm).subset, fun h => _⟩
-  exact ⟨interior_subset.antisymm (subset_closure.trans h),
-    (h.trans interior_subset).antisymm subset_closure⟩
+  refine' ⟨fun h => (h.1.trans h.2.symm).subset, fun h => _⟩
+  exact ⟨(h.trans interior_subset).antisymm subset_closure,
+    interior_subset.antisymm (subset_closure.trans h)⟩
 #align is_clopen_iff_frontier_eq_empty isClopen_iff_frontier_eq_empty
 
 @[simp] alias ⟨IsClopen.frontier_eq, _⟩ := isClopen_iff_frontier_eq_empty
@@ -52,14 +51,14 @@ theorem IsClopen.inter (hs : IsClopen s) (ht : IsClopen t) : IsClopen (s ∩ t)
   ⟨hs.1.inter ht.1, hs.2.inter ht.2⟩
 #align is_clopen.inter IsClopen.inter
 
-theorem isClopen_empty : IsClopen (∅ : Set X) := ⟨isOpen_empty, isClosed_empty⟩
+theorem isClopen_empty : IsClopen (∅ : Set X) := ⟨isClosed_empty, isOpen_empty⟩
 #align is_clopen_empty isClopen_empty
 
-theorem isClopen_univ : IsClopen (univ : Set X) := ⟨isOpen_univ, isClosed_univ⟩
+theorem isClopen_univ : IsClopen (univ : Set X) := ⟨isClosed_univ, isOpen_univ⟩
 #align is_clopen_univ isClopen_univ
 
 theorem IsClopen.compl (hs : IsClopen s) : IsClopen sᶜ :=
-  ⟨hs.2.isOpen_compl, hs.1.isClosed_compl⟩
+  ⟨hs.2.isClosed_compl, hs.1.isOpen_compl⟩
 #align is_clopen.compl IsClopen.compl
 
 @[simp]
@@ -77,12 +76,12 @@ theorem IsClopen.prod {t : Set Y} (hs : IsClopen s) (ht : IsClopen t) : IsClopen
 
 theorem isClopen_iUnion_of_finite [Finite Y] {s : Y → Set X} (h : ∀ i, IsClopen (s i)) :
     IsClopen (⋃ i, s i) :=
-  ⟨isOpen_iUnion (forall_and.1 h).1, isClosed_iUnion_of_finite (forall_and.1 h).2⟩
+  ⟨isClosed_iUnion_of_finite (forall_and.1 h).1, isOpen_iUnion (forall_and.1 h).2⟩
 #align is_clopen_Union isClopen_iUnion_of_finite
 
 theorem Set.Finite.isClopen_biUnion {s : Set Y} {f : Y → Set X} (hs : s.Finite)
     (h : ∀ i ∈ s, IsClopen <| f i) : IsClopen (⋃ i ∈ s, f i) :=
-  ⟨isOpen_biUnion fun i hi => (h i hi).1, hs.isClosed_biUnion fun i hi => (h i hi).2⟩
+  ⟨hs.isClosed_biUnion fun i hi => (h i hi).1, isOpen_biUnion fun i hi => (h i hi).2⟩
 #align is_clopen_bUnion Set.Finite.isClopen_biUnion
 
 theorem isClopen_biUnion_finset {s : Finset Y} {f : Y → Set X}
@@ -92,12 +91,12 @@ theorem isClopen_biUnion_finset {s : Finset Y} {f : Y → Set X}
 
 theorem isClopen_iInter_of_finite [Finite Y] {s : Y → Set X} (h : ∀ i, IsClopen (s i)) :
     IsClopen (⋂ i, s i) :=
-  ⟨isOpen_iInter_of_finite (forall_and.1 h).1, isClosed_iInter (forall_and.1 h).2⟩
+  ⟨isClosed_iInter (forall_and.1 h).1, isOpen_iInter_of_finite (forall_and.1 h).2⟩
 #align is_clopen_Inter isClopen_iInter_of_finite
 
 theorem Set.Finite.isClopen_biInter {s : Set Y} (hs : s.Finite) {f : Y → Set X}
     (h : ∀ i ∈ s, IsClopen (f i)) : IsClopen (⋂ i ∈ s, f i) :=
-  ⟨hs.isOpen_biInter fun i hi => (h i hi).1, isClosed_biInter fun i hi => (h i hi).2⟩
+  ⟨isClosed_biInter fun i hi => (h i hi).1, hs.isOpen_biInter fun i hi => (h i hi).2⟩
 #align is_clopen_bInter Set.Finite.isClopen_biInter
 
 theorem isClopen_biInter_finset {s : Finset Y} {f : Y → Set X}
@@ -112,15 +111,15 @@ theorem IsClopen.preimage {s : Set Y} (h : IsClopen s) {f : X → Y} (hf : Conti
 
 theorem ContinuousOn.preimage_isClopen_of_isClopen {f : X → Y} {s : Set X} {t : Set Y}
     (hf : ContinuousOn f s) (hs : IsClopen s) (ht : IsClopen t) : IsClopen (s ∩ f ⁻¹' t) :=
-  ⟨ContinuousOn.isOpen_inter_preimage hf hs.1 ht.1,
-    ContinuousOn.preimage_isClosed_of_isClosed hf hs.2 ht.2⟩
+  ⟨ContinuousOn.preimage_isClosed_of_isClosed hf hs.1 ht.1,
+    ContinuousOn.isOpen_inter_preimage hf hs.2 ht.2⟩
 #align continuous_on.preimage_clopen_of_clopen ContinuousOn.preimage_isClopen_of_isClopen
 
 /-- The intersection of a disjoint covering by two open sets of a clopen set will be clopen. -/
 theorem isClopen_inter_of_disjoint_cover_clopen {s a b : Set X} (h : IsClopen s) (cover : s ⊆ a ∪ b)
     (ha : IsOpen a) (hb : IsOpen b) (hab : Disjoint a b) : IsClopen (s ∩ a) := by
-  refine' ⟨IsOpen.inter h.1 ha, _⟩
-  have : IsClosed (s ∩ bᶜ) := IsClosed.inter h.2 (isClosed_compl_iff.2 hb)
+  refine' ⟨_, IsOpen.inter h.2 ha⟩
+  have : IsClosed (s ∩ bᶜ) := IsClosed.inter h.1 (isClosed_compl_iff.2 hb)
   convert this using 1
   refine' (inter_subset_inter_right s hab.subset_compl_right).antisymm _
   rintro x ⟨hx₁, hx₂⟩
@@ -129,36 +128,36 @@ theorem isClopen_inter_of_disjoint_cover_clopen {s a b : Set X} (h : IsClopen s)
 
 @[simp]
 theorem isClopen_discrete [DiscreteTopology X] (s : Set X) : IsClopen s :=
-  ⟨isOpen_discrete _, isClosed_discrete _⟩
+  ⟨isClosed_discrete _, isOpen_discrete _⟩
 #align is_clopen_discrete isClopen_discrete
 
 -- porting note: new lemma
 theorem isClopen_range_inl : IsClopen (range (Sum.inl : X → X ⊕ Y)) :=
-  ⟨isOpen_range_inl, isClosed_range_inl⟩
+  ⟨isClosed_range_inl, isOpen_range_inl⟩
 
 -- porting note: new lemma
 theorem isClopen_range_inr : IsClopen (range (Sum.inr : Y → X ⊕ Y)) :=
-  ⟨isOpen_range_inr, isClosed_range_inr⟩
+  ⟨isClosed_range_inr, isOpen_range_inr⟩
 
 theorem isClopen_range_sigmaMk {X : ι → Type*} [∀ i, TopologicalSpace (X i)] {i : ι} :
     IsClopen (Set.range (@Sigma.mk ι X i)) :=
-  ⟨openEmbedding_sigmaMk.open_range, closedEmbedding_sigmaMk.closed_range⟩
+  ⟨closedEmbedding_sigmaMk.closed_range, openEmbedding_sigmaMk.open_range⟩
 #align clopen_range_sigma_mk isClopen_range_sigmaMk
 
 protected theorem QuotientMap.isClopen_preimage {f : X → Y} (hf : QuotientMap f) {s : Set Y} :
     IsClopen (f ⁻¹' s) ↔ IsClopen s :=
-  and_congr hf.isOpen_preimage hf.isClosed_preimage
+  and_congr hf.isClosed_preimage hf.isOpen_preimage
 #align quotient_map.is_clopen_preimage QuotientMap.isClopen_preimage
 
 theorem continuous_boolIndicator_iff_isClopen (U : Set X) :
     Continuous U.boolIndicator ↔ IsClopen U := by
   constructor
   · intro hc
     rw [← U.preimage_boolIndicator_true]
-    exact ⟨(isOpen_discrete _).preimage hc, (isClosed_discrete _).preimage hc⟩
+    exact ⟨(isClosed_discrete _).preimage hc, (isOpen_discrete _).preimage hc, ⟩
   · refine' fun hU => ⟨fun s _ => _⟩
     rcases U.preimage_boolIndicator s with (h | h | h | h) <;> rw [h]
-    exacts [isOpen_univ, hU.1, hU.2.isOpen_compl, isOpen_empty]
+    exacts [isOpen_univ, hU.2, hU.1.isOpen_compl, isOpen_empty]
 #align continuous_bool_indicator_iff_clopen continuous_boolIndicator_iff_isClopen
 
 theorem continuousOn_boolIndicator_iff_isClopen (s U : Set X) :

Mathlib/Topology/ClopenBox.lean

@@ -37,7 +37,7 @@ theorem TopologicalSpace.Clopens.exists_prod_subset (W : Clopens (X × Y)) {a :
     ∃ U : Clopens X, a.1 ∈ U ∧ ∃ V : Clopens Y, a.2 ∈ V ∧ U ×ˢ V ≤ W := by
   have hp : Continuous (fun y : Y ↦ (a.1, y)) := Continuous.Prod.mk _
   let V : Set Y := {y | (a.1, y) ∈ W}
-  have hV : IsCompact V := (W.2.2.preimage hp).isCompact
+  have hV : IsCompact V := (W.2.1.preimage hp).isCompact
   let U : Set X := {x | MapsTo (Prod.mk x) V W}
   have hUV : U ×ˢ V ⊆ W := fun ⟨_, _⟩ hw ↦ hw.1 hw.2
   exact ⟨⟨U, (ContinuousMap.isClopen_setOf_mapsTo hV W.2).preimage
@@ -50,7 +50,7 @@ is a union of finitely many clopen boxes. -/
 theorem TopologicalSpace.Clopens.exists_finset_eq_sup_prod (W : Clopens (X × Y)) :
     ∃ (I : Finset (Clopens X × Clopens Y)), W = I.sup fun i ↦ i.1 ×ˢ i.2 := by
   choose! U hxU V hxV hUV using fun x ↦ W.exists_prod_subset (a := x)
-  rcases W.2.2.isCompact.elim_nhds_subcover (fun x ↦ U x ×ˢ V x) (fun x hx ↦
+  rcases W.2.1.isCompact.elim_nhds_subcover (fun x ↦ U x ×ˢ V x) (fun x hx ↦
     (U x ×ˢ V x).2.isOpen.mem_nhds ⟨hxU x hx, hxV x hx⟩) with ⟨I, hIW, hWI⟩
   classical
   use I.image fun x ↦ (U x, V x)

Mathlib/Topology/CompactOpen.lean

@@ -201,7 +201,7 @@ lemma isClosed_setOf_mapsTo {t : Set Y} (ht : IsClosed t) (s : Set X) :
 
 lemma isClopen_setOf_mapsTo (hK : IsCompact K) (hU : IsClopen U) :
     IsClopen {f : C(X, Y) | MapsTo f K U} :=
-  ⟨isOpen_setOf_mapsTo hK hU.isOpen, isClosed_setOf_mapsTo hU.isClosed K⟩
+  ⟨isClosed_setOf_mapsTo hU.isClosed K, isOpen_setOf_mapsTo hK hU.isOpen⟩
 
 instance [T0Space Y] : T0Space C(X, Y) :=
   t0Space_of_injective_of_continuous DFunLike.coe_injective continuous_coe

Mathlib/Topology/Connected/Basic.lean

@@ -873,7 +873,7 @@ theorem isClopen_iff [PreconnectedSpace α] {s : Set α} : IsClopen s ↔ s = 
         ⟨mt Or.inl h,
           mt (fun h2 => Or.inr <| (by rw [← compl_compl s, h2, compl_empty] : s = univ)) h⟩
       let ⟨_, h2, h3⟩ :=
-        nonempty_inter hs.1 hs.2.isOpen_compl (union_compl_self s) (nonempty_iff_ne_empty.2 h1.1)
+        nonempty_inter hs.2 hs.1.isOpen_compl (union_compl_self s) (nonempty_iff_ne_empty.2 h1.1)
           (nonempty_iff_ne_empty.2 h1.2)
       h3 h2,
     by rintro (rfl | rfl) <;> [exact isClopen_empty; exact isClopen_univ]⟩
@@ -910,7 +910,7 @@ element. -/
 lemma subsingleton_of_disjoint_isOpen_iUnion_eq_univ
     (h_open : ∀ i, IsOpen (s i)) (h_Union : ⋃ i, s i = univ) :
     Subsingleton ι := by
-  refine' subsingleton_of_disjoint_isClopen h_nonempty h_disj (fun i ↦ ⟨h_open i, _⟩)
+  refine' subsingleton_of_disjoint_isClopen h_nonempty h_disj (fun i ↦ ⟨_, h_open i⟩)
   rw [← isOpen_compl_iff, compl_eq_univ_diff, ← h_Union, iUnion_diff]
   refine' isOpen_iUnion (fun j ↦ _)
   rcases eq_or_ne i j with rfl | h_ne
@@ -922,7 +922,7 @@ element. -/
 lemma subsingleton_of_disjoint_isClosed_iUnion_eq_univ [Finite ι]
     (h_closed : ∀ i, IsClosed (s i)) (h_Union : ⋃ i, s i = univ) :
     Subsingleton ι := by
-  refine' subsingleton_of_disjoint_isClopen h_nonempty h_disj (fun i ↦ ⟨_, h_closed i⟩)
+  refine' subsingleton_of_disjoint_isClopen h_nonempty h_disj (fun i ↦ ⟨h_closed i, _⟩)
   rw [← isClosed_compl_iff, compl_eq_univ_diff, ← h_Union, iUnion_diff]
   refine' isClosed_iUnion_of_finite (fun j ↦ _)
   rcases eq_or_ne i j with rfl | h_ne
@@ -968,14 +968,14 @@ lemma PreconnectedSpace.induction₂' [PreconnectedSpace α] (P : α → α →
     (h : ∀ x, ∀ᶠ y in 𝓝 x, P x y ∧ P y x) (h' : Transitive P) (x y : α) :
     P x y := by
   let u := {z | P x z}
-  have A : IsOpen u := by
-    apply isOpen_iff_mem_nhds.2 (fun z hz ↦ ?_)
-    filter_upwards [h z] with t ht
-    exact h' hz ht.1
-  have B : IsClosed u := by
+  have A : IsClosed u := by
     apply isClosed_iff_nhds.2 (fun z hz ↦ ?_)
     rcases hz _ (h z) with ⟨t, ht, h't⟩
     exact h' h't ht.2
+  have B : IsOpen u := by
+    apply isOpen_iff_mem_nhds.2 (fun z hz ↦ ?_)
+    filter_upwards [h z] with t ht
+    exact h' hz ht.1
   have C : u.Nonempty := ⟨x, (mem_of_mem_nhds (h x)).1⟩
   have D : u = Set.univ := IsClopen.eq_univ ⟨A, B⟩ C
   show y ∈ u
@@ -1329,9 +1329,9 @@ theorem isPreconnected_of_forall_constant {s : Set α}
   have hy : y ∉ u := fun y_in_u => eq_empty_iff_forall_not_mem.mp H y ⟨y_in_s, ⟨y_in_u, y_in_v⟩⟩
   have : ContinuousOn u.boolIndicator s := by
     apply (continuousOn_boolIndicator_iff_isClopen _ _).mpr ⟨_, _⟩
-    · exact u_op.preimage continuous_subtype_val
     · rw [preimage_subtype_coe_eq_compl hsuv H]
       exact (v_op.preimage continuous_subtype_val).isClosed_compl
+    · exact u_op.preimage continuous_subtype_val
   simpa [(u.mem_iff_boolIndicator _).mp x_in_u, (u.not_mem_iff_boolIndicator _).mp hy] using
     hs _ this x x_in_s y y_in_s
 #align is_preconnected_of_forall_constant isPreconnected_of_forall_constant

Mathlib/Topology/Connected/LocallyConnected.lean

@@ -83,7 +83,7 @@ theorem isOpen_connectedComponent [LocallyConnectedSpace α] {x : α} :
 
 theorem isClopen_connectedComponent [LocallyConnectedSpace α] {x : α} :
     IsClopen (connectedComponent x) :=
-  ⟨isOpen_connectedComponent, isClosed_connectedComponent⟩
+  ⟨isClosed_connectedComponent, isOpen_connectedComponent⟩
 #align is_clopen_connected_component isClopen_connectedComponent
 
 theorem locallyConnectedSpace_iff_connectedComponentIn_open :

Mathlib/Topology/Connected/PathConnected.lean

@@ -1276,17 +1276,17 @@ theorem pathConnectedSpace_iff_connectedSpace [LocPathConnectedSpace X] :
     rw [pathConnectedSpace_iff_eq]
     use Classical.arbitrary X
     refine' IsClopen.eq_univ ⟨_, _⟩ (by simp)
+    · rw [isClosed_iff_nhds]
+      intro y H
+      rcases (path_connected_basis y).ex_mem with ⟨U, ⟨U_in, hU⟩⟩
+      rcases H U U_in with ⟨z, hz, hz'⟩
+      exact (hU.joinedIn z hz y <| mem_of_mem_nhds U_in).joined.mem_pathComponent hz'
     · rw [isOpen_iff_mem_nhds]
       intro y y_in
       rcases (path_connected_basis y).ex_mem with ⟨U, ⟨U_in, hU⟩⟩
       apply mem_of_superset U_in
       rw [← pathComponent_congr y_in]
       exact hU.subset_pathComponent (mem_of_mem_nhds U_in)
-    · rw [isClosed_iff_nhds]
-      intro y H
-      rcases (path_connected_basis y).ex_mem with ⟨U, ⟨U_in, hU⟩⟩
-      rcases H U U_in with ⟨z, hz, hz'⟩
-      exact (hU.joinedIn z hz y <| mem_of_mem_nhds U_in).joined.mem_pathComponent hz'
 #align path_connected_space_iff_connected_space pathConnectedSpace_iff_connectedSpace
 
 theorem pathConnected_subset_basis [LocPathConnectedSpace X] {U : Set X} (h : IsOpen U)