diff --git a/data/menus.yaml b/data/menus.yaml
index 08980edafc..08a57ff2b8 100644
--- a/data/menus.yaml
+++ b/data/menus.yaml
@@ -35,6 +35,14 @@
     - Undergraduate maths: undergrad.html
     - Wiedijk's 100 theorems: 100.html
 
+- title: Theories
+  items:
+    - Natural Numbers: theories/naturals.html
+    - Linear Algebra: theories/linear_algebra.html
+    - Sets and finite sets: theories/sets.html
+    - Topology: theories/topology.html
+    - Category Theory: theories/category_theory.html
+
 - title: Contributing
   items:
     - Pull request lifecycle: contribute/index.html
diff --git a/templates/theories/category_theory.md b/templates/theories/category_theory.md
index 5eb232d4a1..3cc30b22c0 100644
--- a/templates/theories/category_theory.md
+++ b/templates/theories/category_theory.md
@@ -1,39 +1,20 @@
-<div class="alert alert-info">
-<p>
-We are currently updating the Lean community website to describe working with Lean 4,
-but most of the information you will find here today still describes Lean 3.
-</p>
-<p>
-Pull requests updating this page for Lean 4 are very welcome.
-There is a link at the bottom of this page.
-</p>
-<p>
-Please visit <a href="https://leanprover.zulipchat.com">the leanprover zulip</a>
-and ask for whatever help you need during this transitional period!
-</p>
-<p>
-The website for Lean 3 has been <a href="https://leanprover-community.github.io/lean3/">archived</a>.
-If you need to link to Lean 3 specific resources please link there.
-</p>
-</div>
-
 # Maths in Lean: category theory
 
-The `category` typeclass is defined in [category_theory/category/basic.lean](https://leanprover-community.github.io/mathlib_docs/category_theory/category/basic.html).
-It depends on the type of the objects, so for example we might write `category (Type u)` if we're talking about a category whose objects are types (in universe `u`).
+The `Category` typeclass is defined in [`Mathlib.CategoryTheory.Category.Basic`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/Category/Basic.html).
+It depends on the type of the objects, so for example we might write `Category (Type u)` if we're talking about a category whose objects are types (in universe `u`).
 
-Functors (which are a structure, not a typeclass) are defined in [category_theory/functor/basic.lean](https://leanprover-community.github.io/mathlib_docs/category_theory/functor/basic.html),
+Functors (which are a structure, not a typeclass) are defined in [`Mathlib.CategoryTheory.Functor.Basic`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/Functor/Basic.html),
 along with identity functors and functor composition.
 
-Natural transformations, and their compositions, are defined in [category_theory/natural_transformation.lean](https://leanprover-community.github.io/mathlib_docs/category_theory/natural_transformation.html).
+Natural transformations, and their compositions, are defined in [`Mathlib.CategoryTheory.NatTrans`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/NatTrans.html).
 
 The category of functors and natural transformations between fixed categories `C` and `D`
-is defined in [category_theory/functor/category.lean](https://leanprover-community.github.io/mathlib_docs/category_theory/functor/category.html).
+is defined in [`Mathlib.CategoryTheory.Functor.Category`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/Functor/Category.html).
 
 Cartesian products of categories, functors, and natural transformations appear in
-[category_theory/products/basic.lean](https://leanprover-community.github.io/mathlib_docs/category_theory/products/basic.html). (Product in the sense of limits will appear elsewhere soon!)
+[`Mathlib.CategoryTheory.Products.Basic`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/Products/Basic.html).
 
-The category of types, and the hom pairing functor, are defined in [category_theory/types.lean](https://leanprover-community.github.io/mathlib_docs/category_theory/types.html).
+The category of types, and the hom pairing functor, are defined in [`Mathlib.CategoryTheory.Types`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/Types.html).
 
 ## Notation
 
@@ -58,7 +39,6 @@ We use `≅` for isomorphisms.
 ### Functors
 
 We use `⥤` (`\func`) to denote functors, as in `C ⥤ D` for the type of functors from `C` to `D`.
-(Unfortunately `⇒` is reserved in [`logic.relator`](https://github.com/leanprover-community/mathlib/blob/master/src/logic/relator.lean), so we can't use that here.)
 
 We use `F.obj X` to denote the action of a functor on an object.
 We use `F.map f` to denote the action of a functor on a morphism`.
diff --git a/templates/theories/linear_algebra.md b/templates/theories/linear_algebra.md
index 9feae66efa..7178fbc8fe 100644
--- a/templates/theories/linear_algebra.md
+++ b/templates/theories/linear_algebra.md
@@ -1,140 +1,122 @@
-<div class="alert alert-info">
-<p>
-We are currently updating the Lean community website to describe working with Lean 4,
-but most of the information you will find here today still describes Lean 3.
-</p>
-<p>
-Pull requests updating this page for Lean 4 are very welcome.
-There is a link at the bottom of this page.
-</p>
-<p>
-Please visit <a href="https://leanprover.zulipchat.com">the leanprover zulip</a>
-and ask for whatever help you need during this transitional period!
-</p>
-<p>
-The website for Lean 3 has been <a href="https://leanprover-community.github.io/lean3/">archived</a>.
-If you need to link to Lean 3 specific resources please link there.
-</p>
-</div>
-
 # Maths in Lean: linear algebra
 
 ### Semimodules, Modules and Vector Spaces
 
-#### [`algebra.module`](https://leanprover-community.github.io/mathlib_docs/algebra/module/basic.html)
+#### [`Mathlib.Algebra.Module.Defs`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Module/Defs.html)
 
-This file defines the typeclass `module R M`, which gives an `R`-module structure on the type `M`.
-An additive commutative monoid `M` is a module over the (semi)ring `R` if there is a scalar multiplication `•` (`has_scalar.smul`) that satisfies the expected distributivity axioms for `+` (in `M` and `R`) and `*` (in `R`).
-To define a `module R M` instance, you first need instances for `semiring R` and `add_comm_monoid M`.
+This file defines the typeclass `Module R M`, which gives an `R`-module structure on the type `M`.
+An additive commutative monoid `M` is a module over the (semi)ring `R` if there is a scalar multiplication `•` (`SMul`) that satisfies the expected distributivity axioms for `+` (in `M` and `R`) and `*` (in `R`).
+To define a `Module R M` instance, you first need instances for `Semiring R` and `AddCommMonoid M`.
 By splitting out these dependencies, we avoid instance loops and diamonds.
 
 In general mathematical usage, a module over a semiring is also called a semimodule, and a module over a field is also called a vector space.
-We do not have separate `semimodule` or `vector_space` typeclasses because those requirements are more easily expressed by changing the typeclass instances on `R` (and `M`).
+We do not have separate `Semimodule` or `VectorSpace` typeclasses because those requirements are more easily expressed by changing the typeclass instances on `R` (and `M`).
 In this document, we'll use "module" as the general term for "semimodule, module or vector space" and "ring" as the general term for "(commutative) semiring, ring or field".
 
-Let `m` be an arbitrary type, e.g. `fin n`, then the typical examples are:
+Let `m` be an arbitrary type, e.g. `Fin n`, then the typical examples are:
 `m → ℕ` is an `ℕ`-semimodule, `m → ℤ` is a `ℤ`-module and `m → ℚ` is a `ℚ`-vector space
 (outside of type theory, these are known as `ℕ^m`, `ℤ^m` and `ℚ^m` respectively).
-A ring is a module over itself, with `•` defined as `*` (this equality is stated by the `simp` lemma [`smul_eq_mul`](https://leanprover-community.github.io/mathlib_docs/group_theory/group_action/defs.html#smul_eq_mul)).
+A ring is a module over itself, with `•` defined as `*` (this equality is stated by the `simp` lemma [`smul_eq_mul`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Group/Action/Defs.html#smul_eq_mul)).
 Each additive monoid has a canonical `ℕ`-module structure given by `n • x = x + x + ... + x` (`n` times), and each additive group has a canonical `ℤ`-module structure defined similarly; these also apply for (semi)rings.
 
-The file [`linear_algebra.linear_independent`](https://leanprover-community.github.io/mathlib_docs/linear_algebra/linear_independent.html) defines linear independence for an indexed family in a module.
-To express that a set `s : set M` is linear independent, we view it as a family indexed by itself, written as `linear_independent R (coe : s → M)`.
+The file [`Mathlib.LinearAlgebra.LinearIndependent`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/LinearIndependent.html) defines linear independence for an indexed family in a module.
+To express that a set `s : Set M` is linear independent, we view it as a family indexed by itself, written as `LinearIndependent R ((↑)  : s → M)`.
 
-The file [`linear_algebra.basis`](https://leanprover-community.github.io/mathlib_docs/linear_algebra/basis.html) defines bases for modules.
+The file [`Mathlib.LinearAlgebra.Basis`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/Basis.html) defines bases for modules.
 
-The file [`linear_algebra.dimension`](https://leanprover-community.github.io/mathlib_docs/linear_algebra/dimension.html) defines the `rank` of a module as a cardinal.
+The file [`Mathlib.LinearAlgebra.Dimension.Basic`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/Dimension/Basic.html) defines the `rank` of a module as a cardinal.
 We also use `rank` for the dimension of a vector space, since the dimension is always equal to the rank.
-(In fact, `rank` is currently only defined for vector spaces, as the cardinality of a basis. A definition of rank for all modules still needs to be done.)
 The `rank` of a linear map is defined as the dimension of its image.
 Most definitions in this file are non-computable.
 
-The file [`linear_algebra.finite_dimensional`](https://leanprover-community.github.io/mathlib_docs/linear_algebra/finite_dimensional.html) defines the `finrank` of a module as a natural number.
+The file [`Mathlib.LinearAlgebra.Dimension.Finrank`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/Dimension/Finrank.html) defines the `finrank` of a module as a natural number.
 By convention, the `finrank` is equal to 0 if the rank is infinite.
 
 ### Matrices
 
-#### [`data.matrix.basic`](https://leanprover-community.github.io/mathlib_docs/data/matrix/basic.html)
+#### [`Mathlib.Data.Matrix.Basic`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Matrix/Basic.html)
 
-The type `matrix m n α` contains rectangular, `m` by `n` arrays of elements of the type `α`.
-It is an alias for the type `m → n → α`, under the assumptions `[fintype m] [fintype n]` stating that `m` and `n` have finitely many elements.
-A matrix type can be indexed over arbitrary `fintype`s.
+The type `Matrix m n α` contains rectangular, `m` by `n` arrays of elements of the type `α`.
+It is an alias for the type `m → n → α`. A matrix type can be indexed over arbitrary types.
 For example, the adjacency matrix of a graph could be indexed over the nodes in that graph.
-If you want to specify the dimensions of a matrix as natural numbers `m n : ℕ`, you can use `fin m` and `fin n` as index types.
+If you want to specify the dimensions of a matrix as natural numbers `m n : ℕ`, you can use `Fin m` and `Fin n` as index types.
 
-A matrix is constructed by giving the map from indices to entries: `(λ (i : m) (j : n), (_ : α)) : matrix m n α`.
-For matrices indexed by natural numbers, you can also use the notation defined in [`data.matrix.notation`](https://leanprover-community.github.io/mathlib_docs/data/matrix/notation.html): `![![a, b, c], ![b, c, d]] : matrix (fin 2) (fin 3) α`.
-To get an entry of the matrix `M : matrix m n α` at row `i : m` and column `j : n`,
+A matrix is constructed by giving the map from indices to entries: `(fun (i : m) (j : n) ↦ (_ : α)) : Matrix m n α`.
+However, it is not advisable to construct matrices using terms of the form `fun i j ↦ _` or even `(fun i j ↦ _ : Matrix m n α)`,
+as these are not recognized by Lean as having the right type. Instead, `Matrix.of` should be used.
+For matrices indexed by natural numbers, you can also use the notation defined in [`Mathlib.Data.Matrix.Notation`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Matrix/Notation.html): `![![a, b, c], ![b, c, d]] : Matrix (Fin 2) (Fin 3) α`.
+To get an entry of the matrix `M : Matrix m n α` at row `i : m` and column `j : n`,
 you can apply `M` to the indices: `M i j : α`.
-Lemmas about the entries of a matrix typically end in `_val`: `add_val M N i j : (M + N) i j = M i j + N i j`.
+Lemmas about the entries of a matrix typically end in `_apply`: `Matrix.add_apply M N i j : (M + N) i j = M i j + N i j`.
 
-Matrix multiplication and transpose have notation that is made available by the command `open_locale matrix`.
-The infix operator `⬝` stands for `matrix.mul`,
-and a postfix operator `ᵀ` stands for `matrix.transpose`.
+Matrix multiplication and transpose have notation that is made available by the command `open scoped Matrix`.
+Multiplication of matrices is denoted using `*` as usual. The infix operator `⬝ᵥ` stands for `Matrix.dotProduct`,
+and a postfix operator `ᵀ` stands for `Matrix.transpose`.
 
-When working with matrices, a *vector* means a function `m → α` for an arbitrary `fintype` `m`.
+When working with matrices, a *vector* means a function `m → α` for an arbitrary `Fintype` `m`.
 These have a module (or vector space) structure defined in [`algebra.module.pi`](https://leanprover-community.github.io/mathlib_docs/algebra/module/pi.html)
 consisting of pointwise addition and multiplication.
 The distinction between row and column vectors is only made by the choice of function.
-For example, `mul_vec M v` multiplies a matrix with a column vector `v : m → α` and `vec_mul v M` multiplies a row vector `v : m → α` with a matrix.
-If you use `mul_vec` and `vec_mul` a lot, you might want to consider using a linear map instead (see below).
+For example, `Matrix.mulVec M v` (denoted `M *ᵥ v`) multiplies a matrix with a column vector `v : m → α` and `Matrix.Vecmul v M`
+(denoted `v ᵥ* M`) multiplies a row vector `v : m → α` with a matrix.
+If you use `mulVec` and `Vecmul` a lot, you might want to consider using a linear map instead (see below).
 
-Permutation matrices are defined in [`data.matrix.pequiv`](https://leanprover-community.github.io/mathlib_docs/data/matrix/pequiv.html).
+Permutation matrices are defined in [`Mathlib.LinearAlgebra.Matrix.Permutation`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/Matrix/Permutation.html).
 
-The determinant of a matrix is defined in [`linear_algebra.determinant`](https://leanprover-community.github.io/mathlib_docs/linear_algebra/determinant.html).
+The determinant of a matrix is defined in [`Mathlib.LinearAlgebra.Matrix.Determinant.Basic`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/Matrix/Determinant/Basic.html).
 
-The adjugate and for nonsingular matrices, the inverse is defined in [`linear_algebra.matrix.nonsingular_inverse`](https://leanprover-community.github.io/mathlib_docs/linear_algebra/matrix/nonsingular_inverse.html).
+The adjugate and for nonsingular matrices, the inverse are defined in [`Mathlib.LinearAlgebra.Matrix.Adjugate`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/Matrix/Adjugate.html) and [`Mathlib.LinearAlgebra.Matrix.NonsingularInverse`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.html).
 
-The type `special_linear_group m R` is the group of `m` by `m` matrices with determinant `1`,
-and is defined in [`linear_algebra.special_linear_group`](https://leanprover-community.github.io/mathlib_docs/linear_algebra/special_linear_group.html).
+The type `Matrix.SpecialLinearGroup m R` is the group of `m` by `m` matrices with determinant `1`,
+and is defined in [`Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.html).
 
 ### Linear Maps and Equivalences
 
-#### [`algebra.module.linear_map`](https://leanprover-community.github.io/mathlib_docs/algebra/module/linear_map.html)
+#### [`Mathlib.Algebra.Module.LinearMap.Defs`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Module/LinearMap/Defs.html)
 
-The type `M →[R]ₗ M₂`, or `linear_map R M M₂`, represents `R`-linear maps from the `R`-module `M` to the `R`-module `M₂`.
+The type `M →[R]ₗ M₂`, or `LinearMap R M M₂`, represents `R`-linear maps from the `R`-module `M` to the `R`-module `M₂`.
 These are defined by their action on elements of `M`.
-The type `M ≃[R]ₗ M₂`, or `linear_equiv R M M₂`, is the type of invertible `R`-linear maps from `M` to `M₂`.
+The type `M ≃[R]ₗ M₂`, or `LinearEquiv R M M₂`, is the type of invertible `R`-linear maps from `M` to `M₂`.
 
-The equivalence between matrices and linear maps is formalised in [`linear_algebra.matrix.to_lin`](https://leanprover-community.github.io/mathlib_docs/linear_algebra/matrix/to_lin.html).
-[`to_lin`](https://leanprover-community.github.io/mathlib_docs/linear_algebra/matrix/to_lin.html#matrix.to_lin) shows that `matrix.mul_vec` is a linear equivalence between `matrix m n R` and `(n → R) →[R]ₗ (m → R)`.
-In addition, `linear_map.to_matrix` takes a basis `ι` for `M₁` and `κ` for `M₂`
-and gives the equivalence between `R`-linear maps between `M₁` and `M₂` and `matrix ι κ R`.
+The equivalence between matrices and linear maps is formalized in [`Matrix.toLin`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/Matrix/ToLin.html#Matrix.toLin).
+[`Matrix.toLin'`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/Matrix/ToLin.html#Matrix.toLin') shows that `Matrix.mulVec` is a linear equivalence between `Matrix m n R` and `(n → R) →[R]ₗ (m → R)`.
+In addition, [`LinearMap.toMatrix`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/Matrix/ToLin.html#LinearMap.toMatrix) takes a basis `ι` for `M₁` and `κ` for `M₂`
+and gives the equivalence between `R`-linear maps between `M₁` and `M₂` and `Matrix ι κ R`.
 If you have an explicit basis for your maps, this equivalence allows you to do calculations such as getting the determinant.
 
 The difference between matrices and linear maps is that matrices are in their essence an array of entries
-(which incidentally allows actions such as `matrix.mul_vec`),
+(which incidentally allows actions such as `Matrix.mulVec`),
 while linear maps are in their essence an action on vectors
 (which incidentally can be represented by a matrix if we have a finite basis).
 If you want to do computations, a matrix is a better choice.
 If you want to do proofs without computations, a linear map is a better choice.
 
-The type [`general_linear_group R M`](https://leanprover-community.github.io/mathlib_docs/linear_algebra/basic.html#linear_map.general_linear_group) is the group of invertible `R`-linear maps from `M` to itself.
-`general_linear_equiv R M` is the equivalence between `general_linear_group` and `M ≃[R]ₗ M`.
-`special_linear_group.to_GL` is the embedding from the special linear group (of matrices) to the general linear group (of linear maps).
+The type [`Matrix.GeneralLinearGroup R M`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Defs.html#Matrix.GeneralLinearGroup) is the group of invertible `R`-linear maps from `M` to itself.
+`LinearMap.GeneralLinearGroup.generalLinearEquiv R M` is the equivalence between `GeneralLinearGroup ` and `M ≃[R]ₗ M`.
+`Matrix.SpecialLinearGroup.toGL` is the embedding from the special linear group (of matrices) to the general linear group (of linear maps).
 
-The dual space, consisting of linear maps `M →[R]ₗ R`, is defined in [`linear_algebra.dual`](https://leanprover-community.github.io/mathlib_docs/linear_algebra/dual.html).
+The dual space, consisting of linear maps `M →[R]ₗ R`, is defined in [`Mathlib.LinearAlgebra.Dual`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/Dual.html).
 
 ### Bilinear, Sesquilinear and Quadratic Forms
 
-#### [`linear_algebra.bilinear_form`](https://leanprover-community.github.io/mathlib_docs/linear_algebra/bilinear_form.html)
+#### [`Mathlib.LinearAlgebra.BilinearMap`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/BilinearMap.html)
 
-For an `R`-module `M`, the type `bilin_form R M` is the type of maps `M → M → R` that are linear in both arguments.
-The equivalence between `bilin_form R M` and maps `M →ₗ[R] M →ₗ[R] R` that are linear in both arguments is called `bilin_linear_map_equiv`.
+For an `R`-module `M`, the type `LinearMap.BilinForm R M` is the type of maps `M → M → R` that are linear in both arguments.
+The equivalence between `LinearMap.BilinForm R M` and maps `M →ₗ[R] M →ₗ[R] R` that are linear in both arguments is called `bilin_linear_map_equiv`.
 A matrix `M` corresponds to a bilinear form that maps vectors `v` and `w` to `row v ⬝ M ⬝ col w`.
-The equivalence between `bilin_form R (n → R)` and `matrix n n R` is called [`bilin_form_equiv_matrix`](https://leanprover-community.github.io/mathlib_docs/linear_algebra/bilinear_form.html#bilin_form_equiv_matrix).
+The equivalence between `BilinForm R (n → R)` and `Matrix n n R` is called [`BilinForm.toMatrix`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/Matrix/BilinearForm.html#BilinForm.toMatrix).
 
-#### [`linear_algebra.sesquilinear_form`](https://leanprover-community.github.io/mathlib_docs/linear_algebra/sesquilinear_form.html)
+#### [`Mathlib.LinearAlgebra.SesquilinearForm`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/SesquilinearForm.html)
 
 For an `R`-module `M` and `I : R →+* R`, the type `M →ₗ M →ₛₗ[I] R` is the type of maps `M → M → R` that are linear in the first argument
-and that in the second argument are `I`-[semilinear](https://leanprover-community.github.io/mathlib_docs/algebra/module/linear_map.html#linear_map).
+and that in the second argument are `I`-[semilinear](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Module/LinearMap/Defs.html#LinearMap).
 Semilinearity of `f` with respect to a ring homomorphism `I` means the following equation hold: `f x (a • y) = I a * f x y`.
 
-#### [`linear_algebra.quadratic_form`](https://leanprover-community.github.io/mathlib_docs/linear_algebra/quadratic_form/basic.html)
+#### [`Mathlib.LinearAlgebra.QuadraticForm.Basic`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/QuadraticForm/Basic.html)
 
-For an `R`-module `M`, the type `quadratic_form R M` is the type of maps `f : M → R` such that `f (a • x) = a * a * f x` and `λ x y, f (x + y) - f x - f y` is a bilinear map.
+For an `R`-module `M`, the type `QuadraticForm R M` is the type of maps `f : M → R` such that `f (a • x) = a * a * f x` and `fun x y ↦ f (x + y) - f x - f y` is a bilinear map.
 
 Up to a factor `2`, the theory of quadratic and bilinear forms is equivalent.
-[`bilin_form.to_quadratic_form f`](https://leanprover-community.github.io/mathlib_docs/linear_algebra/quadratic_form/basic.html#bilin_form.to_quadratic_form) is the quadratic form given by `λ x, f x x`.
-[`quadratic_form.associated f`](https://leanprover-community.github.io/mathlib_docs/linear_algebra/quadratic_form.html#quadratic_form.associated) is the bilinear form given by `λ x y, ⅟2 * (f (x + y) - f x - f y)` (if there is a multiplicative inverse of `2`).
-[`quadratic_form.to_matrix`](https://leanprover-community.github.io/mathlib_docs/linear_algebra/quadratic_form.html#quadratic_form.to_matrix) and [`matrix.to_quadratic_form`](https://leanprover-community.github.io/mathlib_docs/linear_algebra/quadratic_form.html#matrix.to_quadratic_form) are the maps between quadratic forms and matrices.
+[`LinearMap.BilinMap.toQuadraticMap f`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/QuadraticForm/Basic.html#LinearMap.BilinMap.toQuadraticMap) is the quadratic form given by `fun x ↦ f x x`.
+[`QuadraticMap.associatedHom f`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/QuadraticForm/Basic.html#QuadraticMap.associatedHom) is the bilinear form given by `fun x y ↦ ⅟2 * (f (x + y) - f x - f y)` (if there is a multiplicative inverse of `2`).
+[`QuadraticMap.toMatrix'`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/QuadraticForm/Basic.html#QuadraticMap.toMatrix') and [`Matrix.toQuadraticMap'`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/QuadraticForm/Basic.html#Matrix.toQuadraticMap') are the maps between quadratic forms and matrices.
diff --git a/templates/theories/naturals.md b/templates/theories/naturals.md
index abb5e10f96..165f8af958 100644
--- a/templates/theories/naturals.md
+++ b/templates/theories/naturals.md
@@ -1,46 +1,27 @@
-<div class="alert alert-info">
-<p>
-We are currently updating the Lean community website to describe working with Lean 4,
-but most of the information you will find here today still describes Lean 3.
-</p>
-<p>
-Pull requests updating this page for Lean 4 are very welcome.
-There is a link at the bottom of this page.
-</p>
-<p>
-Please visit <a href="https://leanprover.zulipchat.com">the leanprover zulip</a>
-and ask for whatever help you need during this transitional period!
-</p>
-<p>
-The website for Lean 3 has been <a href="https://leanprover-community.github.io/lean3/">archived</a>.
-If you need to link to Lean 3 specific resources please link there.
-</p>
-</div>
-
 # Maths in Lean: the natural numbers
 
 The natural numbers begin with zero as is standard in computer
-science. You can call them `nat` or `ℕ` (you get the latter
+science. You can call them `Nat` or `ℕ` (you get the latter
 symbol by typing `\N` in VS Code).
 
 The naturals are what is called an inductive type, with two
-constructors. The first is `nat.zero`, usually written `0` or `(0:ℕ)` in
-practice, which is zero. The other constructor is `nat.succ`, which
+constructors. The first is `Nat.zero`, usually written `0` or `(0 : ℕ)` in
+practice, which is zero. The other constructor is `Nat.succ`, which
 takes a natural as input and outputs the next one.
 
 Addition and multiplication are defined by recursion on the second
 variable and many proofs of basic stuff in the core library are by
 induction on the second variable. The notations `+`, `-`, `*` are shorthand
-for the functions `nat.add`, `nat.sub` and `nat.mul`, and other notations
+for the functions `Nat.add`, `Nat.sub` and `Nat.mul`, and other notations
 (`≤`, `<`, `|`) mean the usual things (get the "divides" symbol with `\|`).
 The `%` symbol denotes modulus (remainder after division).
 
-Here are some of core Lean's functions for working with `nat`.
+Here are some of core Lean's functions for working with `Nat`.
 
 ```lean
 open nat
 
-example : nat.succ (nat.succ 4) = 6 := rfl
+example : Nat.succ (Nat.succ 4) = 6 := rfl
 
 example : 4 - 3 = 1 := rfl
 
@@ -54,7 +35,7 @@ example (m n p : ℕ) : m + p = n + p → m = n := add_right_cancel
 
 example (a b c : ℕ) : a * (b + c) = a * b + a * c := left_distrib a b c
 
-example (m n : ℕ) : succ m ≤ succ n → m ≤ n := le_of_succ_le_succ
+example (m n : ℕ) : succ m ≤ succ n → m ≤ n := Nat.le_of_succ_le_succ
 
 example (a b: ℕ) : a < b → ∀ n, 0 < n → a ^ n < b ^ n := pow_lt_pow_of_lt_left
 ```
@@ -64,18 +45,18 @@ factorials, lowest common multiples, primes, square roots, and some
 modular arithmetic.
 
 ```lean
-import data.nat.dist -- distance function
-import data.nat.gcd -- gcd
-import data.nat.modeq -- modular arithmetic
-import data.nat.prime -- prime number stuff
-import data.nat.sqrt  -- square roots
-import tactic.norm_num -- a tactic for fast computations
+import Mathlib.Data.Nat.Dist -- distance function
+import Mathlib.Data.Nat.GCD.Basic -- gcd
+import Mathlib.Data.Nat.ModEq -- modular arithmetic
+import Mathlib.Data.Nat.Prime.Basic -- prime number stuff
+import Mathlib.Data.Nat.Factors -- factors
+import Mathlib.Tactic.NormNum.Prime -- a tactic for fast computations
 
-open nat
+open Nat
 
-example : fact 4 = 24 := rfl -- factorial
+example : factorial 4 = 24 := rfl -- factorial
 
-example (a : ℕ) : fact a > 0 := fact_pos a
+example (a : ℕ) : factorial a > 0 := factorial_pos a
 
 example : dist 6 4 = 2 := rfl -- distance function
 
@@ -88,14 +69,10 @@ example : lcm 6 4 = 12 := rfl
 example (a b : ℕ) : lcm a b = lcm b a := lcm_comm a b
 example (a b : ℕ) : gcd a b * lcm a b = a * b := gcd_mul_lcm a b
 
-example (a b : ℕ) : (∀ k : ℕ, k > 1 → k ∣ a → ¬ (k ∣ b) ) → coprime a b := coprime_of_dvd
-
 -- type the congruence symbol with \==
 
 example : 5 ≡ 8 [MOD 3] := rfl
 
-example (a b c d m : ℕ) : a ≡ b [MOD m] → c ≡ d [MOD m] → a * c ≡ b * d [MOD m] := modeq.modeq_mul
-
 -- nat.sqrt is integer square root (it rounds down).
 
 #eval sqrt 1000047
@@ -105,13 +82,7 @@ example (a : ℕ) : sqrt (a * a) = a := sqrt_eq a
 
 example (a b : ℕ) : sqrt a < b ↔ a < b * b := sqrt_lt
 
--- nat.prime n returns whether n is prime or not.
--- We can prove 59 is prime if we first tell Lean that primality
--- is decidable. But it's slow because the algorithms are
--- not optimised for the kernel.
-
-instance : decidable (prime 59) := decidable_prime_1 59
-example : prime 59 := dec_trivial
+example : Nat.Prime 59 := by decide
 
 -- (The default instance is `nat.decidable_prime`, which can't be
 -- used by `dec_trivial`, because the kernel would need to unfold
@@ -119,25 +90,26 @@ example : prime 59 := dec_trivial
 
 -- The tactic `norm_num`, amongst other things, provides faster primality testing.
 
-example : prime 104729 := by norm_num
+example : Nat.Prime 104729 := by
+  norm_num
 
-example (p : ℕ) : prime p → p ≥ 2 := prime.two_le
+example (p : ℕ) : Nat.Prime p → p ≥ 2 := Prime.two_le
 
-example (p : ℕ) : prime p ↔ p ≥ 2 ∧ ∀ m, 2 ≤ m → m ≤ sqrt p → ¬ (m ∣ p) := prime_def_le_sqrt
+example (p : ℕ) : Nat.Prime p ↔ p ≥ 2 ∧ ∀ m, 2 ≤ m → m ≤ sqrt p → ¬ (m ∣ p) := prime_def_le_sqrt
 
-example (p : ℕ) : prime p → (∀ m, coprime p m ∨ p ∣ m) := coprime_or_dvd_of_prime
+example (p : ℕ) : Nat.Prime p → (∀ m, Coprime p m ∨ p ∣ m) := coprime_or_dvd_of_prime
 
-example : ∀ n, ∃ p, p ≥ n ∧ prime p := exists_infinite_primes
+example : ∀ n, ∃ p, p ≥ n ∧ Nat.Prime p := exists_infinite_primes
 
--- min_fac returns the smallest prime factor of n (or junk if it doesn't have one)
+-- minFac returns the smallest prime factor of n (or junk if it doesn't have one)
 
-example : min_fac 12 = 2 := rfl
+example : minFac 12 = 2 := rfl
 
--- `factors n` is the prime factorization of `n`, listed in increasing order.
+-- `Nat.primeFactorsList n` is the prime factorization of `n`, listed in increasing order.
 -- This doesn't seem to reduce, and apparently there has not been
 -- an attempt to get the kernel to evaluate it sensibly.
 -- But we can evaluate it in the virtual machine using #eval .
 
-#eval factors (2^32+1)
+#eval primeFactorsList (2^32+1)
 -- [641, 6700417]
 ```
diff --git a/templates/theories/sets.md b/templates/theories/sets.md
index c3600e87d1..c392521655 100644
--- a/templates/theories/sets.md
+++ b/templates/theories/sets.md
@@ -1,29 +1,10 @@
-<div class="alert alert-info">
-<p>
-We are currently updating the Lean community website to describe working with Lean 4,
-but most of the information you will find here today still describes Lean 3.
-</p>
-<p>
-Pull requests updating this page for Lean 4 are very welcome.
-There is a link at the bottom of this page.
-</p>
-<p>
-Please visit <a href="https://leanprover.zulipchat.com">the leanprover zulip</a>
-and ask for whatever help you need during this transitional period!
-</p>
-<p>
-The website for Lean 3 has been <a href="https://leanprover-community.github.io/lean3/">archived</a>.
-If you need to link to Lean 3 specific resources please link there.
-</p>
-</div>
-
 # Maths in Lean: Sets and set-like objects
 
 ### Lists
 
-#### `data.list.basic`
+#### `Mathlib.Data.List.Basic`
 
-`list α` is the type of lists of elements of type α. Lists are finite and ordered, and can contain duplicates. Lists can only contain elements of the same type. Lists are constructed using the cons function, which appends an element of α to the top of a list. Lists are discussed in more detail in TPIL, chapter 7.5
+`List α` is the type of lists of elements of type `α`. Lists are finite and ordered, and can contain duplicates. Lists can only contain elements of the same type. Lists are constructed using the cons function, which appends an element of `α` to the top of a list. Lists are discussed in more detail in TPIL, chapter 7.5
 
 `[1, 1, 2, 4] ≠ [1, 2, 1, 4]`
 
@@ -31,9 +12,9 @@ If you need to link to Lean 3 specific resources please link there.
 
 ### Multisets
 
-#### `data.multiset`
+#### `Mathlib.Data.Multiset.Basic`
 
-`multiset α` is the type of multisets of elements of type α. Multisets are finite and can contain duplicates, but are not ordered. They are defined as the quotient of lists over the `perm` equivalence relation. Multisets can only contain elements of the same type.
+`Multiset α` is the type of multisets of elements of type `α`. Multisets are finite and can contain duplicates, but are not ordered. They are defined as the quotient of lists over the `Perm` equivalence relation. Multisets can only contain elements of the same type.
 
 `{1, 1, 2, 4} = {1, 2, 1, 4}`
 
@@ -41,9 +22,9 @@ If you need to link to Lean 3 specific resources please link there.
 
 ### Finsets
 
-#### `data.finset`
+#### `Mathlib.Data.Finset.Basic`
 
-`finset α` is the type of unordered lists of distinct elements of type α. A finset is contructed from a multiset and a proof that the multiset contains no duplicates. Finsets are finite. Finsets can only contain elements of the same type.
+`Finset α` is the type of unordered lists of distinct elements of type α. A finset is constructed from a multiset and a proof that the multiset contains no duplicates. Finsets are finite. Finsets can only contain elements of the same type.
 
 `{1, 1, 2, 4} = {1, 2, 1, 4}`
 
@@ -51,64 +32,61 @@ If you need to link to Lean 3 specific resources please link there.
 
 ### Sets and subtypes
 
-#### `data.set.basic`
+#### `Mathlib.Data.Set.Basic`
 
-`set α`. A set is defined as a predicate, i.e. a function `α → Prop`. The notation used is `{n : ℕ | 4 ≤ n}` for the set of naturals greater than or equal to 4. Sets can be infinite, and can only contain elements of the same type.
+`Set α`. A set is defined as a predicate, i.e. a function `α → Prop`. The notation used is `{n : ℕ | 4 ≤ n}` for the set of naturals greater than or equal to 4. Sets can be infinite, and can only contain elements of the same type.
 
 A subtype is similar to a set in that it is defined by a predicate. The notation used is `{n : ℕ // 4 ≤ n}` for the type of naturals greater than or equal to 4. However, a subtype is a type rather than a set, and the elements the aforementioned subtype do not have type `ℕ`, they have type `{n : ℕ // 4 ≤ n}`. This means that addition is not defined on this type, and equality between naturals and this type is also undefined. However it is possible to coerce an element of this subtype back into a natural, in the same way that a natural can be coerced into an integer, and then addition and equality behave as normal (see TPIL, chapter 6.7 for more on coercions). To construct an element of a subtype of α, you need an element of α and a proof that it satisfies the predicate, `4` and ``le_refl 4`` in the example below.
 
 ```lean
 def x : {n : ℕ // 4 ≤ n} := ⟨4, le_refl 4⟩
-example : ↑x + 6 = 10 := rfl
+example : (x : ℕ) + 6 = 10 := rfl
 ```
 
 Any set can be used where a type is expected, in which case the set will be coerced into the corresponding subtype.
 
 ```lean
-def S : set ℕ := {n : ℕ | 4 ≤ n}
-example : ∀ n : S, 4 ≤ (n : ℕ) := λ ⟨n, hn⟩, hn
+def S : Set ℕ := {n : ℕ | 4 ≤ n}
+example : ∀ n : S, 4 ≤ (n : ℕ) := fun ⟨n, hn⟩ ↦ hn
 ```
 
 It is useful to use a subtype rather than a set when you need to define functions on subtypes, or when using the cardinal of a subtype.
 
 ### Finite types
 
-#### `data.fintype.basic`
+#### `Mathlib.Data.Fintype.Basic`
 
-`fintype α` means that a type α is finite. It is constructed from a finset containing all elements of a type.
+`Fintype α` means that a type α is finite. It is constructed from a finset containing all elements of a type.
 
 ```lean
-class fintype (α : Type*) :=
-(elems : finset α)
-(complete : ∀ x : α, x ∈ elems)
+class Fintype (α : Type*) where
+  /-- The `Finset` containing all elements of a `Fintype` -/
+  elems : Finset α
+  /-- A proof that `elems` contains every element of the type -/
+  complete : ∀ x : α, x ∈ elems
 ```
 
-`fintype α` is not a proposition, because it contains data, however it is a subsingleton, meaning that any two elements of type `fintype α` are equal.
+`Fintype α` is not a proposition, because it contains data, however it is a subsingleton, meaning that any two elements of type `Fintype α` are equal.
 
-`finset.univ` is the finset containing all elements of a type, given a `fintype α` instance.
+`Finset.univ` is the finset containing all elements of a type, given a `Fintype α` instance.
 
 ### Finite sets
 
-#### `data.set.finite`
-
-The definition of a finite set, distinct from a finset is
-
-```lean
-def finite (s : set α) : Prop := nonempty (fintype s)
-```
+#### `Mathlib.Data.Set.Finite`
 
-This means when the set is coerced into a subtype, the type `fintype s` is nonempty.
-Using `classical.choice`, you can produce an object of type `fintype s` from a proof of `finite s`. There is a function `set.finite.to_finset` which produces a finset from a finite set.
+The definition of a finite set, distinct from a finset is that corresponding type is in bijection with `Fin n` for some `n : ℕ`.
+This means when the set is coerced into a subtype, the type `Fintype s` is nonempty.
+Using `Classical.choose`, you can produce an object of type `Fintype s` from a proof of `Finite s`. There is a function `Set.Finite.toFinset` which produces a finset from a finite set.
 
 ### Cardinals
 
-There are three functions `finset.card`, `fintype.card` and `multiset.card`, which refer to the sizes of finsets, multisets and finite types. For finite cardinals of sets, `fintype.card` can be used, given a proof that the set is finite.
+There are three functions `Finset.card`, `Fintype.card` and `Multiset.card`, which refer to the sizes of finsets, multisets and finite types. For finite cardinals of sets, `Fintype.card` can be used, given a proof that the set is finite.
 
 ```lean
-example : ∀ n : ℕ, fintype.card (fin n) = n := fintype.card_fin
-example : ∀ n : ℕ, finset.card (finset.range n) = n := finset.card_range
+example : ∀ n : ℕ, Fintype.card (Fin n) = n := Fintype.card_fin
+example : ∀ n : ℕ, Finset.card (Finset.range n) = n := Finset.card_range
 ```
 
-Here, `fin n` is the type of naturals less than n, and `finset.range n` is the finset of naturals less than n.
+Here, `Fin n` is the type of naturals less than n, and `Finset.range n` is the finset of naturals less than `n`.
 
-`set_theory.cardinal` contains theory on infinite cardinals
+`Mathlib.SetTheory.Cardinal.Basic` contains theory on infinite cardinals.
diff --git a/templates/theories/topology.md b/templates/theories/topology.md
index 8752ac9a27..1936735c26 100644
--- a/templates/theories/topology.md
+++ b/templates/theories/topology.md
@@ -1,42 +1,22 @@
-<div class="alert alert-info">
-<p>
-We are currently updating the Lean community website to describe working with Lean 4,
-but most of the information you will find here today still describes Lean 3.
-</p>
-<p>
-Pull requests updating this page for Lean 4 are very welcome.
-There is a link at the bottom of this page.
-</p>
-<p>
-Please visit <a href="https://leanprover.zulipchat.com">the leanprover zulip</a>
-and ask for whatever help you need during this transitional period!
-</p>
-<p>
-The website for Lean 3 has been <a href="https://leanprover-community.github.io/lean3/">archived</a>.
-If you need to link to Lean 3 specific resources please link there.
-</p>
-</div>
-
 # Maths in Lean: Topological, uniform and metric spaces
 
-The `topological_space` typeclass is defined in mathlib,
-in `topology/basic.lean`. There are about 18000
-lines of code in `topology` at the time of writing,
-covering the basics of topological spaces, continuous functions,
+The `TopologicalSpace` typeclass is defined in mathlib,
+in `Mathlib.Topology.Defs.Basic`. There a lot of
+lines of code in `topology`,covering the basics of topological spaces, continuous functions,
 topological groups and rings, and infinite sums. These docs
-are just concerned with the contents of the `topological_space.lean`
-file.
+are just concerned with the contents of the `Mathlib.Topology`
+folder.
 
 ### The basic typeclass
 
-The `topological_space` typeclass is an inductive type, defined
-as a structure on a type `α` in the obvious way: there is an `is_open`
-predicate, telling us when `U : set α` is open, and then the axioms
+The `TopologicalSpace` typeclass is an inductive type, defined
+as a structure on a type `α` in the obvious way: there is an `IsOpen`
+predicate, telling us when `U : Set α` is open, and then the axioms
 for a topology (pedantic note: the axiom that the empty set is open
 is omitted, as it follows from the fact that a union of open sets
 is open, applied to the empty union!).
 
-Note that there are two ways of formalising the axiom that an arbitrary
+Note that there are two ways of formalizing the axiom that an arbitrary
 union of open sets is open: one could either ask that given a set
 of open sets, their union is open, or one could ask that given
 a function from some index set `I` to the set of open sets, the union
@@ -44,48 +24,50 @@ of the values of the function is open. Mathlib goes for the first
 one, so the axiom is
 
 ```lean
-is_open_sUnion : ∀(s : set (set α)), (∀t∈s, is_open t) → is_open (⋃₀ s)
+isOpen_sUnion : ∀ (s : Set (set α)), (∀ t ∈ s, IsOpen t) → IsOpen (⋃₀ s)
 ```
 
 and then the index set version is a lemma:
 
 ```lean
-lemma is_open_Union {f : ι → set α} (h : ∀i, is_open (f i)) : is_open (⋃i, f i)
+lemma isOpen_biUnion {f : ι → Set α} {s : Set ι} (h : ∀ i ∈ s, IsOpen (f i)) : IsOpen (⋃ i ∈ s, f i)
 ```
 
 Note the naming conventions, standard across mathlib, that `sUnion`
-is a union over sets and `Union` (with a capital U) is a union over
+is a union over sets and `biUnion` is a union over
 the image of a function on an indexing set. The capital U's are
 to indicate a union of arbitrary size, as opposed to `union`, which
 indicates a union of two sets:
 
 ```lean
-lemma is_open_union (h₁ : is_open s₁) (h₂ : is_open s₂) : is_open (s₁ ∪ s₂)
+lemma IsOpen.union (h₁ : is_open s₁) (h₂ : is_open s₂) : is_open (s₁ ∪ s₂)
 ```
 
-The predicate `is_closed`, and functions `interior`, `closure`, and
+The predicate `IsClosed`, and functions `interior`, `closure`, and
 `frontier` (closure minus interior,
 sometimes called boundary in mathematics) are defined, and basic
 properties about them are proved. For example
 
 ```lean
-import topology.basic
-open topological_space
-variables {X : Type} [topological_space X] {U V C D Y Z : set X}
+import Mathlib.Topology.Basic
+
+
+open TopologicalSpace
+variable {X : Type} [TopologicalSpace X] {U V C D Y Z : Set X}
 
-example : is_closed C → is_closed D → is_closed (C ∪ D) := is_closed_union
+example : IsClosed C → IsClosed D → IsClosed (C ∪ D) := IsClosed.union
 
-example : is_open Cᶜ ↔ is_closed C := is_open_compl_iff
+example : IsOpen Cᶜ ↔ IsClosed C := isOpen_compl_iff
 
-example : is_open U → is_closed C → is_open (U \ C) := is_open_diff
+example : IsOpen U → IsClosed C → IsOpen (U \ C) := IsOpen.sdiff
 
-example : interior Y = Y ↔ is_open Y := interior_eq_iff_open
+example : interior Y = Y ↔ IsOpen Y := interior_eq_iff_isOpen
 
 example : Y ⊆ Z → interior Y ⊆ interior Z := interior_mono
 
-example : is_open Y ↔ ∀ x ∈ Y, ∃ U ⊆ Y, is_open U ∧ x ∈ U := is_open_iff_forall_mem_open
+example : IsOpen Y ↔ ∀ x ∈ Y, ∃ U ⊆ Y, IsOpen U ∧ x ∈ U := isOpen_iff_forall_mem_open
 
-example : closure Y = Y ↔ is_closed Y := closure_eq_iff_is_closed
+example : closure Y = Y ↔ IsClosed Y := closure_eq_iff_isClosed
 
 example : closure Y = (interior Yᶜ)ᶜ := closure_eq_compl_interior_compl
 ```
@@ -105,28 +87,32 @@ Informally, one can think of `F` as the set of "big" subsets of `X`. For example
 
 Note that if `F` is a filter that contains the empty set, then it contains all subsets of `X` by the first axiom. This filter is sometimes called "bottom" (we will see why a little later on). Some references demand that the empty set is not allowed to be in a filter -- Lean does not have this restriction. A filter not containing the empty set is sometimes called a "proper filter".
 
-If `X` is a topological space, and `x ∈ X`, then the _neighbourhood filter_ `𝓝 x` of `x` is the set of subsets `Y` of `X` such that `x` is in the interior of `Y`. One checks easily that this is a filter (technical point: to see that this is actually the definition of `𝓝 x` in mathlib, it helps to know that the set of all filters on a type is a complete lattice, partially ordered using `F ≤ G` iff `G ⊆ F`, so the definition, which involves an inf, is actually a union; also, the definition I give is not literally the definition in mathlib, but `lemma nhds_sets` says that their definition is the one here. Note also that this is why the filter with the most sets is called bottom!).
+If `X` is a topological space, and `x ∈ X`, then the _neighborhood filter_ `𝓝 x` of `x` is the set of subsets `Y` of `X` such that `x` is in the interior of `Y`. One checks easily that this is a filter (technical point: to see that this is actually the definition of `𝓝 x` in mathlib, it helps to know that the set of all filters on a type is a complete lattice, partially ordered using `F ≤ G` iff `G ⊆ F`, so the definition, which involves an inf, is actually a union; also, the definition I give is not literally the definition in mathlib, but `lemma mem_nhds_iff` says that their definition is the one here. Note also that this is why the filter with the most sets is called bottom!).
 
 Why are we interested in these filters? Well, given a map `f` from `ℕ` to a topological space `X`, one can check that the resulting sequence `f 0`, `f 1`, `f 2`... tends to `x ∈ X` if and only if the pre-image of any element in the filter `𝓝 x` is in the cofinite filter on `ℕ` -- this is just another way of saying that given any open set `U` containing `x`, there exists `N` such that for all `n ≥ N`, `f n ∈ U`. So filters provide a way of thinking about limits.
 
 As an example, below are three limits formulated in Lean.
-The example uses the filters `at_top` and `at_bot` that represent "tends to `∞`" and "tends to `-∞`" in a type equipped with an order.
+The example uses the filters `atTop` and `atBot` that represent "tends to `∞`" and "tends to `-∞`" in a type equipped with an order.
 
 ```lean
+open Filter Topology
+
 -- The limit of `2 * x` as `x` tends to `3` is `6`
-example : tendsto (λ x : ℝ, 2 * x) (𝓝 3) (𝓝 6) := sorry
+example : Tendsto (fun x : ℝ ↦ 2 * x) (𝓝 3) (𝓝 6) := sorry
 -- The limit of `1 / x` as `x` tends to `∞` is `0`
-example : tendsto (λ x : ℝ, 1 / x) at_top (𝓝 0) := sorry
+example : Tendsto (fun x : ℝ ↦ 1 / x) atTop (𝓝 0) := sorry
 -- The limit of `x ^ 2` as `x` tends to `-∞` is `∞`
-example : tendsto (λ x : ℝ, x ^ 2) at_bot at_top := sorry
+example : Tendsto (fun x : ℝ ↦ x ^ 2) atBot atTop := sorry
 ```
 
-The _principal filter_ `principal Y` attached to a subset `Y` of a set `X` is the collection of all subsets of `X` that contain `Y`. So it's not difficult to convince yourself that the following results should be true:
+The _principal filter_ `Filter.principal Y` attached to a subset `Y` of a set `X` is the collection of all subsets of `X` that contain `Y`. So it's not difficult to convince yourself that the following results should be true:
 
 ```lean
-example : interior Y = {x | 𝓝 x ≤ filter.principal Y} := interior_eq_nhds
+variable (X : Type) [TopologicalSpace X] (Y : Set X)
+
+example : interior Y = {x | 𝓝 x ≤ Filter.principal Y} := interior_eq_nhds
 
-example : is_open Y ↔ ∀ y ∈ Y, Y ∈ (𝓝 y).sets := is_open_iff_mem_nhds
+example : IsOpen Y ↔ ∀ y ∈ Y, Y ∈ (𝓝 y).sets := isOpen_iff_eventually
 ```
 
 ### Compactness with filters
@@ -138,37 +124,39 @@ for what it means for a sequence to tend to a limit. The definition
 of compactness is also written in filter-theoretic terms:
 
 ```lean
-/-- A set `s` is compact if every filter that contains `s` also meets every
-  neighborhood of some `a ∈ s`. -/
-def compact (Y : set X) := ∀F, F ≠ ⊥ → F ≤ principal Y → ∃y∈Y, F ⊓ 𝓝 y ≠ ⊥
+/-- A set `s` is compact if for every nontrivial filter `f` that contains `s`,
+    there exists `a ∈ s` such that every set of `f` meets every neighborhood of `a`. -/
+def IsCompact (s : Set X) :=
+  ∀ ⦃f⦄ [NeBot f], f ≤ 𝓟 s → ∃ x ∈ s, ClusterPt x f
 ```
 
-Translated, this says that a subset `Y` of a topological space `X` is compact if for every proper filter `F` on `X`, if `Y` is an element of `F` then there's an element `y` of `Y` such that the smallest filter containing both F and the neighbourhood filter of `y` is not the filter of all subsets of `X` either. This should be thought of as being the correct general analogue of the Bolzano-Weierstrass theorem, that in a compact subspace of `ℝ^n`, any sequence has a convergent subsequence.
+Translated, this says that a subset `Y` of a topological space `X` is compact if for every proper filter `F` on `X`, if `Y` is an element of `F` then there's an element `y` of `Y` such that the smallest filter containing both F and the neighborhood filter of `y` is not the filter of all subsets of `X` either. This should be thought of as being the correct general analogue of the Bolzano-Weierstrass theorem, that in a compact subspace of `ℝ^n`, any sequence has a convergent subsequence.
 
 One might ask why this definition of compactness has been chosen, rather than the standard one about open covers having finite subcovers. The reasons for this are in some sense computer-scientific rather than mathematical -- the issue should not be what definition is ultimately chosen (indeed the developers should feel free to choose whatever definition they like as long as it is logically equivalent to the usual one, and they might have reasons related to non-mathematical points such as running times), the issue should be how to prove that the inbuilt definition is equivalent to the one you want to use in practice. And fortunately, we have
 
 ```lean
-example : compact Y ↔
-  (∀ cov : set (set X), (∀ U ∈ cov, is_open U) → Y ⊆ ⋃₀ cov →
-    ∃ fincov ⊆ cov, set.finite fincov ∧ Y ⊆ ⋃₀ fincov) := compact_iff_finite_subcover
+example : IsCompact Y ↔ ∀ {ι : Type} (U : ι → Set X),
+      (∀ i, IsOpen (U i)) → (Y ⊆ ⋃ i, U i) → ∃ t : Finset ι, Y ⊆ ⋃ i ∈ t, U i :=
+    isCompact_iff_finite_subcover
 ```
 
 so the Lean definition is equivalent to the standard one.
 
 ### Hausdorff spaces
 
-In Lean they chose the terminology `t2_space` to mean Hausdorff (perhaps because it is shorter!).
+In Lean they chose the terminology `T2Space` to mean Hausdorff (perhaps because it is shorter!).
 
 ```lean
-class t2_space (X : Type) [topological_space X] :=
-(t2 : ∀x y, x ≠ y → ∃U V : set X, is_open U ∧ is_open V ∧ x ∈ U ∧ y ∈ V ∧ U ∩ V = ∅)
+class T2Space (X : Type u) [TopologicalSpace X] : Prop where
+  /-- Every two points in a Hausdorff space admit disjoint open neighbourhoods. -/
+  t2 : Pairwise fun x y => ∃ u v : Set X, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v
 ```
 
 Of course Hausdorffness is what we need to ensure that limits are unique, but because limits are defined using filters this statements ends up reading as follows:
 
 ```lean
-lemma tendsto_nhds_unique [t2_space X] {f : β → X} {l : filter β} {x y : X}
-  (hl : l ≠ ⊥) (hx : tendsto f l (𝓝 x)) (hb : tendsto f l (𝓝 y)) : x = y
+lemma tendsto_nhds_unique [T2Space X] {f : β → X} {l : Filter β} {x y : X}
+  [l.NeBot] (hx : Tendsto f l (𝓝 x)) (hb : Tendsto f l (𝓝 y)) : x = y
 ```
 
 Note that actually this statement is more general than the classical statement that if a sequence tends to two limits in a Hausdorff space then the limits are the same, because it applies to any non-trivial filter on any set rather than just the cofinite filter on the natural numbers.
@@ -192,10 +180,10 @@ directly. However again we have a theorem which reduces us to checking
 the two usual axioms for a basis:
 
 ```lean
-example (B : set (set X)) (h_open : ∀ V ∈ B, is_open V)
-  (h_nhds : ∀ (x : X) (U : set X), x ∈ U → is_open U → ∃ V ∈ B, x ∈ V ∧ V ⊆ U) :
-is_topological_basis B :=
-is_topological_basis_of_open_of_nhds h_open h_nhds
+example (B : Set (Set X)) (h_open : ∀ V ∈ B, IsOpen V)
+  (h_nhds : ∀ (x : X) (U : Set X), x ∈ U → IsOpen U → ∃ V ∈ B, x ∈ V ∧ V ⊆ U) :
+IsTopologicalBasis B :=
+isTopologicalBasis_of_isOpen_of_nhds h_open h_nhds
 ```
 
 ### Other things
@@ -209,52 +197,44 @@ and things like t1 and t3 spaces.
 
 The following "core" modules form a linear chain of imports. A theorem involving concepts defined in several of these files should be found in the last such file in this ordering.
 
-* `basic`
+* `Mathlib.Topology.Basic`
   Topological spaces. Open and closed subsets, interior, closure and frontier (boundary). Neighborhood filters. Limit of a filter. Locally finite families. Continuity and continuity at a point.
-* `order`
+* `Mathlib.Topology.Order.Basic`
   The complete lattice structure on topologies on a fixed set. Induced and coinduced topologies.
 * `maps`
   Open and closed maps. "Inducing" maps. Embeddings, open embeddings and closed embeddings. Quotient maps.
-* `constructions`
+* `Mathlib.Topology.Constructions`
   Building new topological spaces from old ones: products, sums, subspaces and quotients.
-* `subset_properties`
-  Compactness. Clopen subsets, irreducibility and connectedness. Totally disconnected and totally separated sets and spaces.
-* `separation`
+* `Mathlib.Topology.Separation`
   Separation axioms T₀ through T₄, also known as Kolmogorov, Tychonoff or Fréchet, Hausdorff, regular, and normal spaces respectively.
 
-The remaining directories and files, in no particular order:
+Some of the remaining directories and files, in no particular order:
 
-* `algebra`
+* `Mathlib.Topology.Algebra`
   Topological spaces with compatible algebraic or ordered structure.
-* `category`
+* `Mathlib.Topology.Category`
   The categories of topological spaces, uniform spaces, etc.
-* `instances`
+* `Mathlib.Topology.Instances`
   Specific topological spaces such as the real numbers and the complex numbers.
-* `metric_space`
+* `Mathlib.Topology.MetricSpace`
   The theory of metric spaces; but some notions one might expect to find here are instead generalized to uniform spaces.
-* `sheaves`
+* `Mathlib.Topology.Sheaves`
   Presheaves on a topological space.
-* `uniform_space`
+* `Mathlib.Topology.UniformSpace`
   The theory of uniform spaces, including notions such as completeness, uniform continuity and totally bounded sets.
-* `bases`
+* `Mathlib.Topology.Bases`
   Bases for filters and topological spaces. Separable, first countable and second countable spaces.
-* `bounded_continuous_function`
-  Bounded continuous functions from a topological space to a metric space.
-* `compact_open`
+* `Mathlib.Topology.CompactOpen`
   The compact-open topology on the space of continuous maps between two topological spaces.
-* `continuous_on`
+* `Mathlib.Topology.ContinuousOn`
   Neighborhoods within a subset. Continuity on a subset, and continuity within a subset at a point.
-* `dense_embedding`
+* `Mathlib.Topology.DenseEmbedding`
   Embeddings and other functions with dense image.
-* `homeomorph`
+* `Mathlib.Topology.Homeomorph`
   Homeomorphisms between topological spaces.
-* `list`
+* `Mathlib.Topology.List`
   Topologies on lists and vectors.
-* `local_homeomorph`
-  Homeomorphisms between open subsets of topological spaces.
-* `opens`
-  The complete lattice of open subsets of a topological space. The types of closed and nonempty compact subsets.
-* `sequences`
+* `Mathlib.Topology.Sequences`
   Sequential closure and sequential spaces. Sequentially continuous functions.
-* `stone_cech`
+* `Mathlib.Topology.StoneCech`
   The Stone-Čech compactification of a topological space.