From 37b8fe573f0a6bc9d622141fb7b62da5928ff2bf Mon Sep 17 00:00:00 2001
From: Michael Rothgang <rothgami@math.hu-berlin.de>
Date: Thu, 25 Jan 2024 01:14:18 +0100
Subject: [PATCH 1/2] First version.

---
 Mathlib/Topology/Connected/Basic.lean | 7 +++++++
 Mathlib/Topology/Homeomorph.lean      | 7 +++++++
 2 files changed, 14 insertions(+)

diff --git a/Mathlib/Topology/Connected/Basic.lean b/Mathlib/Topology/Connected/Basic.lean
index e3091aefd5805..651fc5b990023 100644
--- a/Mathlib/Topology/Connected/Basic.lean
+++ b/Mathlib/Topology/Connected/Basic.lean
@@ -707,6 +707,13 @@ theorem Continuous.image_connectedComponent_subset [TopologicalSpace β] {f : α
     ((mem_image f (connectedComponent a) (f a)).2 ⟨a, mem_connectedComponent, rfl⟩)
 #align continuous.image_connected_component_subset Continuous.image_connectedComponent_subset
 
+theorem Continuous.image_connectedComponentIn_subset [TopologicalSpace β] {f : α → β} {s : Set α}
+    {x : α} (hf : Continuous f) (hx : x ∈ s) :
+    f '' connectedComponentIn s x ⊆ connectedComponentIn (f '' s) (f x) :=
+  (isPreconnected_connectedComponentIn.image _ hf.continuousOn).subset_connectedComponentIn
+    (mem_image_of_mem _ <| mem_connectedComponentIn hx)
+    (image_subset _ <| connectedComponentIn_subset _ _)
+
 theorem Continuous.mapsTo_connectedComponent [TopologicalSpace β] {f : α → β} (h : Continuous f)
     (a : α) : MapsTo f (connectedComponent a) (connectedComponent (f a)) :=
   mapsTo'.2 <| h.image_connectedComponent_subset a
diff --git a/Mathlib/Topology/Homeomorph.lean b/Mathlib/Topology/Homeomorph.lean
index b4b116bd5828d..69e59228badfe 100644
--- a/Mathlib/Topology/Homeomorph.lean
+++ b/Mathlib/Topology/Homeomorph.lean
@@ -318,6 +318,13 @@ theorem isConnected_preimage {s : Set Y} (h : X ≃ₜ Y) :
     IsConnected (h ⁻¹' s) ↔ IsConnected s := by
   rw [← image_symm, isConnected_image]
 
+theorem image_connectedComponentIn {s : Set X} (h : X ≃ₜ Y) {x : X} (hx : x ∈ s) :
+    h '' connectedComponentIn s x = connectedComponentIn (h '' s) (h x) := by
+  refine' (h.continuous.image_connectedComponentIn_subset hx).antisymm _
+  have := h.symm.continuous.image_connectedComponentIn_subset (mem_image_of_mem h hx)
+  rwa [image_subset_iff, h.preimage_symm, h.image_symm, h.preimage_image, h.symm_apply_apply]
+    at this
+
 @[simp]
 theorem comap_cocompact (h : X ≃ₜ Y) : comap h (cocompact Y) = cocompact X :=
   (comap_cocompact_le h.continuous).antisymm <|

From a40752866ec0d620ed47e250f8963dfe866cef1b Mon Sep 17 00:00:00 2001
From: Michael Rothgang <rothgami@math.hu-berlin.de>
Date: Thu, 25 Jan 2024 16:56:18 +0100
Subject: [PATCH 2/2] Suggestions from code review.

---
 Mathlib/Topology/Connected/Basic.lean | 9 +++++++--
 Mathlib/Topology/Homeomorph.lean      | 2 +-
 2 files changed, 8 insertions(+), 3 deletions(-)

diff --git a/Mathlib/Topology/Connected/Basic.lean b/Mathlib/Topology/Connected/Basic.lean
index 651fc5b990023..93592ef7897d0 100644
--- a/Mathlib/Topology/Connected/Basic.lean
+++ b/Mathlib/Topology/Connected/Basic.lean
@@ -708,8 +708,8 @@ theorem Continuous.image_connectedComponent_subset [TopologicalSpace β] {f : α
 #align continuous.image_connected_component_subset Continuous.image_connectedComponent_subset
 
 theorem Continuous.image_connectedComponentIn_subset [TopologicalSpace β] {f : α → β} {s : Set α}
-    {x : α} (hf : Continuous f) (hx : x ∈ s) :
-    f '' connectedComponentIn s x ⊆ connectedComponentIn (f '' s) (f x) :=
+    {a : α} (hf : Continuous f) (hx : a ∈ s) :
+    f '' connectedComponentIn s a ⊆ connectedComponentIn (f '' s) (f a) :=
   (isPreconnected_connectedComponentIn.image _ hf.continuousOn).subset_connectedComponentIn
     (mem_image_of_mem _ <| mem_connectedComponentIn hx)
     (image_subset _ <| connectedComponentIn_subset _ _)
@@ -719,6 +719,11 @@ theorem Continuous.mapsTo_connectedComponent [TopologicalSpace β] {f : α → 
   mapsTo'.2 <| h.image_connectedComponent_subset a
 #align continuous.maps_to_connected_component Continuous.mapsTo_connectedComponent
 
+theorem Continuous.mapsTo_connectedComponentIn [TopologicalSpace β] {f : α → β} {s : Set α}
+    (h : Continuous f) {a : α} (hx : a ∈ s) :
+    MapsTo f (connectedComponentIn s a) (connectedComponentIn (f '' s) (f a)) :=
+  mapsTo'.2 <| image_connectedComponentIn_subset h hx
+
 theorem irreducibleComponent_subset_connectedComponent {x : α} :
     irreducibleComponent x ⊆ connectedComponent x :=
   isIrreducible_irreducibleComponent.isConnected.subset_connectedComponent mem_irreducibleComponent
diff --git a/Mathlib/Topology/Homeomorph.lean b/Mathlib/Topology/Homeomorph.lean
index 69e59228badfe..358ce8d5f3963 100644
--- a/Mathlib/Topology/Homeomorph.lean
+++ b/Mathlib/Topology/Homeomorph.lean
@@ -320,7 +320,7 @@ theorem isConnected_preimage {s : Set Y} (h : X ≃ₜ Y) :
 
 theorem image_connectedComponentIn {s : Set X} (h : X ≃ₜ Y) {x : X} (hx : x ∈ s) :
     h '' connectedComponentIn s x = connectedComponentIn (h '' s) (h x) := by
-  refine' (h.continuous.image_connectedComponentIn_subset hx).antisymm _
+  refine (h.continuous.image_connectedComponentIn_subset hx).antisymm ?_
   have := h.symm.continuous.image_connectedComponentIn_subset (mem_image_of_mem h hx)
   rwa [image_subset_iff, h.preimage_symm, h.image_symm, h.preimage_image, h.symm_apply_apply]
     at this