From df7df2a5f78d6bebd0dca8c08c6665352f54b3fa Mon Sep 17 00:00:00 2001
From: ADedecker <anatolededecker@gmail.com>
Date: Mon, 11 May 2026 18:57:12 -0400
Subject: [PATCH 1/5] ++

---
 Mathlib/Logic/Equiv/Quotient.lean | 37 +++++++++++++++++++++++++++++++
 1 file changed, 37 insertions(+)
 create mode 100644 Mathlib/Logic/Equiv/Quotient.lean

diff --git a/Mathlib/Logic/Equiv/Quotient.lean b/Mathlib/Logic/Equiv/Quotient.lean
new file mode 100644
index 00000000000000..8b7c368b79e211
--- /dev/null
+++ b/Mathlib/Logic/Equiv/Quotient.lean
@@ -0,0 +1,37 @@
+/-
+Copyright (c) 2026 Anatole Dedecker. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Anatole Dedecker
+-/
+module
+
+public import Mathlib.Data.Set.Function
+public import Mathlib.Logic.Equiv.Defs
+
+/-!
+# Equivalences and quotients
+
+In this file we provide facts relating `Equiv` and `Quotient`.
+-/
+
+@[expose] public section
+
+open Function Set
+
+variable {α β γ : Type*}
+
+namespace Equiv
+
+@[simps]
+protected def quotCongr {r s : α → α → Prop} (eq : r = s) : Quot r ≃ Quot s where
+  toFun := Quot.lift (Quot.mk s) (by simp [eq, Quot.congr_mk])
+  invFun := sorry
+  left_inv := sorry
+  right_inv := sorry
+
+/-- If `α` is equivalent to `β`, then `Set α` is equivalent to `Set β`. -/
+@[simps]
+protected def congr {α β : Type*} (e : α ≃ β) : Set α ≃ Set β :=
+  ⟨fun s => e '' s, fun t => e.symm '' t, symm_image_image e, symm_image_image e.symm⟩
+
+end Equiv

From 84a1836cc39fc73f32e06ef91e82c26ef7e984e5 Mon Sep 17 00:00:00 2001
From: ADedecker <anatolededecker@gmail.com>
Date: Tue, 12 May 2026 14:59:44 -0400
Subject: [PATCH 2/5] ++

---
 Mathlib/Data/Setoid/Basic.lean            |  8 +++
 Mathlib/Logic/Equiv/Quotient.lean         | 37 -------------
 Mathlib/Topology/Constructions.lean       |  6 +++
 Mathlib/Topology/Homeomorph/Quotient.lean | 64 +++++++++++++++++++++++
 4 files changed, 78 insertions(+), 37 deletions(-)
 delete mode 100644 Mathlib/Logic/Equiv/Quotient.lean
 create mode 100644 Mathlib/Topology/Homeomorph/Quotient.lean

diff --git a/Mathlib/Data/Setoid/Basic.lean b/Mathlib/Data/Setoid/Basic.lean
index edb9c8209339df..0547b8285f1049 100644
--- a/Mathlib/Data/Setoid/Basic.lean
+++ b/Mathlib/Data/Setoid/Basic.lean
@@ -228,6 +228,14 @@ def map_sInf {S : Set (Setoid α)} {s : Setoid α} (h : s ∈ S) :
     Quotient (sInf S) → Quotient s :=
   Setoid.map_of_le fun _ _ a ↦ a s h
 
+/-- The quotient by the trivial relation is equivalent to the original space. -/
+def quotientBotEquiv :
+    Quotient (⊥ : Setoid α) ≃ α where
+  toFun := Quotient.lift id (fun _ _ ↦ id)
+  invFun := Quotient.mk''
+  left_inv := Quotient.ind fun _ ↦ rfl
+  right_inv := fun _ ↦ rfl
+
 section EqvGen
 
 open Relation
diff --git a/Mathlib/Logic/Equiv/Quotient.lean b/Mathlib/Logic/Equiv/Quotient.lean
deleted file mode 100644
index 8b7c368b79e211..00000000000000
--- a/Mathlib/Logic/Equiv/Quotient.lean
+++ /dev/null
@@ -1,37 +0,0 @@
-/-
-Copyright (c) 2026 Anatole Dedecker. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Anatole Dedecker
--/
-module
-
-public import Mathlib.Data.Set.Function
-public import Mathlib.Logic.Equiv.Defs
-
-/-!
-# Equivalences and quotients
-
-In this file we provide facts relating `Equiv` and `Quotient`.
--/
-
-@[expose] public section
-
-open Function Set
-
-variable {α β γ : Type*}
-
-namespace Equiv
-
-@[simps]
-protected def quotCongr {r s : α → α → Prop} (eq : r = s) : Quot r ≃ Quot s where
-  toFun := Quot.lift (Quot.mk s) (by simp [eq, Quot.congr_mk])
-  invFun := sorry
-  left_inv := sorry
-  right_inv := sorry
-
-/-- If `α` is equivalent to `β`, then `Set α` is equivalent to `Set β`. -/
-@[simps]
-protected def congr {α β : Type*} (e : α ≃ β) : Set α ≃ Set β :=
-  ⟨fun s => e '' s, fun t => e.symm '' t, symm_image_image e, symm_image_image e.symm⟩
-
-end Equiv
diff --git a/Mathlib/Topology/Constructions.lean b/Mathlib/Topology/Constructions.lean
index 6f88474bbad152..86330aca6eaff4 100644
--- a/Mathlib/Topology/Constructions.lean
+++ b/Mathlib/Topology/Constructions.lean
@@ -702,6 +702,12 @@ theorem continuous_quot_lift {f : X → Y} (hr : ∀ a b, r a b → f a = f b) (
     Continuous (Quot.lift f hr : Quot r → Y) :=
   continuous_coinduced_dom.2 h
 
+@[continuity, fun_prop]
+theorem continuous_quot_map {r' : Y → Y → Prop} {f : X → Y} (hr : ∀ a b, r a b → r' (f a) (f b))
+    (h : Continuous f) :
+    Continuous (Quot.map f hr : Quot r → Quot r') :=
+  continuous_quot_lift _ (continuous_quot_mk.comp h)
+
 theorem isQuotientMap_quotient_mk' : IsQuotientMap (@Quotient.mk' X s) :=
   isQuotientMap_quot_mk
 
diff --git a/Mathlib/Topology/Homeomorph/Quotient.lean b/Mathlib/Topology/Homeomorph/Quotient.lean
new file mode 100644
index 00000000000000..c27063394665c7
--- /dev/null
+++ b/Mathlib/Topology/Homeomorph/Quotient.lean
@@ -0,0 +1,64 @@
+/-
+Copyright (c) 2026 Anatole Dedecker. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Anatole Dedecker
+-/
+module
+
+public import Mathlib.Topology.Homeomorph.Lemmas
+
+/-!
+# Homeomorphisms between quotient spaces
+-/
+
+@[expose] public section
+
+namespace Homeomorph
+
+variable {α β : Type*} [TopologicalSpace α] [TopologicalSpace β]
+
+namespace Quot
+
+/-- An homeomorphism `e : α ≃ₜ β` generates an homeomorphism between quotient spaces,
+if `ra a₁ a₂ ↔ rb (e a₁) (e a₂)`. -/
+protected def congr {ra : α → α → Prop} {rb : β → β → Prop} (e : α ≃ₜ β)
+    (eq : ∀ a₁ a₂, ra a₁ a₂ ↔ rb (e a₁) (e a₂)) : Quot ra ≃ₜ Quot rb where
+  toEquiv := _root_.Quot.congr e eq
+  continuous_toFun := continuous_quot_map (fun x y ↦ by simp [eq]) e.continuous
+  continuous_invFun := continuous_quot_map (fun x y ↦ by simp [eq]) e.symm.continuous
+
+/-- Quotient spaces for equal relations are homeomorphic. -/
+protected def congrRight {r r' : α → α → Prop} (eq : ∀ a₁ a₂, r a₁ a₂ ↔ r' a₁ a₂) :
+    Quot r ≃ₜ Quot r' := Quot.congr (Homeomorph.refl α) eq
+
+/-- An homeomorphism `e : α ≃ₜ β` generates an equivalence between the quotient space of `α`
+by a relation `ra` and the quotient space of `β` by the image of this relation under `e`. -/
+protected def congrLeft {r : α → α → Prop} (e : α ≃ₜ β) :
+    Quot r ≃ₜ Quot fun b b' => r (e.symm b) (e.symm b') :=
+  Quot.congr e fun _ _ => by simp only [e.symm_apply_apply]
+
+end Quot
+
+namespace Quotient
+
+/-- An homeomorphism `e : α ≃ₜ β` generates an homeomorphism between quotient spaces,
+if `ra a₁ a₂ ↔ rb (e a₁) (e a₂)`. -/
+protected def congr {ra : Setoid α} {rb : Setoid β} (e : α ≃ₜ β)
+    (eq : ∀ a₁ a₂, ra a₁ a₂ ↔ rb (e a₁) (e a₂)) :
+    Quotient ra ≃ₜ Quotient rb := Quot.congr e eq
+
+/-- Quotient spaces for equal relations are homeomorphic. -/
+protected def congrRight {r r' : Setoid α}
+    (eq : ∀ a₁ a₂, r a₁ a₂ ↔ r' a₁ a₂) : Quotient r ≃ₜ Quotient r' :=
+  Quot.congrRight eq
+
+end Quotient
+
+/-- The quotient by the trivial relation is homeomorphic to the original space. -/
+def quotientBot :
+    Quotient (⊥ : Setoid α) ≃ₜ α where
+  toEquiv := Setoid.quotientBotEquiv
+  continuous_toFun := continuous_quot_lift _ continuous_id
+  continuous_invFun := continuous_quot_mk
+
+end Homeomorph

From 1f1edaab0335c6d1b5f847b0cda657c75005977d Mon Sep 17 00:00:00 2001
From: ADedecker <anatolededecker@gmail.com>
Date: Tue, 12 May 2026 15:03:07 -0400
Subject: [PATCH 3/5] mk_all

---
 Mathlib.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Mathlib.lean b/Mathlib.lean
index 4460548cdfeedf..2f45e6efa2056b 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -7714,6 +7714,7 @@ public import Mathlib.Topology.Hom.ContinuousEvalConst
 public import Mathlib.Topology.Hom.Open
 public import Mathlib.Topology.Homeomorph.Defs
 public import Mathlib.Topology.Homeomorph.Lemmas
+public import Mathlib.Topology.Homeomorph.Quotient
 public import Mathlib.Topology.Homeomorph.TransferInstance
 public import Mathlib.Topology.Homotopy.Affine
 public import Mathlib.Topology.Homotopy.Basic

From 2c7958b427f12bb412915db4e90a23a254ce6935 Mon Sep 17 00:00:00 2001
From: ADedecker <anatolededecker@gmail.com>
Date: Tue, 12 May 2026 16:11:23 -0400
Subject: [PATCH 4/5] suggestions

---
 Mathlib/Topology/Homeomorph/Quotient.lean | 38 +++++++++++------------
 1 file changed, 19 insertions(+), 19 deletions(-)

diff --git a/Mathlib/Topology/Homeomorph/Quotient.lean b/Mathlib/Topology/Homeomorph/Quotient.lean
index c27063394665c7..85363c4f59a2d5 100644
--- a/Mathlib/Topology/Homeomorph/Quotient.lean
+++ b/Mathlib/Topology/Homeomorph/Quotient.lean
@@ -15,40 +15,40 @@ public import Mathlib.Topology.Homeomorph.Lemmas
 
 namespace Homeomorph
 
-variable {α β : Type*} [TopologicalSpace α] [TopologicalSpace β]
+variable {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y]
 
 namespace Quot
 
-/-- An homeomorphism `e : α ≃ₜ β` generates an homeomorphism between quotient spaces,
-if `ra a₁ a₂ ↔ rb (e a₁) (e a₂)`. -/
-protected def congr {ra : α → α → Prop} {rb : β → β → Prop} (e : α ≃ₜ β)
-    (eq : ∀ a₁ a₂, ra a₁ a₂ ↔ rb (e a₁) (e a₂)) : Quot ra ≃ₜ Quot rb where
+/-- An homeomorphism `e : X ≃ₜ Y` generXtes an homeomorphism between quotient spaces,
+if `rX a₁ a₂ ↔ rY (e a₁) (e a₂)`. -/
+protected def congr {rX : X → X → Prop} {rY : Y → Y → Prop} (e : X ≃ₜ Y)
+    (eq : ∀ a₁ a₂, rX a₁ a₂ ↔ rY (e a₁) (e a₂)) : Quot rX ≃ₜ Quot rY where
   toEquiv := _root_.Quot.congr e eq
   continuous_toFun := continuous_quot_map (fun x y ↦ by simp [eq]) e.continuous
   continuous_invFun := continuous_quot_map (fun x y ↦ by simp [eq]) e.symm.continuous
 
 /-- Quotient spaces for equal relations are homeomorphic. -/
-protected def congrRight {r r' : α → α → Prop} (eq : ∀ a₁ a₂, r a₁ a₂ ↔ r' a₁ a₂) :
-    Quot r ≃ₜ Quot r' := Quot.congr (Homeomorph.refl α) eq
+protected def congrRight {r r' : X → X → Prop} (eq : ∀ a₁ a₂, r a₁ a₂ ↔ r' a₁ a₂) :
+    Quot r ≃ₜ Quot r' := Quot.congr (Homeomorph.refl X) eq
 
-/-- An homeomorphism `e : α ≃ₜ β` generates an equivalence between the quotient space of `α`
-by a relation `ra` and the quotient space of `β` by the image of this relation under `e`. -/
-protected def congrLeft {r : α → α → Prop} (e : α ≃ₜ β) :
-    Quot r ≃ₜ Quot fun b b' => r (e.symm b) (e.symm b') :=
-  Quot.congr e fun _ _ => by simp only [e.symm_apply_apply]
+/-- An homeomorphism `e : X ≃ₜ Y` generXtes an equivalence between the quotient space of `X`
+by a relation `rX` and the quotient space of `Y` by the image of this relation under `e`. -/
+protected def congrLeft {r : X → X → Prop} (e : X ≃ₜ Y) :
+    Quot r ≃ₜ Quot fun b b' ↦ r (e.symm b) (e.symm b') :=
+  Quot.congr e fun _ _ ↦ by simp only [e.symm_apply_apply]
 
 end Quot
 
 namespace Quotient
 
-/-- An homeomorphism `e : α ≃ₜ β` generates an homeomorphism between quotient spaces,
-if `ra a₁ a₂ ↔ rb (e a₁) (e a₂)`. -/
-protected def congr {ra : Setoid α} {rb : Setoid β} (e : α ≃ₜ β)
-    (eq : ∀ a₁ a₂, ra a₁ a₂ ↔ rb (e a₁) (e a₂)) :
-    Quotient ra ≃ₜ Quotient rb := Quot.congr e eq
+/-- An homeomorphism `e : X ≃ₜ Y` generXtes an homeomorphism between quotient spaces,
+if `rX a₁ a₂ ↔ rY (e a₁) (e a₂)`. -/
+protected def congr {rX : Setoid X} {rY : Setoid Y} (e : X ≃ₜ Y)
+    (eq : ∀ a₁ a₂, rX a₁ a₂ ↔ rY (e a₁) (e a₂)) :
+    Quotient rX ≃ₜ Quotient rY := Quot.congr e eq
 
 /-- Quotient spaces for equal relations are homeomorphic. -/
-protected def congrRight {r r' : Setoid α}
+protected def congrRight {r r' : Setoid X}
     (eq : ∀ a₁ a₂, r a₁ a₂ ↔ r' a₁ a₂) : Quotient r ≃ₜ Quotient r' :=
   Quot.congrRight eq
 
@@ -56,7 +56,7 @@ end Quotient
 
 /-- The quotient by the trivial relation is homeomorphic to the original space. -/
 def quotientBot :
-    Quotient (⊥ : Setoid α) ≃ₜ α where
+    Quotient (⊥ : Setoid X) ≃ₜ X where
   toEquiv := Setoid.quotientBotEquiv
   continuous_toFun := continuous_quot_lift _ continuous_id
   continuous_invFun := continuous_quot_mk

From afdcf3784a5409e7019ca1ef338e4dec6f4dee7d Mon Sep 17 00:00:00 2001
From: ADedecker <anatolededecker@gmail.com>
Date: Tue, 12 May 2026 16:12:53 -0400
Subject: [PATCH 5/5] var names

---
 Mathlib/Topology/Homeomorph/Quotient.lean | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/Mathlib/Topology/Homeomorph/Quotient.lean b/Mathlib/Topology/Homeomorph/Quotient.lean
index 85363c4f59a2d5..5091da4c6fefe1 100644
--- a/Mathlib/Topology/Homeomorph/Quotient.lean
+++ b/Mathlib/Topology/Homeomorph/Quotient.lean
@@ -20,21 +20,21 @@ variable {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y]
 namespace Quot
 
 /-- An homeomorphism `e : X ≃ₜ Y` generXtes an homeomorphism between quotient spaces,
-if `rX a₁ a₂ ↔ rY (e a₁) (e a₂)`. -/
+if `rX x₁ x₂ ↔ rY (e x₁) (e x₂)`. -/
 protected def congr {rX : X → X → Prop} {rY : Y → Y → Prop} (e : X ≃ₜ Y)
-    (eq : ∀ a₁ a₂, rX a₁ a₂ ↔ rY (e a₁) (e a₂)) : Quot rX ≃ₜ Quot rY where
+    (eq : ∀ x₁ x₂, rX x₁ x₂ ↔ rY (e x₁) (e x₂)) : Quot rX ≃ₜ Quot rY where
   toEquiv := _root_.Quot.congr e eq
   continuous_toFun := continuous_quot_map (fun x y ↦ by simp [eq]) e.continuous
   continuous_invFun := continuous_quot_map (fun x y ↦ by simp [eq]) e.symm.continuous
 
 /-- Quotient spaces for equal relations are homeomorphic. -/
-protected def congrRight {r r' : X → X → Prop} (eq : ∀ a₁ a₂, r a₁ a₂ ↔ r' a₁ a₂) :
+protected def congrRight {r r' : X → X → Prop} (eq : ∀ x₁ x₂, r x₁ x₂ ↔ r' x₁ x₂) :
     Quot r ≃ₜ Quot r' := Quot.congr (Homeomorph.refl X) eq
 
 /-- An homeomorphism `e : X ≃ₜ Y` generXtes an equivalence between the quotient space of `X`
 by a relation `rX` and the quotient space of `Y` by the image of this relation under `e`. -/
 protected def congrLeft {r : X → X → Prop} (e : X ≃ₜ Y) :
-    Quot r ≃ₜ Quot fun b b' ↦ r (e.symm b) (e.symm b') :=
+    Quot r ≃ₜ Quot fun y₁ y₂ ↦ r (e.symm y₁) (e.symm y₂) :=
   Quot.congr e fun _ _ ↦ by simp only [e.symm_apply_apply]
 
 end Quot
@@ -42,14 +42,14 @@ end Quot
 namespace Quotient
 
 /-- An homeomorphism `e : X ≃ₜ Y` generXtes an homeomorphism between quotient spaces,
-if `rX a₁ a₂ ↔ rY (e a₁) (e a₂)`. -/
+if `rX x₁ x₂ ↔ rY (e x₁) (e x₂)`. -/
 protected def congr {rX : Setoid X} {rY : Setoid Y} (e : X ≃ₜ Y)
-    (eq : ∀ a₁ a₂, rX a₁ a₂ ↔ rY (e a₁) (e a₂)) :
+    (eq : ∀ x₁ x₂, rX x₁ x₂ ↔ rY (e x₁) (e x₂)) :
     Quotient rX ≃ₜ Quotient rY := Quot.congr e eq
 
 /-- Quotient spaces for equal relations are homeomorphic. -/
 protected def congrRight {r r' : Setoid X}
-    (eq : ∀ a₁ a₂, r a₁ a₂ ↔ r' a₁ a₂) : Quotient r ≃ₜ Quotient r' :=
+    (eq : ∀ x₁ x₂, r x₁ x₂ ↔ r' x₁ x₂) : Quotient r ≃ₜ Quotient r' :=
   Quot.congrRight eq
 
 end Quotient