diff --git a/Mathbin/CategoryTheory/Bicategory/Coherence.lean b/Mathbin/CategoryTheory/Bicategory/Coherence.lean
index baa7f3b87a..621b1d524a 100644
--- a/Mathbin/CategoryTheory/Bicategory/Coherence.lean
+++ b/Mathbin/CategoryTheory/Bicategory/Coherence.lean
@@ -56,20 +56,25 @@ namespace FreeBicategory
 
 variable {B : Type u} [Quiver.{v + 1} B]
 
+#print CategoryTheory.FreeBicategory.inclusionPathAux /-
 /-- Auxiliary definition for `inclusion_path`. -/
 @[simp]
 def inclusionPathAux {a : B} : ∀ {b : B}, Path a b → Hom a b
   | _, nil => Hom.id a
   | _, cons p f => (inclusion_path_aux p).comp (Hom.of f)
 #align category_theory.free_bicategory.inclusion_path_aux CategoryTheory.FreeBicategory.inclusionPathAux
+-/
 
+#print CategoryTheory.FreeBicategory.inclusionPath /-
 /-- The discrete category on the paths includes into the category of 1-morphisms in the free
 bicategory.
 -/
 def inclusionPath (a b : B) : Discrete (Path.{v + 1} a b) ⥤ Hom a b :=
   Discrete.functor inclusionPathAux
 #align category_theory.free_bicategory.inclusion_path CategoryTheory.FreeBicategory.inclusionPath
+-/
 
+#print CategoryTheory.FreeBicategory.preinclusion /-
 /-- The inclusion from the locally discrete bicategory on the path category into the free bicategory
 as a prelax functor. This will be promoted to a pseudofunctor after proving the coherence theorem.
 See `inclusion`.
@@ -81,6 +86,7 @@ def preinclusion (B : Type u) [Quiver.{v + 1} B] :
   map a b := (inclusionPath a b).obj
   zipWith a b f g η := (inclusionPath a b).map η
 #align category_theory.free_bicategory.preinclusion CategoryTheory.FreeBicategory.preinclusion
+-/
 
 @[simp]
 theorem preinclusion_obj (a : B) : (preinclusion B).obj a = a :=
@@ -96,6 +102,7 @@ theorem preinclusion_map₂ {a b : B} (f g : Discrete (Path.{v + 1} a b)) (η :
   exact (inclusion_path a b).map_id _
 #align category_theory.free_bicategory.preinclusion_map₂ CategoryTheory.FreeBicategory.preinclusion_map₂
 
+#print CategoryTheory.FreeBicategory.normalizeAux /-
 /-- The normalization of the composition of `p : path a b` and `f : hom b c`.
 `p` will eventually be taken to be `nil` and we then get the normalization
 of `f` alone, but the auxiliary `p` is necessary for Lean to accept the definition of
@@ -107,6 +114,7 @@ def normalizeAux {a : B} : ∀ {b c : B}, Path a b → Hom b c → Path a c
   | _, _, p, hom.id b => p
   | _, _, p, hom.comp f g => normalize_aux (normalize_aux p f) g
 #align category_theory.free_bicategory.normalize_aux CategoryTheory.FreeBicategory.normalizeAux
+-/
 
 /-
 We may define
@@ -140,6 +148,7 @@ def normalizeIso {a : B} :
     (α_ _ _ _).symm ≪≫ whiskerRightIso (normalize_iso p f) g ≪≫ normalize_iso (normalizeAux p f) g
 #align category_theory.free_bicategory.normalize_iso CategoryTheory.FreeBicategory.normalizeIso
 
+#print CategoryTheory.FreeBicategory.normalizeAux_congr /-
 /-- Given a 2-morphism between `f` and `g` in the free bicategory, we have the equality
 `normalize_aux p f = normalize_aux p g`.
 -/
@@ -156,6 +165,7 @@ theorem normalizeAux_congr {a b c : B} (p : Path a b) {f g : Hom b c} (η : f 
   case whisker_right _ _ _ _ _ _ _ ih => funext; apply congr_arg₂ _ (congr_fun ih p) rfl
   all_goals funext; rfl
 #align category_theory.free_bicategory.normalize_aux_congr CategoryTheory.FreeBicategory.normalizeAux_congr
+-/
 
 /-- The 2-isomorphism `normalize_iso p f` is natural in `f`. -/
 theorem normalize_naturality {a b c : B} (p : Path a b) {f g : Hom b c} (η : f ⟶ g) :
@@ -183,6 +193,7 @@ theorem normalize_naturality {a b c : B} (p : Path a b) {f g : Hom b c} (η : f
   all_goals dsimp; dsimp [id_def, comp_def]; simp
 #align category_theory.free_bicategory.normalize_naturality CategoryTheory.FreeBicategory.normalize_naturality
 
+#print CategoryTheory.FreeBicategory.normalizeAux_nil_comp /-
 @[simp]
 theorem normalizeAux_nil_comp {a b c : B} (f : Hom a b) (g : Hom b c) :
     normalizeAux nil (f.comp g) = (normalizeAux nil f).comp (normalizeAux nil g) :=
@@ -192,7 +203,9 @@ theorem normalizeAux_nil_comp {a b c : B} (f : Hom a b) (g : Hom b c) :
   case of => rfl
   case comp _ _ _ g _ ihf ihg => erw [ihg (f.comp g), ihf f, ihg g, comp_assoc]
 #align category_theory.free_bicategory.normalize_aux_nil_comp CategoryTheory.FreeBicategory.normalizeAux_nil_comp
+-/
 
+#print CategoryTheory.FreeBicategory.normalize /-
 /-- The normalization pseudofunctor for the free bicategory on a quiver `B`. -/
 def normalize (B : Type u) [Quiver.{v + 1} B] :
     Pseudofunctor (FreeBicategory B) (LocallyDiscrete (Paths B))
@@ -203,7 +216,9 @@ def normalize (B : Type u) [Quiver.{v + 1} B] :
   map_id a := eqToIso <| Discrete.ext _ _ rfl
   map_comp a b c f g := eqToIso <| Discrete.ext _ _ <| normalizeAux_nil_comp f g
 #align category_theory.free_bicategory.normalize CategoryTheory.FreeBicategory.normalize
+-/
 
+#print CategoryTheory.FreeBicategory.normalizeUnitIso /-
 /-- Auxiliary definition for `normalize_equiv`. -/
 def normalizeUnitIso (a b : FreeBicategory B) :
     𝟭 (a ⟶ b) ≅ (normalize B).mapFunctor a b ⋙ inclusionPath a b :=
@@ -214,6 +229,7 @@ def normalizeUnitIso (a b : FreeBicategory B) :
       congr 1
       exact normalize_naturality nil η)
 #align category_theory.free_bicategory.normalize_unit_iso CategoryTheory.FreeBicategory.normalizeUnitIso
+-/
 
 /-- Normalization as an equivalence of categories. -/
 def normalizeEquiv (a b : B) : Hom a b ≌ Discrete (Path.{v + 1} a b) :=
@@ -221,10 +237,12 @@ def normalizeEquiv (a b : B) : Hom a b ≌ Discrete (Path.{v + 1} a b) :=
     (Discrete.natIso fun f => eqToIso (by induction f <;> induction f <;> tidy))
 #align category_theory.free_bicategory.normalize_equiv CategoryTheory.FreeBicategory.normalizeEquiv
 
+#print CategoryTheory.FreeBicategory.locally_thin /-
 /-- The coherence theorem for bicategories. -/
 instance locally_thin {a b : FreeBicategory B} : Quiver.IsThin (a ⟶ b) := fun _ _ =>
   ⟨fun η θ => (normalizeEquiv a b).Functor.map_injective (Subsingleton.elim _ _)⟩
 #align category_theory.free_bicategory.locally_thin CategoryTheory.FreeBicategory.locally_thin
+-/
 
 /-- Auxiliary definition for `inclusion`. -/
 def inclusionMapCompAux {a b : B} :
@@ -234,6 +252,7 @@ def inclusionMapCompAux {a b : B} :
   | _, f, cons g₁ g₂ => whiskerRightIso (inclusion_map_comp_aux f g₁) (Hom.of g₂) ≪≫ α_ _ _ _
 #align category_theory.free_bicategory.inclusion_map_comp_aux CategoryTheory.FreeBicategory.inclusionMapCompAux
 
+#print CategoryTheory.FreeBicategory.inclusion /-
 /-- The inclusion pseudofunctor from the locally discrete bicategory on the path category into the
 free bicategory.
 -/
@@ -245,6 +264,7 @@ def inclusion (B : Type u) [Quiver.{v + 1} B] :
     map_id := fun a => Iso.refl (𝟙 a)
     map_comp := fun a b c f g => inclusionMapCompAux f.as g.as }
 #align category_theory.free_bicategory.inclusion CategoryTheory.FreeBicategory.inclusion
+-/
 
 end FreeBicategory
 
diff --git a/Mathbin/Computability/Primrec.lean b/Mathbin/Computability/Primrec.lean
index 9ebe958e9c..ab0ca0e78a 100644
--- a/Mathbin/Computability/Primrec.lean
+++ b/Mathbin/Computability/Primrec.lean
@@ -1399,12 +1399,12 @@ instance array {n} : Primcodable (Array' n α) :=
   ofEquiv _ (Equiv.arrayEquivFin _ _)
 #align primcodable.array Primcodable.array
 
-section Ulower
+section ULower
 
 attribute [local instance 100] Encodable.decidableRangeEncode Encodable.decidableEqOfEncodable
 
 #print Primcodable.ulower /-
-instance ulower : Primcodable (Ulower α) :=
+instance ulower : Primcodable (ULower α) :=
   have : PrimrecPred fun n => Encodable.decode₂ α n ≠ none :=
     PrimrecPred.not
       (Primrec.eq.comp
@@ -1416,7 +1416,7 @@ instance ulower : Primcodable (Ulower α) :=
 #align primcodable.ulower Primcodable.ulower
 -/
 
-end Ulower
+end ULower
 
 end Primcodable
 
@@ -1471,14 +1471,14 @@ theorem option_get {f : α → Option β} {h : ∀ a, (f a).isSome} :
 -/
 
 #print Primrec.ulower_down /-
-theorem ulower_down : Primrec (Ulower.down : α → Ulower α) :=
+theorem ulower_down : Primrec (ULower.down : α → ULower α) :=
   letI : ∀ a, Decidable (a ∈ Set.range (encode : α → ℕ)) := decidable_range_encode _
   subtype_mk Primrec.encode
 #align primrec.ulower_down Primrec.ulower_down
 -/
 
 #print Primrec.ulower_up /-
-theorem ulower_up : Primrec (Ulower.up : Ulower α → α) :=
+theorem ulower_up : Primrec (ULower.up : ULower α → α) :=
   letI : ∀ a, Decidable (a ∈ Set.range (encode : α → ℕ)) := decidable_range_encode _
   option_get (primrec.decode₂.comp subtype_val)
 #align primrec.ulower_up Primrec.ulower_up
diff --git a/Mathbin/Computability/Reduce.lean b/Mathbin/Computability/Reduce.lean
index acfde24725..78dc6ab6f8 100644
--- a/Mathbin/Computability/Reduce.lean
+++ b/Mathbin/Computability/Reduce.lean
@@ -317,16 +317,16 @@ theorem OneOneEquiv.congr_right {α β γ} [Primcodable α] [Primcodable β] [Pr
   and_congr h.le_congr_right h.le_congr_left
 #align one_one_equiv.congr_right OneOneEquiv.congr_right
 
-#print Ulower.down_computable /-
+#print ULower.down_computable /-
 @[simp]
-theorem Ulower.down_computable {α} [Primcodable α] : (Ulower.equiv α).Computable :=
+theorem ULower.down_computable {α} [Primcodable α] : (ULower.equiv α).Computable :=
   ⟨Primrec.ulower_down.to_comp, Primrec.ulower_up.to_comp⟩
-#align ulower.down_computable Ulower.down_computable
+#align ulower.down_computable ULower.down_computable
 -/
 
 #print manyOneEquiv_up /-
-theorem manyOneEquiv_up {α} [Primcodable α] {p : α → Prop} : ManyOneEquiv (p ∘ Ulower.up) p :=
-  ManyOneEquiv.of_equiv Ulower.down_computable.symm
+theorem manyOneEquiv_up {α} [Primcodable α] {p : α → Prop} : ManyOneEquiv (p ∘ ULower.up) p :=
+  ManyOneEquiv.of_equiv ULower.down_computable.symm
 #align many_one_equiv_up manyOneEquiv_up
 -/
 
diff --git a/Mathbin/Logic/Encodable/Basic.lean b/Mathbin/Logic/Encodable/Basic.lean
index 7421bccf67..f5e932e188 100644
--- a/Mathbin/Logic/Encodable/Basic.lean
+++ b/Mathbin/Logic/Encodable/Basic.lean
@@ -592,85 +592,85 @@ instance : Countable ℕ+ :=
   Subtype.countable
 
 -- short-circuit instance search
-section Ulower
+section ULower
 
 attribute [local instance 100] Encodable.decidableRangeEncode
 
-#print Ulower /-
+#print ULower /-
 /-- `ulower α : Type` is an equivalent type in the lowest universe, given `encodable α`. -/
-def Ulower (α : Type _) [Encodable α] : Type :=
+def ULower (α : Type _) [Encodable α] : Type :=
   Set.range (Encodable.encode : α → ℕ)deriving DecidableEq, Encodable
-#align ulower Ulower
+#align ulower ULower
 -/
 
-end Ulower
+end ULower
 
-namespace Ulower
+namespace ULower
 
 variable (α : Type _) [Encodable α]
 
-#print Ulower.equiv /-
+#print ULower.equiv /-
 /-- The equivalence between the encodable type `α` and `ulower α : Type`. -/
-def equiv : α ≃ Ulower α :=
+def equiv : α ≃ ULower α :=
   Encodable.equivRangeEncode α
-#align ulower.equiv Ulower.equiv
+#align ulower.equiv ULower.equiv
 -/
 
 variable {α}
 
-#print Ulower.down /-
+#print ULower.down /-
 /-- Lowers an `a : α` into `ulower α`. -/
-def down (a : α) : Ulower α :=
+def down (a : α) : ULower α :=
   equiv α a
-#align ulower.down Ulower.down
+#align ulower.down ULower.down
 -/
 
-instance [Inhabited α] : Inhabited (Ulower α) :=
+instance [Inhabited α] : Inhabited (ULower α) :=
   ⟨down default⟩
 
-#print Ulower.up /-
+#print ULower.up /-
 /-- Lifts an `a : ulower α` into `α`. -/
-def up (a : Ulower α) : α :=
+def up (a : ULower α) : α :=
   (equiv α).symm a
-#align ulower.up Ulower.up
+#align ulower.up ULower.up
 -/
 
-#print Ulower.down_up /-
+#print ULower.down_up /-
 @[simp]
-theorem down_up {a : Ulower α} : down a.up = a :=
+theorem down_up {a : ULower α} : down a.up = a :=
   Equiv.right_inv _ _
-#align ulower.down_up Ulower.down_up
+#align ulower.down_up ULower.down_up
 -/
 
-#print Ulower.up_down /-
+#print ULower.up_down /-
 @[simp]
 theorem up_down {a : α} : (down a).up = a :=
   Equiv.left_inv _ _
-#align ulower.up_down Ulower.up_down
+#align ulower.up_down ULower.up_down
 -/
 
-#print Ulower.up_eq_up /-
+#print ULower.up_eq_up /-
 @[simp]
-theorem up_eq_up {a b : Ulower α} : a.up = b.up ↔ a = b :=
+theorem up_eq_up {a b : ULower α} : a.up = b.up ↔ a = b :=
   Equiv.apply_eq_iff_eq _
-#align ulower.up_eq_up Ulower.up_eq_up
+#align ulower.up_eq_up ULower.up_eq_up
 -/
 
-#print Ulower.down_eq_down /-
+#print ULower.down_eq_down /-
 @[simp]
 theorem down_eq_down {a b : α} : down a = down b ↔ a = b :=
   Equiv.apply_eq_iff_eq _
-#align ulower.down_eq_down Ulower.down_eq_down
+#align ulower.down_eq_down ULower.down_eq_down
 -/
 
-#print Ulower.ext /-
+#print ULower.ext /-
 @[ext]
-protected theorem ext {a b : Ulower α} : a.up = b.up → a = b :=
+protected theorem ext {a b : ULower α} : a.up = b.up → a = b :=
   up_eq_up.1
-#align ulower.ext Ulower.ext
+#align ulower.ext ULower.ext
 -/
 
-end Ulower
+end ULower
 
 /-
 Choice function for encodable types and decidable predicates.
diff --git a/Mathbin/Topology/Partial.lean b/Mathbin/Topology/Partial.lean
index 43e7f9e5a8..6627933b16 100644
--- a/Mathbin/Topology/Partial.lean
+++ b/Mathbin/Topology/Partial.lean
@@ -61,19 +61,19 @@ theorem ptendsto'_nhds {f : β →. α} {l : Filter β} {a : α} :
 
 variable [TopologicalSpace β]
 
-#print Pcontinuous /-
+#print PContinuous /-
 /-- Continuity of a partial function -/
-def Pcontinuous (f : α →. β) :=
+def PContinuous (f : α →. β) :=
   ∀ s, IsOpen s → IsOpen (f.Preimage s)
-#align pcontinuous Pcontinuous
+#align pcontinuous PContinuous
 -/
 
-theorem open_dom_of_pcontinuous {f : α →. β} (h : Pcontinuous f) : IsOpen f.Dom := by
+theorem open_dom_of_pcontinuous {f : α →. β} (h : PContinuous f) : IsOpen f.Dom := by
   rw [← PFun.preimage_univ] <;> exact h _ isOpen_univ
 #align open_dom_of_pcontinuous open_dom_of_pcontinuous
 
 theorem pcontinuous_iff' {f : α →. β} :
-    Pcontinuous f ↔ ∀ {x y} (h : y ∈ f x), Ptendsto' f (𝓝 x) (𝓝 y) :=
+    PContinuous f ↔ ∀ {x y} (h : y ∈ f x), Ptendsto' f (𝓝 x) (𝓝 y) :=
   by
   constructor
   · intro h x y h'
diff --git a/Mathbin/Topology/Sheaves/SheafOfFunctions.lean b/Mathbin/Topology/Sheaves/SheafOfFunctions.lean
index 2ad5867501..cbe1b9e0ab 100644
--- a/Mathbin/Topology/Sheaves/SheafOfFunctions.lean
+++ b/Mathbin/Topology/Sheaves/SheafOfFunctions.lean
@@ -49,6 +49,7 @@ open TopCat
 
 namespace TopCat.Presheaf
 
+#print TopCat.Presheaf.toTypes_isSheaf /-
 /-- We show that the presheaf of functions to a type `T`
 (no continuity assumptions, just plain functions)
 form a sheaf.
@@ -56,7 +57,7 @@ form a sheaf.
 In fact, the proof is identical when we do this for dependent functions to a type family `T`,
 so we do the more general case.
 -/
-theorem to_Types_isSheaf (T : X → Type u) : (presheafToTypes X T).IsSheaf :=
+theorem toTypes_isSheaf (T : X → Type u) : (presheafToTypes X T).IsSheaf :=
   isSheaf_of_isSheafUniqueGluing_types _ fun ι U sf hsf =>
     -- We use the sheaf condition in terms of unique gluing
   -- U is a family of open sets, indexed by `ι` and `sf` is a compatible family of sections.
@@ -88,32 +89,41 @@ theorem to_Types_isSheaf (T : X → Type u) : (presheafToTypes X T).IsSheaf :=
       convert congr_fun (ht (index x)) ⟨x.1, index_spec x⟩
       ext
       rfl
-#align Top.presheaf.to_Types_is_sheaf TopCat.Presheaf.to_Types_isSheaf
+#align Top.presheaf.to_Types_is_sheaf TopCat.Presheaf.toTypes_isSheaf
+-/
 
+#print TopCat.Presheaf.toType_isSheaf /-
 -- We verify that the non-dependent version is an immediate consequence:
 /-- The presheaf of not-necessarily-continuous functions to
 a target type `T` satsifies the sheaf condition.
 -/
-theorem to_Type_isSheaf (T : Type u) : (presheafToType X T).IsSheaf :=
-  to_Types_isSheaf X fun _ => T
-#align Top.presheaf.to_Type_is_sheaf TopCat.Presheaf.to_Type_isSheaf
+theorem toType_isSheaf (T : Type u) : (presheafToType X T).IsSheaf :=
+  toTypes_isSheaf X fun _ => T
+#align Top.presheaf.to_Type_is_sheaf TopCat.Presheaf.toType_isSheaf
+-/
 
 end TopCat.Presheaf
 
 namespace TopCat
 
+#print TopCat.sheafToTypes /-
 /-- The sheaf of not-necessarily-continuous functions on `X` with values in type family
 `T : X → Type u`.
 -/
 def sheafToTypes (T : X → Type u) : Sheaf (Type u) X :=
-  ⟨presheafToTypes X T, Presheaf.to_Types_isSheaf _ _⟩
+  ⟨presheafToTypes X T, Presheaf.toTypes_isSheaf _ _⟩
 #align Top.sheaf_to_Types TopCat.sheafToTypes
+-/
 
+/- warning: Top.sheaf_to_Type clashes with Top.sheafToType -> TopCat.sheafToType
+Case conversion may be inaccurate. Consider using '#align Top.sheaf_to_Type TopCat.sheafToTypeₓ'. -/
+#print TopCat.sheafToType /-
 /-- The sheaf of not-necessarily-continuous functions on `X` with values in a type `T`.
 -/
 def sheafToType (T : Type u) : Sheaf (Type u) X :=
-  ⟨presheafToType X T, Presheaf.to_Type_isSheaf _ _⟩
+  ⟨presheafToType X T, Presheaf.toType_isSheaf _ _⟩
 #align Top.sheaf_to_Type TopCat.sheafToType
+-/
 
 end TopCat
 
diff --git a/lake-manifest.json b/lake-manifest.json
index f1c4d3d7c5..20d3d57dd9 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": "c8949f21eec31d9c300443c86b8559d76e4c9d32",
+    "rev": "8a76c9bff932f4e52fa48562346af625ba53b599",
     "name": "lean3port",
-    "inputRev?": "c8949f21eec31d9c300443c86b8559d76e4c9d32"}},
+    "inputRev?": "8a76c9bff932f4e52fa48562346af625ba53b599"}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "63c31ccb8aab20a9c7bd01d193b124b50a1dc568",
+    "rev": "3e1d33f82e35a062c0d5281d323366789525b6e8",
     "name": "mathlib",
-    "inputRev?": "63c31ccb8aab20a9c7bd01d193b124b50a1dc568"}},
+    "inputRev?": "3e1d33f82e35a062c0d5281d323366789525b6e8"}},
   {"git":
    {"url": "https://github.com/gebner/quote4",
     "subDir?": null,
diff --git a/lakefile.lean b/lakefile.lean
index ecc68e9c8d..1af255cbd3 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-05-28-10"
+def tag : String := "nightly-2023-05-28-12"
 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"@"c8949f21eec31d9c300443c86b8559d76e4c9d32"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"8a76c9bff932f4e52fa48562346af625ba53b599"
 
 @[default_target]
 lean_lib Mathbin where