diff --git a/Mathbin/Algebra/Algebra/Spectrum.lean b/Mathbin/Algebra/Algebra/Spectrum.lean
index 7716a172d3..f4770cceb9 100644
--- a/Mathbin/Algebra/Algebra/Spectrum.lean
+++ b/Mathbin/Algebra/Algebra/Spectrum.lean
@@ -4,13 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jireh Loreaux
 
 ! This file was ported from Lean 3 source module algebra.algebra.spectrum
-! leanprover-community/mathlib commit 11dcb6b59dc9cc74e053b7ca8569bf6df4ac0f1e
+! leanprover-community/mathlib commit 58a272265b5e05f258161260dd2c5d247213cbd3
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
 import Mathbin.Algebra.Star.Pointwise
 import Mathbin.Algebra.Star.Subalgebra
-import Mathbin.FieldTheory.IsAlgClosed.Basic
 import Mathbin.Tactic.NoncommRing
 
 /-!
@@ -36,8 +35,6 @@ This theory will serve as the foundation for spectral theory in Banach algebras.
   units (of `R`) in `σ (a*b)` coincide with those in `σ (b*a)`.
 * `spectrum.scalar_eq`: in a nontrivial algebra over a field, the spectrum of a scalar is
   a singleton.
-* `spectrum.subset_polynomial_aeval`, `spectrum.map_polynomial_aeval_of_degree_pos`,
-  `spectrum.map_polynomial_aeval_of_nonempty`: variations on the spectral mapping theorem.
 
 ## Notations
 
@@ -100,8 +97,6 @@ end Defs
 
 namespace spectrum
 
-open scoped Polynomial
-
 section ScalarSemiring
 
 variable {R : Type u} {A : Type v}
@@ -224,8 +219,6 @@ theorem smul_mem_smul_iff {a : A} {s : R} {r : Rˣ} : r • s ∈ σ (r • a) 
     isUnit_smul_iff]
 #align spectrum.smul_mem_smul_iff spectrum.smul_mem_smul_iff
 
-open scoped Polynomial
-
 theorem unit_smul_eq_smul (a : A) (r : Rˣ) : σ (r • a) = r • σ a :=
   by
   ext
@@ -333,20 +326,6 @@ theorem sub_singleton_eq (a : A) (r : R) : σ a - {r} = σ (a - ↑ₐ r) := by
   simpa only [neg_sub, neg_eq] using congr_arg Neg.neg (singleton_sub_eq a r)
 #align spectrum.sub_singleton_eq spectrum.sub_singleton_eq
 
-open Polynomial
-
-theorem exists_mem_of_not_isUnit_aeval_prod [IsDomain R] {p : R[X]} {a : A} (hp : p ≠ 0)
-    (h : ¬IsUnit (aeval a (Multiset.map (fun x : R => X - C x) p.roots).Prod)) :
-    ∃ k : R, k ∈ σ a ∧ eval k p = 0 :=
-  by
-  rw [← Multiset.prod_toList, AlgHom.map_list_prod] at h 
-  replace h := mt List.prod_isUnit h
-  simp only [not_forall, exists_prop, aeval_C, Multiset.mem_toList, List.mem_map, aeval_X,
-    exists_exists_and_eq_and, Multiset.mem_map, AlgHom.map_sub] at h 
-  rcases h with ⟨r, r_mem, r_nu⟩
-  exact ⟨r, by rwa [mem_iff, ← IsUnit.sub_iff], by rwa [← is_root.def, ← mem_roots hp]⟩
-#align spectrum.exists_mem_of_not_is_unit_aeval_prod spectrum.exists_mem_of_not_isUnit_aeval_prod
-
 end ScalarRing
 
 section ScalarField
@@ -416,97 +395,6 @@ protected theorem map_inv (a : Aˣ) : (σ (a : A))⁻¹ = σ (↑a⁻¹ : A) :=
     simpa only [Units.val_inv_eq_inv_val] using inv_mem_iff.mp hk
 #align spectrum.map_inv spectrum.map_inv
 
-open Polynomial
-
-/-- Half of the spectral mapping theorem for polynomials. We prove it separately
-because it holds over any field, whereas `spectrum.map_polynomial_aeval_of_degree_pos` and
-`spectrum.map_polynomial_aeval_of_nonempty` need the field to be algebraically closed. -/
-theorem subset_polynomial_aeval (a : A) (p : 𝕜[X]) : (fun k => eval k p) '' σ a ⊆ σ (aeval a p) :=
-  by
-  rintro _ ⟨k, hk, rfl⟩
-  let q := C (eval k p) - p
-  have hroot : is_root q k := by simp only [eval_C, eval_sub, sub_self, is_root.def]
-  rw [← mul_div_eq_iff_is_root, ← neg_mul_neg, neg_sub] at hroot 
-  have aeval_q_eq : ↑ₐ (eval k p) - aeval a p = aeval a q := by
-    simp only [aeval_C, AlgHom.map_sub, sub_left_inj]
-  rw [mem_iff, aeval_q_eq, ← hroot, aeval_mul]
-  have hcomm := (Commute.all (C k - X) (-(q / (X - C k)))).map (aeval a)
-  apply mt fun h => (hcomm.is_unit_mul_iff.mp h).1
-  simpa only [aeval_X, aeval_C, AlgHom.map_sub] using hk
-#align spectrum.subset_polynomial_aeval spectrum.subset_polynomial_aeval
-
-/-- The *spectral mapping theorem* for polynomials.  Note: the assumption `degree p > 0`
-is necessary in case `σ a = ∅`, for then the left-hand side is `∅` and the right-hand side,
-assuming `[nontrivial A]`, is `{k}` where `p = polynomial.C k`. -/
-theorem map_polynomial_aeval_of_degree_pos [IsAlgClosed 𝕜] (a : A) (p : 𝕜[X])
-    (hdeg : 0 < degree p) : σ (aeval a p) = (fun k => eval k p) '' σ a :=
-  by
-  -- handle the easy direction via `spectrum.subset_polynomial_aeval`
-  refine' Set.eq_of_subset_of_subset (fun k hk => _) (subset_polynomial_aeval a p)
-  -- write `C k - p` product of linear factors and a constant; show `C k - p ≠ 0`.
-  have hprod := eq_prod_roots_of_splits_id (IsAlgClosed.splits (C k - p))
-  have h_ne : C k - p ≠ 0 :=
-    ne_zero_of_degree_gt
-      (by rwa [degree_sub_eq_right_of_degree_lt (lt_of_le_of_lt degree_C_le hdeg)])
-  have lead_ne := leading_coeff_ne_zero.mpr h_ne
-  have lead_unit := (Units.map ↑ₐ.toMonoidHom (Units.mk0 _ lead_ne)).IsUnit
-  /- leading coefficient is a unit so product of linear factors is not a unit;
-    apply `exists_mem_of_not_is_unit_aeval_prod`. -/
-  have p_a_eq : aeval a (C k - p) = ↑ₐ k - aeval a p := by
-    simp only [aeval_C, AlgHom.map_sub, sub_left_inj]
-  rw [mem_iff, ← p_a_eq, hprod, aeval_mul, ((Commute.all _ _).map (aeval a)).isUnit_mul_iff,
-    aeval_C] at hk 
-  replace hk := exists_mem_of_not_is_unit_aeval_prod h_ne (not_and.mp hk lead_unit)
-  rcases hk with ⟨r, r_mem, r_ev⟩
-  exact ⟨r, r_mem, symm (by simpa [eval_sub, eval_C, sub_eq_zero] using r_ev)⟩
-#align spectrum.map_polynomial_aeval_of_degree_pos spectrum.map_polynomial_aeval_of_degree_pos
-
-/-- In this version of the spectral mapping theorem, we assume the spectrum
-is nonempty instead of assuming the degree of the polynomial is positive. -/
-theorem map_polynomial_aeval_of_nonempty [IsAlgClosed 𝕜] (a : A) (p : 𝕜[X])
-    (hnon : (σ a).Nonempty) : σ (aeval a p) = (fun k => eval k p) '' σ a :=
-  by
-  nontriviality A
-  refine' Or.elim (le_or_gt (degree p) 0) (fun h => _) (map_polynomial_aeval_of_degree_pos a p)
-  · rw [eq_C_of_degree_le_zero h]
-    simp only [Set.image_congr, eval_C, aeval_C, scalar_eq, Set.Nonempty.image_const hnon]
-#align spectrum.map_polynomial_aeval_of_nonempty spectrum.map_polynomial_aeval_of_nonempty
-
-/-- A specialization of `spectrum.subset_polynomial_aeval` to monic monomials for convenience. -/
-theorem pow_image_subset (a : A) (n : ℕ) : (fun x => x ^ n) '' σ a ⊆ σ (a ^ n) := by
-  simpa only [eval_pow, eval_X, aeval_X_pow] using subset_polynomial_aeval a (X ^ n : 𝕜[X])
-#align spectrum.pow_image_subset spectrum.pow_image_subset
-
-/-- A specialization of `spectrum.map_polynomial_aeval_of_nonempty` to monic monomials for
-convenience. -/
-theorem map_pow_of_pos [IsAlgClosed 𝕜] (a : A) {n : ℕ} (hn : 0 < n) :
-    σ (a ^ n) = (fun x => x ^ n) '' σ a := by
-  simpa only [aeval_X_pow, eval_pow, eval_X] using
-    map_polynomial_aeval_of_degree_pos a (X ^ n : 𝕜[X]) (by rw_mod_cast [degree_X_pow]; exact hn)
-#align spectrum.map_pow_of_pos spectrum.map_pow_of_pos
-
-/-- A specialization of `spectrum.map_polynomial_aeval_of_nonempty` to monic monomials for
-convenience. -/
-theorem map_pow_of_nonempty [IsAlgClosed 𝕜] {a : A} (ha : (σ a).Nonempty) (n : ℕ) :
-    σ (a ^ n) = (fun x => x ^ n) '' σ a := by
-  simpa only [aeval_X_pow, eval_pow, eval_X] using map_polynomial_aeval_of_nonempty a (X ^ n) ha
-#align spectrum.map_pow_of_nonempty spectrum.map_pow_of_nonempty
-
-variable (𝕜)
-
--- We will use this both to show eigenvalues exist, and to prove Schur's lemma.
-/-- Every element `a` in a nontrivial finite-dimensional algebra `A`
-over an algebraically closed field `𝕜` has non-empty spectrum. -/
-theorem nonempty_of_isAlgClosed_of_finiteDimensional [IsAlgClosed 𝕜] [Nontrivial A]
-    [I : FiniteDimensional 𝕜 A] (a : A) : ∃ k : 𝕜, k ∈ σ a :=
-  by
-  obtain ⟨p, ⟨h_mon, h_eval_p⟩⟩ := isIntegral_of_noetherian (IsNoetherian.iff_fg.2 I) a
-  have nu : ¬IsUnit (aeval a p) := by rw [← aeval_def] at h_eval_p ; rw [h_eval_p]; simp
-  rw [eq_prod_roots_of_monic_of_splits_id h_mon (IsAlgClosed.splits p)] at nu 
-  obtain ⟨k, hk, _⟩ := exists_mem_of_not_is_unit_aeval_prod (monic.ne_zero h_mon) nu
-  exact ⟨k, hk⟩
-#align spectrum.nonempty_of_is_alg_closed_of_finite_dimensional spectrum.nonempty_of_isAlgClosed_of_finiteDimensional
-
 end ScalarField
 
 end spectrum
@@ -515,7 +403,7 @@ namespace AlgHom
 
 section CommSemiring
 
-variable {F R A B : Type _} [CommRing R] [Ring A] [Algebra R A] [Ring B] [Algebra R B]
+variable {F R A B : Type _} [CommSemiring R] [Ring A] [Algebra R A] [Ring B] [Algebra R B]
 
 variable [AlgHomClass F R A B]
 
diff --git a/Mathbin/Algebra/Category/Module/Monoidal/Symmetric.lean b/Mathbin/Algebra/Category/Module/Monoidal/Symmetric.lean
index 6a40360a01..4fb14f3e24 100644
--- a/Mathbin/Algebra/Category/Module/Monoidal/Symmetric.lean
+++ b/Mathbin/Algebra/Category/Module/Monoidal/Symmetric.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kevin Buzzard, Scott Morrison, Jakob von Raumer
 
 ! This file was ported from Lean 3 source module algebra.category.Module.monoidal.symmetric
-! leanprover-community/mathlib commit 74403a3b2551b0970855e14ef5e8fd0d6af1bfc2
+! leanprover-community/mathlib commit 36938f775671ff28bea1c0310f1608e4afbb22e0
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -13,6 +13,9 @@ import Mathbin.Algebra.Category.Module.Monoidal.Basic
 
 /-!
 # The symmetric monoidal structure on `Module R`.
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
 -/
 
 
diff --git a/Mathbin/Algebra/Lie/BaseChange.lean b/Mathbin/Algebra/Lie/BaseChange.lean
index 52baeed9a6..7e952a1ea9 100644
--- a/Mathbin/Algebra/Lie/BaseChange.lean
+++ b/Mathbin/Algebra/Lie/BaseChange.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Oliver Nash
 
 ! This file was ported from Lean 3 source module algebra.lie.base_change
-! leanprover-community/mathlib commit 9264b15ee696b7ca83f13c8ad67c83d6eb70b730
+! leanprover-community/mathlib commit 36938f775671ff28bea1c0310f1608e4afbb22e0
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -14,6 +14,9 @@ import Mathbin.Algebra.Lie.TensorProduct
 /-!
 # Extension and restriction of scalars for Lie algebras
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Lie algebras have a well-behaved theory of extension and restriction of scalars.
 
 ## Main definitions
diff --git a/Mathbin/Algebra/Lie/Character.lean b/Mathbin/Algebra/Lie/Character.lean
index a6dcffc51a..3778539c8d 100644
--- a/Mathbin/Algebra/Lie/Character.lean
+++ b/Mathbin/Algebra/Lie/Character.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Oliver Nash
 
 ! This file was ported from Lean 3 source module algebra.lie.character
-! leanprover-community/mathlib commit 132328c4dd48da87adca5d408ca54f315282b719
+! leanprover-community/mathlib commit 36938f775671ff28bea1c0310f1608e4afbb22e0
 ! 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.Dual
 /-!
 # Characters of Lie algebras
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 A character of a Lie algebra `L` over a commutative ring `R` is a morphism of Lie algebras `L → R`,
 where `R` is regarded as a Lie algebra over itself via the ring commutator. For an Abelian Lie
 algebra (e.g., a Cartan subalgebra of a semisimple Lie algebra) a character is just a linear form.
diff --git a/Mathbin/Algebra/Lie/DirectSum.lean b/Mathbin/Algebra/Lie/DirectSum.lean
index a7a5f437f1..72819a64ec 100644
--- a/Mathbin/Algebra/Lie/DirectSum.lean
+++ b/Mathbin/Algebra/Lie/DirectSum.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Oliver Nash
 
 ! This file was ported from Lean 3 source module algebra.lie.direct_sum
-! leanprover-community/mathlib commit c0cc689babd41c0e9d5f02429211ffbe2403472a
+! leanprover-community/mathlib commit 36938f775671ff28bea1c0310f1608e4afbb22e0
 ! 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.Lie.Basic
 /-!
 # Direct sums of Lie algebras and Lie modules
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Direct sums of Lie algebras and Lie modules carry natural algebra and module structures.
 
 ## Tags
diff --git a/Mathbin/Algebra/Lie/Semisimple.lean b/Mathbin/Algebra/Lie/Semisimple.lean
index ec3bcc985c..f32f0e4c6d 100644
--- a/Mathbin/Algebra/Lie/Semisimple.lean
+++ b/Mathbin/Algebra/Lie/Semisimple.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Oliver Nash
 
 ! This file was ported from Lean 3 source module algebra.lie.semisimple
-! leanprover-community/mathlib commit 356447fe00e75e54777321045cdff7c9ea212e60
+! leanprover-community/mathlib commit 36938f775671ff28bea1c0310f1608e4afbb22e0
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -13,6 +13,9 @@ import Mathbin.Algebra.Lie.Solvable
 /-!
 # Semisimple Lie algebras
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 The famous Cartan-Dynkin-Killing classification of semisimple Lie algebras renders them one of the
 most important classes of Lie algebras. In this file we define simple and semisimple Lie algebras
 and prove some basic related results.
diff --git a/Mathbin/Algebra/Lie/SkewAdjoint.lean b/Mathbin/Algebra/Lie/SkewAdjoint.lean
index 9bb89e032a..e191dee583 100644
--- a/Mathbin/Algebra/Lie/SkewAdjoint.lean
+++ b/Mathbin/Algebra/Lie/SkewAdjoint.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Oliver Nash
 
 ! This file was ported from Lean 3 source module algebra.lie.skew_adjoint
-! leanprover-community/mathlib commit 075b3f7d19b9da85a0b54b3e33055a74fc388dec
+! leanprover-community/mathlib commit 36938f775671ff28bea1c0310f1608e4afbb22e0
 ! 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.Matrix.BilinearForm
 /-!
 # Lie algebras of skew-adjoint endomorphisms of a bilinear form
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 When a module carries a bilinear form, the Lie algebra of endomorphisms of the module contains a
 distinguished Lie subalgebra: the skew-adjoint endomorphisms. Such subalgebras are important
 because they provide a simple, explicit construction of the so-called classical Lie algebras.
diff --git a/Mathbin/Algebra/Lie/Solvable.lean b/Mathbin/Algebra/Lie/Solvable.lean
index 606fe78151..bf9dab3d06 100644
--- a/Mathbin/Algebra/Lie/Solvable.lean
+++ b/Mathbin/Algebra/Lie/Solvable.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Oliver Nash
 
 ! This file was ported from Lean 3 source module algebra.lie.solvable
-! leanprover-community/mathlib commit a50170a88a47570ed186b809ca754110590f9476
+! leanprover-community/mathlib commit 36938f775671ff28bea1c0310f1608e4afbb22e0
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -15,6 +15,9 @@ import Mathbin.Order.Hom.Basic
 /-!
 # Solvable Lie algebras
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Like groups, Lie algebras admit a natural concept of solvability. We define this here via the
 derived series and prove some related results. We also define the radical of a Lie algebra and
 prove that it is solvable when the Lie algebra is Noetherian.
diff --git a/Mathbin/Algebra/Module/DedekindDomain.lean b/Mathbin/Algebra/Module/DedekindDomain.lean
index ab2421641a..bef6adf690 100644
--- a/Mathbin/Algebra/Module/DedekindDomain.lean
+++ b/Mathbin/Algebra/Module/DedekindDomain.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Pierre-Alexandre Bazin
 
 ! This file was ported from Lean 3 source module algebra.module.dedekind_domain
-! leanprover-community/mathlib commit cdc34484a07418af43daf8198beaf5c00324bca8
+! leanprover-community/mathlib commit 36938f775671ff28bea1c0310f1608e4afbb22e0
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -14,6 +14,9 @@ import Mathbin.RingTheory.DedekindDomain.Ideal
 /-!
 # Modules over a Dedekind domain
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Over a Dedekind domain, a `I`-torsion module is the internal direct sum of its `p i ^ e i`-torsion
 submodules, where `I = ∏ i, p i ^ e i` is its unique decomposition in prime ideals.
 Therefore, as any finitely generated torsion module is `I`-torsion for some `I`, it is an internal
diff --git a/Mathbin/Algebra/Symmetrized.lean b/Mathbin/Algebra/Symmetrized.lean
index 91458bdb7a..b2db3cc688 100644
--- a/Mathbin/Algebra/Symmetrized.lean
+++ b/Mathbin/Algebra/Symmetrized.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Christopher Hoskin
 
 ! This file was ported from Lean 3 source module algebra.symmetrized
-! leanprover-community/mathlib commit 933547832736be61a5de6576e22db351c6c2fbfd
+! leanprover-community/mathlib commit 36938f775671ff28bea1c0310f1608e4afbb22e0
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -14,6 +14,9 @@ import Mathbin.Algebra.Module.Basic
 /-!
 # Symmetrized algebra
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 A commutative multiplication on a real or complex space can be constructed from any multiplication
 by "symmetrization" i.e
 $$
diff --git a/Mathbin/All.lean b/Mathbin/All.lean
index 8abeaea529..60a438e2c7 100644
--- a/Mathbin/All.lean
+++ b/Mathbin/All.lean
@@ -1807,6 +1807,7 @@ import Mathbin.FieldTheory.IntermediateField
 import Mathbin.FieldTheory.IsAlgClosed.AlgebraicClosure
 import Mathbin.FieldTheory.IsAlgClosed.Basic
 import Mathbin.FieldTheory.IsAlgClosed.Classification
+import Mathbin.FieldTheory.IsAlgClosed.Spectrum
 import Mathbin.FieldTheory.KrullTopology
 import Mathbin.FieldTheory.Laurent
 import Mathbin.FieldTheory.Minpoly.Basic
diff --git a/Mathbin/Analysis/BoxIntegral/Partition/Measure.lean b/Mathbin/Analysis/BoxIntegral/Partition/Measure.lean
index 7d0b4c2e02..05ddca2bf3 100644
--- a/Mathbin/Analysis/BoxIntegral/Partition/Measure.lean
+++ b/Mathbin/Analysis/BoxIntegral/Partition/Measure.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.box_integral.partition.measure
-! leanprover-community/mathlib commit fd5edc43dc4f10b85abfe544b88f82cf13c5f844
+! leanprover-community/mathlib commit 36938f775671ff28bea1c0310f1608e4afbb22e0
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -14,6 +14,9 @@ import Mathbin.MeasureTheory.Measure.Lebesgue.Basic
 /-!
 # Box-additive functions defined by measures
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we prove a few simple facts about rectangular boxes, partitions, and measures:
 
 - given a box `I : box ι`, its coercion to `set (ι → ℝ)` and `I.Icc` are measurable sets;
diff --git a/Mathbin/Analysis/Calculus/FderivAnalytic.lean b/Mathbin/Analysis/Calculus/FderivAnalytic.lean
index 4f21934014..dad31b3c39 100644
--- a/Mathbin/Analysis/Calculus/FderivAnalytic.lean
+++ b/Mathbin/Analysis/Calculus/FderivAnalytic.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.fderiv_analytic
-! leanprover-community/mathlib commit 3bce8d800a6f2b8f63fe1e588fd76a9ff4adcebe
+! leanprover-community/mathlib commit 36938f775671ff28bea1c0310f1608e4afbb22e0
 ! 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.Calculus.ContDiffDef
 /-!
 # Frechet derivatives of analytic functions.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 A function expressible as a power series at a point has a Frechet derivative there.
 Also the special case in terms of `deriv` when the domain is 1-dimensional.
 -/
diff --git a/Mathbin/Analysis/Calculus/Series.lean b/Mathbin/Analysis/Calculus/Series.lean
index 459591c065..35cd582f22 100644
--- a/Mathbin/Analysis/Calculus/Series.lean
+++ b/Mathbin/Analysis/Calculus/Series.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel
 
 ! This file was ported from Lean 3 source module analysis.calculus.series
-! leanprover-community/mathlib commit f2ce6086713c78a7f880485f7917ea547a215982
+! leanprover-community/mathlib commit 36938f775671ff28bea1c0310f1608e4afbb22e0
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -15,6 +15,9 @@ import Mathbin.Data.Nat.Cast.WithTop
 /-!
 # Smoothness of series
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We show that series of functions are continuous, or differentiable, or smooth, when each individual
 function in the series is and additionally suitable uniform summable bounds are satisfied.
 
diff --git a/Mathbin/Analysis/InnerProductSpace/Calculus.lean b/Mathbin/Analysis/InnerProductSpace/Calculus.lean
index a65d0794a4..a519b85987 100644
--- a/Mathbin/Analysis/InnerProductSpace/Calculus.lean
+++ b/Mathbin/Analysis/InnerProductSpace/Calculus.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.inner_product_space.calculus
-! leanprover-community/mathlib commit f9dd3204df14a0749cd456fac1e6849dfe7d2b88
+! leanprover-community/mathlib commit 36938f775671ff28bea1c0310f1608e4afbb22e0
 ! 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.SpecialFunctions.Sqrt
 /-!
 # Calculus in inner product spaces
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we prove that the inner product and square of the norm in an inner space are
 infinitely `ℝ`-smooth. In order to state these results, we need a `normed_space ℝ E`
 instance. Though we can deduce this structure from `inner_product_space 𝕜 E`, this instance may be
diff --git a/Mathbin/Analysis/InnerProductSpace/EuclideanDist.lean b/Mathbin/Analysis/InnerProductSpace/EuclideanDist.lean
index 08ec66415b..7480cbcafc 100644
--- a/Mathbin/Analysis/InnerProductSpace/EuclideanDist.lean
+++ b/Mathbin/Analysis/InnerProductSpace/EuclideanDist.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.inner_product_space.euclidean_dist
-! leanprover-community/mathlib commit 9425b6f8220e53b059f5a4904786c3c4b50fc057
+! leanprover-community/mathlib commit 36938f775671ff28bea1c0310f1608e4afbb22e0
 ! 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.InnerProductSpace.PiL2
 /-!
 # Euclidean distance on a finite dimensional space
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 When we define a smooth bump function on a normed space, it is useful to have a smooth distance on
 the space. Since the default distance is not guaranteed to be smooth, we define `to_euclidean` to be
 an equivalence between a finite dimensional topological vector space and the standard Euclidean
diff --git a/Mathbin/Analysis/NormedSpace/Spectrum.lean b/Mathbin/Analysis/NormedSpace/Spectrum.lean
index 91d6bffc6e..e6b1454f4d 100644
--- a/Mathbin/Analysis/NormedSpace/Spectrum.lean
+++ b/Mathbin/Analysis/NormedSpace/Spectrum.lean
@@ -4,11 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jireh Loreaux
 
 ! This file was ported from Lean 3 source module analysis.normed_space.spectrum
-! leanprover-community/mathlib commit 0b9eaaa7686280fad8cce467f5c3c57ee6ce77f8
+! leanprover-community/mathlib commit 58a272265b5e05f258161260dd2c5d247213cbd3
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
-import Mathbin.Algebra.Algebra.Spectrum
+import Mathbin.FieldTheory.IsAlgClosed.Spectrum
 import Mathbin.Analysis.Complex.Liouville
 import Mathbin.Analysis.Complex.Polynomial
 import Mathbin.Analysis.Analytic.RadiusLiminf
diff --git a/Mathbin/Analysis/ODE/Gronwall.lean b/Mathbin/Analysis/ODE/Gronwall.lean
index 512a4cb386..e3d501262d 100644
--- a/Mathbin/Analysis/ODE/Gronwall.lean
+++ b/Mathbin/Analysis/ODE/Gronwall.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.ODE.gronwall
-! leanprover-community/mathlib commit f2ce6086713c78a7f880485f7917ea547a215982
+! leanprover-community/mathlib commit 36938f775671ff28bea1c0310f1608e4afbb22e0
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -13,6 +13,9 @@ import Mathbin.Analysis.SpecialFunctions.ExpDeriv
 /-!
 # Grönwall's inequality
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 The main technical result of this file is the Grönwall-like inequality
 `norm_le_gronwall_bound_of_norm_deriv_right_le`. It states that if `f : ℝ → E` satisfies `‖f a‖ ≤ δ`
 and `∀ x ∈ [a, b), ‖f' x‖ ≤ K * ‖f x‖ + ε`, then for all `x ∈ [a, b]` we have `‖f x‖ ≤ δ * exp (K *
diff --git a/Mathbin/Analysis/SpecialFunctions/Arsinh.lean b/Mathbin/Analysis/SpecialFunctions/Arsinh.lean
index 6f590a9913..fb4af27518 100644
--- a/Mathbin/Analysis/SpecialFunctions/Arsinh.lean
+++ b/Mathbin/Analysis/SpecialFunctions/Arsinh.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: James Arthur, Chris Hughes, Shing Tak Lam
 
 ! This file was ported from Lean 3 source module analysis.special_functions.arsinh
-! leanprover-community/mathlib commit f2ce6086713c78a7f880485f7917ea547a215982
+! leanprover-community/mathlib commit 36938f775671ff28bea1c0310f1608e4afbb22e0
 ! 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.SpecialFunctions.Log.Basic
 /-!
 # Inverse of the sinh function
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we prove that sinh is bijective and hence has an
 inverse, arsinh.
 
diff --git a/Mathbin/Analysis/SpecialFunctions/Bernstein.lean b/Mathbin/Analysis/SpecialFunctions/Bernstein.lean
index bb5478d6e1..32d6dc6fee 100644
--- a/Mathbin/Analysis/SpecialFunctions/Bernstein.lean
+++ b/Mathbin/Analysis/SpecialFunctions/Bernstein.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 
 ! This file was ported from Lean 3 source module analysis.special_functions.bernstein
-! leanprover-community/mathlib commit 2c1d8ca2812b64f88992a5294ea3dba144755cd1
+! leanprover-community/mathlib commit 36938f775671ff28bea1c0310f1608e4afbb22e0
 ! 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.ContinuousFunction.Compact
 /-!
 # Bernstein approximations and Weierstrass' theorem
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We prove that the Bernstein approximations
 ```
 ∑ k : fin (n+1), f (k/n : ℝ) * n.choose k * x^k * (1-x)^(n-k)
diff --git a/Mathbin/Analysis/SpecialFunctions/CompareExp.lean b/Mathbin/Analysis/SpecialFunctions/CompareExp.lean
index 2148060657..ae91676af8 100644
--- a/Mathbin/Analysis/SpecialFunctions/CompareExp.lean
+++ b/Mathbin/Analysis/SpecialFunctions/CompareExp.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.special_functions.compare_exp
-! leanprover-community/mathlib commit 0b9eaaa7686280fad8cce467f5c3c57ee6ce77f8
+! leanprover-community/mathlib commit 36938f775671ff28bea1c0310f1608e4afbb22e0
 ! 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.Asymptotics.SpecificAsymptotics
 /-!
 # Growth estimates on `x ^ y` for complex `x`, `y`
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Let `l` be a filter on `ℂ` such that `complex.re` tends to infinity along `l` and `complex.im z`
 grows at a subexponential rate compared to `complex.re z`. Then
 
diff --git a/Mathbin/Analysis/SpecialFunctions/Complex/LogDeriv.lean b/Mathbin/Analysis/SpecialFunctions/Complex/LogDeriv.lean
index 2061d3c0af..c51e02342f 100644
--- a/Mathbin/Analysis/SpecialFunctions/Complex/LogDeriv.lean
+++ b/Mathbin/Analysis/SpecialFunctions/Complex/LogDeriv.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Abhimanyu Pallavi Sudhir, Jean Lo, Calle Sönne, Benjamin Davidson
 
 ! This file was ported from Lean 3 source module analysis.special_functions.complex.log_deriv
-! leanprover-community/mathlib commit 6a5c85000ab93fe5dcfdf620676f614ba8e18c26
+! leanprover-community/mathlib commit 36938f775671ff28bea1c0310f1608e4afbb22e0
 ! 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.SpecialFunctions.ExpDeriv
 /-!
 # Differentiability of the complex `log` function
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 -/
 
 
diff --git a/Mathbin/Analysis/SpecialFunctions/Log/Deriv.lean b/Mathbin/Analysis/SpecialFunctions/Log/Deriv.lean
index e7a4efb825..39cbb2adee 100644
--- a/Mathbin/Analysis/SpecialFunctions/Log/Deriv.lean
+++ b/Mathbin/Analysis/SpecialFunctions/Log/Deriv.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Abhimanyu Pallavi Sudhir, Jean Lo, Calle Sönne
 
 ! This file was ported from Lean 3 source module analysis.special_functions.log.deriv
-! leanprover-community/mathlib commit 3bce8d800a6f2b8f63fe1e588fd76a9ff4adcebe
+! leanprover-community/mathlib commit 36938f775671ff28bea1c0310f1608e4afbb22e0
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -16,6 +16,9 @@ import Mathbin.Analysis.SpecialFunctions.ExpDeriv
 /-!
 # Derivative and series expansion of real logarithm
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we prove that `real.log` is infinitely smooth at all nonzero `x : ℝ`. We also prove
 that the series `∑' n : ℕ, x ^ (n + 1) / (n + 1)` converges to `(-real.log (1 - x))` for all
 `x : ℝ`, `|x| < 1`.
diff --git a/Mathbin/Analysis/SpecialFunctions/Trigonometric/ArctanDeriv.lean b/Mathbin/Analysis/SpecialFunctions/Trigonometric/ArctanDeriv.lean
index 81f20367c7..e67e3401bf 100644
--- a/Mathbin/Analysis/SpecialFunctions/Trigonometric/ArctanDeriv.lean
+++ b/Mathbin/Analysis/SpecialFunctions/Trigonometric/ArctanDeriv.lean
@@ -97,25 +97,31 @@ theorem hasDerivAt_arctan (x : ℝ) : HasDerivAt arctan (1 / (1 + x ^ 2)) x :=
   (hasStrictDerivAt_arctan x).HasDerivAt
 #align real.has_deriv_at_arctan Real.hasDerivAt_arctan
 
+#print Real.differentiableAt_arctan /-
 theorem differentiableAt_arctan (x : ℝ) : DifferentiableAt ℝ arctan x :=
   (hasDerivAt_arctan x).DifferentiableAt
 #align real.differentiable_at_arctan Real.differentiableAt_arctan
+-/
 
+#print Real.differentiable_arctan /-
 theorem differentiable_arctan : Differentiable ℝ arctan :=
   differentiableAt_arctan
 #align real.differentiable_arctan Real.differentiable_arctan
+-/
 
 @[simp]
 theorem deriv_arctan : deriv arctan = fun x => 1 / (1 + x ^ 2) :=
   funext fun x => (hasDerivAt_arctan x).deriv
 #align real.deriv_arctan Real.deriv_arctan
 
+#print Real.contDiff_arctan /-
 theorem contDiff_arctan {n : ℕ∞} : ContDiff ℝ n arctan :=
   contDiff_iff_contDiffAt.2 fun x =>
     have : cos (arctan x) ≠ 0 := (cos_arctan_pos x).ne'
     tanLocalHomeomorph.contDiffAt_symm_deriv (by simpa) trivial (hasDerivAt_tan this)
       (contDiffAt_tan.2 this)
 #align real.cont_diff_arctan Real.contDiff_arctan
+-/
 
 end Real
 
@@ -193,42 +199,58 @@ theorem fderiv_arctan (hc : DifferentiableAt ℝ f x) :
   hc.HasFDerivAt.arctan.fderiv
 #align fderiv_arctan fderiv_arctan
 
+#print DifferentiableWithinAt.arctan /-
 theorem DifferentiableWithinAt.arctan (hf : DifferentiableWithinAt ℝ f s x) :
     DifferentiableWithinAt ℝ (fun x => Real.arctan (f x)) s x :=
   hf.HasFDerivWithinAt.arctan.DifferentiableWithinAt
 #align differentiable_within_at.arctan DifferentiableWithinAt.arctan
+-/
 
+#print DifferentiableAt.arctan /-
 @[simp]
 theorem DifferentiableAt.arctan (hc : DifferentiableAt ℝ f x) :
     DifferentiableAt ℝ (fun x => arctan (f x)) x :=
   hc.HasFDerivAt.arctan.DifferentiableAt
 #align differentiable_at.arctan DifferentiableAt.arctan
+-/
 
+#print DifferentiableOn.arctan /-
 theorem DifferentiableOn.arctan (hc : DifferentiableOn ℝ f s) :
     DifferentiableOn ℝ (fun x => arctan (f x)) s := fun x h => (hc x h).arctan
 #align differentiable_on.arctan DifferentiableOn.arctan
+-/
 
+#print Differentiable.arctan /-
 @[simp]
 theorem Differentiable.arctan (hc : Differentiable ℝ f) : Differentiable ℝ fun x => arctan (f x) :=
   fun x => (hc x).arctan
 #align differentiable.arctan Differentiable.arctan
+-/
 
+#print ContDiffAt.arctan /-
 theorem ContDiffAt.arctan (h : ContDiffAt ℝ n f x) : ContDiffAt ℝ n (fun x => arctan (f x)) x :=
   contDiff_arctan.ContDiffAt.comp x h
 #align cont_diff_at.arctan ContDiffAt.arctan
+-/
 
+#print ContDiff.arctan /-
 theorem ContDiff.arctan (h : ContDiff ℝ n f) : ContDiff ℝ n fun x => arctan (f x) :=
   contDiff_arctan.comp h
 #align cont_diff.arctan ContDiff.arctan
+-/
 
+#print ContDiffWithinAt.arctan /-
 theorem ContDiffWithinAt.arctan (h : ContDiffWithinAt ℝ n f s x) :
     ContDiffWithinAt ℝ n (fun x => arctan (f x)) s x :=
   contDiff_arctan.comp_contDiffWithinAt h
 #align cont_diff_within_at.arctan ContDiffWithinAt.arctan
+-/
 
+#print ContDiffOn.arctan /-
 theorem ContDiffOn.arctan (h : ContDiffOn ℝ n f s) : ContDiffOn ℝ n (fun x => arctan (f x)) s :=
   contDiff_arctan.comp_contDiffOn h
 #align cont_diff_on.arctan ContDiffOn.arctan
+-/
 
 end fderiv
 
diff --git a/Mathbin/Analysis/SpecialFunctions/Trigonometric/Deriv.lean b/Mathbin/Analysis/SpecialFunctions/Trigonometric/Deriv.lean
index 419fe4f1f0..3193b2b327 100644
--- a/Mathbin/Analysis/SpecialFunctions/Trigonometric/Deriv.lean
+++ b/Mathbin/Analysis/SpecialFunctions/Trigonometric/Deriv.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Abhimanyu Pallavi Sudhir, Jean Lo, Calle Sönne, Benjamin Davidson
 
 ! This file was ported from Lean 3 source module analysis.special_functions.trigonometric.deriv
-! leanprover-community/mathlib commit 2c1d8ca2812b64f88992a5294ea3dba144755cd1
+! leanprover-community/mathlib commit 36938f775671ff28bea1c0310f1608e4afbb22e0
 ! 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.SpecialFunctions.Trigonometric.Basic
 /-!
 # Differentiability of trigonometric functions
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 ## Main statements
 
 The differentiability of the usual trigonometric functions is proved, and their derivatives are
diff --git a/Mathbin/Analysis/SpecialFunctions/Trigonometric/InverseDeriv.lean b/Mathbin/Analysis/SpecialFunctions/Trigonometric/InverseDeriv.lean
index 36c7436ae3..51420a862a 100644
--- a/Mathbin/Analysis/SpecialFunctions/Trigonometric/InverseDeriv.lean
+++ b/Mathbin/Analysis/SpecialFunctions/Trigonometric/InverseDeriv.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Abhimanyu Pallavi Sudhir, Jean Lo, Calle Sönne, Benjamin Davidson
 
 ! This file was ported from Lean 3 source module analysis.special_functions.trigonometric.inverse_deriv
-! leanprover-community/mathlib commit f2ce6086713c78a7f880485f7917ea547a215982
+! leanprover-community/mathlib commit 36938f775671ff28bea1c0310f1608e4afbb22e0
 ! 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.SpecialFunctions.Trigonometric.Deriv
 /-!
 # derivatives of the inverse trigonometric functions
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Derivatives of `arcsin` and `arccos`.
 -/
 
diff --git a/Mathbin/CategoryTheory/Bicategory/NaturalTransformation.lean b/Mathbin/CategoryTheory/Bicategory/NaturalTransformation.lean
index a620068913..f76f6817f3 100644
--- a/Mathbin/CategoryTheory/Bicategory/NaturalTransformation.lean
+++ b/Mathbin/CategoryTheory/Bicategory/NaturalTransformation.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yuma Mizuno
 
 ! This file was ported from Lean 3 source module category_theory.bicategory.natural_transformation
-! leanprover-community/mathlib commit 4ff75f5b8502275a4c2eb2d2f02bdf84d7fb8993
+! leanprover-community/mathlib commit 36938f775671ff28bea1c0310f1608e4afbb22e0
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -13,6 +13,9 @@ import Mathbin.CategoryTheory.Bicategory.Functor
 /-!
 # Oplax natural transformations
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Just as there are natural transformations between functors, there are oplax natural transformations
 between oplax functors. The equality in the naturality of natural transformations is replaced by a
 specified 2-morphism `F.map f ≫ app b ⟶ app a ≫ G.map f` in the case of oplax natural
diff --git a/Mathbin/CategoryTheory/Monoidal/OfChosenFiniteProducts/Symmetric.lean b/Mathbin/CategoryTheory/Monoidal/OfChosenFiniteProducts/Symmetric.lean
index 8d4ce31c60..31c4b3f06e 100644
--- a/Mathbin/CategoryTheory/Monoidal/OfChosenFiniteProducts/Symmetric.lean
+++ b/Mathbin/CategoryTheory/Monoidal/OfChosenFiniteProducts/Symmetric.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison, Simon Hudon
 
 ! This file was ported from Lean 3 source module category_theory.monoidal.of_chosen_finite_products.symmetric
-! leanprover-community/mathlib commit 95a87616d63b3cb49d3fe678d416fbe9c4217bf4
+! leanprover-community/mathlib commit 36938f775671ff28bea1c0310f1608e4afbb22e0
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -14,6 +14,9 @@ import Mathbin.CategoryTheory.Monoidal.OfChosenFiniteProducts.Basic
 /-!
 # The symmetric monoidal structure on a category with chosen finite products.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 -/
 
 
diff --git a/Mathbin/CategoryTheory/Monoidal/Rigid/FunctorCategory.lean b/Mathbin/CategoryTheory/Monoidal/Rigid/FunctorCategory.lean
index f2de48139a..cf49d7498f 100644
--- a/Mathbin/CategoryTheory/Monoidal/Rigid/FunctorCategory.lean
+++ b/Mathbin/CategoryTheory/Monoidal/Rigid/FunctorCategory.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 
 ! This file was ported from Lean 3 source module category_theory.monoidal.rigid.functor_category
-! leanprover-community/mathlib commit a6275694804455fe8995bd530e86b67ddab5cff1
+! leanprover-community/mathlib commit 36938f775671ff28bea1c0310f1608e4afbb22e0
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -14,6 +14,9 @@ import Mathbin.CategoryTheory.Monoidal.FunctorCategory
 /-!
 # Functors from a groupoid into a right/left rigid category form a right/left rigid category.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 (Using the pointwise monoidal structure on the functor category.)
 -/
 
diff --git a/Mathbin/CategoryTheory/Monoidal/Rigid/OfEquivalence.lean b/Mathbin/CategoryTheory/Monoidal/Rigid/OfEquivalence.lean
index e71ea8c716..57735a87aa 100644
--- a/Mathbin/CategoryTheory/Monoidal/Rigid/OfEquivalence.lean
+++ b/Mathbin/CategoryTheory/Monoidal/Rigid/OfEquivalence.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 
 ! This file was ported from Lean 3 source module category_theory.monoidal.rigid.of_equivalence
-! leanprover-community/mathlib commit a6275694804455fe8995bd530e86b67ddab5cff1
+! leanprover-community/mathlib commit 36938f775671ff28bea1c0310f1608e4afbb22e0
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -12,6 +12,9 @@ import Mathbin.CategoryTheory.Monoidal.Rigid.Basic
 
 /-!
 # Transport rigid structures over a monoidal equivalence.
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
 -/
 
 
diff --git a/Mathbin/CategoryTheory/Monoidal/Types/Symmetric.lean b/Mathbin/CategoryTheory/Monoidal/Types/Symmetric.lean
index 505442d7b3..a9247c63e6 100644
--- a/Mathbin/CategoryTheory/Monoidal/Types/Symmetric.lean
+++ b/Mathbin/CategoryTheory/Monoidal/Types/Symmetric.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Michael Jendrusch, Scott Morrison
 
 ! This file was ported from Lean 3 source module category_theory.monoidal.types.symmetric
-! leanprover-community/mathlib commit 95a87616d63b3cb49d3fe678d416fbe9c4217bf4
+! leanprover-community/mathlib commit 36938f775671ff28bea1c0310f1608e4afbb22e0
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -13,6 +13,9 @@ import Mathbin.CategoryTheory.Monoidal.Types.Basic
 
 /-!
 # The category of types is a symmetric monoidal category
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
 -/
 
 
diff --git a/Mathbin/CategoryTheory/Preadditive/Schur.lean b/Mathbin/CategoryTheory/Preadditive/Schur.lean
index 1e68c1c493..f4795d28ca 100644
--- a/Mathbin/CategoryTheory/Preadditive/Schur.lean
+++ b/Mathbin/CategoryTheory/Preadditive/Schur.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus Himmel, Scott Morrison
 
 ! This file was ported from Lean 3 source module category_theory.preadditive.schur
-! leanprover-community/mathlib commit 5ec62c8106221a3f9160e4e4fcc3eed79fe213e9
+! leanprover-community/mathlib commit 58a272265b5e05f258161260dd2c5d247213cbd3
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -12,7 +12,7 @@ import Mathbin.Algebra.Group.Ext
 import Mathbin.CategoryTheory.Simple
 import Mathbin.CategoryTheory.Linear.Basic
 import Mathbin.CategoryTheory.Endomorphism
-import Mathbin.Algebra.Algebra.Spectrum
+import Mathbin.FieldTheory.IsAlgClosed.Spectrum
 
 /-!
 # Schur's lemma
diff --git a/Mathbin/CategoryTheory/Sites/Canonical.lean b/Mathbin/CategoryTheory/Sites/Canonical.lean
index f3a9f284b3..1b10c6e247 100644
--- a/Mathbin/CategoryTheory/Sites/Canonical.lean
+++ b/Mathbin/CategoryTheory/Sites/Canonical.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Bhavik Mehta
 
 ! This file was ported from Lean 3 source module category_theory.sites.canonical
-! leanprover-community/mathlib commit 9e7c80f638149bfb3504ba8ff48dfdbfc949fb1a
+! leanprover-community/mathlib commit 36938f775671ff28bea1c0310f1608e4afbb22e0
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -13,6 +13,9 @@ import Mathbin.CategoryTheory.Sites.SheafOfTypes
 /-!
 # The canonical topology on a category
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We define the finest (largest) Grothendieck topology for which a given presheaf `P` is a sheaf.
 This is well defined since if `P` is a sheaf for a topology `J`, then it is a sheaf for any
 coarser (smaller) topology. Nonetheless we define the topology explicitly by specifying its sieves:
diff --git a/Mathbin/Data/Complex/ExponentialBounds.lean b/Mathbin/Data/Complex/ExponentialBounds.lean
index d5bba1327a..bdb286f5e8 100644
--- a/Mathbin/Data/Complex/ExponentialBounds.lean
+++ b/Mathbin/Data/Complex/ExponentialBounds.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Joseph Myers
 
 ! This file was ported from Lean 3 source module data.complex.exponential_bounds
-! leanprover-community/mathlib commit 402f8982dddc1864bd703da2d6e2ee304a866973
+! leanprover-community/mathlib commit 36938f775671ff28bea1c0310f1608e4afbb22e0
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -13,6 +13,9 @@ import Mathbin.Analysis.SpecialFunctions.Log.Deriv
 
 /-!
 # Bounds on specific values of the exponential
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
 -/
 
 
diff --git a/Mathbin/Data/Nat/SqrtNormNum.lean b/Mathbin/Data/Nat/SqrtNormNum.lean
index 8f3c39cd3e..b061d3f3ec 100644
--- a/Mathbin/Data/Nat/SqrtNormNum.lean
+++ b/Mathbin/Data/Nat/SqrtNormNum.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 
 ! This file was ported from Lean 3 source module data.nat.sqrt_norm_num
-! leanprover-community/mathlib commit ca80c8b003dcb3f7dbe0017d2e951bc687b9ad3f
+! leanprover-community/mathlib commit 36938f775671ff28bea1c0310f1608e4afbb22e0
 ! 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.Nat.Sqrt
 
 /-! ### `norm_num` plugin for `sqrt`
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 The `norm_num` plugin evaluates `sqrt` by bounding it between consecutive integers.
 -/
 
diff --git a/Mathbin/FieldTheory/IsAlgClosed/Spectrum.lean b/Mathbin/FieldTheory/IsAlgClosed/Spectrum.lean
new file mode 100644
index 0000000000..f500360c9a
--- /dev/null
+++ b/Mathbin/FieldTheory/IsAlgClosed/Spectrum.lean
@@ -0,0 +1,182 @@
+/-
+Copyright (c) 2021 Jireh Loreaux. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jireh Loreaux
+
+! This file was ported from Lean 3 source module field_theory.is_alg_closed.spectrum
+! leanprover-community/mathlib commit 58a272265b5e05f258161260dd2c5d247213cbd3
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathbin.Algebra.Algebra.Spectrum
+import Mathbin.FieldTheory.IsAlgClosed.Basic
+
+/-!
+# Spectrum mapping theorem
+
+This file develops proves the spectral mapping theorem for polynomials over algebraically closed
+fields. In particular, if `a` is an element of an `𝕜`-algebra `A` where `𝕜` is a field, and
+`p : 𝕜[X]` is a polynomial, then the spectrum of `polynomial.aeval a p` contains the image of the
+spectrum of `a` under `(λ k, polynomial.eval k p)`. When `𝕜` is algebraically closed, these are in
+fact equal (assuming either that the spectrum of `a` is nonempty or the polynomial has positive
+degree), which is the **spectral mapping theorem**.
+
+In addition, this file contains the fact that every element of a finite dimensional nontrivial
+algebra over an algebraically closed field has nonempty spectrum. In particular, this is used in
+`module.End.exists_eigenvalue` to show that every linear map from a vector space to itself has an
+eigenvalue.
+
+## Main statements
+
+* `spectrum.subset_polynomial_aeval`, `spectrum.map_polynomial_aeval_of_degree_pos`,
+  `spectrum.map_polynomial_aeval_of_nonempty`: variations on the **spectral mapping theorem**.
+* `spectrum.nonempty_of_is_alg_closed_of_finite_dimensional`: the spectrum is nonempty for any
+  element of a nontrivial finite dimensional algebra over an algebraically closed field.
+
+## Notations
+
+* `σ a` : `spectrum R a` of `a : A`
+-/
+
+
+namespace spectrum
+
+open Set Polynomial
+
+open scoped Pointwise Polynomial
+
+universe u v
+
+section ScalarRing
+
+variable {R : Type u} {A : Type v}
+
+variable [CommRing R] [Ring A] [Algebra R A]
+
+-- mathport name: exprσ
+local notation "σ" => spectrum R
+
+-- mathport name: «expr↑ₐ»
+local notation "↑ₐ" => algebraMap R A
+
+theorem exists_mem_of_not_isUnit_aeval_prod [IsDomain R] {p : R[X]} {a : A} (hp : p ≠ 0)
+    (h : ¬IsUnit (aeval a (Multiset.map (fun x : R => X - C x) p.roots).Prod)) :
+    ∃ k : R, k ∈ σ a ∧ eval k p = 0 :=
+  by
+  rw [← Multiset.prod_toList, AlgHom.map_list_prod] at h 
+  replace h := mt List.prod_isUnit h
+  simp only [not_forall, exists_prop, aeval_C, Multiset.mem_toList, List.mem_map, aeval_X,
+    exists_exists_and_eq_and, Multiset.mem_map, AlgHom.map_sub] at h 
+  rcases h with ⟨r, r_mem, r_nu⟩
+  exact ⟨r, by rwa [mem_iff, ← IsUnit.sub_iff], by rwa [← is_root.def, ← mem_roots hp]⟩
+#align spectrum.exists_mem_of_not_is_unit_aeval_prod spectrum.exists_mem_of_not_isUnit_aeval_prod
+
+end ScalarRing
+
+section ScalarField
+
+variable {𝕜 : Type u} {A : Type v}
+
+variable [Field 𝕜] [Ring A] [Algebra 𝕜 A]
+
+-- mathport name: exprσ
+local notation "σ" => spectrum 𝕜
+
+-- mathport name: «expr↑ₐ»
+local notation "↑ₐ" => algebraMap 𝕜 A
+
+open Polynomial
+
+/-- Half of the spectral mapping theorem for polynomials. We prove it separately
+because it holds over any field, whereas `spectrum.map_polynomial_aeval_of_degree_pos` and
+`spectrum.map_polynomial_aeval_of_nonempty` need the field to be algebraically closed. -/
+theorem subset_polynomial_aeval (a : A) (p : 𝕜[X]) : (fun k => eval k p) '' σ a ⊆ σ (aeval a p) :=
+  by
+  rintro _ ⟨k, hk, rfl⟩
+  let q := C (eval k p) - p
+  have hroot : is_root q k := by simp only [eval_C, eval_sub, sub_self, is_root.def]
+  rw [← mul_div_eq_iff_is_root, ← neg_mul_neg, neg_sub] at hroot 
+  have aeval_q_eq : ↑ₐ (eval k p) - aeval a p = aeval a q := by
+    simp only [aeval_C, AlgHom.map_sub, sub_left_inj]
+  rw [mem_iff, aeval_q_eq, ← hroot, aeval_mul]
+  have hcomm := (Commute.all (C k - X) (-(q / (X - C k)))).map (aeval a)
+  apply mt fun h => (hcomm.is_unit_mul_iff.mp h).1
+  simpa only [aeval_X, aeval_C, AlgHom.map_sub] using hk
+#align spectrum.subset_polynomial_aeval spectrum.subset_polynomial_aeval
+
+/-- The *spectral mapping theorem* for polynomials.  Note: the assumption `degree p > 0`
+is necessary in case `σ a = ∅`, for then the left-hand side is `∅` and the right-hand side,
+assuming `[nontrivial A]`, is `{k}` where `p = polynomial.C k`. -/
+theorem map_polynomial_aeval_of_degree_pos [IsAlgClosed 𝕜] (a : A) (p : 𝕜[X])
+    (hdeg : 0 < degree p) : σ (aeval a p) = (fun k => eval k p) '' σ a :=
+  by
+  -- handle the easy direction via `spectrum.subset_polynomial_aeval`
+  refine' Set.eq_of_subset_of_subset (fun k hk => _) (subset_polynomial_aeval a p)
+  -- write `C k - p` product of linear factors and a constant; show `C k - p ≠ 0`.
+  have hprod := eq_prod_roots_of_splits_id (IsAlgClosed.splits (C k - p))
+  have h_ne : C k - p ≠ 0 :=
+    ne_zero_of_degree_gt
+      (by rwa [degree_sub_eq_right_of_degree_lt (lt_of_le_of_lt degree_C_le hdeg)])
+  have lead_ne := leading_coeff_ne_zero.mpr h_ne
+  have lead_unit := (Units.map ↑ₐ.toMonoidHom (Units.mk0 _ lead_ne)).IsUnit
+  /- leading coefficient is a unit so product of linear factors is not a unit;
+    apply `exists_mem_of_not_is_unit_aeval_prod`. -/
+  have p_a_eq : aeval a (C k - p) = ↑ₐ k - aeval a p := by
+    simp only [aeval_C, AlgHom.map_sub, sub_left_inj]
+  rw [mem_iff, ← p_a_eq, hprod, aeval_mul, ((Commute.all _ _).map (aeval a)).isUnit_mul_iff,
+    aeval_C] at hk 
+  replace hk := exists_mem_of_not_is_unit_aeval_prod h_ne (not_and.mp hk lead_unit)
+  rcases hk with ⟨r, r_mem, r_ev⟩
+  exact ⟨r, r_mem, symm (by simpa [eval_sub, eval_C, sub_eq_zero] using r_ev)⟩
+#align spectrum.map_polynomial_aeval_of_degree_pos spectrum.map_polynomial_aeval_of_degree_pos
+
+/-- In this version of the spectral mapping theorem, we assume the spectrum
+is nonempty instead of assuming the degree of the polynomial is positive. -/
+theorem map_polynomial_aeval_of_nonempty [IsAlgClosed 𝕜] (a : A) (p : 𝕜[X])
+    (hnon : (σ a).Nonempty) : σ (aeval a p) = (fun k => eval k p) '' σ a :=
+  by
+  nontriviality A
+  refine' Or.elim (le_or_gt (degree p) 0) (fun h => _) (map_polynomial_aeval_of_degree_pos a p)
+  · rw [eq_C_of_degree_le_zero h]
+    simp only [Set.image_congr, eval_C, aeval_C, scalar_eq, Set.Nonempty.image_const hnon]
+#align spectrum.map_polynomial_aeval_of_nonempty spectrum.map_polynomial_aeval_of_nonempty
+
+/-- A specialization of `spectrum.subset_polynomial_aeval` to monic monomials for convenience. -/
+theorem pow_image_subset (a : A) (n : ℕ) : (fun x => x ^ n) '' σ a ⊆ σ (a ^ n) := by
+  simpa only [eval_pow, eval_X, aeval_X_pow] using subset_polynomial_aeval a (X ^ n : 𝕜[X])
+#align spectrum.pow_image_subset spectrum.pow_image_subset
+
+/-- A specialization of `spectrum.map_polynomial_aeval_of_nonempty` to monic monomials for
+convenience. -/
+theorem map_pow_of_pos [IsAlgClosed 𝕜] (a : A) {n : ℕ} (hn : 0 < n) :
+    σ (a ^ n) = (fun x => x ^ n) '' σ a := by
+  simpa only [aeval_X_pow, eval_pow, eval_X] using
+    map_polynomial_aeval_of_degree_pos a (X ^ n : 𝕜[X]) (by rw_mod_cast [degree_X_pow]; exact hn)
+#align spectrum.map_pow_of_pos spectrum.map_pow_of_pos
+
+/-- A specialization of `spectrum.map_polynomial_aeval_of_nonempty` to monic monomials for
+convenience. -/
+theorem map_pow_of_nonempty [IsAlgClosed 𝕜] {a : A} (ha : (σ a).Nonempty) (n : ℕ) :
+    σ (a ^ n) = (fun x => x ^ n) '' σ a := by
+  simpa only [aeval_X_pow, eval_pow, eval_X] using map_polynomial_aeval_of_nonempty a (X ^ n) ha
+#align spectrum.map_pow_of_nonempty spectrum.map_pow_of_nonempty
+
+variable (𝕜)
+
+-- We will use this both to show eigenvalues exist, and to prove Schur's lemma.
+/-- Every element `a` in a nontrivial finite-dimensional algebra `A`
+over an algebraically closed field `𝕜` has non-empty spectrum. -/
+theorem nonempty_of_isAlgClosed_of_finiteDimensional [IsAlgClosed 𝕜] [Nontrivial A]
+    [I : FiniteDimensional 𝕜 A] (a : A) : (σ a).Nonempty :=
+  by
+  obtain ⟨p, ⟨h_mon, h_eval_p⟩⟩ := isIntegral_of_noetherian (IsNoetherian.iff_fg.2 I) a
+  have nu : ¬IsUnit (aeval a p) := by rw [← aeval_def] at h_eval_p ; rw [h_eval_p]; simp
+  rw [eq_prod_roots_of_monic_of_splits_id h_mon (IsAlgClosed.splits p)] at nu 
+  obtain ⟨k, hk, _⟩ := exists_mem_of_not_is_unit_aeval_prod (monic.ne_zero h_mon) nu
+  exact ⟨k, hk⟩
+#align spectrum.nonempty_of_is_alg_closed_of_finite_dimensional spectrum.nonempty_of_isAlgClosed_of_finiteDimensional
+
+end ScalarField
+
+end spectrum
+
diff --git a/Mathbin/FieldTheory/Laurent.lean b/Mathbin/FieldTheory/Laurent.lean
index 875accc7e6..e30e3ddb37 100644
--- a/Mathbin/FieldTheory/Laurent.lean
+++ b/Mathbin/FieldTheory/Laurent.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yakov Pechersky
 
 ! This file was ported from Lean 3 source module field_theory.laurent
-! leanprover-community/mathlib commit 70fd9563a21e7b963887c9360bd29b2393e6225a
+! leanprover-community/mathlib commit 36938f775671ff28bea1c0310f1608e4afbb22e0
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -14,6 +14,9 @@ import Mathbin.FieldTheory.Ratfunc
 /-!
 # Laurent expansions of rational functions
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 ## Main declarations
 
 * `ratfunc.laurent`: the Laurent expansion of the rational function `f` at `r`, as an `alg_hom`.
diff --git a/Mathbin/Geometry/Manifold/Instances/Real.lean b/Mathbin/Geometry/Manifold/Instances/Real.lean
index cc53f3de6e..32c1dc2dfd 100644
--- a/Mathbin/Geometry/Manifold/Instances/Real.lean
+++ b/Mathbin/Geometry/Manifold/Instances/Real.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel
 
 ! This file was ported from Lean 3 source module geometry.manifold.instances.real
-! leanprover-community/mathlib commit 6a033cb3d188a12ca5c509b33e2eaac1c61916cd
+! leanprover-community/mathlib commit 36938f775671ff28bea1c0310f1608e4afbb22e0
 ! 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.InnerProductSpace.PiL2
 /-!
 # Constructing examples of manifolds over ℝ
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We introduce the necessary bits to be able to define manifolds modelled over `ℝ^n`, boundaryless
 or with boundary or with corners. As a concrete example, we construct explicitly the manifold with
 boundary structure on the real interval `[x, y]`.
diff --git a/Mathbin/Geometry/Manifold/Instances/UnitsOfNormedAlgebra.lean b/Mathbin/Geometry/Manifold/Instances/UnitsOfNormedAlgebra.lean
index 81fc10947c..773322fb6f 100644
--- a/Mathbin/Geometry/Manifold/Instances/UnitsOfNormedAlgebra.lean
+++ b/Mathbin/Geometry/Manifold/Instances/UnitsOfNormedAlgebra.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Nicolò Cavalleri, Heather Macbeth
 
 ! This file was ported from Lean 3 source module geometry.manifold.instances.units_of_normed_algebra
-! leanprover-community/mathlib commit ef901ea68d3bb1dd08f8bc3034ab6b32b2e6ecdf
+! leanprover-community/mathlib commit 36938f775671ff28bea1c0310f1608e4afbb22e0
 ! 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.Units
 /-!
 # Units of a normed algebra
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file is a stub, containing a construction of the charted space structure on the group of units
 of a complete normed ring `R`, and of the smooth manifold structure on the group of units of a
 complete normed `𝕜`-algebra `R`.
diff --git a/Mathbin/Geometry/Manifold/Metrizable.lean b/Mathbin/Geometry/Manifold/Metrizable.lean
index 0bd1206540..97e8165ed9 100644
--- a/Mathbin/Geometry/Manifold/Metrizable.lean
+++ b/Mathbin/Geometry/Manifold/Metrizable.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 geometry.manifold.metrizable
-! leanprover-community/mathlib commit d1bd9c5df2867c1cb463bc6364446d57bdd9f7f1
+! leanprover-community/mathlib commit 36938f775671ff28bea1c0310f1608e4afbb22e0
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -15,6 +15,9 @@ import Mathbin.Topology.MetricSpace.Metrizable
 /-!
 # Metrizability of a σ-compact manifold
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we show that a σ-compact Hausdorff topological manifold over a finite dimensional real
 vector space is metrizable.
 -/
diff --git a/Mathbin/Geometry/Manifold/SmoothManifoldWithCorners.lean b/Mathbin/Geometry/Manifold/SmoothManifoldWithCorners.lean
index 3999b15d1e..e672c56d2a 100644
--- a/Mathbin/Geometry/Manifold/SmoothManifoldWithCorners.lean
+++ b/Mathbin/Geometry/Manifold/SmoothManifoldWithCorners.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel
 
 ! This file was ported from Lean 3 source module geometry.manifold.smooth_manifold_with_corners
-! leanprover-community/mathlib commit ddec54a71a0dd025c05445d467f1a2b7d586a3ba
+! leanprover-community/mathlib commit 36938f775671ff28bea1c0310f1608e4afbb22e0
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -14,6 +14,9 @@ import Mathbin.Geometry.Manifold.ChartedSpace
 /-!
 # Smooth manifolds (possibly with boundary or corners)
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 A smooth manifold is a manifold modelled on a normed vector space, or a subset like a
 half-space (to get manifolds with boundaries) for which the changes of coordinates are smooth maps.
 We define a model with corners as a map `I : H → E` embedding nicely the topological space `H` in
diff --git a/Mathbin/GroupTheory/Transfer.lean b/Mathbin/GroupTheory/Transfer.lean
index fee4a02492..ab6d37df5d 100644
--- a/Mathbin/GroupTheory/Transfer.lean
+++ b/Mathbin/GroupTheory/Transfer.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Thomas Browning
 
 ! This file was ported from Lean 3 source module group_theory.transfer
-! leanprover-community/mathlib commit 56489b558d42c30f6aac5947cafc9a594f60813b
+! leanprover-community/mathlib commit 36938f775671ff28bea1c0310f1608e4afbb22e0
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -14,6 +14,9 @@ import Mathbin.GroupTheory.Sylow
 /-!
 # The Transfer Homomorphism
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we construct the transfer homomorphism.
 
 ## Main definitions
diff --git a/Mathbin/LinearAlgebra/Eigenspace.lean b/Mathbin/LinearAlgebra/Eigenspace.lean
index f054b7c98a..c689654313 100644
--- a/Mathbin/LinearAlgebra/Eigenspace.lean
+++ b/Mathbin/LinearAlgebra/Eigenspace.lean
@@ -4,11 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Alexander Bentkamp
 
 ! This file was ported from Lean 3 source module linear_algebra.eigenspace
-! leanprover-community/mathlib commit f0c8bf9245297a541f468be517f1bde6195105e9
+! leanprover-community/mathlib commit 58a272265b5e05f258161260dd2c5d247213cbd3
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
-import Mathbin.Algebra.Algebra.Spectrum
+import Mathbin.FieldTheory.IsAlgClosed.Spectrum
 import Mathbin.Order.Hom.Basic
 import Mathbin.LinearAlgebra.GeneralLinearGroup
 
diff --git a/Mathbin/LinearAlgebra/QuadraticForm/Basic.lean b/Mathbin/LinearAlgebra/QuadraticForm/Basic.lean
index 8d4953c4fe..4a9af2ab83 100644
--- a/Mathbin/LinearAlgebra/QuadraticForm/Basic.lean
+++ b/Mathbin/LinearAlgebra/QuadraticForm/Basic.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Anne Baanen, Kexing Ying, Eric Wieser
 
 ! This file was ported from Lean 3 source module linear_algebra.quadratic_form.basic
-! leanprover-community/mathlib commit 11b92770e4d49ff3982504c4dab918ac0887fe33
+! leanprover-community/mathlib commit 36938f775671ff28bea1c0310f1608e4afbb22e0
 ! 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.Matrix.Symmetric
 /-!
 # Quadratic forms
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines quadratic forms over a `R`-module `M`.
 A quadratic form on a ring `R` is a map `Q : M → R` such that:
 * `quadratic_form.map_smul`: `Q (a • x) = a * a * Q x`
diff --git a/Mathbin/MeasureTheory/Function/ContinuousMapDense.lean b/Mathbin/MeasureTheory/Function/ContinuousMapDense.lean
index 9cf781f8f8..7953dfd822 100644
--- a/Mathbin/MeasureTheory/Function/ContinuousMapDense.lean
+++ b/Mathbin/MeasureTheory/Function/ContinuousMapDense.lean
@@ -249,7 +249,7 @@ theorem Integrable.exists_hasCompactSupport_integral_sub_le [LocallyCompactSpace
 /- ./././Mathport/Syntax/Translate/Basic.lean:635:2: warning: expanding binder collection (s «expr ⊆ » t) -/
 /-- Any function in `ℒp` can be approximated by bounded continuous functions when `p < ∞`,
 version in terms of `snorm`. -/
-theorem Memℒp.exists_bounded_continuous_snorm_sub_le [μ.WeaklyRegular] (hp : p ≠ ∞) {f : α → E}
+theorem Memℒp.exists_boundedContinuous_snorm_sub_le [μ.WeaklyRegular] (hp : p ≠ ∞) {f : α → E}
     (hf : Memℒp f p μ) {ε : ℝ≥0∞} (hε : ε ≠ 0) :
     ∃ g : α →ᵇ E, snorm (f - g) p μ ≤ ε ∧ Memℒp g p μ :=
   by
@@ -300,11 +300,11 @@ theorem Memℒp.exists_bounded_continuous_snorm_sub_le [μ.WeaklyRegular] (hp :
     simp only [sub_add_sub_cancel]
   refine' ⟨f, I3, f_cont, f_mem, _⟩
   exact (BoundedContinuousFunction.ofNormedAddCommGroup f f_cont _ f_bound).bounded_range
-#align measure_theory.mem_ℒp.exists_bounded_continuous_snorm_sub_le MeasureTheory.Memℒp.exists_bounded_continuous_snorm_sub_le
+#align measure_theory.mem_ℒp.exists_bounded_continuous_snorm_sub_le MeasureTheory.Memℒp.exists_boundedContinuous_snorm_sub_le
 
 /-- Any function in `ℒp` can be approximated by bounded continuous functions when `0 < p < ∞`,
 version in terms of `∫`. -/
-theorem Memℒp.exists_bounded_continuous_integral_rpow_sub_le [μ.WeaklyRegular] {p : ℝ} (hp : 0 < p)
+theorem Memℒp.exists_boundedContinuous_integral_rpow_sub_le [μ.WeaklyRegular] {p : ℝ} (hp : 0 < p)
     {f : α → E} (hf : Memℒp f (ENNReal.ofReal p) μ) {ε : ℝ} (hε : 0 < ε) :
     ∃ g : α →ᵇ E, (∫ x, ‖f x - g x‖ ^ p ∂μ) ≤ ε ∧ Memℒp g (ENNReal.ofReal p) μ :=
   by
@@ -319,28 +319,28 @@ theorem Memℒp.exists_bounded_continuous_integral_rpow_sub_le [μ.WeaklyRegular
     ENNReal.ofReal_le_ofReal_iff I.le, one_div, ENNReal.toReal_ofReal hp.le,
     Real.rpow_le_rpow_iff _ hε.le (inv_pos.2 hp)] at hg 
   exact integral_nonneg fun x => Real.rpow_nonneg_of_nonneg (norm_nonneg _) _
-#align measure_theory.mem_ℒp.exists_bounded_continuous_integral_rpow_sub_le MeasureTheory.Memℒp.exists_bounded_continuous_integral_rpow_sub_le
+#align measure_theory.mem_ℒp.exists_bounded_continuous_integral_rpow_sub_le MeasureTheory.Memℒp.exists_boundedContinuous_integral_rpow_sub_le
 
 /-- Any integrable function can be approximated by bounded continuous functions,
 version in terms of `∫⁻`. -/
-theorem Integrable.exists_bounded_continuous_lintegral_sub_le [μ.WeaklyRegular] {f : α → E}
+theorem Integrable.exists_boundedContinuous_lintegral_sub_le [μ.WeaklyRegular] {f : α → E}
     (hf : Integrable f μ) {ε : ℝ≥0∞} (hε : ε ≠ 0) :
     ∃ g : α →ᵇ E, (∫⁻ x, ‖f x - g x‖₊ ∂μ) ≤ ε ∧ Integrable g μ :=
   by
   simp only [← mem_ℒp_one_iff_integrable, ← snorm_one_eq_lintegral_nnnorm] at hf ⊢
   exact hf.exists_bounded_continuous_snorm_sub_le ENNReal.one_ne_top hε
-#align measure_theory.integrable.exists_bounded_continuous_lintegral_sub_le MeasureTheory.Integrable.exists_bounded_continuous_lintegral_sub_le
+#align measure_theory.integrable.exists_bounded_continuous_lintegral_sub_le MeasureTheory.Integrable.exists_boundedContinuous_lintegral_sub_le
 
 /-- Any integrable function can be approximated by bounded continuous functions,
 version in terms of `∫`. -/
-theorem Integrable.exists_bounded_continuous_integral_sub_le [μ.WeaklyRegular] {f : α → E}
+theorem Integrable.exists_boundedContinuous_integral_sub_le [μ.WeaklyRegular] {f : α → E}
     (hf : Integrable f μ) {ε : ℝ} (hε : 0 < ε) :
     ∃ g : α →ᵇ E, (∫ x, ‖f x - g x‖ ∂μ) ≤ ε ∧ Integrable g μ :=
   by
   simp only [← mem_ℒp_one_iff_integrable, ← snorm_one_eq_lintegral_nnnorm, ← ENNReal.ofReal_one] at
     hf ⊢
   simpa using hf.exists_bounded_continuous_integral_rpow_sub_le zero_lt_one hε
-#align measure_theory.integrable.exists_bounded_continuous_integral_sub_le MeasureTheory.Integrable.exists_bounded_continuous_integral_sub_le
+#align measure_theory.integrable.exists_bounded_continuous_integral_sub_le MeasureTheory.Integrable.exists_boundedContinuous_integral_sub_le
 
 namespace Lp
 
@@ -357,7 +357,7 @@ theorem boundedContinuousFunction_dense [SecondCountableTopologyEither α E] [_i
   intro ε hε
   have A : ENNReal.ofReal ε ≠ 0 := by simp only [Ne.def, ENNReal.ofReal_eq_zero, not_le, hε]
   obtain ⟨g, hg, g_mem⟩ : ∃ g : α →ᵇ E, snorm (f - g) p μ ≤ ENNReal.ofReal ε ∧ mem_ℒp g p μ
-  exact (Lp.mem_ℒp f).exists_bounded_continuous_snorm_sub_le hp A
+  exact (Lp.mem_ℒp f).exists_boundedContinuous_snorm_sub_le hp A
   refine' ⟨g_mem.to_Lp _, _, ⟨g, rfl⟩⟩
   simp only [dist_eq_norm, Metric.mem_closedBall']
   rw [Lp.norm_def]
diff --git a/Mathbin/MeasureTheory/Function/SpecialFunctions/Arctan.lean b/Mathbin/MeasureTheory/Function/SpecialFunctions/Arctan.lean
index 01fa64532a..5b6678b183 100644
--- a/Mathbin/MeasureTheory/Function/SpecialFunctions/Arctan.lean
+++ b/Mathbin/MeasureTheory/Function/SpecialFunctions/Arctan.lean
@@ -19,10 +19,12 @@ import Mathbin.MeasureTheory.Constructions.BorelSpace.Basic
 
 namespace Real
 
+#print Real.measurable_arctan /-
 @[measurability]
 theorem measurable_arctan : Measurable arctan :=
   continuous_arctan.Measurable
 #align real.measurable_arctan Real.measurable_arctan
+-/
 
 end Real
 
@@ -32,10 +34,12 @@ open Real
 
 variable {α : Type _} {m : MeasurableSpace α} {f : α → ℝ} (hf : Measurable f)
 
+#print Measurable.arctan /-
 @[measurability]
 theorem Measurable.arctan : Measurable fun x => arctan (f x) :=
   measurable_arctan.comp hf
 #align measurable.arctan Measurable.arctan
+-/
 
 end RealComposition
 
diff --git a/Mathbin/MeasureTheory/Integral/Bochner.lean b/Mathbin/MeasureTheory/Integral/Bochner.lean
index cd4a4f6bbd..65080527ab 100644
--- a/Mathbin/MeasureTheory/Integral/Bochner.lean
+++ b/Mathbin/MeasureTheory/Integral/Bochner.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Zhouhang Zhou, Yury Kudryashov, Sébastien Gouëzel, Rémy Degenne
 
 ! This file was ported from Lean 3 source module measure_theory.integral.bochner
-! leanprover-community/mathlib commit 8f9fea08977f7e450770933ee6abb20733b47c92
+! leanprover-community/mathlib commit 36938f775671ff28bea1c0310f1608e4afbb22e0
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -13,6 +13,9 @@ import Mathbin.MeasureTheory.Integral.SetToL1
 /-!
 # Bochner integral
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 The Bochner integral extends the definition of the Lebesgue integral to functions that map from a
 measure space into a Banach space (complete normed vector space). It is constructed here by
 extending the integral on simple functions.
diff --git a/Mathbin/MeasureTheory/Integral/VitaliCaratheodory.lean b/Mathbin/MeasureTheory/Integral/VitaliCaratheodory.lean
index 3e1175c322..55ce79d0fb 100644
--- a/Mathbin/MeasureTheory/Integral/VitaliCaratheodory.lean
+++ b/Mathbin/MeasureTheory/Integral/VitaliCaratheodory.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel
 
 ! This file was ported from Lean 3 source module measure_theory.integral.vitali_caratheodory
-! leanprover-community/mathlib commit 57ac39bd365c2f80589a700f9fbb664d3a1a30c2
+! leanprover-community/mathlib commit 36938f775671ff28bea1c0310f1608e4afbb22e0
 ! 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.Ereal
 /-!
 # Vitali-Carathéodory theorem
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Vitali-Carathéodory theorem asserts the following. Consider an integrable function `f : α → ℝ` on
 a space with a regular measure. Then there exists a function `g : α → ereal` such that `f x < g x`
 everywhere, `g` is lower semicontinuous, and the integral of `g` is arbitrarily close to that of
diff --git a/Mathbin/MeasureTheory/Measure/FiniteMeasure.lean b/Mathbin/MeasureTheory/Measure/FiniteMeasure.lean
index b468593163..d393d213de 100644
--- a/Mathbin/MeasureTheory/Measure/FiniteMeasure.lean
+++ b/Mathbin/MeasureTheory/Measure/FiniteMeasure.lean
@@ -107,19 +107,23 @@ associated weak topology (essentially the weak-star topology on the dual of `Ω
 
 variable {Ω : Type _} [MeasurableSpace Ω]
 
+#print MeasureTheory.FiniteMeasure /-
 /-- Finite measures are defined as the subtype of measures that have the property of being finite
 measures (i.e., their total mass is finite). -/
 def MeasureTheory.FiniteMeasure (Ω : Type _) [MeasurableSpace Ω] : Type _ :=
   { μ : Measure Ω // IsFiniteMeasure μ }
 #align measure_theory.finite_measure MeasureTheory.FiniteMeasure
+-/
 
 /-- A finite measure can be interpreted as a measure. -/
 instance : Coe (FiniteMeasure Ω) (MeasureTheory.Measure Ω) :=
   coeSubtype
 
+#print MeasureTheory.FiniteMeasure.isFiniteMeasure /-
 instance isFiniteMeasure (μ : FiniteMeasure Ω) : IsFiniteMeasure (μ : Measure Ω) :=
   μ.Prop
 #align measure_theory.finite_measure.is_finite_measure MeasureTheory.FiniteMeasure.isFiniteMeasure
+-/
 
 instance : CoeFun (FiniteMeasure Ω) fun _ => Set Ω → ℝ≥0 :=
   ⟨fun μ s => (μ s).toNNReal⟩
@@ -129,46 +133,60 @@ theorem coeFn_eq_toNNReal_coeFn_to_measure (ν : FiniteMeasure Ω) :
   rfl
 #align measure_theory.finite_measure.coe_fn_eq_to_nnreal_coe_fn_to_measure MeasureTheory.FiniteMeasure.coeFn_eq_toNNReal_coeFn_to_measure
 
+#print MeasureTheory.FiniteMeasure.ennreal_coeFn_eq_coeFn_toMeasure /-
 @[simp]
-theorem eNNReal_coeFn_eq_coeFn_to_measure (ν : FiniteMeasure Ω) (s : Set Ω) :
+theorem ennreal_coeFn_eq_coeFn_toMeasure (ν : FiniteMeasure Ω) (s : Set Ω) :
     (ν s : ℝ≥0∞) = (ν : Measure Ω) s :=
   ENNReal.coe_toNNReal (measure_lt_top (↑ν) s).Ne
-#align measure_theory.finite_measure.ennreal_coe_fn_eq_coe_fn_to_measure MeasureTheory.FiniteMeasure.eNNReal_coeFn_eq_coeFn_to_measure
+#align measure_theory.finite_measure.ennreal_coe_fn_eq_coe_fn_to_measure MeasureTheory.FiniteMeasure.ennreal_coeFn_eq_coeFn_toMeasure
+-/
 
+#print MeasureTheory.FiniteMeasure.val_eq_toMeasure /-
 @[simp]
-theorem val_eq_to_measure (ν : FiniteMeasure Ω) : ν.val = (ν : Measure Ω) :=
+theorem val_eq_toMeasure (ν : FiniteMeasure Ω) : ν.val = (ν : Measure Ω) :=
   rfl
-#align measure_theory.finite_measure.val_eq_to_measure MeasureTheory.FiniteMeasure.val_eq_to_measure
+#align measure_theory.finite_measure.val_eq_to_measure MeasureTheory.FiniteMeasure.val_eq_toMeasure
+-/
 
-theorem coe_injective : Function.Injective (coe : FiniteMeasure Ω → Measure Ω) :=
+#print MeasureTheory.FiniteMeasure.toMeasure_injective /-
+theorem toMeasure_injective : Function.Injective (coe : FiniteMeasure Ω → Measure Ω) :=
   Subtype.coe_injective
-#align measure_theory.finite_measure.coe_injective MeasureTheory.FiniteMeasure.coe_injective
+#align measure_theory.finite_measure.coe_injective MeasureTheory.FiniteMeasure.toMeasure_injective
+-/
 
+#print MeasureTheory.FiniteMeasure.apply_mono /-
 theorem apply_mono (μ : FiniteMeasure Ω) {s₁ s₂ : Set Ω} (h : s₁ ⊆ s₂) : μ s₁ ≤ μ s₂ :=
   by
   change ((μ : Measure Ω) s₁).toNNReal ≤ ((μ : Measure Ω) s₂).toNNReal
   have key : (μ : Measure Ω) s₁ ≤ (μ : Measure Ω) s₂ := (μ : Measure Ω).mono h
   apply (ENNReal.toNNReal_le_toNNReal (measure_ne_top _ s₁) (measure_ne_top _ s₂)).mpr key
 #align measure_theory.finite_measure.apply_mono MeasureTheory.FiniteMeasure.apply_mono
+-/
 
+#print MeasureTheory.FiniteMeasure.mass /-
 /-- The (total) mass of a finite measure `μ` is `μ univ`, i.e., the cast to `nnreal` of
 `(μ : measure Ω) univ`. -/
 def mass (μ : FiniteMeasure Ω) : ℝ≥0 :=
   μ univ
 #align measure_theory.finite_measure.mass MeasureTheory.FiniteMeasure.mass
+-/
 
+#print MeasureTheory.FiniteMeasure.ennreal_mass /-
 @[simp]
-theorem eNNReal_mass {μ : FiniteMeasure Ω} : (μ.mass : ℝ≥0∞) = (μ : Measure Ω) univ :=
-  eNNReal_coeFn_eq_coeFn_to_measure μ Set.univ
-#align measure_theory.finite_measure.ennreal_mass MeasureTheory.FiniteMeasure.eNNReal_mass
+theorem ennreal_mass {μ : FiniteMeasure Ω} : (μ.mass : ℝ≥0∞) = (μ : Measure Ω) univ :=
+  ennreal_coeFn_eq_coeFn_toMeasure μ Set.univ
+#align measure_theory.finite_measure.ennreal_mass MeasureTheory.FiniteMeasure.ennreal_mass
+-/
 
-instance hasZero : Zero (FiniteMeasure Ω) where zero := ⟨0, MeasureTheory.isFiniteMeasureZero⟩
-#align measure_theory.finite_measure.has_zero MeasureTheory.FiniteMeasure.hasZero
+#print MeasureTheory.FiniteMeasure.instZero /-
+instance instZero : Zero (FiniteMeasure Ω) where zero := ⟨0, MeasureTheory.isFiniteMeasureZero⟩
+#align measure_theory.finite_measure.has_zero MeasureTheory.FiniteMeasure.instZero
+-/
 
 @[simp]
-theorem Zero.mass : (0 : FiniteMeasure Ω).mass = 0 :=
+theorem MeasureTheory.FiniteMeasure.zero_mass : (0 : FiniteMeasure Ω).mass = 0 :=
   rfl
-#align measure_theory.finite_measure.zero.mass MeasureTheory.FiniteMeasure.Zero.mass
+#align measure_theory.finite_measure.zero.mass MeasureTheory.FiniteMeasure.zero_mass
 
 @[simp]
 theorem mass_zero_iff (μ : FiniteMeasure Ω) : μ.mass = 0 ↔ μ = 0 :=
@@ -185,18 +203,22 @@ theorem mass_nonzero_iff (μ : FiniteMeasure Ω) : μ.mass ≠ 0 ↔ μ ≠ 0 :=
   exact finite_measure.mass_zero_iff μ
 #align measure_theory.finite_measure.mass_nonzero_iff MeasureTheory.FiniteMeasure.mass_nonzero_iff
 
+#print MeasureTheory.FiniteMeasure.eq_of_forall_toMeasure_apply_eq /-
 @[ext]
-theorem eq_of_forall_measure_apply_eq (μ ν : FiniteMeasure Ω)
+theorem eq_of_forall_toMeasure_apply_eq (μ ν : FiniteMeasure Ω)
     (h : ∀ s : Set Ω, MeasurableSet s → (μ : Measure Ω) s = (ν : Measure Ω) s) : μ = ν := by ext1;
   ext1 s s_mble; exact h s s_mble
-#align measure_theory.finite_measure.eq_of_forall_measure_apply_eq MeasureTheory.FiniteMeasure.eq_of_forall_measure_apply_eq
+#align measure_theory.finite_measure.eq_of_forall_measure_apply_eq MeasureTheory.FiniteMeasure.eq_of_forall_toMeasure_apply_eq
+-/
 
+#print MeasureTheory.FiniteMeasure.eq_of_forall_apply_eq /-
 theorem eq_of_forall_apply_eq (μ ν : FiniteMeasure Ω)
     (h : ∀ s : Set Ω, MeasurableSet s → μ s = ν s) : μ = ν :=
   by
   ext1 s s_mble
   simpa [ennreal_coe_fn_eq_coe_fn_to_measure] using congr_arg (coe : ℝ≥0 → ℝ≥0∞) (h s s_mble)
 #align measure_theory.finite_measure.eq_of_forall_apply_eq MeasureTheory.FiniteMeasure.eq_of_forall_apply_eq
+-/
 
 instance : Inhabited (FiniteMeasure Ω) :=
   ⟨0⟩
@@ -209,20 +231,24 @@ variable {R : Type _} [SMul R ℝ≥0] [SMul R ℝ≥0∞] [IsScalarTower R ℝ
 instance : SMul R (FiniteMeasure Ω)
     where smul (c : R) μ := ⟨c • μ, MeasureTheory.isFiniteMeasureSMulOfNNRealTower⟩
 
+#print MeasureTheory.FiniteMeasure.toMeasure_zero /-
 @[simp, norm_cast]
-theorem coe_zero : (coe : FiniteMeasure Ω → Measure Ω) 0 = 0 :=
+theorem toMeasure_zero : (coe : FiniteMeasure Ω → Measure Ω) 0 = 0 :=
   rfl
-#align measure_theory.finite_measure.coe_zero MeasureTheory.FiniteMeasure.coe_zero
+#align measure_theory.finite_measure.coe_zero MeasureTheory.FiniteMeasure.toMeasure_zero
+-/
 
+#print MeasureTheory.FiniteMeasure.toMeasure_add /-
 @[simp, norm_cast]
-theorem coe_add (μ ν : FiniteMeasure Ω) : ↑(μ + ν) = (↑μ + ↑ν : Measure Ω) :=
+theorem toMeasure_add (μ ν : FiniteMeasure Ω) : ↑(μ + ν) = (↑μ + ↑ν : Measure Ω) :=
   rfl
-#align measure_theory.finite_measure.coe_add MeasureTheory.FiniteMeasure.coe_add
+#align measure_theory.finite_measure.coe_add MeasureTheory.FiniteMeasure.toMeasure_add
+-/
 
 @[simp, norm_cast]
-theorem coe_smul (c : R) (μ : FiniteMeasure Ω) : ↑(c • μ) = (c • ↑μ : Measure Ω) :=
+theorem toMeasure_smul (c : R) (μ : FiniteMeasure Ω) : ↑(c • μ) = (c • ↑μ : Measure Ω) :=
   rfl
-#align measure_theory.finite_measure.coe_smul MeasureTheory.FiniteMeasure.coe_smul
+#align measure_theory.finite_measure.coe_smul MeasureTheory.FiniteMeasure.toMeasure_smul
 
 @[simp, norm_cast]
 theorem coeFn_zero : (⇑(0 : FiniteMeasure Ω) : Set Ω → ℝ≥0) = (0 : Set Ω → ℝ≥0) := by funext; rfl
@@ -240,36 +266,40 @@ theorem coeFn_smul [IsScalarTower R ℝ≥0 ℝ≥0] (c : R) (μ : FiniteMeasure
 #align measure_theory.finite_measure.coe_fn_smul MeasureTheory.FiniteMeasure.coeFn_smul
 
 instance : AddCommMonoid (FiniteMeasure Ω) :=
-  coe_injective.AddCommMonoid coe coe_zero coe_add fun _ _ => coe_smul _ _
+  toMeasure_injective.AddCommMonoid coe toMeasure_zero toMeasure_add fun _ _ => toMeasure_smul _ _
 
 /-- Coercion is an `add_monoid_hom`. -/
 @[simps]
-def coeAddMonoidHom : FiniteMeasure Ω →+ Measure Ω
+def toMeasureAddMonoidHom : FiniteMeasure Ω →+ Measure Ω
     where
   toFun := coe
-  map_zero' := coe_zero
-  map_add' := coe_add
-#align measure_theory.finite_measure.coe_add_monoid_hom MeasureTheory.FiniteMeasure.coeAddMonoidHom
+  map_zero' := toMeasure_zero
+  map_add' := toMeasure_add
+#align measure_theory.finite_measure.coe_add_monoid_hom MeasureTheory.FiniteMeasure.toMeasureAddMonoidHom
 
 instance {Ω : Type _} [MeasurableSpace Ω] : Module ℝ≥0 (FiniteMeasure Ω) :=
-  Function.Injective.module _ coeAddMonoidHom coe_injective coe_smul
+  Function.Injective.module _ toMeasureAddMonoidHom toMeasure_injective toMeasure_smul
 
 @[simp]
 theorem coeFn_smul_apply [IsScalarTower R ℝ≥0 ℝ≥0] (c : R) (μ : FiniteMeasure Ω) (s : Set Ω) :
     (c • μ) s = c • μ s := by simp only [coe_fn_smul, Pi.smul_apply]
 #align measure_theory.finite_measure.coe_fn_smul_apply MeasureTheory.FiniteMeasure.coeFn_smul_apply
 
+#print MeasureTheory.FiniteMeasure.restrict /-
 /-- Restrict a finite measure μ to a set A. -/
 def restrict (μ : FiniteMeasure Ω) (A : Set Ω) : FiniteMeasure Ω
     where
   val := (μ : Measure Ω).restrict A
   property := MeasureTheory.isFiniteMeasureRestrict μ A
 #align measure_theory.finite_measure.restrict MeasureTheory.FiniteMeasure.restrict
+-/
 
+#print MeasureTheory.FiniteMeasure.restrict_measure_eq /-
 theorem restrict_measure_eq (μ : FiniteMeasure Ω) (A : Set Ω) :
     (μ.restrict A : Measure Ω) = (μ : Measure Ω).restrict A :=
   rfl
 #align measure_theory.finite_measure.restrict_measure_eq MeasureTheory.FiniteMeasure.restrict_measure_eq
+-/
 
 theorem restrict_apply_measure (μ : FiniteMeasure Ω) (A : Set Ω) {s : Set Ω}
     (s_mble : MeasurableSet s) : (μ.restrict A : Measure Ω) s = (μ : Measure Ω) (s ∩ A) :=
@@ -283,9 +313,11 @@ theorem restrict_apply (μ : FiniteMeasure Ω) (A : Set Ω) {s : Set Ω} (s_mble
   exact measure.restrict_apply s_mble
 #align measure_theory.finite_measure.restrict_apply MeasureTheory.FiniteMeasure.restrict_apply
 
+#print MeasureTheory.FiniteMeasure.restrict_mass /-
 theorem restrict_mass (μ : FiniteMeasure Ω) (A : Set Ω) : (μ.restrict A).mass = μ A := by
   simp only [mass, restrict_apply μ A MeasurableSet.univ, univ_inter]
 #align measure_theory.finite_measure.restrict_mass MeasureTheory.FiniteMeasure.restrict_mass
+-/
 
 theorem restrict_eq_zero_iff (μ : FiniteMeasure Ω) (A : Set Ω) : μ.restrict A = 0 ↔ μ A = 0 := by
   rw [← mass_zero_iff, restrict_mass]
@@ -300,17 +332,17 @@ variable [TopologicalSpace Ω]
 /-- The pairing of a finite (Borel) measure `μ` with a nonnegative bounded continuous
 function is obtained by (Lebesgue) integrating the (test) function against the measure.
 This is `finite_measure.test_against_nn`. -/
-def testAgainstNn (μ : FiniteMeasure Ω) (f : Ω →ᵇ ℝ≥0) : ℝ≥0 :=
+def testAgainstNN (μ : FiniteMeasure Ω) (f : Ω →ᵇ ℝ≥0) : ℝ≥0 :=
   (∫⁻ ω, f ω ∂(μ : Measure Ω)).toNNReal
-#align measure_theory.finite_measure.test_against_nn MeasureTheory.FiniteMeasure.testAgainstNn
+#align measure_theory.finite_measure.test_against_nn MeasureTheory.FiniteMeasure.testAgainstNN
 
-theorem BoundedContinuousFunction.Nnreal.to_eNNReal_comp_measurable {Ω : Type _}
+theorem BoundedContinuousFunction.NNReal.coe_ennreal_comp_measurable {Ω : Type _}
     [TopologicalSpace Ω] [MeasurableSpace Ω] [OpensMeasurableSpace Ω] (f : Ω →ᵇ ℝ≥0) :
     Measurable fun ω => (f ω : ℝ≥0∞) :=
   measurable_coe_nnreal_ennreal.comp f.Continuous.Measurable
-#align bounded_continuous_function.nnreal.to_ennreal_comp_measurable BoundedContinuousFunction.Nnreal.to_eNNReal_comp_measurable
+#align bounded_continuous_function.nnreal.to_ennreal_comp_measurable BoundedContinuousFunction.NNReal.coe_ennreal_comp_measurable
 
-theorem MeasureTheory.lintegral_lt_top_of_bounded_continuous_to_nNReal (μ : Measure Ω)
+theorem MeasureTheory.lintegral_lt_top_of_boundedContinuous_to_nnreal (μ : Measure Ω)
     [IsFiniteMeasure μ] (f : Ω →ᵇ ℝ≥0) : (∫⁻ ω, f ω ∂μ) < ∞ :=
   by
   apply IsFiniteMeasure.lintegral_lt_top_of_bounded_to_eNNReal
@@ -323,67 +355,70 @@ theorem MeasureTheory.lintegral_lt_top_of_bounded_continuous_to_nNReal (μ : Mea
     ext
     simp only [Real.coe_toNNReal', max_eq_left_iff, Subtype.coe_mk, coe_nndist]
   rwa [Eq] at key 
-#align measure_theory.lintegral_lt_top_of_bounded_continuous_to_nnreal MeasureTheory.lintegral_lt_top_of_bounded_continuous_to_nNReal
+#align measure_theory.lintegral_lt_top_of_bounded_continuous_to_nnreal MeasureTheory.lintegral_lt_top_of_boundedContinuous_to_nnreal
 
 @[simp]
-theorem testAgainstNn_coe_eq {μ : FiniteMeasure Ω} {f : Ω →ᵇ ℝ≥0} :
-    (μ.testAgainstNn f : ℝ≥0∞) = ∫⁻ ω, f ω ∂(μ : Measure Ω) :=
-  ENNReal.coe_toNNReal (lintegral_lt_top_of_bounded_continuous_to_nNReal _ f).Ne
-#align measure_theory.finite_measure.test_against_nn_coe_eq MeasureTheory.FiniteMeasure.testAgainstNn_coe_eq
+theorem testAgainstNN_coe_eq {μ : FiniteMeasure Ω} {f : Ω →ᵇ ℝ≥0} :
+    (μ.testAgainstNN f : ℝ≥0∞) = ∫⁻ ω, f ω ∂(μ : Measure Ω) :=
+  ENNReal.coe_toNNReal (lintegral_lt_top_of_boundedContinuous_to_nnreal _ f).Ne
+#align measure_theory.finite_measure.test_against_nn_coe_eq MeasureTheory.FiniteMeasure.testAgainstNN_coe_eq
 
-theorem testAgainstNn_const (μ : FiniteMeasure Ω) (c : ℝ≥0) :
-    μ.testAgainstNn (BoundedContinuousFunction.const Ω c) = c * μ.mass := by
+theorem testAgainstNN_const (μ : FiniteMeasure Ω) (c : ℝ≥0) :
+    μ.testAgainstNN (BoundedContinuousFunction.const Ω c) = c * μ.mass := by
   simp [← ENNReal.coe_eq_coe]
-#align measure_theory.finite_measure.test_against_nn_const MeasureTheory.FiniteMeasure.testAgainstNn_const
+#align measure_theory.finite_measure.test_against_nn_const MeasureTheory.FiniteMeasure.testAgainstNN_const
 
-theorem testAgainstNn_mono (μ : FiniteMeasure Ω) {f g : Ω →ᵇ ℝ≥0} (f_le_g : (f : Ω → ℝ≥0) ≤ g) :
-    μ.testAgainstNn f ≤ μ.testAgainstNn g :=
+theorem testAgainstNN_mono (μ : FiniteMeasure Ω) {f g : Ω →ᵇ ℝ≥0} (f_le_g : (f : Ω → ℝ≥0) ≤ g) :
+    μ.testAgainstNN f ≤ μ.testAgainstNN g :=
   by
   simp only [← ENNReal.coe_le_coe, test_against_nn_coe_eq]
   exact lintegral_mono fun ω => ENNReal.coe_mono (f_le_g ω)
-#align measure_theory.finite_measure.test_against_nn_mono MeasureTheory.FiniteMeasure.testAgainstNn_mono
+#align measure_theory.finite_measure.test_against_nn_mono MeasureTheory.FiniteMeasure.testAgainstNN_mono
 
 @[simp]
-theorem testAgainstNn_zero (μ : FiniteMeasure Ω) : μ.testAgainstNn 0 = 0 := by
+theorem testAgainstNN_zero (μ : FiniteMeasure Ω) : μ.testAgainstNN 0 = 0 := by
   simpa only [MulZeroClass.zero_mul] using μ.test_against_nn_const 0
-#align measure_theory.finite_measure.test_against_nn_zero MeasureTheory.FiniteMeasure.testAgainstNn_zero
+#align measure_theory.finite_measure.test_against_nn_zero MeasureTheory.FiniteMeasure.testAgainstNN_zero
 
+#print MeasureTheory.FiniteMeasure.testAgainstNN_one /-
 @[simp]
-theorem testAgainstNn_one (μ : FiniteMeasure Ω) : μ.testAgainstNn 1 = μ.mass :=
+theorem testAgainstNN_one (μ : FiniteMeasure Ω) : μ.testAgainstNN 1 = μ.mass :=
   by
   simp only [test_against_nn, coe_one, Pi.one_apply, ENNReal.coe_one, lintegral_one]
   rfl
-#align measure_theory.finite_measure.test_against_nn_one MeasureTheory.FiniteMeasure.testAgainstNn_one
+#align measure_theory.finite_measure.test_against_nn_one MeasureTheory.FiniteMeasure.testAgainstNN_one
+-/
 
 @[simp]
-theorem Zero.testAgainstNn_apply (f : Ω →ᵇ ℝ≥0) : (0 : FiniteMeasure Ω).testAgainstNn f = 0 := by
+theorem MeasureTheory.FiniteMeasure.zero_testAgainstNN_apply (f : Ω →ᵇ ℝ≥0) :
+    (0 : FiniteMeasure Ω).testAgainstNN f = 0 := by
   simp only [test_against_nn, coe_zero, lintegral_zero_measure, ENNReal.zero_toNNReal]
-#align measure_theory.finite_measure.zero.test_against_nn_apply MeasureTheory.FiniteMeasure.Zero.testAgainstNn_apply
+#align measure_theory.finite_measure.zero.test_against_nn_apply MeasureTheory.FiniteMeasure.zero_testAgainstNN_apply
 
-theorem Zero.testAgainstNn : (0 : FiniteMeasure Ω).testAgainstNn = 0 := by funext;
-  simp only [zero.test_against_nn_apply, Pi.zero_apply]
-#align measure_theory.finite_measure.zero.test_against_nn MeasureTheory.FiniteMeasure.Zero.testAgainstNn
+theorem MeasureTheory.FiniteMeasure.zero_testAgainstNN : (0 : FiniteMeasure Ω).testAgainstNN = 0 :=
+  by funext; simp only [zero.test_against_nn_apply, Pi.zero_apply]
+#align measure_theory.finite_measure.zero.test_against_nn MeasureTheory.FiniteMeasure.zero_testAgainstNN
 
 @[simp]
-theorem smul_testAgainstNn_apply (c : ℝ≥0) (μ : FiniteMeasure Ω) (f : Ω →ᵇ ℝ≥0) :
-    (c • μ).testAgainstNn f = c • μ.testAgainstNn f := by
+theorem smul_testAgainstNN_apply (c : ℝ≥0) (μ : FiniteMeasure Ω) (f : Ω →ᵇ ℝ≥0) :
+    (c • μ).testAgainstNN f = c • μ.testAgainstNN f := by
   simp only [test_against_nn, coe_smul, smul_eq_mul, ← ENNReal.smul_toNNReal, ENNReal.smul_def,
     lintegral_smul_measure]
-#align measure_theory.finite_measure.smul_test_against_nn_apply MeasureTheory.FiniteMeasure.smul_testAgainstNn_apply
+#align measure_theory.finite_measure.smul_test_against_nn_apply MeasureTheory.FiniteMeasure.smul_testAgainstNN_apply
 
 variable [OpensMeasurableSpace Ω]
 
-theorem testAgainstNn_add (μ : FiniteMeasure Ω) (f₁ f₂ : Ω →ᵇ ℝ≥0) :
-    μ.testAgainstNn (f₁ + f₂) = μ.testAgainstNn f₁ + μ.testAgainstNn f₂ :=
+theorem testAgainstNN_add (μ : FiniteMeasure Ω) (f₁ f₂ : Ω →ᵇ ℝ≥0) :
+    μ.testAgainstNN (f₁ + f₂) = μ.testAgainstNN f₁ + μ.testAgainstNN f₂ :=
   by
   simp only [← ENNReal.coe_eq_coe, BoundedContinuousFunction.coe_add, ENNReal.coe_add, Pi.add_apply,
     test_against_nn_coe_eq]
-  exact lintegral_add_left (BoundedContinuousFunction.Nnreal.to_eNNReal_comp_measurable _) _
-#align measure_theory.finite_measure.test_against_nn_add MeasureTheory.FiniteMeasure.testAgainstNn_add
+  exact lintegral_add_left (BoundedContinuousFunction.NNReal.coe_ennreal_comp_measurable _) _
+#align measure_theory.finite_measure.test_against_nn_add MeasureTheory.FiniteMeasure.testAgainstNN_add
 
-theorem testAgainstNn_smul [IsScalarTower R ℝ≥0 ℝ≥0] [PseudoMetricSpace R] [Zero R]
+theorem testAgainstNN_smul [IsScalarTower R ℝ≥0 ℝ≥0] [PseudoMetricSpace R] [Zero R]
     [BoundedSMul R ℝ≥0] (μ : FiniteMeasure Ω) (c : R) (f : Ω →ᵇ ℝ≥0) :
-    μ.testAgainstNn (c • f) = c • μ.testAgainstNn f :=
+    μ.testAgainstNN (c • f) = c • μ.testAgainstNN f :=
   by
   simp only [← ENNReal.coe_eq_coe, BoundedContinuousFunction.coe_smul, test_against_nn_coe_eq,
     ENNReal.coe_smul]
@@ -391,11 +426,11 @@ theorem testAgainstNn_smul [IsScalarTower R ℝ≥0 ℝ≥0] [PseudoMetricSpace
     smul_eq_mul]
   exact
     @lintegral_const_mul _ _ (μ : Measure Ω) (c • 1) _
-      (BoundedContinuousFunction.Nnreal.to_eNNReal_comp_measurable f)
-#align measure_theory.finite_measure.test_against_nn_smul MeasureTheory.FiniteMeasure.testAgainstNn_smul
+      (BoundedContinuousFunction.NNReal.coe_ennreal_comp_measurable f)
+#align measure_theory.finite_measure.test_against_nn_smul MeasureTheory.FiniteMeasure.testAgainstNN_smul
 
-theorem testAgainstNn_lipschitz_estimate (μ : FiniteMeasure Ω) (f g : Ω →ᵇ ℝ≥0) :
-    μ.testAgainstNn f ≤ μ.testAgainstNn g + nndist f g * μ.mass :=
+theorem testAgainstNN_lipschitz_estimate (μ : FiniteMeasure Ω) (f g : Ω →ᵇ ℝ≥0) :
+    μ.testAgainstNN f ≤ μ.testAgainstNN g + nndist f g * μ.mass :=
   by
   simp only [← μ.test_against_nn_const (nndist f g), ← test_against_nn_add, ← ENNReal.coe_le_coe,
     BoundedContinuousFunction.coe_add, const_apply, ENNReal.coe_add, Pi.add_apply,
@@ -411,10 +446,10 @@ theorem testAgainstNn_lipschitz_estimate (μ : FiniteMeasure Ω) (f g : Ω →
   have le : (f ω : ℝ≥0∞) ≤ (g ω : ℝ≥0∞) + nndist f g := by rw [← ENNReal.coe_add];
     exact ENNReal.coe_mono le'
   rwa [coe_nnreal_ennreal_nndist] at le 
-#align measure_theory.finite_measure.test_against_nn_lipschitz_estimate MeasureTheory.FiniteMeasure.testAgainstNn_lipschitz_estimate
+#align measure_theory.finite_measure.test_against_nn_lipschitz_estimate MeasureTheory.FiniteMeasure.testAgainstNN_lipschitz_estimate
 
-theorem testAgainstNn_lipschitz (μ : FiniteMeasure Ω) :
-    LipschitzWith μ.mass fun f : Ω →ᵇ ℝ≥0 => μ.testAgainstNn f :=
+theorem testAgainstNN_lipschitz (μ : FiniteMeasure Ω) :
+    LipschitzWith μ.mass fun f : Ω →ᵇ ℝ≥0 => μ.testAgainstNN f :=
   by
   rw [lipschitzWith_iff_dist_le_mul]
   intro f₁ f₂
@@ -432,46 +467,46 @@ theorem testAgainstNn_lipschitz (μ : FiniteMeasure Ω) :
     suffices ↑(μ.test_against_nn f₁) ≤ ↑(μ.test_against_nn f₂) + ↑μ.mass * dist f₁ f₂ by linarith
     have key := NNReal.coe_mono key'
     rwa [NNReal.coe_add, NNReal.coe_mul] at key 
-#align measure_theory.finite_measure.test_against_nn_lipschitz MeasureTheory.FiniteMeasure.testAgainstNn_lipschitz
+#align measure_theory.finite_measure.test_against_nn_lipschitz MeasureTheory.FiniteMeasure.testAgainstNN_lipschitz
 
 /-- Finite measures yield elements of the `weak_dual` of bounded continuous nonnegative
 functions via `measure_theory.finite_measure.test_against_nn`, i.e., integration. -/
-def toWeakDualBcnn (μ : FiniteMeasure Ω) : WeakDual ℝ≥0 (Ω →ᵇ ℝ≥0)
+def toWeakDualBCNN (μ : FiniteMeasure Ω) : WeakDual ℝ≥0 (Ω →ᵇ ℝ≥0)
     where
-  toFun f := μ.testAgainstNn f
-  map_add' := testAgainstNn_add μ
-  map_smul' := testAgainstNn_smul μ
-  cont := μ.testAgainstNn_lipschitz.Continuous
-#align measure_theory.finite_measure.to_weak_dual_bcnn MeasureTheory.FiniteMeasure.toWeakDualBcnn
+  toFun f := μ.testAgainstNN f
+  map_add' := testAgainstNN_add μ
+  map_smul' := testAgainstNN_smul μ
+  cont := μ.testAgainstNN_lipschitz.Continuous
+#align measure_theory.finite_measure.to_weak_dual_bcnn MeasureTheory.FiniteMeasure.toWeakDualBCNN
 
 @[simp]
-theorem coe_toWeakDualBcnn (μ : FiniteMeasure Ω) : ⇑μ.toWeakDualBcnn = μ.testAgainstNn :=
+theorem coe_toWeakDualBCNN (μ : FiniteMeasure Ω) : ⇑μ.toWeakDualBCNN = μ.testAgainstNN :=
   rfl
-#align measure_theory.finite_measure.coe_to_weak_dual_bcnn MeasureTheory.FiniteMeasure.coe_toWeakDualBcnn
+#align measure_theory.finite_measure.coe_to_weak_dual_bcnn MeasureTheory.FiniteMeasure.coe_toWeakDualBCNN
 
 @[simp]
-theorem toWeakDualBcnn_apply (μ : FiniteMeasure Ω) (f : Ω →ᵇ ℝ≥0) :
-    μ.toWeakDualBcnn f = (∫⁻ x, f x ∂(μ : Measure Ω)).toNNReal :=
+theorem toWeakDualBCNN_apply (μ : FiniteMeasure Ω) (f : Ω →ᵇ ℝ≥0) :
+    μ.toWeakDualBCNN f = (∫⁻ x, f x ∂(μ : Measure Ω)).toNNReal :=
   rfl
-#align measure_theory.finite_measure.to_weak_dual_bcnn_apply MeasureTheory.FiniteMeasure.toWeakDualBcnn_apply
+#align measure_theory.finite_measure.to_weak_dual_bcnn_apply MeasureTheory.FiniteMeasure.toWeakDualBCNN_apply
 
 /-- The topology of weak convergence on `measure_theory.finite_measure Ω` is inherited (induced)
 from the weak-* topology on `weak_dual ℝ≥0 (Ω →ᵇ ℝ≥0)` via the function
 `measure_theory.finite_measure.to_weak_dual_bcnn`. -/
 instance : TopologicalSpace (FiniteMeasure Ω) :=
-  TopologicalSpace.induced toWeakDualBcnn inferInstance
+  TopologicalSpace.induced toWeakDualBCNN inferInstance
 
-theorem toWeakDualBcnn_continuous : Continuous (@toWeakDualBcnn Ω _ _ _) :=
+theorem toWeakDualBCNN_continuous : Continuous (@toWeakDualBCNN Ω _ _ _) :=
   continuous_induced_dom
-#align measure_theory.finite_measure.to_weak_dual_bcnn_continuous MeasureTheory.FiniteMeasure.toWeakDualBcnn_continuous
+#align measure_theory.finite_measure.to_weak_dual_bcnn_continuous MeasureTheory.FiniteMeasure.toWeakDualBCNN_continuous
 
 /- Integration of (nonnegative bounded continuous) test functions against finite Borel measures
 depends continuously on the measure. -/
-theorem continuous_testAgainstNn_eval (f : Ω →ᵇ ℝ≥0) :
-    Continuous fun μ : FiniteMeasure Ω => μ.testAgainstNn f :=
+theorem continuous_testAgainstNN_eval (f : Ω →ᵇ ℝ≥0) :
+    Continuous fun μ : FiniteMeasure Ω => μ.testAgainstNN f :=
   (by apply (WeakBilin.eval_continuous _ _).comp to_weak_dual_bcnn_continuous :
-    Continuous ((fun φ : WeakDual ℝ≥0 (Ω →ᵇ ℝ≥0) => φ f) ∘ toWeakDualBcnn))
-#align measure_theory.finite_measure.continuous_test_against_nn_eval MeasureTheory.FiniteMeasure.continuous_testAgainstNn_eval
+    Continuous ((fun φ : WeakDual ℝ≥0 (Ω →ᵇ ℝ≥0) => φ f) ∘ toWeakDualBCNN))
+#align measure_theory.finite_measure.continuous_test_against_nn_eval MeasureTheory.FiniteMeasure.continuous_testAgainstNN_eval
 
 /-- The total mass of a finite measure depends continuously on the measure. -/
 theorem continuous_mass : Continuous fun μ : FiniteMeasure Ω => μ.mass := by
@@ -486,36 +521,36 @@ theorem Filter.Tendsto.mass {γ : Type _} {F : Filter γ} {μs : γ → FiniteMe
 
 theorem tendsto_iff_weak_star_tendsto {γ : Type _} {F : Filter γ} {μs : γ → FiniteMeasure Ω}
     {μ : FiniteMeasure Ω} :
-    Tendsto μs F (𝓝 μ) ↔ Tendsto (fun i => (μs i).toWeakDualBcnn) F (𝓝 μ.toWeakDualBcnn) :=
+    Tendsto μs F (𝓝 μ) ↔ Tendsto (fun i => (μs i).toWeakDualBCNN) F (𝓝 μ.toWeakDualBCNN) :=
   Inducing.tendsto_nhds_iff ⟨rfl⟩
 #align measure_theory.finite_measure.tendsto_iff_weak_star_tendsto MeasureTheory.FiniteMeasure.tendsto_iff_weak_star_tendsto
 
-theorem tendsto_iff_forall_toWeakDualBcnn_tendsto {γ : Type _} {F : Filter γ}
+theorem tendsto_iff_forall_toWeakDualBCNN_tendsto {γ : Type _} {F : Filter γ}
     {μs : γ → FiniteMeasure Ω} {μ : FiniteMeasure Ω} :
     Tendsto μs F (𝓝 μ) ↔
-      ∀ f : Ω →ᵇ ℝ≥0, Tendsto (fun i => (μs i).toWeakDualBcnn f) F (𝓝 (μ.toWeakDualBcnn f)) :=
+      ∀ f : Ω →ᵇ ℝ≥0, Tendsto (fun i => (μs i).toWeakDualBCNN f) F (𝓝 (μ.toWeakDualBCNN f)) :=
   by rw [tendsto_iff_weak_star_tendsto, tendsto_iff_forall_eval_tendsto_topDualPairing]; rfl
-#align measure_theory.finite_measure.tendsto_iff_forall_to_weak_dual_bcnn_tendsto MeasureTheory.FiniteMeasure.tendsto_iff_forall_toWeakDualBcnn_tendsto
+#align measure_theory.finite_measure.tendsto_iff_forall_to_weak_dual_bcnn_tendsto MeasureTheory.FiniteMeasure.tendsto_iff_forall_toWeakDualBCNN_tendsto
 
-theorem tendsto_iff_forall_testAgainstNn_tendsto {γ : Type _} {F : Filter γ}
+theorem tendsto_iff_forall_testAgainstNN_tendsto {γ : Type _} {F : Filter γ}
     {μs : γ → FiniteMeasure Ω} {μ : FiniteMeasure Ω} :
     Tendsto μs F (𝓝 μ) ↔
-      ∀ f : Ω →ᵇ ℝ≥0, Tendsto (fun i => (μs i).testAgainstNn f) F (𝓝 (μ.testAgainstNn f)) :=
+      ∀ f : Ω →ᵇ ℝ≥0, Tendsto (fun i => (μs i).testAgainstNN f) F (𝓝 (μ.testAgainstNN f)) :=
   by rw [finite_measure.tendsto_iff_forall_to_weak_dual_bcnn_tendsto]; rfl
-#align measure_theory.finite_measure.tendsto_iff_forall_test_against_nn_tendsto MeasureTheory.FiniteMeasure.tendsto_iff_forall_testAgainstNn_tendsto
+#align measure_theory.finite_measure.tendsto_iff_forall_test_against_nn_tendsto MeasureTheory.FiniteMeasure.tendsto_iff_forall_testAgainstNN_tendsto
 
 /-- If the total masses of finite measures tend to zero, then the measures tend to
 zero. This formulation concerns the associated functionals on bounded continuous
 nonnegative test functions. See `finite_measure.tendsto_zero_of_tendsto_zero_mass` for
 a formulation stating the weak convergence of measures. -/
-theorem tendsto_zero_testAgainstNn_of_tendsto_zero_mass {γ : Type _} {F : Filter γ}
+theorem tendsto_zero_testAgainstNN_of_tendsto_zero_mass {γ : Type _} {F : Filter γ}
     {μs : γ → FiniteMeasure Ω} (mass_lim : Tendsto (fun i => (μs i).mass) F (𝓝 0)) (f : Ω →ᵇ ℝ≥0) :
-    Tendsto (fun i => (μs i).testAgainstNn f) F (𝓝 0) :=
+    Tendsto (fun i => (μs i).testAgainstNN f) F (𝓝 0) :=
   by
   apply tendsto_iff_dist_tendsto_zero.mpr
-  have obs := fun i => (μs i).testAgainstNn_lipschitz_estimate f 0
+  have obs := fun i => (μs i).testAgainstNN_lipschitz_estimate f 0
   simp_rw [test_against_nn_zero, zero_add] at obs 
-  simp_rw [show ∀ i, dist ((μs i).testAgainstNn f) 0 = (μs i).testAgainstNn f by
+  simp_rw [show ∀ i, dist ((μs i).testAgainstNN f) 0 = (μs i).testAgainstNN f by
       simp only [dist_nndist, NNReal.nndist_zero_eq_val', eq_self_iff_true, imp_true_iff]]
   refine' squeeze_zero (fun i => NNReal.coe_nonneg _) obs _
   simp_rw [NNReal.coe_mul]
@@ -525,7 +560,7 @@ theorem tendsto_zero_testAgainstNn_of_tendsto_zero_mass {γ : Type _} {F : Filte
     exact (nnreal.continuous_coe.tendsto 0).comp mass_lim
   have key := tendsto_mul.comp lim_pair
   rwa [MulZeroClass.mul_zero] at key 
-#align measure_theory.finite_measure.tendsto_zero_test_against_nn_of_tendsto_zero_mass MeasureTheory.FiniteMeasure.tendsto_zero_testAgainstNn_of_tendsto_zero_mass
+#align measure_theory.finite_measure.tendsto_zero_test_against_nn_of_tendsto_zero_mass MeasureTheory.FiniteMeasure.tendsto_zero_testAgainstNN_of_tendsto_zero_mass
 
 /-- If the total masses of finite measures tend to zero, then the measures tend to zero. -/
 theorem tendsto_zero_of_tendsto_zero_mass {γ : Type _} {F : Filter γ} {μs : γ → FiniteMeasure Ω}
@@ -617,17 +652,17 @@ This formulation assumes:
 A related result using `measure_theory.lintegral` for integration is
 `measure_theory.finite_measure.tendsto_lintegral_nn_filter_of_le_const`.
 -/
-theorem tendsto_testAgainstNn_filter_of_le_const {ι : Type _} {L : Filter ι}
+theorem tendsto_testAgainstNN_filter_of_le_const {ι : Type _} {L : Filter ι}
     [L.IsCountablyGenerated] {μ : FiniteMeasure Ω} {fs : ι → Ω →ᵇ ℝ≥0} {c : ℝ≥0}
     (fs_le_const : ∀ᶠ i in L, ∀ᵐ ω : Ω ∂(μ : Measure Ω), fs i ω ≤ c) {f : Ω →ᵇ ℝ≥0}
     (fs_lim : ∀ᵐ ω : Ω ∂(μ : Measure Ω), Tendsto (fun i => fs i ω) L (𝓝 (f ω))) :
-    Tendsto (fun i => μ.testAgainstNn (fs i)) L (𝓝 (μ.testAgainstNn f)) :=
+    Tendsto (fun i => μ.testAgainstNN (fs i)) L (𝓝 (μ.testAgainstNN f)) :=
   by
   apply
     (ENNReal.tendsto_toNNReal
         (lintegral_lt_top_of_bounded_continuous_to_nnreal (μ : Measure Ω) f).Ne).comp
   exact tendsto_lintegral_nn_filter_of_le_const μ fs_le_const fs_lim
-#align measure_theory.finite_measure.tendsto_test_against_nn_filter_of_le_const MeasureTheory.FiniteMeasure.tendsto_testAgainstNn_filter_of_le_const
+#align measure_theory.finite_measure.tendsto_test_against_nn_filter_of_le_const MeasureTheory.FiniteMeasure.tendsto_testAgainstNN_filter_of_le_const
 
 /-- A bounded convergence theorem for a finite measure:
 If a sequence of bounded continuous non-negative functions are uniformly bounded by a constant and
@@ -640,14 +675,14 @@ Related results:
  * `measure_theory.finite_measure.tendsto_lintegral_nn_of_le_const`:
    using `measure_theory.lintegral` for integration.
 -/
-theorem tendsto_testAgainstNn_of_le_const {μ : FiniteMeasure Ω} {fs : ℕ → Ω →ᵇ ℝ≥0} {c : ℝ≥0}
+theorem tendsto_testAgainstNN_of_le_const {μ : FiniteMeasure Ω} {fs : ℕ → Ω →ᵇ ℝ≥0} {c : ℝ≥0}
     (fs_le_const : ∀ n ω, fs n ω ≤ c) {f : Ω →ᵇ ℝ≥0}
     (fs_lim : ∀ ω, Tendsto (fun n => fs n ω) atTop (𝓝 (f ω))) :
-    Tendsto (fun n => μ.testAgainstNn (fs n)) atTop (𝓝 (μ.testAgainstNn f)) :=
-  tendsto_testAgainstNn_filter_of_le_const
+    Tendsto (fun n => μ.testAgainstNN (fs n)) atTop (𝓝 (μ.testAgainstNN f)) :=
+  tendsto_testAgainstNN_filter_of_le_const
     (eventually_of_forall fun n => eventually_of_forall (fs_le_const n))
     (eventually_of_forall fs_lim)
-#align measure_theory.finite_measure.tendsto_test_against_nn_of_le_const MeasureTheory.FiniteMeasure.tendsto_testAgainstNn_of_le_const
+#align measure_theory.finite_measure.tendsto_test_against_nn_of_le_const MeasureTheory.FiniteMeasure.tendsto_testAgainstNN_of_le_const
 
 end FiniteMeasureBoundedConvergence
 
@@ -663,15 +698,15 @@ condition that the integrals of all bounded continuous real-valued functions con
 
 variable {Ω : Type _} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω]
 
-theorem integrable_of_bounded_continuous_to_nNReal (μ : Measure Ω) [IsFiniteMeasure μ]
+theorem integrable_of_boundedContinuous_to_nnreal (μ : Measure Ω) [IsFiniteMeasure μ]
     (f : Ω →ᵇ ℝ≥0) : Integrable ((coe : ℝ≥0 → ℝ) ∘ ⇑f) μ :=
   by
   refine' ⟨(nnreal.continuous_coe.comp f.continuous).Measurable.AEStronglyMeasurable, _⟩
   simp only [has_finite_integral, NNReal.nnnorm_eq]
   exact lintegral_lt_top_of_bounded_continuous_to_nnreal _ f
-#align measure_theory.finite_measure.integrable_of_bounded_continuous_to_nnreal MeasureTheory.FiniteMeasure.integrable_of_bounded_continuous_to_nNReal
+#align measure_theory.finite_measure.integrable_of_bounded_continuous_to_nnreal MeasureTheory.FiniteMeasure.integrable_of_boundedContinuous_to_nnreal
 
-theorem integrable_of_bounded_continuous_to_real (μ : Measure Ω) [IsFiniteMeasure μ] (f : Ω →ᵇ ℝ) :
+theorem integrable_of_boundedContinuous_to_real (μ : Measure Ω) [IsFiniteMeasure μ] (f : Ω →ᵇ ℝ) :
     Integrable (⇑f) μ :=
   by
   refine' ⟨f.continuous.measurable.ae_strongly_measurable, _⟩
@@ -684,7 +719,7 @@ theorem integrable_of_bounded_continuous_to_real (μ : Measure Ω) [IsFiniteMeas
   · exact ENNReal.ofReal_lt_top
   · exact aux ▸ integrable_of_bounded_continuous_to_nnreal μ f.nnnorm
   · exact eventually_of_forall fun ω => norm_nonneg (f ω)
-#align measure_theory.finite_measure.integrable_of_bounded_continuous_to_real MeasureTheory.FiniteMeasure.integrable_of_bounded_continuous_to_real
+#align measure_theory.finite_measure.integrable_of_bounded_continuous_to_real MeasureTheory.FiniteMeasure.integrable_of_boundedContinuous_to_real
 
 theorem BoundedContinuousFunction.integral_eq_integral_nnrealPart_sub (μ : Measure Ω)
     [IsFiniteMeasure μ] (f : Ω →ᵇ ℝ) :
@@ -693,11 +728,11 @@ theorem BoundedContinuousFunction.integral_eq_integral_nnrealPart_sub (μ : Meas
     integrable_of_bounded_continuous_to_nnreal]
 #align bounded_continuous_function.integral_eq_integral_nnreal_part_sub BoundedContinuousFunction.integral_eq_integral_nnrealPart_sub
 
-theorem lintegral_lt_top_of_bounded_continuous_to_real {Ω : Type _} [MeasurableSpace Ω]
+theorem lintegral_lt_top_of_boundedContinuous_to_real {Ω : Type _} [MeasurableSpace Ω]
     [TopologicalSpace Ω] (μ : Measure Ω) [IsFiniteMeasure μ] (f : Ω →ᵇ ℝ) :
     (∫⁻ ω, ENNReal.ofReal (f ω) ∂μ) < ∞ :=
-  lintegral_lt_top_of_bounded_continuous_to_nNReal _ f.nnrealPart
-#align measure_theory.finite_measure.lintegral_lt_top_of_bounded_continuous_to_real MeasureTheory.FiniteMeasure.lintegral_lt_top_of_bounded_continuous_to_real
+  lintegral_lt_top_of_boundedContinuous_to_nnreal _ f.nnrealPart
+#align measure_theory.finite_measure.lintegral_lt_top_of_bounded_continuous_to_real MeasureTheory.FiniteMeasure.lintegral_lt_top_of_boundedContinuous_to_real
 
 theorem tendsto_of_forall_integral_tendsto {γ : Type _} {F : Filter γ} {μs : γ → FiniteMeasure Ω}
     {μ : FiniteMeasure Ω}
@@ -728,7 +763,7 @@ theorem tendsto_of_forall_integral_tendsto {γ : Type _} {F : Filter γ} {μs :
   simpa only [← aux, ← auxs] using h f₀
 #align measure_theory.finite_measure.tendsto_of_forall_integral_tendsto MeasureTheory.FiniteMeasure.tendsto_of_forall_integral_tendsto
 
-theorem BoundedContinuousFunction.Nnreal.toReal_lintegral_eq_integral (f : Ω →ᵇ ℝ≥0)
+theorem BoundedContinuousFunction.NNReal.toReal_lintegral_eq_integral (f : Ω →ᵇ ℝ≥0)
     (μ : Measure Ω) : (∫⁻ x, (f x : ℝ≥0∞) ∂μ).toReal = ∫ x, f x ∂μ :=
   by
   rw [integral_eq_lintegral_of_nonneg_ae _
@@ -736,7 +771,7 @@ theorem BoundedContinuousFunction.Nnreal.toReal_lintegral_eq_integral (f : Ω 
   · simp only [ENNReal.ofReal_coe_nnreal]
   · apply eventually_of_forall
     simp only [Pi.zero_apply, NNReal.zero_le_coe, imp_true_iff]
-#align bounded_continuous_function.nnreal.to_real_lintegral_eq_integral BoundedContinuousFunction.Nnreal.toReal_lintegral_eq_integral
+#align bounded_continuous_function.nnreal.to_real_lintegral_eq_integral BoundedContinuousFunction.NNReal.toReal_lintegral_eq_integral
 
 /-- A characterization of weak convergence in terms of integrals of bounded continuous
 real-valued functions. -/
@@ -765,7 +800,7 @@ theorem tendsto_iff_forall_integral_tendsto {γ : Type _} {F : Filter γ} {μs :
       (ENNReal.toReal ∘ fun i : γ => ∫⁻ x : Ω, ↑(g x) ∂(μs i : Measure Ω)) = fun i : γ =>
         (∫⁻ x : Ω, ↑(g x) ∂(μs i : Measure Ω)).toReal :=
     fun _ => rfl
-  simp_rw [aux, BoundedContinuousFunction.Nnreal.toReal_lintegral_eq_integral] at tends_pos
+  simp_rw [aux, BoundedContinuousFunction.NNReal.toReal_lintegral_eq_integral] at tends_pos
     tends_neg 
   exact tendsto.sub tends_pos tends_neg
 #align measure_theory.finite_measure.tendsto_iff_forall_integral_tendsto MeasureTheory.FiniteMeasure.tendsto_iff_forall_integral_tendsto
diff --git a/Mathbin/MeasureTheory/Measure/Haar/NormedSpace.lean b/Mathbin/MeasureTheory/Measure/Haar/NormedSpace.lean
index 0e49536892..e7d1f5caa3 100644
--- a/Mathbin/MeasureTheory/Measure/Haar/NormedSpace.lean
+++ b/Mathbin/MeasureTheory/Measure/Haar/NormedSpace.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn, Sébastien Gouëzel
 
 ! This file was ported from Lean 3 source module measure_theory.measure.haar.normed_space
-! leanprover-community/mathlib commit b84aee748341da06a6d78491367e2c0e9f15e8a5
+! leanprover-community/mathlib commit 36938f775671ff28bea1c0310f1608e4afbb22e0
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -14,6 +14,9 @@ import Mathbin.MeasureTheory.Integral.Bochner
 /-!
 # Basic properties of Haar measures on real vector spaces
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 -/
 
 
diff --git a/Mathbin/MeasureTheory/Measure/Lebesgue/EqHaar.lean b/Mathbin/MeasureTheory/Measure/Lebesgue/EqHaar.lean
index a5411ee499..5ad1accb72 100644
--- a/Mathbin/MeasureTheory/Measure/Lebesgue/EqHaar.lean
+++ b/Mathbin/MeasureTheory/Measure/Lebesgue/EqHaar.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn, Sébastien Gouëzel
 
 ! This file was ported from Lean 3 source module measure_theory.measure.lebesgue.eq_haar
-! leanprover-community/mathlib commit fd5edc43dc4f10b85abfe544b88f82cf13c5f844
+! leanprover-community/mathlib commit 36938f775671ff28bea1c0310f1608e4afbb22e0
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -18,6 +18,9 @@ import Mathbin.MeasureTheory.Measure.Doubling
 /-!
 # Relationship between the Haar and Lebesgue measures
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We prove that the Haar measure and Lebesgue measure are equal on `ℝ` and on `ℝ^ι`, in
 `measure_theory.add_haar_measure_eq_volume` and `measure_theory.add_haar_measure_eq_volume_pi`.
 
diff --git a/Mathbin/MeasureTheory/Measure/ProbabilityMeasure.lean b/Mathbin/MeasureTheory/Measure/ProbabilityMeasure.lean
index aee8a9e268..7e1abc1530 100644
--- a/Mathbin/MeasureTheory/Measure/ProbabilityMeasure.lean
+++ b/Mathbin/MeasureTheory/Measure/ProbabilityMeasure.lean
@@ -209,10 +209,10 @@ theorem toFiniteMeasure_nonzero (μ : ProbabilityMeasure Ω) : μ.toFiniteMeasur
 
 variable [TopologicalSpace Ω] [OpensMeasurableSpace Ω]
 
-theorem testAgainstNn_lipschitz (μ : ProbabilityMeasure Ω) :
-    LipschitzWith 1 fun f : Ω →ᵇ ℝ≥0 => μ.toFiniteMeasure.testAgainstNn f :=
-  μ.mass_toFiniteMeasure ▸ μ.toFiniteMeasure.testAgainstNn_lipschitz
-#align measure_theory.probability_measure.test_against_nn_lipschitz MeasureTheory.ProbabilityMeasure.testAgainstNn_lipschitz
+theorem testAgainstNN_lipschitz (μ : ProbabilityMeasure Ω) :
+    LipschitzWith 1 fun f : Ω →ᵇ ℝ≥0 => μ.toFiniteMeasure.testAgainstNN f :=
+  μ.mass_toFiniteMeasure ▸ μ.toFiniteMeasure.testAgainstNN_lipschitz
+#align measure_theory.probability_measure.test_against_nn_lipschitz MeasureTheory.ProbabilityMeasure.testAgainstNN_lipschitz
 
 /-- The topology of weak convergence on `measure_theory.probability_measure Ω`. This is inherited
 (induced) from the topology of weak convergence of finite measures via the inclusion
@@ -228,31 +228,31 @@ theorem toFiniteMeasure_continuous :
 /-- Probability measures yield elements of the `weak_dual` of bounded continuous nonnegative
 functions via `measure_theory.finite_measure.test_against_nn`, i.e., integration. -/
 def toWeakDualBcnn : ProbabilityMeasure Ω → WeakDual ℝ≥0 (Ω →ᵇ ℝ≥0) :=
-  FiniteMeasure.toWeakDualBcnn ∘ toFiniteMeasure
+  FiniteMeasure.toWeakDualBCNN ∘ toFiniteMeasure
 #align measure_theory.probability_measure.to_weak_dual_bcnn MeasureTheory.ProbabilityMeasure.toWeakDualBcnn
 
 @[simp]
 theorem coe_toWeakDualBcnn (μ : ProbabilityMeasure Ω) :
-    ⇑μ.toWeakDualBcnn = μ.toFiniteMeasure.testAgainstNn :=
+    ⇑μ.toWeakDualBCNN = μ.toFiniteMeasure.testAgainstNN :=
   rfl
 #align measure_theory.probability_measure.coe_to_weak_dual_bcnn MeasureTheory.ProbabilityMeasure.coe_toWeakDualBcnn
 
 @[simp]
 theorem toWeakDualBcnn_apply (μ : ProbabilityMeasure Ω) (f : Ω →ᵇ ℝ≥0) :
-    μ.toWeakDualBcnn f = (∫⁻ ω, f ω ∂(μ : Measure Ω)).toNNReal :=
+    μ.toWeakDualBCNN f = (∫⁻ ω, f ω ∂(μ : Measure Ω)).toNNReal :=
   rfl
 #align measure_theory.probability_measure.to_weak_dual_bcnn_apply MeasureTheory.ProbabilityMeasure.toWeakDualBcnn_apply
 
-theorem toWeakDualBcnn_continuous : Continuous fun μ : ProbabilityMeasure Ω => μ.toWeakDualBcnn :=
-  FiniteMeasure.toWeakDualBcnn_continuous.comp toFiniteMeasure_continuous
+theorem toWeakDualBcnn_continuous : Continuous fun μ : ProbabilityMeasure Ω => μ.toWeakDualBCNN :=
+  FiniteMeasure.toWeakDualBCNN_continuous.comp toFiniteMeasure_continuous
 #align measure_theory.probability_measure.to_weak_dual_bcnn_continuous MeasureTheory.ProbabilityMeasure.toWeakDualBcnn_continuous
 
 /- Integration of (nonnegative bounded continuous) test functions against Borel probability
 measures depends continuously on the measure. -/
-theorem continuous_testAgainstNn_eval (f : Ω →ᵇ ℝ≥0) :
-    Continuous fun μ : ProbabilityMeasure Ω => μ.toFiniteMeasure.testAgainstNn f :=
-  (FiniteMeasure.continuous_testAgainstNn_eval f).comp toFiniteMeasure_continuous
-#align measure_theory.probability_measure.continuous_test_against_nn_eval MeasureTheory.ProbabilityMeasure.continuous_testAgainstNn_eval
+theorem continuous_testAgainstNN_eval (f : Ω →ᵇ ℝ≥0) :
+    Continuous fun μ : ProbabilityMeasure Ω => μ.toFiniteMeasure.testAgainstNN f :=
+  (FiniteMeasure.continuous_testAgainstNN_eval f).comp toFiniteMeasure_continuous
+#align measure_theory.probability_measure.continuous_test_against_nn_eval MeasureTheory.ProbabilityMeasure.continuous_testAgainstNN_eval
 
 -- The canonical mapping from probability measures to finite measures is an embedding.
 theorem toFiniteMeasure_embedding (Ω : Type _) [MeasurableSpace Ω] [TopologicalSpace Ω]
@@ -398,46 +398,46 @@ theorem average_eq_integral_normalize {E : Type _} [NormedAddCommGroup E] [Norme
 
 variable [TopologicalSpace Ω]
 
-theorem testAgainstNn_eq_mass_mul (f : Ω →ᵇ ℝ≥0) :
-    μ.testAgainstNn f = μ.mass * μ.normalize.toFiniteMeasure.testAgainstNn f :=
+theorem testAgainstNN_eq_mass_mul (f : Ω →ᵇ ℝ≥0) :
+    μ.testAgainstNN f = μ.mass * μ.normalize.toFiniteMeasure.testAgainstNN f :=
   by
   nth_rw 1 [μ.self_eq_mass_smul_normalize]
   rw [μ.normalize.to_finite_measure.smul_test_against_nn_apply μ.mass f, smul_eq_mul]
-#align measure_theory.finite_measure.test_against_nn_eq_mass_mul MeasureTheory.FiniteMeasure.testAgainstNn_eq_mass_mul
+#align measure_theory.finite_measure.test_against_nn_eq_mass_mul MeasureTheory.FiniteMeasure.testAgainstNN_eq_mass_mul
 
-theorem normalize_testAgainstNn (nonzero : μ ≠ 0) (f : Ω →ᵇ ℝ≥0) :
-    μ.normalize.toFiniteMeasure.testAgainstNn f = μ.mass⁻¹ * μ.testAgainstNn f := by
+theorem normalize_testAgainstNN (nonzero : μ ≠ 0) (f : Ω →ᵇ ℝ≥0) :
+    μ.normalize.toFiniteMeasure.testAgainstNN f = μ.mass⁻¹ * μ.testAgainstNN f := by
   simp [μ.test_against_nn_eq_mass_mul, μ.mass_nonzero_iff.mpr nonzero]
-#align measure_theory.finite_measure.normalize_test_against_nn MeasureTheory.FiniteMeasure.normalize_testAgainstNn
+#align measure_theory.finite_measure.normalize_test_against_nn MeasureTheory.FiniteMeasure.normalize_testAgainstNN
 
 variable [OpensMeasurableSpace Ω]
 
 variable {μ}
 
-theorem tendsto_testAgainstNn_of_tendsto_normalize_testAgainstNn_of_tendsto_mass {γ : Type _}
+theorem tendsto_testAgainstNN_of_tendsto_normalize_testAgainstNN_of_tendsto_mass {γ : Type _}
     {F : Filter γ} {μs : γ → FiniteMeasure Ω}
     (μs_lim : Tendsto (fun i => (μs i).normalize) F (𝓝 μ.normalize))
     (mass_lim : Tendsto (fun i => (μs i).mass) F (𝓝 μ.mass)) (f : Ω →ᵇ ℝ≥0) :
-    Tendsto (fun i => (μs i).testAgainstNn f) F (𝓝 (μ.testAgainstNn f)) :=
+    Tendsto (fun i => (μs i).testAgainstNN f) F (𝓝 (μ.testAgainstNN f)) :=
   by
   by_cases h_mass : μ.mass = 0
   · simp only [μ.mass_zero_iff.mp h_mass, zero.test_against_nn_apply, zero.mass,
       eq_self_iff_true] at *
     exact tendsto_zero_test_against_nn_of_tendsto_zero_mass mass_lim f
-  simp_rw [fun i => (μs i).testAgainstNn_eq_mass_mul f, μ.test_against_nn_eq_mass_mul f]
+  simp_rw [fun i => (μs i).testAgainstNN_eq_mass_mul f, μ.test_against_nn_eq_mass_mul f]
   rw [probability_measure.tendsto_nhds_iff_to_finite_measures_tendsto_nhds] at μs_lim 
   rw [tendsto_iff_forall_test_against_nn_tendsto] at μs_lim 
   have lim_pair :
-    tendsto (fun i => (⟨(μs i).mass, (μs i).normalize.toFiniteMeasure.testAgainstNn f⟩ : ℝ≥0 × ℝ≥0))
+    tendsto (fun i => (⟨(μs i).mass, (μs i).normalize.toFiniteMeasure.testAgainstNN f⟩ : ℝ≥0 × ℝ≥0))
       F (𝓝 ⟨μ.mass, μ.normalize.to_finite_measure.test_against_nn f⟩) :=
     (Prod.tendsto_iff _ _).mpr ⟨mass_lim, μs_lim f⟩
   exact tendsto_mul.comp lim_pair
-#align measure_theory.finite_measure.tendsto_test_against_nn_of_tendsto_normalize_test_against_nn_of_tendsto_mass MeasureTheory.FiniteMeasure.tendsto_testAgainstNn_of_tendsto_normalize_testAgainstNn_of_tendsto_mass
+#align measure_theory.finite_measure.tendsto_test_against_nn_of_tendsto_normalize_test_against_nn_of_tendsto_mass MeasureTheory.FiniteMeasure.tendsto_testAgainstNN_of_tendsto_normalize_testAgainstNN_of_tendsto_mass
 
-theorem tendsto_normalize_testAgainstNn_of_tendsto {γ : Type _} {F : Filter γ}
+theorem tendsto_normalize_testAgainstNN_of_tendsto {γ : Type _} {F : Filter γ}
     {μs : γ → FiniteMeasure Ω} (μs_lim : Tendsto μs F (𝓝 μ)) (nonzero : μ ≠ 0) (f : Ω →ᵇ ℝ≥0) :
-    Tendsto (fun i => (μs i).normalize.toFiniteMeasure.testAgainstNn f) F
-      (𝓝 (μ.normalize.toFiniteMeasure.testAgainstNn f)) :=
+    Tendsto (fun i => (μs i).normalize.toFiniteMeasure.testAgainstNN f) F
+      (𝓝 (μ.normalize.toFiniteMeasure.testAgainstNN f)) :=
   by
   have lim_mass := μs_lim.mass
   have aux : {(0 : ℝ≥0)}ᶜ ∈ 𝓝 μ.mass :=
@@ -448,21 +448,21 @@ theorem tendsto_normalize_testAgainstNn_of_tendsto {γ : Type _} {F : Filter γ}
     exact lim_mass aux
   have eve :
     ∀ᶠ i in F,
-      (μs i).normalize.toFiniteMeasure.testAgainstNn f = (μs i).mass⁻¹ * (μs i).testAgainstNn f :=
+      (μs i).normalize.toFiniteMeasure.testAgainstNN f = (μs i).mass⁻¹ * (μs i).testAgainstNN f :=
     by
     filter_upwards [eventually_iff.mp eventually_nonzero]
     intro i hi
     apply normalize_test_against_nn _ hi
   simp_rw [tendsto_congr' eve, μ.normalize_test_against_nn nonzero]
   have lim_pair :
-    tendsto (fun i => (⟨(μs i).mass⁻¹, (μs i).testAgainstNn f⟩ : ℝ≥0 × ℝ≥0)) F
+    tendsto (fun i => (⟨(μs i).mass⁻¹, (μs i).testAgainstNN f⟩ : ℝ≥0 × ℝ≥0)) F
       (𝓝 ⟨μ.mass⁻¹, μ.test_against_nn f⟩) :=
     by
     refine' (Prod.tendsto_iff _ _).mpr ⟨_, _⟩
     · exact (continuous_on_inv₀.continuous_at aux).Tendsto.comp lim_mass
     · exact tendsto_iff_forall_test_against_nn_tendsto.mp μs_lim f
   exact tendsto_mul.comp lim_pair
-#align measure_theory.finite_measure.tendsto_normalize_test_against_nn_of_tendsto MeasureTheory.FiniteMeasure.tendsto_normalize_testAgainstNn_of_tendsto
+#align measure_theory.finite_measure.tendsto_normalize_test_against_nn_of_tendsto MeasureTheory.FiniteMeasure.tendsto_normalize_testAgainstNN_of_tendsto
 
 /-- If the normalized versions of finite measures converge weakly and their total masses
 also converge, then the finite measures themselves converge weakly. -/
diff --git a/Mathbin/NumberTheory/Liouville/Measure.lean b/Mathbin/NumberTheory/Liouville/Measure.lean
index b87a449705..75972921b0 100644
--- a/Mathbin/NumberTheory/Liouville/Measure.lean
+++ b/Mathbin/NumberTheory/Liouville/Measure.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 number_theory.liouville.measure
-! leanprover-community/mathlib commit fd5edc43dc4f10b85abfe544b88f82cf13c5f844
+! leanprover-community/mathlib commit 36938f775671ff28bea1c0310f1608e4afbb22e0
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -16,6 +16,9 @@ import Mathbin.Analysis.PSeries
 /-!
 # Volume of the set of Liouville numbers
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we prove that the set of Liouville numbers with exponent (irrationality measure)
 strictly greater than two is a set of Lebesuge measure zero, see
 `volume_Union_set_of_liouville_with`.
diff --git a/Mathbin/RingTheory/DedekindDomain/Ideal.lean b/Mathbin/RingTheory/DedekindDomain/Ideal.lean
index 9972ce3b33..f494fe18cd 100644
--- a/Mathbin/RingTheory/DedekindDomain/Ideal.lean
+++ b/Mathbin/RingTheory/DedekindDomain/Ideal.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenji Nakagawa, Anne Baanen, Filippo A. E. Nuccio
 
 ! This file was ported from Lean 3 source module ring_theory.dedekind_domain.ideal
-! leanprover-community/mathlib commit 2bbc7e3884ba234309d2a43b19144105a753292e
+! leanprover-community/mathlib commit 36938f775671ff28bea1c0310f1608e4afbb22e0
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -20,6 +20,9 @@ import Mathbin.RingTheory.ChainOfDivisors
 /-!
 # Dedekind domains and ideals
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file, we show a ring is a Dedekind domain iff all fractional ideals are invertible.
 Then we prove some results on the unique factorization monoid structure of the ideals.
 
diff --git a/Mathbin/RingTheory/Polynomial/Bernstein.lean b/Mathbin/RingTheory/Polynomial/Bernstein.lean
index fd0334d577..df95f811e2 100644
--- a/Mathbin/RingTheory/Polynomial/Bernstein.lean
+++ b/Mathbin/RingTheory/Polynomial/Bernstein.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 
 ! This file was ported from Lean 3 source module ring_theory.polynomial.bernstein
-! leanprover-community/mathlib commit bbeb185db4ccee8ed07dc48449414ebfa39cb821
+! leanprover-community/mathlib commit 36938f775671ff28bea1c0310f1608e4afbb22e0
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -18,6 +18,9 @@ import Mathbin.Data.MvPolynomial.Pderiv
 /-!
 # Bernstein polynomials
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 The definition of the Bernstein polynomials
 ```
 bernstein_polynomial (R : Type*) [comm_ring R] (n ν : ℕ) : R[X] :=
diff --git a/Mathbin/RingTheory/WittVector/Defs.lean b/Mathbin/RingTheory/WittVector/Defs.lean
index 1fec24e65e..bb50b7705a 100644
--- a/Mathbin/RingTheory/WittVector/Defs.lean
+++ b/Mathbin/RingTheory/WittVector/Defs.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin, Robert Y. Lewis
 
 ! This file was ported from Lean 3 source module ring_theory.witt_vector.defs
-! leanprover-community/mathlib commit f1944b30c97c5eb626e498307dec8b022a05bd0a
+! leanprover-community/mathlib commit 36938f775671ff28bea1c0310f1608e4afbb22e0
 ! 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.WittVector.StructurePolynomial
 /-!
 # Witt vectors
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we define the type of `p`-typical Witt vectors and ring operations on it.
 The ring axioms are verified in `ring_theory/witt_vector/basic.lean`.
 
diff --git a/Mathbin/RingTheory/WittVector/StructurePolynomial.lean b/Mathbin/RingTheory/WittVector/StructurePolynomial.lean
index 1d62f01cf9..4034f4f1d2 100644
--- a/Mathbin/RingTheory/WittVector/StructurePolynomial.lean
+++ b/Mathbin/RingTheory/WittVector/StructurePolynomial.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin, Robert Y. Lewis
 
 ! This file was ported from Lean 3 source module ring_theory.witt_vector.structure_polynomial
-! leanprover-community/mathlib commit 70fd9563a21e7b963887c9360bd29b2393e6225a
+! leanprover-community/mathlib commit 36938f775671ff28bea1c0310f1608e4afbb22e0
 ! 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.WittVector.WittPolynomial
 /-!
 # Witt structure polynomials
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we prove the main theorem that makes the whole theory of Witt vectors work.
 Briefly, consider a polynomial `Φ : mv_polynomial idx ℤ` over the integers,
 with polynomials variables indexed by an arbitrary type `idx`.
diff --git a/Mathbin/Topology/ContinuousFunction/StoneWeierstrass.lean b/Mathbin/Topology/ContinuousFunction/StoneWeierstrass.lean
index 0711d0b06f..0f23fc1de8 100644
--- a/Mathbin/Topology/ContinuousFunction/StoneWeierstrass.lean
+++ b/Mathbin/Topology/ContinuousFunction/StoneWeierstrass.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison, Heather Macbeth
 
 ! This file was ported from Lean 3 source module topology.continuous_function.stone_weierstrass
-! leanprover-community/mathlib commit 16e59248c0ebafabd5d071b1cd41743eb8698ffb
+! leanprover-community/mathlib commit 36938f775671ff28bea1c0310f1608e4afbb22e0
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -14,6 +14,9 @@ import Mathbin.Data.IsROrC.Basic
 /-!
 # The Stone-Weierstrass theorem
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 If a subalgebra `A` of `C(X, ℝ)`, where `X` is a compact topological space,
 separates points, then it is dense.
 
diff --git a/Mathbin/Topology/ContinuousFunction/Weierstrass.lean b/Mathbin/Topology/ContinuousFunction/Weierstrass.lean
index c4926ebcb2..fdeba0b18e 100644
--- a/Mathbin/Topology/ContinuousFunction/Weierstrass.lean
+++ b/Mathbin/Topology/ContinuousFunction/Weierstrass.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 
 ! This file was ported from Lean 3 source module topology.continuous_function.weierstrass
-! leanprover-community/mathlib commit 17ef379e997badd73e5eabb4d38f11919ab3c4b3
+! leanprover-community/mathlib commit 36938f775671ff28bea1c0310f1608e4afbb22e0
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -14,6 +14,9 @@ import Mathbin.Topology.Algebra.Algebra
 /-!
 # The Weierstrass approximation theorem for continuous functions on `[a,b]`
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We've already proved the Weierstrass approximation theorem
 in the sense that we've shown that the Bernstein approximations
 to a continuous function on `[0,1]` converge uniformly.
diff --git a/Mathbin/Topology/Order/Hom/Esakia.lean b/Mathbin/Topology/Order/Hom/Esakia.lean
index 994f98bb7c..089de3c8ba 100644
--- a/Mathbin/Topology/Order/Hom/Esakia.lean
+++ b/Mathbin/Topology/Order/Hom/Esakia.lean
@@ -40,19 +40,24 @@ open Function
 
 variable {F α β γ δ : Type _}
 
+#print PseudoEpimorphism /-
 /-- The type of pseudo-epimorphisms, aka p-morphisms, aka bounded maps, from `α` to `β`. -/
 structure PseudoEpimorphism (α β : Type _) [Preorder α] [Preorder β] extends α →o β where
   exists_map_eq_of_map_le' ⦃a : α⦄ ⦃b : β⦄ : to_fun a ≤ b → ∃ c, a ≤ c ∧ to_fun c = b
 #align pseudo_epimorphism PseudoEpimorphism
+-/
 
+#print EsakiaHom /-
 /-- The type of Esakia morphisms, aka continuous pseudo-epimorphisms, from `α` to `β`. -/
 structure EsakiaHom (α β : Type _) [TopologicalSpace α] [Preorder α] [TopologicalSpace β]
     [Preorder β] extends α →Co β where
   exists_map_eq_of_map_le' ⦃a : α⦄ ⦃b : β⦄ : to_fun a ≤ b → ∃ c, a ≤ c ∧ to_fun c = b
 #align esakia_hom EsakiaHom
+-/
 
 section
 
+#print PseudoEpimorphismClass /-
 /-- `pseudo_epimorphism_class F α β` states that `F` is a type of `⊔`-preserving morphisms.
 
 You should extend this class when you extend `pseudo_epimorphism`. -/
@@ -60,7 +65,9 @@ class PseudoEpimorphismClass (F : Type _) (α β : outParam <| Type _) [Preorder
     [Preorder β] extends RelHomClass F ((· ≤ ·) : α → α → Prop) ((· ≤ ·) : β → β → Prop) where
   exists_map_eq_of_map_le (f : F) ⦃a : α⦄ ⦃b : β⦄ : f a ≤ b → ∃ c, a ≤ c ∧ f c = b
 #align pseudo_epimorphism_class PseudoEpimorphismClass
+-/
 
+#print EsakiaHomClass /-
 /-- `esakia_hom_class F α β` states that `F` is a type of lattice morphisms.
 
 You should extend this class when you extend `esakia_hom`. -/
@@ -68,6 +75,7 @@ class EsakiaHomClass (F : Type _) (α β : outParam <| Type _) [TopologicalSpace
     [TopologicalSpace β] [Preorder β] extends ContinuousOrderHomClass F α β where
   exists_map_eq_of_map_le (f : F) ⦃a : α⦄ ⦃b : β⦄ : f a ≤ b → ∃ c, a ≤ c ∧ f c = b
 #align esakia_hom_class EsakiaHomClass
+-/
 
 end
 
@@ -83,6 +91,7 @@ instance (priority := 100) PseudoEpimorphismClass.toTopHomClass [PartialOrder α
       rw [← top_le_iff.1 h.1, h.2] }
 #align pseudo_epimorphism_class.to_top_hom_class PseudoEpimorphismClass.toTopHomClass
 
+#print OrderIsoClass.toPseudoEpimorphismClass /-
 -- See note [lower instance priority]
 instance (priority := 100) OrderIsoClass.toPseudoEpimorphismClass [Preorder α] [Preorder β]
     [OrderIsoClass F α β] : PseudoEpimorphismClass F α β :=
@@ -90,12 +99,15 @@ instance (priority := 100) OrderIsoClass.toPseudoEpimorphismClass [Preorder α]
     exists_map_eq_of_map_le := fun f a b h =>
       ⟨EquivLike.inv f b, (le_map_inv_iff f).2 h, EquivLike.right_inv _ _⟩ }
 #align order_iso_class.to_pseudo_epimorphism_class OrderIsoClass.toPseudoEpimorphismClass
+-/
 
+#print EsakiaHomClass.toPseudoEpimorphismClass /-
 -- See note [lower instance priority]
 instance (priority := 100) EsakiaHomClass.toPseudoEpimorphismClass [TopologicalSpace α] [Preorder α]
     [TopologicalSpace β] [Preorder β] [EsakiaHomClass F α β] : PseudoEpimorphismClass F α β :=
   { ‹EsakiaHomClass F α β› with }
 #align esakia_hom_class.to_pseudo_epimorphism_class EsakiaHomClass.toPseudoEpimorphismClass
+-/
 
 instance [Preorder α] [Preorder β] [PseudoEpimorphismClass F α β] :
     CoeTC F (PseudoEpimorphism α β) :=
@@ -151,10 +163,12 @@ theorem copy_eq (f : PseudoEpimorphism α β) (f' : α → β) (h : f' = f) : f.
 
 variable (α)
 
+#print PseudoEpimorphism.id /-
 /-- `id` as a `pseudo_epimorphism`. -/
 protected def id : PseudoEpimorphism α α :=
   ⟨OrderHom.id, fun a b h => ⟨b, h, rfl⟩⟩
 #align pseudo_epimorphism.id PseudoEpimorphism.id
+-/
 
 instance : Inhabited (PseudoEpimorphism α α) :=
   ⟨PseudoEpimorphism.id α⟩
@@ -176,6 +190,7 @@ theorem id_apply (a : α) : PseudoEpimorphism.id α a = a :=
   rfl
 #align pseudo_epimorphism.id_apply PseudoEpimorphism.id_apply
 
+#print PseudoEpimorphism.comp /-
 /-- Composition of `pseudo_epimorphism`s as a `pseudo_epimorphism`. -/
 def comp (g : PseudoEpimorphism β γ) (f : PseudoEpimorphism α β) : PseudoEpimorphism α γ :=
   ⟨g.toOrderHom.comp f.toOrderHom, fun a b h₀ =>
@@ -184,6 +199,7 @@ def comp (g : PseudoEpimorphism β γ) (f : PseudoEpimorphism α β) : PseudoEpi
     obtain ⟨b, h₂, rfl⟩ := f.exists_map_eq_of_map_le' h₁
     exact ⟨b, h₂, rfl⟩⟩
 #align pseudo_epimorphism.comp PseudoEpimorphism.comp
+-/
 
 @[simp]
 theorem coe_comp (g : PseudoEpimorphism β γ) (f : PseudoEpimorphism α β) :
@@ -239,10 +255,12 @@ namespace EsakiaHom
 variable [TopologicalSpace α] [Preorder α] [TopologicalSpace β] [Preorder β] [TopologicalSpace γ]
   [Preorder γ] [TopologicalSpace δ] [Preorder δ]
 
+#print EsakiaHom.toPseudoEpimorphism /-
 /-- Reinterpret an `esakia_hom` as a `pseudo_epimorphism`. -/
 def toPseudoEpimorphism (f : EsakiaHom α β) : PseudoEpimorphism α β :=
   { f with }
 #align esakia_hom.to_pseudo_epimorphism EsakiaHom.toPseudoEpimorphism
+-/
 
 instance : EsakiaHomClass (EsakiaHom α β) α β
     where
@@ -285,10 +303,12 @@ theorem copy_eq (f : EsakiaHom α β) (f' : α → β) (h : f' = f) : f.copy f'
 
 variable (α)
 
+#print EsakiaHom.id /-
 /-- `id` as an `esakia_hom`. -/
 protected def id : EsakiaHom α α :=
   ⟨ContinuousOrderHom.id α, fun a b h => ⟨b, h, rfl⟩⟩
 #align esakia_hom.id EsakiaHom.id
+-/
 
 instance : Inhabited (EsakiaHom α α) :=
   ⟨EsakiaHom.id α⟩
@@ -316,6 +336,7 @@ theorem id_apply (a : α) : EsakiaHom.id α a = a :=
   rfl
 #align esakia_hom.id_apply EsakiaHom.id_apply
 
+#print EsakiaHom.comp /-
 /-- Composition of `esakia_hom`s as an `esakia_hom`. -/
 def comp (g : EsakiaHom β γ) (f : EsakiaHom α β) : EsakiaHom α γ :=
   ⟨g.toContinuousOrderHom.comp f.toContinuousOrderHom, fun a b h₀ =>
@@ -324,6 +345,7 @@ def comp (g : EsakiaHom β γ) (f : EsakiaHom α β) : EsakiaHom α γ :=
     obtain ⟨b, h₂, rfl⟩ := f.exists_map_eq_of_map_le' h₁
     exact ⟨b, h₂, rfl⟩⟩
 #align esakia_hom.comp EsakiaHom.comp
+-/
 
 @[simp]
 theorem coe_comp (g : EsakiaHom β γ) (f : EsakiaHom α β) : (g.comp f : α → γ) = g ∘ f :=
diff --git a/README.md b/README.md
index 59bceedfea..1dff1a0d83 100644
--- a/README.md
+++ b/README.md
@@ -1,4 +1,4 @@
-Tracking mathlib commit: [`a3209ddf94136d36e5e5c624b10b2a347cc9d090`](https://github.com/leanprover-community/mathlib/commit/a3209ddf94136d36e5e5c624b10b2a347cc9d090)
+Tracking mathlib commit: [`58a272265b5e05f258161260dd2c5d247213cbd3`](https://github.com/leanprover-community/mathlib/commit/58a272265b5e05f258161260dd2c5d247213cbd3)
 
 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 b8a7dce790..28757c7043 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -4,15 +4,15 @@
  [{"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "a89979832ffaf69de8cfbf3384e601562b4105e0",
+    "rev": "cf4d1bf58e325227f7961b337fb62937b0f7d0f7",
     "name": "lean3port",
-    "inputRev?": "a89979832ffaf69de8cfbf3384e601562b4105e0"}},
+    "inputRev?": "cf4d1bf58e325227f7961b337fb62937b0f7d0f7"}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "e0ca1161c0494df5793db83cd31488e3d2e558f7",
+    "rev": "04a303a345f00c2b378600cb2f68c57b4f616cf3",
     "name": "mathlib",
-    "inputRev?": "e0ca1161c0494df5793db83cd31488e3d2e558f7"}},
+    "inputRev?": "04a303a345f00c2b378600cb2f68c57b4f616cf3"}},
   {"git":
    {"url": "https://github.com/gebner/quote4",
     "subDir?": null,
diff --git a/lakefile.lean b/lakefile.lean
index 9b17078d70..c437e2b149 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-07-01"
+def tag : String := "nightly-2023-06-07-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"@"a89979832ffaf69de8cfbf3384e601562b4105e0"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"cf4d1bf58e325227f7961b337fb62937b0f7d0f7"
 
 @[default_target]
 lean_lib Mathbin where
diff --git a/upstream-rev b/upstream-rev
index 1dc5ecdb4a..f22a7e64dc 100644
--- a/upstream-rev
+++ b/upstream-rev
@@ -1 +1 @@
-a3209ddf94136d36e5e5c624b10b2a347cc9d090
+58a272265b5e05f258161260dd2c5d247213cbd3