diff --git a/Mathbin/AlgebraicGeometry/GammaSpecAdjunction.lean b/Mathbin/AlgebraicGeometry/GammaSpecAdjunction.lean
index c38d158f56..0c1e577787 100644
--- a/Mathbin/AlgebraicGeometry/GammaSpecAdjunction.lean
+++ b/Mathbin/AlgebraicGeometry/GammaSpecAdjunction.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Junyan Xu
 
 ! This file was ported from Lean 3 source module algebraic_geometry.Gamma_Spec_adjunction
-! leanprover-community/mathlib commit d39590fc8728fbf6743249802486f8c91ffe07bc
+! leanprover-community/mathlib commit 5d0c76894ada7940957143163d7b921345474cbc
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -15,6 +15,9 @@ import Mathbin.CategoryTheory.Adjunction.Reflective
 /-!
 # Adjunction between `Γ` and `Spec`
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We define the adjunction `Γ_Spec.adjunction : Γ ⊣ Spec` by defining the unit (`to_Γ_Spec`,
 in multiple steps in this file) and counit (done in Spec.lean) and checking that they satisfy
 the left and right triangle identities. The constructions and proofs make use of
diff --git a/Mathbin/AlgebraicGeometry/OpenImmersion/Scheme.lean b/Mathbin/AlgebraicGeometry/OpenImmersion/Scheme.lean
index 7e57d31bc9..9f28de6a59 100644
--- a/Mathbin/AlgebraicGeometry/OpenImmersion/Scheme.lean
+++ b/Mathbin/AlgebraicGeometry/OpenImmersion/Scheme.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andrew Yang
 
 ! This file was ported from Lean 3 source module algebraic_geometry.open_immersion.Scheme
-! leanprover-community/mathlib commit 533f62f4dd62a5aad24a04326e6e787c8f7e98b1
+! leanprover-community/mathlib commit 5d0c76894ada7940957143163d7b921345474cbc
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -15,6 +15,9 @@ import Mathbin.CategoryTheory.Limits.Shapes.CommSq
 /-!
 # Open immersions of schemes
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 -/
 
 
diff --git a/Mathbin/All.lean b/Mathbin/All.lean
index c4ca950628..28227589ab 100644
--- a/Mathbin/All.lean
+++ b/Mathbin/All.lean
@@ -585,6 +585,7 @@ import Mathbin.Analysis.Complex.Schwarz
 import Mathbin.Analysis.Complex.UnitDisc.Basic
 import Mathbin.Analysis.Complex.UpperHalfPlane.Basic
 import Mathbin.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty
+import Mathbin.Analysis.Complex.UpperHalfPlane.Manifold
 import Mathbin.Analysis.Complex.UpperHalfPlane.Metric
 import Mathbin.Analysis.Complex.UpperHalfPlane.Topology
 import Mathbin.Analysis.ConstantSpeed
@@ -2338,7 +2339,8 @@ import Mathbin.NumberTheory.LucasLehmer
 import Mathbin.NumberTheory.LucasPrimality
 import Mathbin.NumberTheory.ModularForms.Basic
 import Mathbin.NumberTheory.ModularForms.CongruenceSubgroups
-import Mathbin.NumberTheory.ModularForms.JacobiTheta
+import Mathbin.NumberTheory.ModularForms.JacobiTheta.Basic
+import Mathbin.NumberTheory.ModularForms.JacobiTheta.Manifold
 import Mathbin.NumberTheory.ModularForms.SlashActions
 import Mathbin.NumberTheory.ModularForms.SlashInvariantForms
 import Mathbin.NumberTheory.Modular
@@ -3106,6 +3108,7 @@ import Mathbin.Topology.MetricSpace.CauSeqFilter
 import Mathbin.Topology.MetricSpace.Closeds
 import Mathbin.Topology.MetricSpace.Completion
 import Mathbin.Topology.MetricSpace.Contracting
+import Mathbin.Topology.MetricSpace.Dilation
 import Mathbin.Topology.MetricSpace.EmetricParacompact
 import Mathbin.Topology.MetricSpace.EmetricSpace
 import Mathbin.Topology.MetricSpace.Equicontinuity
diff --git a/Mathbin/Analysis/Calculus/Implicit.lean b/Mathbin/Analysis/Calculus/Implicit.lean
index e8c1f0090b..8f28eb2c87 100644
--- a/Mathbin/Analysis/Calculus/Implicit.lean
+++ b/Mathbin/Analysis/Calculus/Implicit.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 
 ! This file was ported from Lean 3 source module analysis.calculus.implicit
-! leanprover-community/mathlib commit f2ce6086713c78a7f880485f7917ea547a215982
+! leanprover-community/mathlib commit 5d0c76894ada7940957143163d7b921345474cbc
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -14,6 +14,9 @@ import Mathbin.Analysis.NormedSpace.Complemented
 /-!
 # Implicit function theorem
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We prove three versions of the implicit function theorem. First we define a structure
 `implicit_function_data` that holds arguments for the most general version of the implicit function
 theorem, see `implicit_function_data.implicit_function`
diff --git a/Mathbin/Analysis/Complex/UpperHalfPlane/Manifold.lean b/Mathbin/Analysis/Complex/UpperHalfPlane/Manifold.lean
new file mode 100644
index 0000000000..27678900f8
--- /dev/null
+++ b/Mathbin/Analysis/Complex/UpperHalfPlane/Manifold.lean
@@ -0,0 +1,41 @@
+/-
+Copyright (c) 2022 Chris Birkbeck. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Chris Birkbeck
+
+! This file was ported from Lean 3 source module analysis.complex.upper_half_plane.manifold
+! leanprover-community/mathlib commit 57f9349f2fe19d2de7207e99b0341808d977cdcf
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathbin.Analysis.Complex.UpperHalfPlane.Topology
+import Mathbin.Geometry.Manifold.ContMdiffMfderiv
+
+/-!
+# Manifold structure on the upper half plane.
+
+In this file we define the complex manifold structure on the upper half-plane.
+-/
+
+
+open scoped UpperHalfPlane Manifold
+
+namespace UpperHalfPlane
+
+noncomputable instance : ChartedSpace ℂ ℍ :=
+  UpperHalfPlane.openEmbedding_coe.singletonChartedSpace
+
+instance : SmoothManifoldWithCorners 𝓘(ℂ) ℍ :=
+  UpperHalfPlane.openEmbedding_coe.singleton_smoothManifoldWithCorners 𝓘(ℂ)
+
+/-- The inclusion map `ℍ → ℂ` is a smooth map of manifolds. -/
+theorem smooth_coe : Smooth 𝓘(ℂ) 𝓘(ℂ) (coe : ℍ → ℂ) := fun x => contMdiffAt_extChartAt
+#align upper_half_plane.smooth_coe UpperHalfPlane.smooth_coe
+
+/-- The inclusion map `ℍ → ℂ` is a differentiable map of manifolds. -/
+theorem mdifferentiable_coe : Mdifferentiable 𝓘(ℂ) 𝓘(ℂ) (coe : ℍ → ℂ) :=
+  smooth_coe.Mdifferentiable
+#align upper_half_plane.mdifferentiable_coe UpperHalfPlane.mdifferentiable_coe
+
+end UpperHalfPlane
+
diff --git a/Mathbin/Analysis/Complex/UpperHalfPlane/Topology.lean b/Mathbin/Analysis/Complex/UpperHalfPlane/Topology.lean
index d566d1be87..cead676944 100644
--- a/Mathbin/Analysis/Complex/UpperHalfPlane/Topology.lean
+++ b/Mathbin/Analysis/Complex/UpperHalfPlane/Topology.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury G. Kudryashov
 
 ! This file was ported from Lean 3 source module analysis.complex.upper_half_plane.topology
-! leanprover-community/mathlib commit f0c8bf9245297a541f468be517f1bde6195105e9
+! leanprover-community/mathlib commit 57f9349f2fe19d2de7207e99b0341808d977cdcf
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -14,7 +14,6 @@ import Mathbin.Analysis.Convex.Normed
 import Mathbin.Analysis.Convex.Complex
 import Mathbin.Analysis.Complex.ReImTopology
 import Mathbin.Topology.Homotopy.Contractible
-import Mathbin.Geometry.Manifold.ContMdiffMfderiv
 
 /-!
 # Topology on the upper half plane
@@ -28,7 +27,7 @@ noncomputable section
 
 open Set Filter Function TopologicalSpace Complex
 
-open scoped Filter Topology UpperHalfPlane Manifold
+open scoped Filter Topology UpperHalfPlane
 
 namespace UpperHalfPlane
 
@@ -80,22 +79,5 @@ instance : NoncompactSpace ℍ := by
 instance : LocallyCompactSpace ℍ :=
   openEmbedding_coe.LocallyCompactSpace
 
-instance UpperHalfPlane.chartedSpace : ChartedSpace ℂ ℍ :=
-  UpperHalfPlane.openEmbedding_coe.singletonChartedSpace
-#align upper_half_plane.upper_half_plane.charted_space UpperHalfPlane.UpperHalfPlane.chartedSpace
-
-instance UpperHalfPlane.smoothManifoldWithCorners : SmoothManifoldWithCorners 𝓘(ℂ) ℍ :=
-  UpperHalfPlane.openEmbedding_coe.singleton_smoothManifoldWithCorners 𝓘(ℂ)
-#align upper_half_plane.upper_half_plane.smooth_manifold_with_corners UpperHalfPlane.UpperHalfPlane.smoothManifoldWithCorners
-
-/-- The inclusion map `ℍ → ℂ` is a smooth map of manifolds. -/
-theorem smooth_coe : Smooth 𝓘(ℂ) 𝓘(ℂ) (coe : ℍ → ℂ) := fun x => contMdiffAt_extChartAt
-#align upper_half_plane.smooth_coe UpperHalfPlane.smooth_coe
-
-/-- The inclusion map `ℍ → ℂ` is a differentiable map of manifolds. -/
-theorem mdifferentiable_coe : Mdifferentiable 𝓘(ℂ) 𝓘(ℂ) (coe : ℍ → ℂ) :=
-  smooth_coe.Mdifferentiable
-#align upper_half_plane.mdifferentiable_coe UpperHalfPlane.mdifferentiable_coe
-
 end UpperHalfPlane
 
diff --git a/Mathbin/Analysis/Matrix.lean b/Mathbin/Analysis/Matrix.lean
index b0500188b8..0e54efba92 100644
--- a/Mathbin/Analysis/Matrix.lean
+++ b/Mathbin/Analysis/Matrix.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Heather Macbeth, Eric Wieser
 
 ! This file was ported from Lean 3 source module analysis.matrix
-! leanprover-community/mathlib commit 46b633fd842bef9469441c0209906f6dddd2b4f5
+! leanprover-community/mathlib commit 5d0c76894ada7940957143163d7b921345474cbc
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -15,6 +15,9 @@ import Mathbin.Analysis.InnerProductSpace.PiL2
 /-!
 # Matrices as a normed space
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we provide the following non-instances for norms on matrices:
 
 * The elementwise norm:
diff --git a/Mathbin/Analysis/NormedSpace/MatrixExponential.lean b/Mathbin/Analysis/NormedSpace/MatrixExponential.lean
index c4fb0acc4e..87e2145972 100644
--- a/Mathbin/Analysis/NormedSpace/MatrixExponential.lean
+++ b/Mathbin/Analysis/NormedSpace/MatrixExponential.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser
 
 ! This file was ported from Lean 3 source module analysis.normed_space.matrix_exponential
-! leanprover-community/mathlib commit 1e3201306d4d9eb1fd54c60d7c4510ad5126f6f9
+! leanprover-community/mathlib commit 5d0c76894ada7940957143163d7b921345474cbc
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -18,6 +18,9 @@ import Mathbin.Topology.UniformSpace.Matrix
 /-!
 # Lemmas about the matrix exponential
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file, we provide results about `exp` on `matrix`s over a topological or normed algebra.
 Note that generic results over all topological spaces such as `exp_zero` can be used on matrices
 without issue, so are not repeated here. The topological results specific to matrices are:
diff --git a/Mathbin/Analysis/NormedSpace/Star/Matrix.lean b/Mathbin/Analysis/NormedSpace/Star/Matrix.lean
index 6cb4f76e21..f214f23225 100644
--- a/Mathbin/Analysis/NormedSpace/Star/Matrix.lean
+++ b/Mathbin/Analysis/NormedSpace/Star/Matrix.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Hans Parshall
 
 ! This file was ported from Lean 3 source module analysis.normed_space.star.matrix
-! leanprover-community/mathlib commit 468b141b14016d54b479eb7a0fff1e360b7e3cf6
+! leanprover-community/mathlib commit 5d0c76894ada7940957143163d7b921345474cbc
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -16,6 +16,9 @@ import Mathbin.LinearAlgebra.UnitaryGroup
 /-!
 # Unitary matrices
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file collects facts about the unitary matrices over `𝕜` (either `ℝ` or `ℂ`).
 -/
 
diff --git a/Mathbin/Data/Matrix/Invertible.lean b/Mathbin/Data/Matrix/Invertible.lean
index b37ba30f58..49e9de4a61 100644
--- a/Mathbin/Data/Matrix/Invertible.lean
+++ b/Mathbin/Data/Matrix/Invertible.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser
 
 ! This file was ported from Lean 3 source module data.matrix.invertible
-! leanprover-community/mathlib commit 722b3b152ddd5e0cf21c0a29787c76596cb6b422
+! leanprover-community/mathlib commit 5d0c76894ada7940957143163d7b921345474cbc
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -13,6 +13,9 @@ import Mathbin.Data.Matrix.Basic
 
 /-! # Extra lemmas about invertible matrices
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Many of the `invertible` lemmas are about `*`; this restates them to be about `⬝`.
 
 For lemmas about the matrix inverse in terms of the determinant and adjugate, see `matrix.has_inv`
diff --git a/Mathbin/LinearAlgebra/CliffordAlgebra/Basic.lean b/Mathbin/LinearAlgebra/CliffordAlgebra/Basic.lean
index f1a45b5b89..a55374d407 100644
--- a/Mathbin/LinearAlgebra/CliffordAlgebra/Basic.lean
+++ b/Mathbin/LinearAlgebra/CliffordAlgebra/Basic.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser, Utensil Song
 
 ! This file was ported from Lean 3 source module linear_algebra.clifford_algebra.basic
-! leanprover-community/mathlib commit d46774d43797f5d1f507a63a6e904f7a533ae74a
+! leanprover-community/mathlib commit 5d0c76894ada7940957143163d7b921345474cbc
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -15,6 +15,9 @@ import Mathbin.LinearAlgebra.QuadraticForm.Isometry
 /-!
 # Clifford Algebras
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We construct the Clifford algebra of a module `M` over a commutative ring `R`, equipped with
 a quadratic_form `Q`.
 
diff --git a/Mathbin/LinearAlgebra/ExteriorAlgebra/Basic.lean b/Mathbin/LinearAlgebra/ExteriorAlgebra/Basic.lean
index c0d5db22f5..ff878ddfd4 100644
--- a/Mathbin/LinearAlgebra/ExteriorAlgebra/Basic.lean
+++ b/Mathbin/LinearAlgebra/ExteriorAlgebra/Basic.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Zhangir Azerbayev, Adam Topaz, Eric Wieser
 
 ! This file was ported from Lean 3 source module linear_algebra.exterior_algebra.basic
-! leanprover-community/mathlib commit b8d2eaa69d69ce8f03179a5cda774fc0cde984e4
+! leanprover-community/mathlib commit 5d0c76894ada7940957143163d7b921345474cbc
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -14,6 +14,9 @@ import Mathbin.LinearAlgebra.Alternating
 /-!
 # Exterior Algebras
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We construct the exterior algebra of a module `M` over a commutative semiring `R`.
 
 ## Notation
diff --git a/Mathbin/NumberTheory/Cyclotomic/Basic.lean b/Mathbin/NumberTheory/Cyclotomic/Basic.lean
index b82647bb14..50feb54173 100644
--- a/Mathbin/NumberTheory/Cyclotomic/Basic.lean
+++ b/Mathbin/NumberTheory/Cyclotomic/Basic.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Riccardo Brasca
 
 ! This file was ported from Lean 3 source module number_theory.cyclotomic.basic
-! leanprover-community/mathlib commit 4b05d3f4f0601dca8abf99c4ec99187682ed0bba
+! leanprover-community/mathlib commit 5d0c76894ada7940957143163d7b921345474cbc
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -15,6 +15,9 @@ import Mathbin.FieldTheory.Galois
 /-!
 # Cyclotomic extensions
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Let `A` and `B` be commutative rings with `algebra A B`. For `S : set ℕ+`, we define a class
 `is_cyclotomic_extension S A B` expressing the fact that `B` is obtained from `A` by adding `n`-th
 primitive roots of unity, for all `n ∈ S`.
diff --git a/Mathbin/NumberTheory/Cyclotomic/PrimitiveRoots.lean b/Mathbin/NumberTheory/Cyclotomic/PrimitiveRoots.lean
index 337d31e608..81e278b297 100644
--- a/Mathbin/NumberTheory/Cyclotomic/PrimitiveRoots.lean
+++ b/Mathbin/NumberTheory/Cyclotomic/PrimitiveRoots.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Alex Best, Riccardo Brasca, Eric Rodriguez
 
 ! This file was ported from Lean 3 source module number_theory.cyclotomic.primitive_roots
-! leanprover-community/mathlib commit 5bfbcca0a7ffdd21cf1682e59106d6c942434a32
+! leanprover-community/mathlib commit 5d0c76894ada7940957143163d7b921345474cbc
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -18,6 +18,9 @@ import Mathbin.RingTheory.Polynomial.Cyclotomic.Expand
 
 /-!
 # Primitive roots in cyclotomic fields
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
 If `is_cyclotomic_extension {n} A B`, we define an element `zeta n A B : B` that is a primitive
 `n`th-root of unity in `B` and we study its properties. We also prove related theorems under the
 more general assumption of just being a primitive root, for reasons described in the implementation
diff --git a/Mathbin/NumberTheory/ModularForms/Basic.lean b/Mathbin/NumberTheory/ModularForms/Basic.lean
index 1db8381682..9a400684b6 100644
--- a/Mathbin/NumberTheory/ModularForms/Basic.lean
+++ b/Mathbin/NumberTheory/ModularForms/Basic.lean
@@ -4,12 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Birkbeck
 
 ! This file was ported from Lean 3 source module number_theory.modular_forms.basic
-! leanprover-community/mathlib commit 59150e4a8ab64a88e35d5cfa0a17b762a68acfe9
+! leanprover-community/mathlib commit 57f9349f2fe19d2de7207e99b0341808d977cdcf
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
 import Mathbin.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty
-import Mathbin.Analysis.Complex.UpperHalfPlane.Topology
+import Mathbin.Analysis.Complex.UpperHalfPlane.Manifold
 import Mathbin.NumberTheory.ModularForms.SlashInvariantForms
 
 /-!
diff --git a/Mathbin/NumberTheory/ModularForms/JacobiTheta.lean b/Mathbin/NumberTheory/ModularForms/JacobiTheta/Basic.lean
similarity index 94%
rename from Mathbin/NumberTheory/ModularForms/JacobiTheta.lean
rename to Mathbin/NumberTheory/ModularForms/JacobiTheta/Basic.lean
index 762a8ec919..55b2d28b10 100644
--- a/Mathbin/NumberTheory/ModularForms/JacobiTheta.lean
+++ b/Mathbin/NumberTheory/ModularForms/JacobiTheta/Basic.lean
@@ -3,8 +3,8 @@ Copyright (c) 2023 David Loeffler. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: David Loeffler
 
-! This file was ported from Lean 3 source module number_theory.modular_forms.jacobi_theta
-! leanprover-community/mathlib commit c720ca1664115159ac610a74e079287d052cf8d0
+! This file was ported from Lean 3 source module number_theory.modular_forms.jacobi_theta.basic
+! leanprover-community/mathlib commit 57f9349f2fe19d2de7207e99b0341808d977cdcf
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -25,9 +25,9 @@ show that `θ` is differentiable on `ℍ`, and `θ(τ) - 1` has exponential deca
 -/
 
 
-open Complex Real Asymptotics
+open Complex Real Asymptotics Filter
 
-open scoped Real BigOperators UpperHalfPlane Manifold
+open scoped Real BigOperators UpperHalfPlane
 
 /-- Jacobi's theta function `∑' (n : ℤ), exp (π * I * n ^ 2 * τ)`. -/
 noncomputable def jacobiTheta (z : ℂ) : ℂ :=
@@ -168,7 +168,7 @@ theorem norm_jacobiTheta_sub_one_le {z : ℂ} (hz : 0 < im z) :
 
 /-- The norm of `jacobi_theta τ - 1` decays exponentially as `im τ → ∞`. -/
 theorem isBigO_at_im_infty_jacobiTheta_sub_one :
-    IsBigO (Filter.comap im Filter.atTop) (fun τ => jacobiTheta τ - 1) fun τ => rexp (-π * τ.im) :=
+    (fun τ => jacobiTheta τ - 1) =O[comap im atTop] fun τ => rexp (-π * τ.im) :=
   by
   simp_rw [is_O, is_O_with, Filter.eventually_comap, Filter.eventually_atTop]
   refine'
@@ -202,10 +202,6 @@ theorem differentiableAt_jacobiTheta {z : ℂ} (hz : 0 < im z) : DifferentiableA
   exact differentiable_on_tsum_of_summable_norm bd_s h1 h2 fun i w hw => le_bd (le_of_lt hw) i
 #align differentiable_at_jacobi_theta differentiableAt_jacobiTheta
 
-theorem mdifferentiable_jacobiTheta : Mdifferentiable 𝓘(ℂ) 𝓘(ℂ) (jacobiTheta ∘ coe : ℍ → ℂ) :=
-  fun τ => (differentiableAt_jacobiTheta τ.2).MdifferentiableAt.comp τ τ.mdifferentiable_coe
-#align mdifferentiable_jacobi_theta mdifferentiable_jacobiTheta
-
 theorem continuousAt_jacobiTheta {z : ℂ} (hz : 0 < im z) : ContinuousAt jacobiTheta z :=
   (differentiableAt_jacobiTheta hz).ContinuousAt
 #align continuous_at_jacobi_theta continuousAt_jacobiTheta
diff --git a/Mathbin/NumberTheory/ModularForms/JacobiTheta/Manifold.lean b/Mathbin/NumberTheory/ModularForms/JacobiTheta/Manifold.lean
new file mode 100644
index 0000000000..fd0fe69357
--- /dev/null
+++ b/Mathbin/NumberTheory/ModularForms/JacobiTheta/Manifold.lean
@@ -0,0 +1,31 @@
+/-
+Copyright (c) 2023 David Loeffler. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: David Loeffler
+
+! This file was ported from Lean 3 source module number_theory.modular_forms.jacobi_theta.manifold
+! leanprover-community/mathlib commit 57f9349f2fe19d2de7207e99b0341808d977cdcf
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathbin.NumberTheory.ModularForms.JacobiTheta.Basic
+import Mathbin.Analysis.Complex.UpperHalfPlane.Manifold
+
+/-!
+# Manifold differentiability of the Jacobi's theta function
+
+In this file we reformulate differentiability of the Jacobi's theta function in terms of manifold
+differentiability.
+
+## TODO
+
+Prove smoothness (in terms of `smooth`).
+-/
+
+
+open scoped UpperHalfPlane Manifold
+
+theorem mdifferentiable_jacobiTheta : Mdifferentiable 𝓘(ℂ) 𝓘(ℂ) (jacobiTheta ∘ coe : ℍ → ℂ) :=
+  fun τ => (differentiableAt_jacobiTheta τ.2).MdifferentiableAt.comp τ τ.mdifferentiable_coe
+#align mdifferentiable_jacobi_theta mdifferentiable_jacobiTheta
+
diff --git a/Mathbin/NumberTheory/NumberField/Embeddings.lean b/Mathbin/NumberTheory/NumberField/Embeddings.lean
index 97a3c86bd2..d742516c9e 100644
--- a/Mathbin/NumberTheory/NumberField/Embeddings.lean
+++ b/Mathbin/NumberTheory/NumberField/Embeddings.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Alex J. Best, Xavier Roblot
 
 ! This file was ported from Lean 3 source module number_theory.number_field.embeddings
-! leanprover-community/mathlib commit caa58cbf5bfb7f81ccbaca4e8b8ac4bc2b39cc1c
+! leanprover-community/mathlib commit 5d0c76894ada7940957143163d7b921345474cbc
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -16,6 +16,9 @@ import Mathbin.Topology.Instances.Complex
 
 /-!
 # Embeddings of number fields
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
 This file defines the embeddings of a number field into an algebraic closed field.
 
 ## Main Results
diff --git a/Mathbin/NumberTheory/NumberField/Units.lean b/Mathbin/NumberTheory/NumberField/Units.lean
index 7463709709..09abc160e5 100644
--- a/Mathbin/NumberTheory/NumberField/Units.lean
+++ b/Mathbin/NumberTheory/NumberField/Units.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Xavier Roblot
 
 ! This file was ported from Lean 3 source module number_theory.number_field.units
-! leanprover-community/mathlib commit 00f91228655eecdcd3ac97a7fd8dbcb139fe990a
+! leanprover-community/mathlib commit 5d0c76894ada7940957143163d7b921345474cbc
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -12,6 +12,9 @@ import Mathbin.NumberTheory.NumberField.Norm
 
 /-!
 # Units of a number field
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
 We prove results about the group `(𝓞 K)ˣ` of units of the ring of integers `𝓞 K` of a number
 field `K`.
 
diff --git a/Mathbin/NumberTheory/ZetaFunction.lean b/Mathbin/NumberTheory/ZetaFunction.lean
index 4b6cd5f80f..c59d6519eb 100644
--- a/Mathbin/NumberTheory/ZetaFunction.lean
+++ b/Mathbin/NumberTheory/ZetaFunction.lean
@@ -4,12 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: David Loeffler
 
 ! This file was ported from Lean 3 source module number_theory.zeta_function
-! leanprover-community/mathlib commit 81843c08659063f91486be95a617b5e9ec93c9da
+! leanprover-community/mathlib commit 57f9349f2fe19d2de7207e99b0341808d977cdcf
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
 import Mathbin.Analysis.SpecialFunctions.Gamma.Beta
-import Mathbin.NumberTheory.ModularForms.JacobiTheta
+import Mathbin.NumberTheory.ModularForms.JacobiTheta.Basic
 import Mathbin.NumberTheory.ZetaValues
 
 /-!
diff --git a/Mathbin/NumberTheory/Zsqrtd/GaussianInt.lean b/Mathbin/NumberTheory/Zsqrtd/GaussianInt.lean
index 440647deb3..50ab156898 100644
--- a/Mathbin/NumberTheory/Zsqrtd/GaussianInt.lean
+++ b/Mathbin/NumberTheory/Zsqrtd/GaussianInt.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes
 
 ! This file was ported from Lean 3 source module number_theory.zsqrtd.gaussian_int
-! leanprover-community/mathlib commit 5b2fe80501ff327b9109fb09b7cc8c325cd0d7d9
+! leanprover-community/mathlib commit 5d0c76894ada7940957143163d7b921345474cbc
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -15,6 +15,9 @@ import Mathbin.RingTheory.PrincipalIdealDomain
 /-!
 # Gaussian integers
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 The Gaussian integers are complex integer, complex numbers whose real and imaginary parts are both
 integers.
 
diff --git a/Mathbin/RingTheory/DedekindDomain/AdicValuation.lean b/Mathbin/RingTheory/DedekindDomain/AdicValuation.lean
index 347c2dd45c..8087001137 100644
--- a/Mathbin/RingTheory/DedekindDomain/AdicValuation.lean
+++ b/Mathbin/RingTheory/DedekindDomain/AdicValuation.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: María Inés de Frutos-Fernández
 
 ! This file was ported from Lean 3 source module ring_theory.dedekind_domain.adic_valuation
-! leanprover-community/mathlib commit f0c8bf9245297a541f468be517f1bde6195105e9
+! leanprover-community/mathlib commit 5d0c76894ada7940957143163d7b921345474cbc
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -16,6 +16,9 @@ import Mathbin.Algebra.Order.Group.TypeTags
 
 /-!
 # Adic valuations on Dedekind domains
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
 Given a Dedekind domain `R` of Krull dimension 1 and a maximal ideal `v` of `R`, we define the
 `v`-adic valuation on `R` and its extension to the field of fractions `K` of `R`.
 We prove several properties of this valuation, including the existence of uniformizers.
diff --git a/Mathbin/RingTheory/DedekindDomain/FiniteAdeleRing.lean b/Mathbin/RingTheory/DedekindDomain/FiniteAdeleRing.lean
index 229abb27dd..032738f0eb 100644
--- a/Mathbin/RingTheory/DedekindDomain/FiniteAdeleRing.lean
+++ b/Mathbin/RingTheory/DedekindDomain/FiniteAdeleRing.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: María Inés de Frutos-Fernández
 
 ! This file was ported from Lean 3 source module ring_theory.dedekind_domain.finite_adele_ring
-! leanprover-community/mathlib commit f0c8bf9245297a541f468be517f1bde6195105e9
+! leanprover-community/mathlib commit 5d0c76894ada7940957143163d7b921345474cbc
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -12,6 +12,9 @@ import Mathbin.RingTheory.DedekindDomain.AdicValuation
 
 /-!
 # The finite adèle ring of a Dedekind domain
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
 We define the ring of finite adèles of a Dedekind domain `R`.
 
 ## Main definitions
diff --git a/Mathbin/RingTheory/DedekindDomain/SInteger.lean b/Mathbin/RingTheory/DedekindDomain/SInteger.lean
index c8bc82bbac..fa2fd0590a 100644
--- a/Mathbin/RingTheory/DedekindDomain/SInteger.lean
+++ b/Mathbin/RingTheory/DedekindDomain/SInteger.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: David Kurniadi Angdinata
 
 ! This file was ported from Lean 3 source module ring_theory.dedekind_domain.S_integer
-! leanprover-community/mathlib commit 00ab77614e085c9ef49479babba1a7d826d3232e
+! leanprover-community/mathlib commit 5d0c76894ada7940957143163d7b921345474cbc
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -13,6 +13,9 @@ import Mathbin.RingTheory.DedekindDomain.AdicValuation
 /-!
 # `S`-integers and `S`-units of fraction fields of Dedekind domains
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Let `K` be the field of fractions of a Dedekind domain `R`, and let `S` be a set of prime ideals in
 the height one spectrum of `R`. An `S`-integer of `K` is defined to have `v`-adic valuation at most
 one for all primes ideals `v` away from `S`, whereas an `S`-unit of `Kˣ` is defined to have `v`-adic
diff --git a/Mathbin/RingTheory/Discriminant.lean b/Mathbin/RingTheory/Discriminant.lean
index c36b73d74c..7abf20f837 100644
--- a/Mathbin/RingTheory/Discriminant.lean
+++ b/Mathbin/RingTheory/Discriminant.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Riccardo Brasca
 
 ! This file was ported from Lean 3 source module ring_theory.discriminant
-! leanprover-community/mathlib commit 3e068ece210655b7b9a9477c3aff38a492400aa1
+! leanprover-community/mathlib commit 5d0c76894ada7940957143163d7b921345474cbc
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -15,6 +15,9 @@ import Mathbin.NumberTheory.NumberField.Basic
 /-!
 # Discriminant of a family of vectors
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Given an `A`-algebra `B` and `b`, an `ι`-indexed family of elements of `B`, we define the
 *discriminant* of `b` as the determinant of the matrix whose `(i j)`-th element is the trace of
 `b i * b j`.
diff --git a/Mathbin/RingTheory/Ideal/Norm.lean b/Mathbin/RingTheory/Ideal/Norm.lean
index e918e308ae..637411a463 100644
--- a/Mathbin/RingTheory/Ideal/Norm.lean
+++ b/Mathbin/RingTheory/Ideal/Norm.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Anne Baanen, Alex J. Best
 
 ! This file was ported from Lean 3 source module ring_theory.ideal.norm
-! leanprover-community/mathlib commit f0c8bf9245297a541f468be517f1bde6195105e9
+! leanprover-community/mathlib commit 5d0c76894ada7940957143163d7b921345474cbc
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -22,6 +22,9 @@ import Mathbin.RingTheory.Localization.Norm
 
 # Ideal norms
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines the absolute ideal norm `ideal.abs_norm (I : ideal R) : ℕ` as the cardinality of
 the quotient `R ⧸ I` (setting it to 0 if the cardinality is infinite),
 and the relative ideal norm `ideal.span_norm R (I : ideal S) : ideal S` as the ideal spanned by
diff --git a/Mathbin/Topology/MetricSpace/Dilation.lean b/Mathbin/Topology/MetricSpace/Dilation.lean
new file mode 100644
index 0000000000..bef9f1a93e
--- /dev/null
+++ b/Mathbin/Topology/MetricSpace/Dilation.lean
@@ -0,0 +1,499 @@
+/-
+Copyright (c) 2022 Hanting Zhang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Dilations of emetric and metric spaces
+Authors: Hanting Zhang
+
+! This file was ported from Lean 3 source module topology.metric_space.dilation
+! leanprover-community/mathlib commit 93f880918cb51905fd51b76add8273cbc27718ab
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathbin.Topology.MetricSpace.Antilipschitz
+import Mathbin.Data.FunLike.Basic
+
+/-!
+# Dilations
+
+We define dilations, i.e., maps between emetric spaces that satisfy
+`edist (f x) (f y) = r * edist x y` for some `r ∉ {0, ∞}`.
+
+The value `r = 0` is not allowed because we want dilations of (e)metric spaces to be automatically
+injective. The value `r = ∞` is not allowed because this way we can define `dilation.ratio f : ℝ≥0`,
+not `dilation.ratio f : ℝ≥0∞`. Also, we do not often need maps sending distinct points to points at
+infinite distance.
+
+## Main defintions
+
+* `dilation.ratio f : ℝ≥0`: the value of `r` in the relation above, defaulting to 1 in the case
+  where it is not well-defined.
+
+## Implementation notes
+
+The type of dilations defined in this file are also referred to as "similarities" or "similitudes"
+by other authors. The name `dilation` was choosen to match the Wikipedia name.
+
+Since a lot of elementary properties don't require `eq_of_dist_eq_zero` we start setting up the
+theory for `pseudo_emetric_space` and we specialize to `pseudo_metric_space` and `metric_space` when
+needed.
+
+## TODO
+
+- Introduce dilation equivs.
+- Refactor the `isometry` API to match the `*_hom_class` API below.
+
+## References
+
+- https://en.wikipedia.org/wiki/Dilation_(metric_space)
+- [Marcel Berger, *Geometry*][berger1987]
+-/
+
+
+noncomputable section
+
+open Function Set
+
+open scoped Topology ENNReal NNReal Classical
+
+section Defs
+
+variable (α : Type _) (β : Type _) [PseudoEMetricSpace α] [PseudoEMetricSpace β]
+
+/-- A dilation is a map that uniformly scales the edistance between any two points.  -/
+structure Dilation where
+  toFun : α → β
+  edist_eq' : ∃ r : ℝ≥0, r ≠ 0 ∧ ∀ x y : α, edist (to_fun x) (to_fun y) = r * edist x y
+#align dilation Dilation
+
+/-- `dilation_class F α β r` states that `F` is a type of `r`-dilations.
+You should extend this typeclass when you extend `dilation`.
+-/
+class DilationClass (F : Type _) (α β : outParam <| Type _) [PseudoEMetricSpace α]
+    [PseudoEMetricSpace β] extends FunLike F α fun _ => β where
+  edist_eq' : ∀ f : F, ∃ r : ℝ≥0, r ≠ 0 ∧ ∀ x y : α, edist (f x) (f y) = r * edist x y
+#align dilation_class DilationClass
+
+end Defs
+
+namespace Dilation
+
+variable {α : Type _} {β : Type _} {γ : Type _} {F : Type _} {G : Type _}
+
+section Setup
+
+variable [PseudoEMetricSpace α] [PseudoEMetricSpace β]
+
+instance toDilationClass : DilationClass (Dilation α β) α β
+    where
+  coe := toFun
+  coe_injective' f g h := by cases f <;> cases g <;> congr
+  edist_eq' f := edist_eq' f
+#align dilation.to_dilation_class Dilation.toDilationClass
+
+instance : CoeFun (Dilation α β) fun _ => α → β :=
+  FunLike.hasCoeToFun
+
+@[simp]
+theorem toFun_eq_coe {f : Dilation α β} : f.toFun = (f : α → β) :=
+  rfl
+#align dilation.to_fun_eq_coe Dilation.toFun_eq_coe
+
+@[simp]
+theorem coe_mk (f : α → β) (h) : ⇑(⟨f, h⟩ : Dilation α β) = f :=
+  rfl
+#align dilation.coe_mk Dilation.coe_mk
+
+theorem congr_fun {f g : Dilation α β} (h : f = g) (x : α) : f x = g x :=
+  FunLike.congr_fun h x
+#align dilation.congr_fun Dilation.congr_fun
+
+theorem congr_arg (f : Dilation α β) {x y : α} (h : x = y) : f x = f y :=
+  FunLike.congr_arg f h
+#align dilation.congr_arg Dilation.congr_arg
+
+@[ext]
+theorem ext {f g : Dilation α β} (h : ∀ x, f x = g x) : f = g :=
+  FunLike.ext f g h
+#align dilation.ext Dilation.ext
+
+theorem ext_iff {f g : Dilation α β} : f = g ↔ ∀ x, f x = g x :=
+  FunLike.ext_iff
+#align dilation.ext_iff Dilation.ext_iff
+
+@[simp]
+theorem mk_coe (f : Dilation α β) (h) : Dilation.mk f h = f :=
+  ext fun _ => rfl
+#align dilation.mk_coe Dilation.mk_coe
+
+/-- Copy of a `dilation` with a new `to_fun` equal to the old one. Useful to fix definitional
+equalities. -/
+@[simps (config := { fullyApplied := false })]
+protected def copy (f : Dilation α β) (f' : α → β) (h : f' = ⇑f) : Dilation α β
+    where
+  toFun := f'
+  edist_eq' := h.symm ▸ f.edist_eq'
+#align dilation.copy Dilation.copy
+
+theorem copy_eq_self (f : Dilation α β) {f' : α → β} (h : f' = f) : f.copy f' h = f :=
+  FunLike.ext' h
+#align dilation.copy_eq_self Dilation.copy_eq_self
+
+/-- The ratio of a dilation `f`. If the ratio is undefined (i.e., the distance between any two
+points in `α` is either zero or infinity), then we choose one as the ratio. -/
+def ratio [DilationClass F α β] (f : F) : ℝ≥0 :=
+  if ∀ x y : α, edist x y = 0 ∨ edist x y = ⊤ then 1 else (DilationClass.edist_eq' f).some
+#align dilation.ratio Dilation.ratio
+
+theorem ratio_ne_zero [DilationClass F α β] (f : F) : ratio f ≠ 0 :=
+  by
+  rw [ratio]; split_ifs
+  · exact one_ne_zero
+  exact (DilationClass.edist_eq' f).choose_spec.1
+#align dilation.ratio_ne_zero Dilation.ratio_ne_zero
+
+theorem ratio_pos [DilationClass F α β] (f : F) : 0 < ratio f :=
+  (ratio_ne_zero f).bot_lt
+#align dilation.ratio_pos Dilation.ratio_pos
+
+@[simp]
+theorem edist_eq [DilationClass F α β] (f : F) (x y : α) :
+    edist (f x) (f y) = ratio f * edist x y :=
+  by
+  rw [ratio]; split_ifs with key
+  · rcases DilationClass.edist_eq' f with ⟨r, hne, hr⟩
+    replace hr := hr x y
+    cases key x y
+    · simp only [hr, h, MulZeroClass.mul_zero]
+    · simp [hr, h, hne]
+  exact (DilationClass.edist_eq' f).choose_spec.2 x y
+#align dilation.edist_eq Dilation.edist_eq
+
+@[simp]
+theorem nndist_eq {α β F : Type _} [PseudoMetricSpace α] [PseudoMetricSpace β] [DilationClass F α β]
+    (f : F) (x y : α) : nndist (f x) (f y) = ratio f * nndist x y := by
+  simp only [← ENNReal.coe_eq_coe, ← edist_nndist, ENNReal.coe_mul, edist_eq]
+#align dilation.nndist_eq Dilation.nndist_eq
+
+@[simp]
+theorem dist_eq {α β F : Type _} [PseudoMetricSpace α] [PseudoMetricSpace β] [DilationClass F α β]
+    (f : F) (x y : α) : dist (f x) (f y) = ratio f * dist x y := by
+  simp only [dist_nndist, nndist_eq, NNReal.coe_mul]
+#align dilation.dist_eq Dilation.dist_eq
+
+/-- The `ratio` is equal to the distance ratio for any two points with nonzero finite distance.
+`dist` and `nndist` versions below -/
+theorem ratio_unique [DilationClass F α β] {f : F} {x y : α} {r : ℝ≥0} (h₀ : edist x y ≠ 0)
+    (htop : edist x y ≠ ⊤) (hr : edist (f x) (f y) = r * edist x y) : r = ratio f := by
+  simpa only [hr, ENNReal.mul_eq_mul_right h₀ htop, ENNReal.coe_eq_coe] using edist_eq f x y
+#align dilation.ratio_unique Dilation.ratio_unique
+
+/-- The `ratio` is equal to the distance ratio for any two points
+with nonzero finite distance; `nndist` version -/
+theorem ratio_unique_of_nndist_ne_zero {α β F : Type _} [PseudoMetricSpace α] [PseudoMetricSpace β]
+    [DilationClass F α β] {f : F} {x y : α} {r : ℝ≥0} (hxy : nndist x y ≠ 0)
+    (hr : nndist (f x) (f y) = r * nndist x y) : r = ratio f :=
+  ratio_unique (by rwa [edist_nndist, ENNReal.coe_ne_zero]) (edist_ne_top x y)
+    (by rw [edist_nndist, edist_nndist, hr, ENNReal.coe_mul])
+#align dilation.ratio_unique_of_nndist_ne_zero Dilation.ratio_unique_of_nndist_ne_zero
+
+/-- The `ratio` is equal to the distance ratio for any two points
+with nonzero finite distance; `dist` version -/
+theorem ratio_unique_of_dist_ne_zero {α β} {F : Type _} [PseudoMetricSpace α] [PseudoMetricSpace β]
+    [DilationClass F α β] {f : F} {x y : α} {r : ℝ≥0} (hxy : dist x y ≠ 0)
+    (hr : dist (f x) (f y) = r * dist x y) : r = ratio f :=
+  ratio_unique_of_nndist_ne_zero (NNReal.coe_ne_zero.1 hxy) <|
+    NNReal.eq <| by rw [coe_nndist, hr, NNReal.coe_mul, coe_nndist]
+#align dilation.ratio_unique_of_dist_ne_zero Dilation.ratio_unique_of_dist_ne_zero
+
+/-- Alternative `dilation` constructor when the distance hypothesis is over `nndist` -/
+def mkOfNndistEq {α β} [PseudoMetricSpace α] [PseudoMetricSpace β] (f : α → β)
+    (h : ∃ r : ℝ≥0, r ≠ 0 ∧ ∀ x y : α, nndist (f x) (f y) = r * nndist x y) : Dilation α β
+    where
+  toFun := f
+  edist_eq' := by
+    rcases h with ⟨r, hne, h⟩
+    refine' ⟨r, hne, fun x y => _⟩
+    rw [edist_nndist, edist_nndist, ← ENNReal.coe_mul, h x y]
+#align dilation.mk_of_nndist_eq Dilation.mkOfNndistEq
+
+@[simp]
+theorem coe_mkOfNndistEq {α β} [PseudoMetricSpace α] [PseudoMetricSpace β] (f : α → β) (h) :
+    ⇑(mkOfNndistEq f h : Dilation α β) = f :=
+  rfl
+#align dilation.coe_mk_of_nndist_eq Dilation.coe_mkOfNndistEq
+
+@[simp]
+theorem mk_coe_of_nndist_eq {α β} [PseudoMetricSpace α] [PseudoMetricSpace β] (f : Dilation α β)
+    (h) : Dilation.mkOfNndistEq f h = f :=
+  ext fun _ => rfl
+#align dilation.mk_coe_of_nndist_eq Dilation.mk_coe_of_nndist_eq
+
+/-- Alternative `dilation` constructor when the distance hypothesis is over `dist` -/
+def mkOfDistEq {α β} [PseudoMetricSpace α] [PseudoMetricSpace β] (f : α → β)
+    (h : ∃ r : ℝ≥0, r ≠ 0 ∧ ∀ x y : α, dist (f x) (f y) = r * dist x y) : Dilation α β :=
+  mkOfNndistEq f <|
+    h.imp fun r hr =>
+      ⟨hr.1, fun x y => NNReal.eq <| by rw [coe_nndist, hr.2, NNReal.coe_mul, coe_nndist]⟩
+#align dilation.mk_of_dist_eq Dilation.mkOfDistEq
+
+@[simp]
+theorem coe_mkOfDistEq {α β} [PseudoMetricSpace α] [PseudoMetricSpace β] (f : α → β) (h) :
+    ⇑(mkOfDistEq f h : Dilation α β) = f :=
+  rfl
+#align dilation.coe_mk_of_dist_eq Dilation.coe_mkOfDistEq
+
+@[simp]
+theorem mk_coe_of_dist_eq {α β} [PseudoMetricSpace α] [PseudoMetricSpace β] (f : Dilation α β) (h) :
+    Dilation.mkOfDistEq f h = f :=
+  ext fun _ => rfl
+#align dilation.mk_coe_of_dist_eq Dilation.mk_coe_of_dist_eq
+
+end Setup
+
+section PseudoEmetricDilation
+
+variable [PseudoEMetricSpace α] [PseudoEMetricSpace β] [PseudoEMetricSpace γ]
+
+variable [DilationClass F α β] [DilationClass G β γ]
+
+variable (f : F) (g : G) {x y z : α} {s : Set α}
+
+theorem lipschitz : LipschitzWith (ratio f) (f : α → β) := fun x y => (edist_eq f x y).le
+#align dilation.lipschitz Dilation.lipschitz
+
+theorem antilipschitz : AntilipschitzWith (ratio f)⁻¹ (f : α → β) := fun x y =>
+  by
+  have hr : ratio f ≠ 0 := ratio_ne_zero f
+  exact_mod_cast
+    (ENNReal.mul_le_iff_le_inv (ENNReal.coe_ne_zero.2 hr) ENNReal.coe_ne_top).1 (edist_eq f x y).ge
+#align dilation.antilipschitz Dilation.antilipschitz
+
+/-- A dilation from an emetric space is injective -/
+protected theorem injective {α : Type _} [EMetricSpace α] [DilationClass F α β] (f : F) :
+    Injective f :=
+  (antilipschitz f).Injective
+#align dilation.injective Dilation.injective
+
+/-- The identity is a dilation -/
+protected def id (α) [PseudoEMetricSpace α] : Dilation α α
+    where
+  toFun := id
+  edist_eq' := ⟨1, one_ne_zero, fun x y => by simp only [id.def, ENNReal.coe_one, one_mul]⟩
+#align dilation.id Dilation.id
+
+instance : Inhabited (Dilation α α) :=
+  ⟨Dilation.id α⟩
+
+@[simp, protected]
+theorem coe_id : ⇑(Dilation.id α) = id :=
+  rfl
+#align dilation.coe_id Dilation.coe_id
+
+theorem id_ratio : ratio (Dilation.id α) = 1 :=
+  by
+  by_cases h : ∀ x y : α, edist x y = 0 ∨ edist x y = ∞
+  · rw [ratio, if_pos h]
+  · push_neg at h 
+    rcases h with ⟨x, y, hne⟩
+    refine' (ratio_unique hne.1 hne.2 _).symm
+    simp
+#align dilation.id_ratio Dilation.id_ratio
+
+/-- The composition of dilations is a dilation -/
+def comp (g : Dilation β γ) (f : Dilation α β) : Dilation α γ
+    where
+  toFun := g ∘ f
+  edist_eq' :=
+    ⟨ratio g * ratio f, mul_ne_zero (ratio_ne_zero g) (ratio_ne_zero f), fun x y => by
+      simp only [edist_eq, ENNReal.coe_mul]; ring⟩
+#align dilation.comp Dilation.comp
+
+theorem comp_assoc {δ : Type _} [PseudoEMetricSpace δ] (f : Dilation α β) (g : Dilation β γ)
+    (h : Dilation γ δ) : (h.comp g).comp f = h.comp (g.comp f) :=
+  rfl
+#align dilation.comp_assoc Dilation.comp_assoc
+
+@[simp]
+theorem coe_comp (g : Dilation β γ) (f : Dilation α β) : (g.comp f : α → γ) = g ∘ f :=
+  rfl
+#align dilation.coe_comp Dilation.coe_comp
+
+theorem comp_apply (g : Dilation β γ) (f : Dilation α β) (x : α) : (g.comp f : α → γ) x = g (f x) :=
+  rfl
+#align dilation.comp_apply Dilation.comp_apply
+
+/-- Ratio of the composition `g.comp f` of two dilations is the product of their ratios. We assume
+that the domain `α` of `f` is nontrivial, otherwise `ratio f = ratio (g.comp f) = 1` but `ratio g`
+may have any value. -/
+@[simp]
+theorem comp_ratio {g : Dilation β γ} {f : Dilation α β}
+    (hne : ∃ x y : α, edist x y ≠ 0 ∧ edist x y ≠ ⊤) : ratio (g.comp f) = ratio g * ratio f :=
+  by
+  rcases hne with ⟨x, y, hα⟩
+  have hgf := (edist_eq (g.comp f) x y).symm
+  simp only [dist_eq, coe_comp, ← mul_assoc, mul_eq_mul_right_iff] at hgf 
+  rw [edist_eq, edist_eq, ← mul_assoc, ENNReal.mul_eq_mul_right hα.1 hα.2] at hgf 
+  rwa [← ENNReal.coe_eq_coe, ENNReal.coe_mul]
+#align dilation.comp_ratio Dilation.comp_ratio
+
+@[simp]
+theorem comp_id (f : Dilation α β) : f.comp (Dilation.id α) = f :=
+  ext fun x => rfl
+#align dilation.comp_id Dilation.comp_id
+
+@[simp]
+theorem id_comp (f : Dilation α β) : (Dilation.id β).comp f = f :=
+  ext fun x => rfl
+#align dilation.id_comp Dilation.id_comp
+
+instance : Monoid (Dilation α α) where
+  one := Dilation.id α
+  mul := comp
+  mul_one := comp_id
+  one_mul := id_comp
+  mul_assoc f g h := comp_assoc _ _ _
+
+theorem one_def : (1 : Dilation α α) = Dilation.id α :=
+  rfl
+#align dilation.one_def Dilation.one_def
+
+theorem mul_def (f g : Dilation α α) : f * g = f.comp g :=
+  rfl
+#align dilation.mul_def Dilation.mul_def
+
+@[simp]
+theorem coe_one : ⇑(1 : Dilation α α) = id :=
+  rfl
+#align dilation.coe_one Dilation.coe_one
+
+@[simp]
+theorem coe_mul (f g : Dilation α α) : ⇑(f * g) = f ∘ g :=
+  rfl
+#align dilation.coe_mul Dilation.coe_mul
+
+theorem cancel_right {g₁ g₂ : Dilation β γ} {f : Dilation α β} (hf : Surjective f) :
+    g₁.comp f = g₂.comp f ↔ g₁ = g₂ :=
+  ⟨fun h => Dilation.ext <| hf.forall.2 (ext_iff.1 h), fun h => h ▸ rfl⟩
+#align dilation.cancel_right Dilation.cancel_right
+
+theorem cancel_left {g : Dilation β γ} {f₁ f₂ : Dilation α β} (hg : Injective g) :
+    g.comp f₁ = g.comp f₂ ↔ f₁ = f₂ :=
+  ⟨fun h => Dilation.ext fun x => hg <| by rw [← comp_apply, h, comp_apply], fun h => h ▸ rfl⟩
+#align dilation.cancel_left Dilation.cancel_left
+
+/-- A dilation from a metric space is a uniform inducing map -/
+protected theorem uniformInducing : UniformInducing (f : α → β) :=
+  (antilipschitz f).UniformInducing (lipschitz f).UniformContinuous
+#align dilation.uniform_inducing Dilation.uniformInducing
+
+theorem tendsto_nhds_iff {ι : Type _} {g : ι → α} {a : Filter ι} {b : α} :
+    Filter.Tendsto g a (𝓝 b) ↔ Filter.Tendsto ((f : α → β) ∘ g) a (𝓝 (f b)) :=
+  (Dilation.uniformInducing f).Inducing.tendsto_nhds_iff
+#align dilation.tendsto_nhds_iff Dilation.tendsto_nhds_iff
+
+/-- A dilation is continuous. -/
+theorem to_continuous : Continuous (f : α → β) :=
+  (lipschitz f).Continuous
+#align dilation.to_continuous Dilation.to_continuous
+
+/-- Dilations scale the diameter by `ratio f` in pseudoemetric spaces. -/
+theorem ediam_image (s : Set α) : EMetric.diam ((f : α → β) '' s) = ratio f * EMetric.diam s :=
+  by
+  refine' ((lipschitz f).ediam_image_le s).antisymm _
+  apply ENNReal.mul_le_of_le_div'
+  rw [div_eq_mul_inv, mul_comm, ← ENNReal.coe_inv]
+  exacts [(antilipschitz f).le_mul_ediam_image s, ratio_ne_zero f]
+#align dilation.ediam_image Dilation.ediam_image
+
+/-- A dilation scales the diameter of the range by `ratio f`. -/
+theorem ediam_range : EMetric.diam (range (f : α → β)) = ratio f * EMetric.diam (univ : Set α) := by
+  rw [← image_univ]; exact ediam_image f univ
+#align dilation.ediam_range Dilation.ediam_range
+
+/-- A dilation maps balls to balls and scales the radius by `ratio f`. -/
+theorem mapsTo_emetric_ball (x : α) (r : ℝ≥0∞) :
+    MapsTo (f : α → β) (EMetric.ball x r) (EMetric.ball (f x) (ratio f * r)) := fun y hy =>
+  (edist_eq f y x).trans_lt <|
+    (ENNReal.mul_lt_mul_left (ENNReal.coe_ne_zero.2 <| ratio_ne_zero f) ENNReal.coe_ne_top).2 hy
+#align dilation.maps_to_emetric_ball Dilation.mapsTo_emetric_ball
+
+/-- A dilation maps closed balls to closed balls and scales the radius by `ratio f`. -/
+theorem mapsTo_emetric_closedBall (x : α) (r' : ℝ≥0∞) :
+    MapsTo (f : α → β) (EMetric.closedBall x r') (EMetric.closedBall (f x) (ratio f * r')) :=
+  fun y hy => (edist_eq f y x).trans_le <| mul_le_mul_left' hy _
+#align dilation.maps_to_emetric_closed_ball Dilation.mapsTo_emetric_closedBall
+
+theorem comp_continuousOn_iff {γ} [TopologicalSpace γ] {g : γ → α} {s : Set γ} :
+    ContinuousOn ((f : α → β) ∘ g) s ↔ ContinuousOn g s :=
+  (Dilation.uniformInducing f).Inducing.continuousOn_iff.symm
+#align dilation.comp_continuous_on_iff Dilation.comp_continuousOn_iff
+
+theorem comp_continuous_iff {γ} [TopologicalSpace γ] {g : γ → α} :
+    Continuous ((f : α → β) ∘ g) ↔ Continuous g :=
+  (Dilation.uniformInducing f).Inducing.continuous_iff.symm
+#align dilation.comp_continuous_iff Dilation.comp_continuous_iff
+
+end PseudoEmetricDilation
+
+--section
+section EmetricDilation
+
+variable [EMetricSpace α]
+
+/-- A dilation from a metric space is a uniform embedding -/
+protected theorem uniformEmbedding [PseudoEMetricSpace β] [DilationClass F α β] (f : F) :
+    UniformEmbedding f :=
+  (antilipschitz f).UniformEmbedding (lipschitz f).UniformContinuous
+#align dilation.uniform_embedding Dilation.uniformEmbedding
+
+/-- A dilation from a metric space is an embedding -/
+protected theorem embedding [PseudoEMetricSpace β] [DilationClass F α β] (f : F) :
+    Embedding (f : α → β) :=
+  (Dilation.uniformEmbedding f).Embedding
+#align dilation.embedding Dilation.embedding
+
+/-- A dilation from a complete emetric space is a closed embedding -/
+protected theorem closedEmbedding [CompleteSpace α] [EMetricSpace β] [DilationClass F α β] (f : F) :
+    ClosedEmbedding f :=
+  (antilipschitz f).ClosedEmbedding (lipschitz f).UniformContinuous
+#align dilation.closed_embedding Dilation.closedEmbedding
+
+end EmetricDilation
+
+--section
+section PseudoMetricDilation
+
+variable [PseudoMetricSpace α] [PseudoMetricSpace β] [DilationClass F α β] (f : F)
+
+/-- A dilation scales the diameter by `ratio f` in pseudometric spaces. -/
+theorem diam_image (s : Set α) : Metric.diam ((f : α → β) '' s) = ratio f * Metric.diam s := by
+  simp [Metric.diam, ediam_image, ENNReal.toReal_mul]
+#align dilation.diam_image Dilation.diam_image
+
+theorem diam_range : Metric.diam (range (f : α → β)) = ratio f * Metric.diam (univ : Set α) := by
+  rw [← image_univ, diam_image]
+#align dilation.diam_range Dilation.diam_range
+
+/-- A dilation maps balls to balls and scales the radius by `ratio f`. -/
+theorem mapsTo_ball (x : α) (r' : ℝ) :
+    MapsTo (f : α → β) (Metric.ball x r') (Metric.ball (f x) (ratio f * r')) := fun y hy =>
+  (dist_eq f y x).trans_lt <| (mul_lt_mul_left <| NNReal.coe_pos.2 <| ratio_pos f).2 hy
+#align dilation.maps_to_ball Dilation.mapsTo_ball
+
+/-- A dilation maps spheres to spheres and scales the radius by `ratio f`. -/
+theorem mapsTo_sphere (x : α) (r' : ℝ) :
+    MapsTo (f : α → β) (Metric.sphere x r') (Metric.sphere (f x) (ratio f * r')) := fun y hy =>
+  Metric.mem_sphere.mp hy ▸ dist_eq f y x
+#align dilation.maps_to_sphere Dilation.mapsTo_sphere
+
+/-- A dilation maps closed balls to closed balls and scales the radius by `ratio f`. -/
+theorem mapsTo_closedBall (x : α) (r' : ℝ) :
+    MapsTo (f : α → β) (Metric.closedBall x r') (Metric.closedBall (f x) (ratio f * r')) :=
+  fun y hy => (dist_eq f y x).trans_le <| mul_le_mul_of_nonneg_left hy (NNReal.coe_nonneg _)
+#align dilation.maps_to_closed_ball Dilation.mapsTo_closedBall
+
+end PseudoMetricDilation
+
+-- section
+end Dilation
+
diff --git a/README.md b/README.md
index e68835142c..b83966d420 100644
--- a/README.md
+++ b/README.md
@@ -1,4 +1,4 @@
-Tracking mathlib commit: [`d30d31261cdb4d2f5e612eabc3c4bf45556350d5`](https://github.com/leanprover-community/mathlib/commit/d30d31261cdb4d2f5e612eabc3c4bf45556350d5)
+Tracking mathlib commit: [`93f880918cb51905fd51b76add8273cbc27718ab`](https://github.com/leanprover-community/mathlib/commit/93f880918cb51905fd51b76add8273cbc27718ab)
 
 You should use this repository to inspect the Lean 4 files that `mathport` has generated from mathlib3.
 Please run `lake build` first, to download a copy of the generated `.olean` files.
diff --git a/lake-manifest.json b/lake-manifest.json
index 3f35e9c13c..978fb48aba 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -10,15 +10,15 @@
   {"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "4aeeeacae219002275eac747dbff5fb7be023ef4",
+    "rev": "820a550d4e0a21bfb76e9dac322ac7618a393eaf",
     "name": "lean3port",
-    "inputRev?": "4aeeeacae219002275eac747dbff5fb7be023ef4"}},
+    "inputRev?": "820a550d4e0a21bfb76e9dac322ac7618a393eaf"}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "08077c3330913e903d9e2cc34b4ad6242b71c891",
+    "rev": "21ebfc78e19fd960961d247c0a80f2d8d0e57957",
     "name": "mathlib",
-    "inputRev?": "08077c3330913e903d9e2cc34b4ad6242b71c891"}},
+    "inputRev?": "21ebfc78e19fd960961d247c0a80f2d8d0e57957"}},
   {"git":
    {"url": "https://github.com/gebner/quote4",
     "subDir?": null,
diff --git a/lakefile.lean b/lakefile.lean
index 18fab74a67..ff1cdcad49 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -4,7 +4,7 @@ open Lake DSL System
 -- Usually the `tag` will be of the form `nightly-2021-11-22`.
 -- If you would like to use an artifact from a PR build,
 -- it will be of the form `pr-branchname-sha`.
-def tag : String := "nightly-2023-06-24-01"
+def tag : String := "nightly-2023-06-24-03"
 def releaseRepo : String := "leanprover-community/mathport"
 def oleanTarName : String := "mathlib3-binport.tar.gz"
 
@@ -38,7 +38,7 @@ target fetchOleans (_pkg : Package) : Unit := do
     untarReleaseArtifact releaseRepo tag oleanTarName libDir
   return .nil
 
-require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"4aeeeacae219002275eac747dbff5fb7be023ef4"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"820a550d4e0a21bfb76e9dac322ac7618a393eaf"
 
 @[default_target]
 lean_lib Mathbin where
diff --git a/upstream-rev b/upstream-rev
index 523920b0d7..0615fdf4e6 100644
--- a/upstream-rev
+++ b/upstream-rev
@@ -1 +1 @@
-d30d31261cdb4d2f5e612eabc3c4bf45556350d5
+93f880918cb51905fd51b76add8273cbc27718ab