bump to nightly-2023-05-21-16

mathlib commit leanprover-community/mathlib@33c67ae

Mathbin/Algebra/Group/Units.lean

@@ -1230,7 +1230,7 @@ protected theorem mul_right_cancel (h : IsUnit b) : a * b = c * b → a = c :=
 lean 3 declaration is
   forall {M : Type.{u1}} [_inst_1 : Monoid.{u1} M] {a : M}, (IsUnit.{u1} M _inst_1 a) -> (Function.Injective.{succ u1, succ u1} M M (HMul.hMul.{u1, u1, u1} M M M (instHMul.{u1} M (MulOneClass.toHasMul.{u1} M (Monoid.toMulOneClass.{u1} M _inst_1))) a))
 but is expected to have type
-  forall {M : Type.{u1}} [_inst_1 : Monoid.{u1} M] {a : M}, (IsUnit.{u1} M _inst_1 a) -> (Function.Injective.{succ u1, succ u1} M M ((fun (x._@.Mathlib.Algebra.Group.Units._hyg.7119 : M) (x._@.Mathlib.Algebra.Group.Units._hyg.7121 : M) => HMul.hMul.{u1, u1, u1} M M M (instHMul.{u1} M (MulOneClass.toMul.{u1} M (Monoid.toMulOneClass.{u1} M _inst_1))) x._@.Mathlib.Algebra.Group.Units._hyg.7119 x._@.Mathlib.Algebra.Group.Units._hyg.7121) a))
+  forall {M : Type.{u1}} [_inst_1 : Monoid.{u1} M] {a : M}, (IsUnit.{u1} M _inst_1 a) -> (Function.Injective.{succ u1, succ u1} M M ((fun (x._@.Mathlib.Algebra.Group.Units._hyg.7116 : M) (x._@.Mathlib.Algebra.Group.Units._hyg.7118 : M) => HMul.hMul.{u1, u1, u1} M M M (instHMul.{u1} M (MulOneClass.toMul.{u1} M (Monoid.toMulOneClass.{u1} M _inst_1))) x._@.Mathlib.Algebra.Group.Units._hyg.7116 x._@.Mathlib.Algebra.Group.Units._hyg.7118) a))
 Case conversion may be inaccurate. Consider using '#align is_unit.mul_right_injective IsUnit.mul_right_injectiveₓ'. -/
 @[to_additive]
 protected theorem mul_right_injective (h : IsUnit a) : Injective ((· * ·) a) := fun _ _ =>

Mathbin/MeasureTheory/Constructions/BorelSpace/Complex.lean

@@ -16,18 +16,30 @@ import Mathbin.MeasureTheory.Constructions.BorelSpace.Basic
 
 noncomputable section
 
+#print IsROrC.measurableSpace /-
 instance (priority := 900) IsROrC.measurableSpace {𝕜 : Type _} [IsROrC 𝕜] : MeasurableSpace 𝕜 :=
   borel 𝕜
 #align is_R_or_C.measurable_space IsROrC.measurableSpace
+-/
 
+#print IsROrC.borelSpace /-
 instance (priority := 900) IsROrC.borelSpace {𝕜 : Type _} [IsROrC 𝕜] : BorelSpace 𝕜 :=
   ⟨rfl⟩
 #align is_R_or_C.borel_space IsROrC.borelSpace
+-/
 
+#print Complex.measurableSpace /-
 instance Complex.measurableSpace : MeasurableSpace ℂ :=
   borel ℂ
 #align complex.measurable_space Complex.measurableSpace
+-/
 
+/- warning: complex.borel_space -> Complex.borelSpace is a dubious translation:
+lean 3 declaration is
+  BorelSpace.{0} Complex (UniformSpace.toTopologicalSpace.{0} Complex (PseudoMetricSpace.toUniformSpace.{0} Complex (SeminormedRing.toPseudoMetricSpace.{0} Complex (SeminormedCommRing.toSemiNormedRing.{0} Complex (NormedCommRing.toSeminormedCommRing.{0} Complex (NormedField.toNormedCommRing.{0} Complex Complex.normedField)))))) Complex.measurableSpace
+but is expected to have type
+  BorelSpace.{0} Complex (UniformSpace.toTopologicalSpace.{0} Complex (PseudoMetricSpace.toUniformSpace.{0} Complex (SeminormedRing.toPseudoMetricSpace.{0} Complex (SeminormedCommRing.toSeminormedRing.{0} Complex (NormedCommRing.toSeminormedCommRing.{0} Complex (NormedField.toNormedCommRing.{0} Complex Complex.instNormedFieldComplex)))))) Complex.measurableSpace
+Case conversion may be inaccurate. Consider using '#align complex.borel_space Complex.borelSpaceₓ'. -/
 instance Complex.borelSpace : BorelSpace ℂ :=
   ⟨rfl⟩
 #align complex.borel_space Complex.borelSpace

lake-manifest.json

@@ -4,15 +4,15 @@
  [{"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "66e8913c4e7ecfb6485692941d195e9b96b2616b",
+    "rev": "882a5a2b0b8f43ca4dc9b89a5447565e6c9e9196",
     "name": "lean3port",
-    "inputRev?": "66e8913c4e7ecfb6485692941d195e9b96b2616b"}},
+    "inputRev?": "882a5a2b0b8f43ca4dc9b89a5447565e6c9e9196"}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "542f2e564670085b3b5ee475637efdb052dc9c08",
+    "rev": "54991d4b205a7765d2f9107dd410f3c7b793da2b",
     "name": "mathlib",
-    "inputRev?": "542f2e564670085b3b5ee475637efdb052dc9c08"}},
+    "inputRev?": "54991d4b205a7765d2f9107dd410f3c7b793da2b"}},
   {"git":
    {"url": "https://github.com/gebner/quote4",
     "subDir?": null,

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-21-14"
+def tag : String := "nightly-2023-05-21-16"
 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"@"66e8913c4e7ecfb6485692941d195e9b96b2616b"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"882a5a2b0b8f43ca4dc9b89a5447565e6c9e9196"
 
 @[default_target]
 lean_lib Mathbin where