diff --git a/Mathbin/Algebra/Lie/OfAssociative.lean b/Mathbin/Algebra/Lie/OfAssociative.lean
index 9d0114f0e4..66b8e4f65c 100644
--- a/Mathbin/Algebra/Lie/OfAssociative.lean
+++ b/Mathbin/Algebra/Lie/OfAssociative.lean
@@ -213,11 +213,11 @@ theorem toLieHom_coe : f.toLieHom = ↑f :=
   rfl
 #align alg_hom.to_lie_hom_coe AlgHom.toLieHom_coe
 
-#print AlgHom.coe_to_lieHom /-
+#print AlgHom.coe_toLieHom /-
 @[simp]
-theorem coe_to_lieHom : ((f : A →ₗ⁅R⁆ B) : A → B) = f :=
+theorem coe_toLieHom : ((f : A →ₗ⁅R⁆ B) : A → B) = f :=
   rfl
-#align alg_hom.coe_to_lie_hom AlgHom.coe_to_lieHom
+#align alg_hom.coe_to_lie_hom AlgHom.coe_toLieHom
 -/
 
 #print AlgHom.toLieHom_apply /-
@@ -226,24 +226,24 @@ theorem toLieHom_apply (x : A) : f.toLieHom x = f x :=
 #align alg_hom.to_lie_hom_apply AlgHom.toLieHom_apply
 -/
 
-#print AlgHom.to_lieHom_id /-
+#print AlgHom.toLieHom_id /-
 @[simp]
-theorem to_lieHom_id : (AlgHom.id R A : A →ₗ⁅R⁆ A) = LieHom.id :=
+theorem toLieHom_id : (AlgHom.id R A : A →ₗ⁅R⁆ A) = LieHom.id :=
   rfl
-#align alg_hom.to_lie_hom_id AlgHom.to_lieHom_id
+#align alg_hom.to_lie_hom_id AlgHom.toLieHom_id
 -/
 
-#print AlgHom.to_lieHom_comp /-
+#print AlgHom.toLieHom_comp /-
 @[simp]
-theorem to_lieHom_comp : (g.comp f : A →ₗ⁅R⁆ C) = (g : B →ₗ⁅R⁆ C).comp (f : A →ₗ⁅R⁆ B) :=
+theorem toLieHom_comp : (g.comp f : A →ₗ⁅R⁆ C) = (g : B →ₗ⁅R⁆ C).comp (f : A →ₗ⁅R⁆ B) :=
   rfl
-#align alg_hom.to_lie_hom_comp AlgHom.to_lieHom_comp
+#align alg_hom.to_lie_hom_comp AlgHom.toLieHom_comp
 -/
 
-#print AlgHom.to_lieHom_injective /-
-theorem to_lieHom_injective {f g : A →ₐ[R] B} (h : (f : A →ₗ⁅R⁆ B) = (g : A →ₗ⁅R⁆ B)) : f = g := by
+#print AlgHom.toLieHom_injective /-
+theorem toLieHom_injective {f g : A →ₐ[R] B} (h : (f : A →ₗ⁅R⁆ B) = (g : A →ₗ⁅R⁆ B)) : f = g := by
   ext a; exact LieHom.congr_fun h a
-#align alg_hom.to_lie_hom_injective AlgHom.to_lieHom_injective
+#align alg_hom.to_lie_hom_injective AlgHom.toLieHom_injective
 -/
 
 end AlgHom
diff --git a/Mathbin/Algebra/Lie/UniversalEnveloping.lean b/Mathbin/Algebra/Lie/UniversalEnveloping.lean
index 7626e47dad..eb271fac7f 100644
--- a/Mathbin/Algebra/Lie/UniversalEnveloping.lean
+++ b/Mathbin/Algebra/Lie/UniversalEnveloping.lean
@@ -115,14 +115,14 @@ def lift : (L →ₗ⁅R⁆ A) ≃ (UniversalEnvelopingAlgebra R L →ₐ[R] A)
   invFun F := (F : UniversalEnvelopingAlgebra R L →ₗ⁅R⁆ A).comp (ι R)
   left_inv f := by ext;
     simp only [ι, mk_alg_hom, TensorAlgebra.lift_ι_apply, LieHom.coe_toLinearMap,
-      LinearMap.toFun_eq_coe, LinearMap.coe_comp, LieHom.coe_comp, AlgHom.coe_to_lieHom,
+      LinearMap.toFun_eq_coe, LinearMap.coe_comp, LieHom.coe_comp, AlgHom.coe_toLieHom,
       LieHom.coe_mk, Function.comp_apply, AlgHom.toLinearMap_apply,
       RingQuot.liftAlgHom_mkAlgHom_apply]
   right_inv F := by ext;
     simp only [ι, mk_alg_hom, TensorAlgebra.lift_ι_apply, LieHom.coe_toLinearMap,
       LinearMap.toFun_eq_coe, LinearMap.coe_comp, LieHom.coe_linearMap_comp,
       AlgHom.comp_toLinearMap, Function.comp_apply, AlgHom.toLinearMap_apply,
-      RingQuot.liftAlgHom_mkAlgHom_apply, AlgHom.coe_to_lieHom, LieHom.coe_mk]
+      RingQuot.liftAlgHom_mkAlgHom_apply, AlgHom.coe_toLieHom, LieHom.coe_mk]
 #align universal_enveloping_algebra.lift UniversalEnvelopingAlgebra.lift
 -/
 
diff --git a/Mathbin/FieldTheory/Fixed.lean b/Mathbin/FieldTheory/Fixed.lean
index bcad7537fb..115e1552b9 100644
--- a/Mathbin/FieldTheory/Fixed.lean
+++ b/Mathbin/FieldTheory/Fixed.lean
@@ -112,10 +112,10 @@ instance : IsInvariantSubfield M (FixedPoints.subfield M F)
 instance : SMulCommClass M (FixedPoints.subfield M F) F
     where smul_comm m f f' := show m • (↑f * f') = f * m • f' by rw [smul_mul', f.prop m]
 
-#print FixedPoints.smul_comm_class' /-
-instance smul_comm_class' : SMulCommClass (FixedPoints.subfield M F) M F :=
+#print FixedPoints.smulCommClass' /-
+instance smulCommClass' : SMulCommClass (FixedPoints.subfield M F) M F :=
   SMulCommClass.symm _ _ _
-#align fixed_points.smul_comm_class' FixedPoints.smul_comm_class'
+#align fixed_points.smul_comm_class' FixedPoints.smulCommClass'
 -/
 
 #print FixedPoints.smul /-
diff --git a/Mathbin/MeasureTheory/Group/AddCircle.lean b/Mathbin/MeasureTheory/Group/AddCircle.lean
index 481d2a7697..463bb715ea 100644
--- a/Mathbin/MeasureTheory/Group/AddCircle.lean
+++ b/Mathbin/MeasureTheory/Group/AddCircle.lean
@@ -34,6 +34,7 @@ namespace AddCircle
 
 variable {T : ℝ} [hT : Fact (0 < T)]
 
+#print AddCircle.closedBall_ae_eq_ball /-
 theorem closedBall_ae_eq_ball {x : AddCircle T} {ε : ℝ} : closedBall x ε =ᵐ[volume] ball x ε :=
   by
   cases' le_or_lt ε 0 with hε hε
@@ -54,7 +55,9 @@ theorem closedBall_ae_eq_ball {x : AddCircle T} {ε : ℝ} : closedBall x ε =
       le_of_tendsto this (mem_nhds_within_Iio_iff_exists_Ioo_subset.mpr ⟨0, hε, fun r hr => _⟩)
     exact measure_mono (closed_ball_subset_ball hr.2)
 #align add_circle.closed_ball_ae_eq_ball AddCircle.closedBall_ae_eq_ball
+-/
 
+#print AddCircle.isAddFundamentalDomain_of_ae_ball /-
 /-- Let `G` be the subgroup of `add_circle T` generated by a point `u` of finite order `n : ℕ`. Then
 any set `I` that is almost equal to a ball of radius `T / 2n` is a fundamental domain for the action
 of `G` on `add_circle T` by left addition. -/
@@ -100,7 +103,9 @@ theorem isAddFundamentalDomain_of_ae_ball (I : Set <| AddCircle T) (u x : AddCir
       nsmul_eq_mul, mul_div_cancel' T (lt_of_lt_of_le zero_lt_one hn).Ne.symm]
     exact le_refl _
 #align add_circle.is_add_fundamental_domain_of_ae_ball AddCircle.isAddFundamentalDomain_of_ae_ball
+-/
 
+#print AddCircle.volume_of_add_preimage_eq /-
 theorem volume_of_add_preimage_eq (s I : Set <| AddCircle T) (u x : AddCircle T)
     (hu : IsOfFinAddOrder u) (hs : (u +ᵥ s : Set <| AddCircle T) =ᵐ[volume] s)
     (hI : I =ᵐ[volume] ball x (T / (2 * addOrderOf u))) :
@@ -114,6 +119,7 @@ theorem volume_of_add_preimage_eq (s I : Set <| AddCircle T) (u x : AddCircle T)
       hsG,
     add_order_eq_card_zmultiples' u, Nat.card_eq_fintype_card]
 #align add_circle.volume_of_add_preimage_eq AddCircle.volume_of_add_preimage_eq
+-/
 
 end AddCircle
 
diff --git a/Mathbin/MeasureTheory/Group/FundamentalDomain.lean b/Mathbin/MeasureTheory/Group/FundamentalDomain.lean
index 4491fe3107..e85d2159df 100644
--- a/Mathbin/MeasureTheory/Group/FundamentalDomain.lean
+++ b/Mathbin/MeasureTheory/Group/FundamentalDomain.lean
@@ -196,13 +196,13 @@ theorem image_of_equiv {ν : Measure β} (h : IsFundamentalDomain G s μ) (f : 
 #align measure_theory.is_add_fundamental_domain.image_of_equiv MeasureTheory.IsAddFundamentalDomain.image_of_equiv
 -/
 
-#print MeasureTheory.IsFundamentalDomain.pairwise_aEDisjoint_of_ac /-
+#print MeasureTheory.IsFundamentalDomain.pairwise_aedisjoint_of_ac /-
 @[to_additive]
-theorem pairwise_aEDisjoint_of_ac {ν} (h : IsFundamentalDomain G s μ) (hν : ν ≪ μ) :
+theorem pairwise_aedisjoint_of_ac {ν} (h : IsFundamentalDomain G s μ) (hν : ν ≪ μ) :
     Pairwise fun g₁ g₂ : G => AEDisjoint ν (g₁ • s) (g₂ • s) :=
   h.AEDisjoint.mono fun g₁ g₂ H => hν H
-#align measure_theory.is_fundamental_domain.pairwise_ae_disjoint_of_ac MeasureTheory.IsFundamentalDomain.pairwise_aEDisjoint_of_ac
-#align measure_theory.is_add_fundamental_domain.pairwise_ae_disjoint_of_ac MeasureTheory.IsAddFundamentalDomain.pairwise_aEDisjoint_of_ac
+#align measure_theory.is_fundamental_domain.pairwise_ae_disjoint_of_ac MeasureTheory.IsFundamentalDomain.pairwise_aedisjoint_of_ac
+#align measure_theory.is_add_fundamental_domain.pairwise_ae_disjoint_of_ac MeasureTheory.IsAddFundamentalDomain.pairwise_aedisjoint_of_ac
 -/
 
 #print MeasureTheory.IsFundamentalDomain.smul_of_comm /-
diff --git a/lake-manifest.json b/lake-manifest.json
index 4bbd6a1aca..89751d89c4 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -10,15 +10,15 @@
   {"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "e656a660cfcafb2fc537ec4f671868e1ad13de30",
+    "rev": "3251301db9793a040fe6bcca02194b42c4b5d237",
     "name": "lean3port",
-    "inputRev?": "e656a660cfcafb2fc537ec4f671868e1ad13de30"}},
+    "inputRev?": "3251301db9793a040fe6bcca02194b42c4b5d237"}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "6a2b5d294656e23078405eeddff6b61d1852d91b",
+    "rev": "40442633cad526e8b34f7b699a0349f513f00f20",
     "name": "mathlib",
-    "inputRev?": "6a2b5d294656e23078405eeddff6b61d1852d91b"}},
+    "inputRev?": "40442633cad526e8b34f7b699a0349f513f00f20"}},
   {"git":
    {"url": "https://github.com/gebner/quote4",
     "subDir?": null,
diff --git a/lakefile.lean b/lakefile.lean
index ca6a440f1e..cf9f23c8e8 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-19-07"
+def tag : String := "nightly-2023-06-19-09"
 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"@"e656a660cfcafb2fc537ec4f671868e1ad13de30"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"3251301db9793a040fe6bcca02194b42c4b5d237"
 
 @[default_target]
 lean_lib Mathbin where