From 724eff208245711448b900fff6f7039a4af14dfa Mon Sep 17 00:00:00 2001
From: Johan Commelin <johan@commelin.net>
Date: Thu, 4 Jan 2024 09:31:40 +0100
Subject: [PATCH 1/5] feat(AlgebraicTopology/SingularSet): factor topology out
 of `SimplicialSet` into new file

---
 Mathlib/AlgebraicTopology/SimplicialSet.lean | 30 +--------
 Mathlib/AlgebraicTopology/SingularSet.lean   | 71 ++++++++++++++++++++
 2 files changed, 73 insertions(+), 28 deletions(-)
 create mode 100644 Mathlib/AlgebraicTopology/SingularSet.lean

diff --git a/Mathlib/AlgebraicTopology/SimplicialSet.lean b/Mathlib/AlgebraicTopology/SimplicialSet.lean
index 97ac48140b7e6..b461fc6ea1f2e 100644
--- a/Mathlib/AlgebraicTopology/SimplicialSet.lean
+++ b/Mathlib/AlgebraicTopology/SimplicialSet.lean
@@ -4,15 +4,15 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin, Scott Morrison, Adam Topaz
 -/
 import Mathlib.AlgebraicTopology.SimplicialObject
-import Mathlib.AlgebraicTopology.TopologicalSimplex
 import Mathlib.CategoryTheory.Limits.Presheaf
 import Mathlib.CategoryTheory.Limits.Shapes.Types
 import Mathlib.CategoryTheory.Yoneda
-import Mathlib.Topology.Category.TopCat.Limits.Basic
 
 #align_import algebraic_topology.simplicial_set from "leanprover-community/mathlib"@"178a32653e369dce2da68dc6b2694e385d484ef1"
 
 /-!
+# Simplicial sets
+
 A simplicial set is just a simplicial object in `Type`,
 i.e. a `Type`-valued presheaf on the simplex category.
 
@@ -218,29 +218,3 @@ set_option linter.uppercaseLean3 false in
 end Augmented
 
 end SSet
-
-/-- The functor associating the singular simplicial set to a topological space. -/
-noncomputable def TopCat.toSSet : TopCat ⥤ SSet :=
-  ColimitAdj.restrictedYoneda SimplexCategory.toTop
-set_option linter.uppercaseLean3 false in
-#align Top.to_sSet TopCat.toSSet
-
-/-- The geometric realization functor. -/
-noncomputable def SSet.toTop : SSet ⥤ TopCat :=
-  ColimitAdj.extendAlongYoneda SimplexCategory.toTop
-set_option linter.uppercaseLean3 false in
-#align sSet.to_Top SSet.toTop
-
-/-- Geometric realization is left adjoint to the singular simplicial set construction. -/
-noncomputable def sSetTopAdj : SSet.toTop ⊣ TopCat.toSSet :=
-  ColimitAdj.yonedaAdjunction _
-set_option linter.uppercaseLean3 false in
-#align sSet_Top_adj sSetTopAdj
-
-/-- The geometric realization of the representable simplicial sets agree
-  with the usual topological simplices. -/
-noncomputable def SSet.toTopSimplex :
-    (yoneda : SimplexCategory ⥤ _) ⋙ SSet.toTop ≅ SimplexCategory.toTop :=
-  ColimitAdj.isExtensionAlongYoneda _
-set_option linter.uppercaseLean3 false in
-#align sSet.to_Top_simplex SSet.toTopSimplex
diff --git a/Mathlib/AlgebraicTopology/SingularSet.lean b/Mathlib/AlgebraicTopology/SingularSet.lean
new file mode 100644
index 0000000000000..7f28a5751c4ef
--- /dev/null
+++ b/Mathlib/AlgebraicTopology/SingularSet.lean
@@ -0,0 +1,71 @@
+/-
+Copyright (c) 2024 Johan Commelin. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johan Commelin, Scott Morrison, Adam Topaz
+-/
+import Mathlib.AlgebraicTopology.SimplicialSet
+import Mathlib.AlgebraicTopology.TopologicalSimplex
+import Mathlib.Topology.Category.TopCat.Limits.Basic
+
+/-!
+# The singular simplicial set of a topological space and geometric realization of a simplicial set
+
+The *singular simplicial set* `TopCat.to_SSet.obj X` of a topological space `X`
+has as `n`-simplices the continuous maps `[n].toTop → X`.
+Here, `[n].toTop` is the standard topological `n`-simplex,
+defined as `{ f : Fin (n+1) → ℝ≥0 // ∑ i, f i = 1 }` with its subspace topology.
+
+The *geometric realization* functor `SSet.toTop.obj` is left adjoint to `TopCat.toSSet`.
+It is the left Kan extension of `SimplexCategory.toTop` along the Yoneda embedding.
+
+# Main definitions
+
+* `TopCat.toSSet : TopCat ⥤ SSet` is the functor
+  assigning the singular simplicial set to a topological space.
+* `SSet.toTop : SSet ⥤ TopCat` is the functor
+  assigning the geometric realization to a simplicial set.
+* `sSetTopAdj : SSet.toTop ⊣ TopCat.toSSet` is the adjunction between these two functors.
+
+## TODO
+
+- Show that the singular simplicial set is a Kan complex.
+- Show the adjunction `sSetTopAdj` is a Quillen adjunction.
+
+-/
+
+open CategoryTheory
+
+/-- The functor associating the *singular simplicial set* to a topological space.
+
+Let `X` be a topological space.
+Then the singular simplicial set of `X`
+has as `n`-simplices the continuous maps `[n].toTop → X`.
+Here, `[n].toTop` is the standard topological `n`-simplex,
+defined as `{ f : Fin (n+1) → ℝ≥0 // ∑ i, f i = 1 }` with its subspace topology. -/
+noncomputable def TopCat.toSSet : TopCat ⥤ SSet :=
+  ColimitAdj.restrictedYoneda SimplexCategory.toTop
+set_option linter.uppercaseLean3 false in
+#align Top.to_sSet TopCat.toSSet
+
+/-- The *geometric realization functor* is
+the left Kan extension of `SimplexCategory.toTop` along the Yoneda embedding.
+
+It is left adjoint to `TopCat.toSSet`, as witnessed by `sSetTopAdj`. -/
+noncomputable def SSet.toTop : SSet ⥤ TopCat :=
+  ColimitAdj.extendAlongYoneda SimplexCategory.toTop
+set_option linter.uppercaseLean3 false in
+#align sSet.to_Top SSet.toTop
+
+/-- Geometric realization is left adjoint to the singular simplicial set construction. -/
+noncomputable def sSetTopAdj : SSet.toTop ⊣ TopCat.toSSet :=
+  ColimitAdj.yonedaAdjunction _
+set_option linter.uppercaseLean3 false in
+#align sSet_Top_adj sSetTopAdj
+
+/-- The geometric realization of the representable simplicial sets agree
+  with the usual topological simplices. -/
+noncomputable def SSet.toTopSimplex :
+    (yoneda : SimplexCategory ⥤ _) ⋙ SSet.toTop ≅ SimplexCategory.toTop :=
+  ColimitAdj.isExtensionAlongYoneda _
+set_option linter.uppercaseLean3 false in
+#align sSet.to_Top_simplex SSet.toTopSimplex

From aa24615bf7c6b8a757d63895b6a72d1e69a59e1a Mon Sep 17 00:00:00 2001
From: Johan Commelin <johan@commelin.net>
Date: Thu, 4 Jan 2024 09:37:46 +0100
Subject: [PATCH 2/5] fix docs in other file

---
 Mathlib/AlgebraicTopology/TopologicalSimplex.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/AlgebraicTopology/TopologicalSimplex.lean b/Mathlib/AlgebraicTopology/TopologicalSimplex.lean
index c82c145c8499c..bc7fd855f2ca4 100644
--- a/Mathlib/AlgebraicTopology/TopologicalSimplex.lean
+++ b/Mathlib/AlgebraicTopology/TopologicalSimplex.lean
@@ -14,7 +14,7 @@ import Mathlib.Topology.Instances.NNReal
 
 We define the natural functor from `SimplexCategory` to `TopCat` sending `[n]` to the
 topological `n`-simplex.
-This is used to define `TopCat.toSSet` in `AlgebraicTopology.SimplicialSet`.
+This is used to define `TopCat.toSSet` in `AlgebraicTopology.SingularSet`.
 -/
 
 

From 01ada7e6d70dab9e3aa5f5b434817d4c8ec2e539 Mon Sep 17 00:00:00 2001
From: Johan Commelin <johan@commelin.net>
Date: Thu, 4 Jan 2024 10:49:37 +0100
Subject: [PATCH 3/5] chore(AlgebraicTopology/TopologicalSimplex): clean up,
 golf

---
 .../AlgebraicTopology/TopologicalSimplex.lean | 55 +++++--------------
 Mathlib/Data/Finset/Basic.lean                |  7 +++
 2 files changed, 22 insertions(+), 40 deletions(-)

diff --git a/Mathlib/AlgebraicTopology/TopologicalSimplex.lean b/Mathlib/AlgebraicTopology/TopologicalSimplex.lean
index bc7fd855f2ca4..2e9bbacef373b 100644
--- a/Mathlib/AlgebraicTopology/TopologicalSimplex.lean
+++ b/Mathlib/AlgebraicTopology/TopologicalSimplex.lean
@@ -17,6 +17,7 @@ topological `n`-simplex.
 This is used to define `TopCat.toSSet` in `AlgebraicTopology.SingularSet`.
 -/
 
+set_option linter.uppercaseLean3 false
 
 noncomputable section
 
@@ -24,19 +25,15 @@ namespace SimplexCategory
 
 open Simplicial NNReal BigOperators Classical CategoryTheory
 
-attribute [local instance]
-  CategoryTheory.ConcreteCategory.hasCoeToSort CategoryTheory.ConcreteCategory.funLike
+attribute [local instance] ConcreteCategory.hasCoeToSort ConcreteCategory.funLike
 
 -- porting note: added, should be moved
-instance (x : SimplexCategory) : Fintype (CategoryTheory.ConcreteCategory.forget.obj x) := by
-  change (Fintype (Fin _))
-  infer_instance
+instance (x : SimplexCategory) : Fintype (ConcreteCategory.forget.obj x) :=
+  inferInstanceAs (Fintype (Fin _))
 
 /-- The topological simplex associated to `x : SimplexCategory`.
   This is the object part of the functor `SimplexCategory.toTop`. -/
-def toTopObj (x : SimplexCategory) :=
-  { f : x → ℝ≥0 | ∑ i, f i = 1 }
-set_option linter.uppercaseLean3 false in
+def toTopObj (x : SimplexCategory) := { f : x → ℝ≥0 | ∑ i, f i = 1 }
 #align simplex_category.to_Top_obj SimplexCategory.toTopObj
 
 instance (x : SimplexCategory) : CoeFun x.toTopObj fun _ => x → ℝ≥0 :=
@@ -45,35 +42,23 @@ instance (x : SimplexCategory) : CoeFun x.toTopObj fun _ => x → ℝ≥0 :=
 @[ext]
 theorem toTopObj.ext {x : SimplexCategory} (f g : x.toTopObj) : (f : x → ℝ≥0) = g → f = g :=
   Subtype.ext
-set_option linter.uppercaseLean3 false in
 #align simplex_category.to_Top_obj.ext SimplexCategory.toTopObj.ext
 
 /-- A morphism in `SimplexCategory` induces a map on the associated topological spaces. -/
-def toTopMap {x y : SimplexCategory} (f : x ⟶ y) : x.toTopObj → y.toTopObj := fun g =>
-  ⟨fun i => ∑ j in Finset.univ.filter fun k => f k = i, g j, by
-    simp only [Finset.sum_congr, toTopObj, Set.mem_setOf]
+def toTopMap {x y : SimplexCategory} (f : x ⟶ y) (g : x.toTopObj) : y.toTopObj :=
+  ⟨fun i => ∑ j in Finset.univ.filter (f · = i), g j, by
+    simp only [toTopObj, Set.mem_setOf]
     rw [← Finset.sum_biUnion]
-    have hg := g.2
-    dsimp [toTopObj] at hg
-    convert hg
-    · simp [Finset.eq_univ_iff_forall]
-    · intro i _ j _ h
-      rw [Function.onFun, disjoint_iff_inf_le]
-      intro e he
-      simp only [Finset.bot_eq_empty, Finset.not_mem_empty]
-      apply h
-      simp only [Finset.mem_univ, forall_true_left,
-        ge_iff_le, Finset.le_eq_subset, Finset.inf_eq_inter, Finset.mem_inter,
-        Finset.mem_filter, true_and] at he
-      rw [← he.1, he.2]⟩
-set_option linter.uppercaseLean3 false in
+    · have hg : ∑ i : (forget SimplexCategory).obj x, g i = 1 := g.2
+      convert hg
+      simp [Finset.eq_univ_iff_forall]
+    · apply Set.pairwiseDisjoint_filter⟩
 #align simplex_category.to_Top_map SimplexCategory.toTopMap
 
 @[simp]
 theorem coe_toTopMap {x y : SimplexCategory} (f : x ⟶ y) (g : x.toTopObj) (i : y) :
-    toTopMap f g i = ∑ j in Finset.univ.filter fun k => f k = i, g j :=
+    toTopMap f g i = ∑ j in Finset.univ.filter (f · = i), g j :=
   rfl
-set_option linter.uppercaseLean3 false in
 #align simplex_category.coe_to_Top_map SimplexCategory.coe_toTopMap
 
 @[continuity]
@@ -81,7 +66,6 @@ theorem continuous_toTopMap {x y : SimplexCategory} (f : x ⟶ y) : Continuous (
   refine' Continuous.subtype_mk (continuous_pi fun i => _) _
   dsimp only [coe_toTopMap]
   exact continuous_finset_sum _ (fun j _ => (continuous_apply _).comp continuous_subtype_val)
-set_option linter.uppercaseLean3 false in
 #align simplex_category.continuous_to_Top_map SimplexCategory.continuous_toTopMap
 
 /-- The functor associating the topological `n`-simplex to `[n] : SimplexCategory`. -/
@@ -94,7 +78,7 @@ def toTop : SimplexCategory ⥤ TopCat where
     ext f
     apply toTopObj.ext
     funext i
-    change (Finset.univ.filter fun k => k = i).sum _ = _
+    change (Finset.univ.filter (· = i)).sum _ = _
     simp [Finset.sum_filter, CategoryTheory.id_apply]
   map_comp := fun f g => by
     ext h
@@ -109,16 +93,7 @@ def toTop : SimplexCategory ⥤ TopCat where
     · apply Finset.sum_congr
       · exact Finset.ext (fun j => ⟨fun hj => by simpa using hj, fun hj => by simpa using hj⟩)
       · tauto
-    · intro j _ k _ h
-      rw [Function.onFun, disjoint_iff_inf_le]
-      intro e he
-      simp only [Finset.bot_eq_empty, Finset.not_mem_empty]
-      apply h
-      simp only [Finset.mem_univ, forall_true_left,
-        ge_iff_le, Finset.le_eq_subset, Finset.inf_eq_inter, Finset.mem_inter,
-        Finset.mem_filter, true_and] at he
-      rw [← he.1, he.2]
-set_option linter.uppercaseLean3 false in
+    · apply Set.pairwiseDisjoint_filter
 #align simplex_category.to_Top SimplexCategory.toTop
 
 -- These lemmas have always been bad (#7657), but leanprover/lean4#2644 made `simp` start noticing
diff --git a/Mathlib/Data/Finset/Basic.lean b/Mathlib/Data/Finset/Basic.lean
index f1de472f9c74d..88d67dbe2fa6e 100644
--- a/Mathlib/Data/Finset/Basic.lean
+++ b/Mathlib/Data/Finset/Basic.lean
@@ -2917,6 +2917,13 @@ theorem filter_disj_union (s : Finset α) (t : Finset α) (h : Disjoint s t) :
   eq_of_veq <| Multiset.filter_add _ _ _
 #align finset.filter_disj_union Finset.filter_disj_union
 
+lemma _root_.Set.pairwiseDisjoint_filter [DecidableEq β] (f : α → β) (s : Set β) (t : Finset α) :
+    s.PairwiseDisjoint fun x ↦ t.filter (f · = x) := by
+  rintro i - j - h u hi hj x hx
+  obtain ⟨-, rfl⟩ : x ∈ t ∧ f x = i := by simpa using hi hx
+  obtain ⟨-, rfl⟩ : x ∈ t ∧ f x = j := by simpa using hj hx
+  contradiction
+
 theorem filter_cons {a : α} (s : Finset α) (ha : a ∉ s) :
     filter p (cons a s ha) =
       (if p a then {a} else ∅ : Finset α).disjUnion (filter p s)

From 91fe3dfa1e92ca3d5911086501d6ceb8c3e11eee Mon Sep 17 00:00:00 2001
From: Johan Commelin <johan@commelin.net>
Date: Thu, 4 Jan 2024 10:52:18 +0100
Subject: [PATCH 4/5] add new file to Mathlib.lean

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

diff --git a/Mathlib.lean b/Mathlib.lean
index 0febcb1a2dc25..df08301f68c70 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -556,6 +556,7 @@ import Mathlib.AlgebraicTopology.Quasicategory
 import Mathlib.AlgebraicTopology.SimplexCategory
 import Mathlib.AlgebraicTopology.SimplicialObject
 import Mathlib.AlgebraicTopology.SimplicialSet
+import Mathlib.AlgebraicTopology.SingularSet
 import Mathlib.AlgebraicTopology.SplitSimplicialObject
 import Mathlib.AlgebraicTopology.TopologicalSimplex
 import Mathlib.Analysis.Analytic.Basic

From f3537ac983463842257ff888339a6feb6796f3c6 Mon Sep 17 00:00:00 2001
From: Johan Commelin <johan@commelin.net>
Date: Fri, 5 Jan 2024 07:21:32 +0100
Subject: [PATCH 5/5] no need to depend on other PR

---
 Mathlib.lean                                  |  1 -
 Mathlib/AlgebraicTopology/SimplicialSet.lean  | 30 +++++++-
 Mathlib/AlgebraicTopology/SingularSet.lean    | 71 -------------------
 .../AlgebraicTopology/TopologicalSimplex.lean |  2 +-
 4 files changed, 29 insertions(+), 75 deletions(-)
 delete mode 100644 Mathlib/AlgebraicTopology/SingularSet.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index df08301f68c70..0febcb1a2dc25 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -556,7 +556,6 @@ import Mathlib.AlgebraicTopology.Quasicategory
 import Mathlib.AlgebraicTopology.SimplexCategory
 import Mathlib.AlgebraicTopology.SimplicialObject
 import Mathlib.AlgebraicTopology.SimplicialSet
-import Mathlib.AlgebraicTopology.SingularSet
 import Mathlib.AlgebraicTopology.SplitSimplicialObject
 import Mathlib.AlgebraicTopology.TopologicalSimplex
 import Mathlib.Analysis.Analytic.Basic
diff --git a/Mathlib/AlgebraicTopology/SimplicialSet.lean b/Mathlib/AlgebraicTopology/SimplicialSet.lean
index b461fc6ea1f2e..97ac48140b7e6 100644
--- a/Mathlib/AlgebraicTopology/SimplicialSet.lean
+++ b/Mathlib/AlgebraicTopology/SimplicialSet.lean
@@ -4,15 +4,15 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin, Scott Morrison, Adam Topaz
 -/
 import Mathlib.AlgebraicTopology.SimplicialObject
+import Mathlib.AlgebraicTopology.TopologicalSimplex
 import Mathlib.CategoryTheory.Limits.Presheaf
 import Mathlib.CategoryTheory.Limits.Shapes.Types
 import Mathlib.CategoryTheory.Yoneda
+import Mathlib.Topology.Category.TopCat.Limits.Basic
 
 #align_import algebraic_topology.simplicial_set from "leanprover-community/mathlib"@"178a32653e369dce2da68dc6b2694e385d484ef1"
 
 /-!
-# Simplicial sets
-
 A simplicial set is just a simplicial object in `Type`,
 i.e. a `Type`-valued presheaf on the simplex category.
 
@@ -218,3 +218,29 @@ set_option linter.uppercaseLean3 false in
 end Augmented
 
 end SSet
+
+/-- The functor associating the singular simplicial set to a topological space. -/
+noncomputable def TopCat.toSSet : TopCat ⥤ SSet :=
+  ColimitAdj.restrictedYoneda SimplexCategory.toTop
+set_option linter.uppercaseLean3 false in
+#align Top.to_sSet TopCat.toSSet
+
+/-- The geometric realization functor. -/
+noncomputable def SSet.toTop : SSet ⥤ TopCat :=
+  ColimitAdj.extendAlongYoneda SimplexCategory.toTop
+set_option linter.uppercaseLean3 false in
+#align sSet.to_Top SSet.toTop
+
+/-- Geometric realization is left adjoint to the singular simplicial set construction. -/
+noncomputable def sSetTopAdj : SSet.toTop ⊣ TopCat.toSSet :=
+  ColimitAdj.yonedaAdjunction _
+set_option linter.uppercaseLean3 false in
+#align sSet_Top_adj sSetTopAdj
+
+/-- The geometric realization of the representable simplicial sets agree
+  with the usual topological simplices. -/
+noncomputable def SSet.toTopSimplex :
+    (yoneda : SimplexCategory ⥤ _) ⋙ SSet.toTop ≅ SimplexCategory.toTop :=
+  ColimitAdj.isExtensionAlongYoneda _
+set_option linter.uppercaseLean3 false in
+#align sSet.to_Top_simplex SSet.toTopSimplex
diff --git a/Mathlib/AlgebraicTopology/SingularSet.lean b/Mathlib/AlgebraicTopology/SingularSet.lean
deleted file mode 100644
index 7f28a5751c4ef..0000000000000
--- a/Mathlib/AlgebraicTopology/SingularSet.lean
+++ /dev/null
@@ -1,71 +0,0 @@
-/-
-Copyright (c) 2024 Johan Commelin. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Johan Commelin, Scott Morrison, Adam Topaz
--/
-import Mathlib.AlgebraicTopology.SimplicialSet
-import Mathlib.AlgebraicTopology.TopologicalSimplex
-import Mathlib.Topology.Category.TopCat.Limits.Basic
-
-/-!
-# The singular simplicial set of a topological space and geometric realization of a simplicial set
-
-The *singular simplicial set* `TopCat.to_SSet.obj X` of a topological space `X`
-has as `n`-simplices the continuous maps `[n].toTop → X`.
-Here, `[n].toTop` is the standard topological `n`-simplex,
-defined as `{ f : Fin (n+1) → ℝ≥0 // ∑ i, f i = 1 }` with its subspace topology.
-
-The *geometric realization* functor `SSet.toTop.obj` is left adjoint to `TopCat.toSSet`.
-It is the left Kan extension of `SimplexCategory.toTop` along the Yoneda embedding.
-
-# Main definitions
-
-* `TopCat.toSSet : TopCat ⥤ SSet` is the functor
-  assigning the singular simplicial set to a topological space.
-* `SSet.toTop : SSet ⥤ TopCat` is the functor
-  assigning the geometric realization to a simplicial set.
-* `sSetTopAdj : SSet.toTop ⊣ TopCat.toSSet` is the adjunction between these two functors.
-
-## TODO
-
-- Show that the singular simplicial set is a Kan complex.
-- Show the adjunction `sSetTopAdj` is a Quillen adjunction.
-
--/
-
-open CategoryTheory
-
-/-- The functor associating the *singular simplicial set* to a topological space.
-
-Let `X` be a topological space.
-Then the singular simplicial set of `X`
-has as `n`-simplices the continuous maps `[n].toTop → X`.
-Here, `[n].toTop` is the standard topological `n`-simplex,
-defined as `{ f : Fin (n+1) → ℝ≥0 // ∑ i, f i = 1 }` with its subspace topology. -/
-noncomputable def TopCat.toSSet : TopCat ⥤ SSet :=
-  ColimitAdj.restrictedYoneda SimplexCategory.toTop
-set_option linter.uppercaseLean3 false in
-#align Top.to_sSet TopCat.toSSet
-
-/-- The *geometric realization functor* is
-the left Kan extension of `SimplexCategory.toTop` along the Yoneda embedding.
-
-It is left adjoint to `TopCat.toSSet`, as witnessed by `sSetTopAdj`. -/
-noncomputable def SSet.toTop : SSet ⥤ TopCat :=
-  ColimitAdj.extendAlongYoneda SimplexCategory.toTop
-set_option linter.uppercaseLean3 false in
-#align sSet.to_Top SSet.toTop
-
-/-- Geometric realization is left adjoint to the singular simplicial set construction. -/
-noncomputable def sSetTopAdj : SSet.toTop ⊣ TopCat.toSSet :=
-  ColimitAdj.yonedaAdjunction _
-set_option linter.uppercaseLean3 false in
-#align sSet_Top_adj sSetTopAdj
-
-/-- The geometric realization of the representable simplicial sets agree
-  with the usual topological simplices. -/
-noncomputable def SSet.toTopSimplex :
-    (yoneda : SimplexCategory ⥤ _) ⋙ SSet.toTop ≅ SimplexCategory.toTop :=
-  ColimitAdj.isExtensionAlongYoneda _
-set_option linter.uppercaseLean3 false in
-#align sSet.to_Top_simplex SSet.toTopSimplex
diff --git a/Mathlib/AlgebraicTopology/TopologicalSimplex.lean b/Mathlib/AlgebraicTopology/TopologicalSimplex.lean
index 2e9bbacef373b..61119b4e97e59 100644
--- a/Mathlib/AlgebraicTopology/TopologicalSimplex.lean
+++ b/Mathlib/AlgebraicTopology/TopologicalSimplex.lean
@@ -14,7 +14,7 @@ import Mathlib.Topology.Instances.NNReal
 
 We define the natural functor from `SimplexCategory` to `TopCat` sending `[n]` to the
 topological `n`-simplex.
-This is used to define `TopCat.toSSet` in `AlgebraicTopology.SingularSet`.
+This is used to define `TopCat.toSSet` in `AlgebraicTopology.SimplicialSet`.
 -/
 
 set_option linter.uppercaseLean3 false