diff --git a/Mathbin/LinearAlgebra/FreeModule/Finite/Basic.lean b/Mathbin/LinearAlgebra/FreeModule/Finite/Basic.lean
index 3faacc5da2..5ca2312db4 100644
--- a/Mathbin/LinearAlgebra/FreeModule/Finite/Basic.lean
+++ b/Mathbin/LinearAlgebra/FreeModule/Finite/Basic.lean
@@ -55,6 +55,12 @@ variable [AddCommGroup N] [Module R N] [Module.Free R N]
 
 variable {R}
 
+/- warning: module.finite.of_basis -> Module.Finite.of_basis is a dubious translation:
+lean 3 declaration is
+  forall {R : Type.{u1}} {M : Type.{u2}} {ι : Type.{u3}} [_inst_8 : CommRing.{u1} R] [_inst_9 : AddCommGroup.{u2} M] [_inst_10 : Module.{u1, u2} R M (Ring.toSemiring.{u1} R (CommRing.toRing.{u1} R _inst_8)) (AddCommGroup.toAddCommMonoid.{u2} M _inst_9)] [_inst_11 : Finite.{succ u3} ι], (Basis.{u3, u1, u2} ι R M (Ring.toSemiring.{u1} R (CommRing.toRing.{u1} R _inst_8)) (AddCommGroup.toAddCommMonoid.{u2} M _inst_9) _inst_10) -> (Module.Finite.{u1, u2} R M (Ring.toSemiring.{u1} R (CommRing.toRing.{u1} R _inst_8)) (AddCommGroup.toAddCommMonoid.{u2} M _inst_9) _inst_10)
+but is expected to have type
+  forall {R : Type.{u3}} {M : Type.{u2}} {ι : Type.{u1}} [_inst_8 : CommRing.{u3} R] [_inst_9 : AddCommGroup.{u2} M] [_inst_10 : Module.{u3, u2} R M (Ring.toSemiring.{u3} R (CommRing.toRing.{u3} R _inst_8)) (AddCommGroup.toAddCommMonoid.{u2} M _inst_9)] [_inst_11 : Finite.{succ u1} ι], (Basis.{u1, u3, u2} ι R M (Ring.toSemiring.{u3} R (CommRing.toRing.{u3} R _inst_8)) (AddCommGroup.toAddCommMonoid.{u2} M _inst_9) _inst_10) -> (Module.Finite.{u3, u2} R M (Ring.toSemiring.{u3} R (CommRing.toRing.{u3} R _inst_8)) (AddCommGroup.toAddCommMonoid.{u2} M _inst_9) _inst_10)
+Case conversion may be inaccurate. Consider using '#align module.finite.of_basis Module.Finite.of_basisₓ'. -/
 /-- A free module with a basis indexed by a `fintype` is finite. -/
 theorem Module.Finite.of_basis {R M ι : Type _} [CommRing R] [AddCommGroup M] [Module R M]
     [Finite ι] (b : Basis ι R M) : Module.Finite R M :=
@@ -65,6 +71,7 @@ theorem Module.Finite.of_basis {R M ι : Type _} [CommRing R] [AddCommGroup M] [
     simp only [Set.image_univ, Finset.coe_univ, Finset.coe_image, Basis.span_eq]
 #align module.finite.of_basis Module.Finite.of_basis
 
+#print Module.Finite.matrix /-
 instance Module.Finite.matrix {ι₁ ι₂ : Type _} [Finite ι₁] [Finite ι₂] :
     Module.Finite R (Matrix ι₁ ι₂ R) :=
   by
@@ -72,6 +79,7 @@ instance Module.Finite.matrix {ι₁ ι₂ : Type _} [Finite ι₁] [Finite ι
   cases nonempty_fintype ι₂
   exact Module.Finite.of_basis (Pi.basis fun i => Pi.basisFun R _)
 #align module.finite.matrix Module.Finite.matrix
+-/
 
 end CommRing
 
diff --git a/Mathbin/Order/RelIso/Basic.lean b/Mathbin/Order/RelIso/Basic.lean
index 43298ccf43..ed840cc322 100644
--- a/Mathbin/Order/RelIso/Basic.lean
+++ b/Mathbin/Order/RelIso/Basic.lean
@@ -655,6 +655,12 @@ protected theorem wellFounded : ∀ (f : r ↪r s) (h : WellFounded s), WellFoun
   | f, ⟨H⟩ => ⟨fun a => f.Acc _ (H _)⟩
 #align rel_embedding.well_founded RelEmbedding.wellFounded
 
+/- warning: rel_embedding.is_well_founded -> RelEmbedding.isWellFounded is a dubious translation:
+lean 3 declaration is
+  forall {α : Type.{u1}} {β : Type.{u2}} {r : α -> α -> Prop} {s : β -> β -> Prop}, (RelEmbedding.{u1, u2} α β r s) -> (forall [_inst_1 : IsWellFounded.{u2} β s], IsWellFounded.{u1} α r)
+but is expected to have type
+  forall {α : Type.{u2}} {β : Type.{u1}} {r : α -> α -> Prop} {s : β -> β -> Prop}, (RelEmbedding.{u2, u1} α β r s) -> (forall [_inst_1 : IsWellFounded.{u1} β s], IsWellFounded.{u2} α r)
+Case conversion may be inaccurate. Consider using '#align rel_embedding.is_well_founded RelEmbedding.isWellFoundedₓ'. -/
 protected theorem isWellFounded (f : r ↪r s) [IsWellFounded β s] : IsWellFounded α r :=
   ⟨f.WellFounded IsWellFounded.wf⟩
 #align rel_embedding.is_well_founded RelEmbedding.isWellFounded
@@ -671,15 +677,19 @@ protected theorem isWellOrder : ∀ (f : r ↪r s) [IsWellOrder β s], IsWellOrd
 
 end RelEmbedding
 
+#print Subtype.wellFoundedLT /-
 instance Subtype.wellFoundedLT [LT α] [WellFoundedLT α] (p : α → Prop) :
     WellFoundedLT (Subtype p) :=
   (Subtype.relEmbedding (· < ·) p).IsWellFounded
 #align subtype.well_founded_lt Subtype.wellFoundedLT
+-/
 
+#print Subtype.wellFoundedGT /-
 instance Subtype.wellFoundedGT [LT α] [WellFoundedGT α] (p : α → Prop) :
     WellFoundedGT (Subtype p) :=
   (Subtype.relEmbedding (· > ·) p).IsWellFounded
 #align subtype.well_founded_gt Subtype.wellFoundedGT
+-/
 
 #print Quotient.mkRelHom /-
 /-- `quotient.mk` as a relation homomorphism between the relation and the lift of a relation. -/
diff --git a/lake-manifest.json b/lake-manifest.json
index e5b2030826..688e74443a 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": "e72e7d793670d13e625d84f16b0f5ef6254b9052",
+    "rev": "fd9e682418488176e5abc6fd1ebf9f1ca8a38b1a",
     "name": "lean3port",
-    "inputRev?": "e72e7d793670d13e625d84f16b0f5ef6254b9052"}},
+    "inputRev?": "fd9e682418488176e5abc6fd1ebf9f1ca8a38b1a"}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "00f161707e0de5b1c508e7bd9032e1c0a295c74e",
+    "rev": "05186d6b6b04357326f679db65b90e45c6c8f8ed",
     "name": "mathlib",
-    "inputRev?": "00f161707e0de5b1c508e7bd9032e1c0a295c74e"}},
+    "inputRev?": "05186d6b6b04357326f679db65b90e45c6c8f8ed"}},
   {"git":
    {"url": "https://github.com/gebner/quote4",
     "subDir?": null,
diff --git a/lakefile.lean b/lakefile.lean
index ed0f6992e6..2d098ab73b 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-04-10-14"
+def tag : String := "nightly-2023-04-10-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"@"e72e7d793670d13e625d84f16b0f5ef6254b9052"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"fd9e682418488176e5abc6fd1ebf9f1ca8a38b1a"
 
 @[default_target]
 lean_lib Mathbin where