diff --git a/Mathbin/Data/MvPolynomial/Cardinal.lean b/Mathbin/Data/MvPolynomial/Cardinal.lean
index 8d93bb7794..f120e322b9 100644
--- a/Mathbin/Data/MvPolynomial/Cardinal.lean
+++ b/Mathbin/Data/MvPolynomial/Cardinal.lean
@@ -33,6 +33,12 @@ section TwoUniverses
 
 variable {σ : Type u} {R : Type v} [CommSemiring R]
 
+/- warning: mv_polynomial.cardinal_mk_eq_max_lift -> MvPolynomial.cardinal_mk_eq_max_lift is a dubious translation:
+lean 3 declaration is
+  forall {σ : Type.{u1}} {R : Type.{u2}} [_inst_1 : CommSemiring.{u2} R] [_inst_2 : Nonempty.{succ u1} σ] [_inst_3 : Nontrivial.{u2} R], Eq.{succ (succ (max u1 u2))} Cardinal.{max u1 u2} (Cardinal.mk.{max u1 u2} (MvPolynomial.{u1, u2} σ R _inst_1)) (LinearOrder.max.{succ (max u1 u2)} Cardinal.{max u1 u2} (CanonicallyLinearOrderedAddMonoid.toLinearOrder.{succ (max u1 u2)} Cardinal.{max u1 u2} Cardinal.canonicallyLinearOrderedAddMonoid.{max u1 u2}) (LinearOrder.max.{succ (max u1 u2)} Cardinal.{max u1 u2} (CanonicallyLinearOrderedAddMonoid.toLinearOrder.{succ (max u1 u2)} Cardinal.{max u1 u2} Cardinal.canonicallyLinearOrderedAddMonoid.{max u1 u2}) (Cardinal.lift.{u1, u2} (Cardinal.mk.{u2} R)) (Cardinal.lift.{u2, u1} (Cardinal.mk.{u1} σ))) Cardinal.aleph0.{max u1 u2})
+but is expected to have type
+  forall {σ : Type.{u1}} {R : Type.{u2}} [_inst_1 : CommSemiring.{u2} R] [_inst_2 : Nonempty.{succ u1} σ] [_inst_3 : Nontrivial.{u2} R], Eq.{max (succ (succ u1)) (succ (succ u2))} Cardinal.{max u2 u1} (Cardinal.mk.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1)) (Max.max.{max (succ u1) (succ u2)} Cardinal.{max u2 u1} (CanonicallyLinearOrderedAddMonoid.toMax.{max (succ u1) (succ u2)} Cardinal.{max u2 u1} Cardinal.instCanonicallyLinearOrderedAddMonoidCardinal.{max u1 u2}) (Max.max.{max (succ u1) (succ u2)} Cardinal.{max u2 u1} (CanonicallyLinearOrderedAddMonoid.toMax.{max (succ u1) (succ u2)} Cardinal.{max u2 u1} Cardinal.instCanonicallyLinearOrderedAddMonoidCardinal.{max u1 u2}) (Cardinal.lift.{u1, u2} (Cardinal.mk.{u2} R)) (Cardinal.lift.{u2, u1} (Cardinal.mk.{u1} σ))) Cardinal.aleph0.{max u1 u2})
+Case conversion may be inaccurate. Consider using '#align mv_polynomial.cardinal_mk_eq_max_lift MvPolynomial.cardinal_mk_eq_max_liftₓ'. -/
 @[simp]
 theorem cardinal_mk_eq_max_lift [Nonempty σ] [Nontrivial R] :
     (#MvPolynomial σ R) = max (max (Cardinal.lift.{u} <| (#R)) <| Cardinal.lift.{v} <| (#σ)) ℵ₀ :=
@@ -40,11 +46,19 @@ theorem cardinal_mk_eq_max_lift [Nonempty σ] [Nontrivial R] :
     rw [mk_finsupp_nat, max_assoc, lift_max, lift_aleph_0, max_comm]
 #align mv_polynomial.cardinal_mk_eq_max_lift MvPolynomial.cardinal_mk_eq_max_lift
 
+#print MvPolynomial.cardinal_mk_eq_lift /-
 @[simp]
 theorem cardinal_mk_eq_lift [IsEmpty σ] : (#MvPolynomial σ R) = Cardinal.lift.{u} (#R) :=
   ((isEmptyRingEquiv R σ).toEquiv.trans Equiv.ulift.{u}.symm).cardinal_eq
 #align mv_polynomial.cardinal_mk_eq_lift MvPolynomial.cardinal_mk_eq_lift
+-/
 
+/- warning: mv_polynomial.cardinal_lift_mk_le_max -> MvPolynomial.cardinal_lift_mk_le_max is a dubious translation:
+lean 3 declaration is
+  forall {σ : Type.{u1}} {R : Type.{u2}} [_inst_2 : CommSemiring.{u2} R], LE.le.{succ (max u1 u2)} Cardinal.{max u1 u2} Cardinal.hasLe.{max u1 u2} (Cardinal.mk.{max u1 u2} (MvPolynomial.{u1, u2} σ R _inst_2)) (LinearOrder.max.{succ (max u1 u2)} Cardinal.{max u1 u2} (CanonicallyLinearOrderedAddMonoid.toLinearOrder.{succ (max u1 u2)} Cardinal.{max u1 u2} Cardinal.canonicallyLinearOrderedAddMonoid.{max u1 u2}) (LinearOrder.max.{succ (max u1 u2)} Cardinal.{max u1 u2} (CanonicallyLinearOrderedAddMonoid.toLinearOrder.{succ (max u1 u2)} Cardinal.{max u1 u2} Cardinal.canonicallyLinearOrderedAddMonoid.{max u1 u2}) (Cardinal.lift.{u1, u2} (Cardinal.mk.{u2} R)) (Cardinal.lift.{u2, u1} (Cardinal.mk.{u1} σ))) Cardinal.aleph0.{max u1 u2})
+but is expected to have type
+  forall {σ : Type.{u1}} {R : Type.{u2}} [_inst_2 : CommSemiring.{u2} R], LE.le.{max (succ u1) (succ u2)} Cardinal.{max u2 u1} Cardinal.instLECardinal.{max u1 u2} (Cardinal.mk.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_2)) (Max.max.{max (succ u1) (succ u2)} Cardinal.{max u2 u1} (CanonicallyLinearOrderedAddMonoid.toMax.{max (succ u1) (succ u2)} Cardinal.{max u2 u1} Cardinal.instCanonicallyLinearOrderedAddMonoidCardinal.{max u1 u2}) (Max.max.{max (succ u1) (succ u2)} Cardinal.{max u2 u1} (CanonicallyLinearOrderedAddMonoid.toMax.{max (succ u1) (succ u2)} Cardinal.{max u2 u1} Cardinal.instCanonicallyLinearOrderedAddMonoidCardinal.{max u1 u2}) (Cardinal.lift.{u1, u2} (Cardinal.mk.{u2} R)) (Cardinal.lift.{u2, u1} (Cardinal.mk.{u1} σ))) Cardinal.aleph0.{max u1 u2})
+Case conversion may be inaccurate. Consider using '#align mv_polynomial.cardinal_lift_mk_le_max MvPolynomial.cardinal_lift_mk_le_maxₓ'. -/
 theorem cardinal_lift_mk_le_max {σ : Type u} {R : Type v} [CommSemiring R] :
     (#MvPolynomial σ R) ≤ max (max (Cardinal.lift.{u} <| (#R)) <| Cardinal.lift.{v} <| (#σ)) ℵ₀ :=
   by
@@ -59,10 +73,22 @@ end TwoUniverses
 
 variable {σ R : Type u} [CommSemiring R]
 
+/- warning: mv_polynomial.cardinal_mk_eq_max -> MvPolynomial.cardinal_mk_eq_max is a dubious translation:
+lean 3 declaration is
+  forall {σ : Type.{u1}} {R : Type.{u1}} [_inst_1 : CommSemiring.{u1} R] [_inst_2 : Nonempty.{succ u1} σ] [_inst_3 : Nontrivial.{u1} R], Eq.{succ (succ u1)} Cardinal.{u1} (Cardinal.mk.{u1} (MvPolynomial.{u1, u1} σ R _inst_1)) (LinearOrder.max.{succ u1} Cardinal.{u1} (CanonicallyLinearOrderedAddMonoid.toLinearOrder.{succ u1} Cardinal.{u1} Cardinal.canonicallyLinearOrderedAddMonoid.{u1}) (LinearOrder.max.{succ u1} Cardinal.{u1} (CanonicallyLinearOrderedAddMonoid.toLinearOrder.{succ u1} Cardinal.{u1} Cardinal.canonicallyLinearOrderedAddMonoid.{u1}) (Cardinal.mk.{u1} R) (Cardinal.mk.{u1} σ)) Cardinal.aleph0.{u1})
+but is expected to have type
+  forall {σ : Type.{u1}} {R : Type.{u1}} [_inst_1 : CommSemiring.{u1} R] [_inst_2 : Nonempty.{succ u1} σ] [_inst_3 : Nontrivial.{u1} R], Eq.{succ (succ u1)} Cardinal.{u1} (Cardinal.mk.{u1} (MvPolynomial.{u1, u1} σ R _inst_1)) (Max.max.{succ u1} Cardinal.{u1} (CanonicallyLinearOrderedAddMonoid.toMax.{succ u1} Cardinal.{u1} Cardinal.instCanonicallyLinearOrderedAddMonoidCardinal.{u1}) (Max.max.{succ u1} Cardinal.{u1} (CanonicallyLinearOrderedAddMonoid.toMax.{succ u1} Cardinal.{u1} Cardinal.instCanonicallyLinearOrderedAddMonoidCardinal.{u1}) (Cardinal.mk.{u1} R) (Cardinal.mk.{u1} σ)) Cardinal.aleph0.{u1})
+Case conversion may be inaccurate. Consider using '#align mv_polynomial.cardinal_mk_eq_max MvPolynomial.cardinal_mk_eq_maxₓ'. -/
 theorem cardinal_mk_eq_max [Nonempty σ] [Nontrivial R] :
     (#MvPolynomial σ R) = max (max (#R) (#σ)) ℵ₀ := by simp
 #align mv_polynomial.cardinal_mk_eq_max MvPolynomial.cardinal_mk_eq_max
 
+/- warning: mv_polynomial.cardinal_mk_le_max -> MvPolynomial.cardinal_mk_le_max is a dubious translation:
+lean 3 declaration is
+  forall {σ : Type.{u1}} {R : Type.{u1}} [_inst_1 : CommSemiring.{u1} R], LE.le.{succ u1} Cardinal.{u1} Cardinal.hasLe.{u1} (Cardinal.mk.{u1} (MvPolynomial.{u1, u1} σ R _inst_1)) (LinearOrder.max.{succ u1} Cardinal.{u1} (CanonicallyLinearOrderedAddMonoid.toLinearOrder.{succ u1} Cardinal.{u1} Cardinal.canonicallyLinearOrderedAddMonoid.{u1}) (LinearOrder.max.{succ u1} Cardinal.{u1} (CanonicallyLinearOrderedAddMonoid.toLinearOrder.{succ u1} Cardinal.{u1} Cardinal.canonicallyLinearOrderedAddMonoid.{u1}) (Cardinal.mk.{u1} R) (Cardinal.mk.{u1} σ)) Cardinal.aleph0.{u1})
+but is expected to have type
+  forall {σ : Type.{u1}} {R : Type.{u1}} [_inst_1 : CommSemiring.{u1} R], LE.le.{succ u1} Cardinal.{u1} Cardinal.instLECardinal.{u1} (Cardinal.mk.{u1} (MvPolynomial.{u1, u1} σ R _inst_1)) (Max.max.{succ u1} Cardinal.{u1} (CanonicallyLinearOrderedAddMonoid.toMax.{succ u1} Cardinal.{u1} Cardinal.instCanonicallyLinearOrderedAddMonoidCardinal.{u1}) (Max.max.{succ u1} Cardinal.{u1} (CanonicallyLinearOrderedAddMonoid.toMax.{succ u1} Cardinal.{u1} Cardinal.instCanonicallyLinearOrderedAddMonoidCardinal.{u1}) (Cardinal.mk.{u1} R) (Cardinal.mk.{u1} σ)) Cardinal.aleph0.{u1})
+Case conversion may be inaccurate. Consider using '#align mv_polynomial.cardinal_mk_le_max MvPolynomial.cardinal_mk_le_maxₓ'. -/
 /-- The cardinality of the multivariate polynomial ring, `mv_polynomial σ R` is at most the maximum
 of `#R`, `#σ` and `ℵ₀` -/
 theorem cardinal_mk_le_max : (#MvPolynomial σ R) ≤ max (max (#R) (#σ)) ℵ₀ :=
diff --git a/lake-manifest.json b/lake-manifest.json
index c2bded646d..5bc1379543 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": "ca4d48a00d4308de24e99d8c1213c538ddbee443",
+    "rev": "ebe85b657b92a77dd442882aa6d36cde1ad77b17",
     "name": "lean3port",
-    "inputRev?": "ca4d48a00d4308de24e99d8c1213c538ddbee443"}},
+    "inputRev?": "ebe85b657b92a77dd442882aa6d36cde1ad77b17"}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "ea4e0dd0dd8021d1677b63fbbe5eab18e5186318",
+    "rev": "780abda658d8deb26194b60c0e90f1ee4010f807",
     "name": "mathlib",
-    "inputRev?": "ea4e0dd0dd8021d1677b63fbbe5eab18e5186318"}},
+    "inputRev?": "780abda658d8deb26194b60c0e90f1ee4010f807"}},
   {"git":
    {"url": "https://github.com/gebner/quote4",
     "subDir?": null,
diff --git a/lakefile.lean b/lakefile.lean
index 04a3aabe21..1a9a671aa6 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-03-26-18"
+def tag : String := "nightly-2023-03-26-20"
 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"@"ca4d48a00d4308de24e99d8c1213c538ddbee443"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"ebe85b657b92a77dd442882aa6d36cde1ad77b17"
 
 @[default_target]
 lean_lib Mathbin where