bump to nightly-2023-03-27-08

mathlib commit leanprover-community/mathlib@ce86f4e

Mathbin/Computability/TuringMachine.lean

@@ -3511,7 +3511,7 @@ def trNormal : stmt₂ → stmt₁
 lean 3 declaration is
   forall {K : Type.{u1}} [_inst_1 : DecidableEq.{succ u1} K] {Γ : K -> Type.{u2}} {Λ : Type.{u3}} [_inst_2 : Inhabited.{succ u3} Λ] {σ : Type.{u4}} [_inst_3 : Inhabited.{succ u4} σ] {k : K} (s : Turing.TM2to1.StAct.{u1, u2, u4} K _inst_1 Γ σ _inst_3 k) (q : Turing.TM2.Stmt.{u1, u2, u3, u4} K (fun (a : K) (b : K) => _inst_1 a b) Γ Λ σ), Eq.{max (succ (max u1 u2)) (succ (max u1 u2 u3 u4)) (succ u4)} (Turing.TM1.Stmt.{max u1 u2, max u1 u2 u3 u4, u4} (Turing.TM2to1.Γ'.{u1, u2} K _inst_1 Γ) (Turing.TM2to1.Γ'.inhabited.{u1, u2} K _inst_1 Γ) (Turing.TM2to1.Λ'.{u1, u2, u3, u4} K _inst_1 Γ Λ _inst_2 σ _inst_3) σ) (Turing.TM2to1.trNormal.{u1, u2, u3, u4} K _inst_1 Γ Λ _inst_2 σ _inst_3 (Turing.TM2to1.stRun.{u1, u2, u3, u4} K _inst_1 Γ Λ _inst_2 σ _inst_3 k s q)) (Turing.TM1.Stmt.goto.{max u1 u2, max u1 u2 u3 u4, u4} (Turing.TM2to1.Γ'.{u1, u2} K _inst_1 Γ) (Turing.TM2to1.Γ'.inhabited.{u1, u2} K _inst_1 Γ) (Turing.TM2to1.Λ'.{u1, u2, u3, u4} K _inst_1 Γ Λ _inst_2 σ _inst_3) σ (fun (_x : Turing.TM2to1.Γ'.{u1, u2} K _inst_1 Γ) (_x : σ) => Turing.TM2to1.Λ'.go.{u1, u2, u3, u4} K _inst_1 Γ Λ _inst_2 σ _inst_3 k s q))
 but is expected to have type
-  forall {K : Type.{u4}} {_inst_1 : K -> Type.{u3}} {Γ : Type.{u1}} {Λ : Type.{u2}} {_inst_2 : K} (σ : Turing.TM2to1.StAct.{u4, u3, u2} K _inst_1 Λ _inst_2) (_inst_3 : Turing.TM2.Stmt.{u4, u3, u1, u2} K _inst_1 Γ Λ), Eq.{max (max (max (succ u4) (succ u3)) (succ u1)) (succ u2)} (Turing.TM1.Stmt.{max u3 u4, max (max (max u2 u1) u3) u4, u2} (Turing.TM2to1.Γ'.{u4, u3} K _inst_1) (Turing.TM2to1.Λ'.{u4, u3, u1, u2} K _inst_1 Γ Λ) Λ) (Turing.TM2to1.trNormal.{u4, u3, u1, u2} K _inst_1 Γ Λ (Turing.TM2to1.stRun.{u4, u3, u1, u2} K _inst_1 Γ Λ _inst_2 σ _inst_3)) (Turing.TM1.Stmt.goto.{max u4 u3, max (max (max u2 u1) u3) u4, u2} (Turing.TM2to1.Γ'.{u4, u3} K _inst_1) (Turing.TM2to1.Λ'.{u4, u3, u1, u2} K _inst_1 Γ Λ) Λ (fun (x._@.Mathlib.Computability.TuringMachine._hyg.57664 : Turing.TM2to1.Γ'.{u4, u3} K _inst_1) (x._@.Mathlib.Computability.TuringMachine._hyg.57666 : Λ) => Turing.TM2to1.Λ'.go.{u4, u3, u1, u2} K _inst_1 Γ Λ _inst_2 σ _inst_3))
+  forall {K : Type.{u4}} {_inst_1 : K -> Type.{u3}} {Γ : Type.{u1}} {Λ : Type.{u2}} {_inst_2 : K} (σ : Turing.TM2to1.StAct.{u4, u3, u2} K _inst_1 Λ _inst_2) (_inst_3 : Turing.TM2.Stmt.{u4, u3, u1, u2} K _inst_1 Γ Λ), Eq.{max (max (max (succ u4) (succ u3)) (succ u1)) (succ u2)} (Turing.TM1.Stmt.{max u3 u4, max (max (max u2 u1) u3) u4, u2} (Turing.TM2to1.Γ'.{u4, u3} K _inst_1) (Turing.TM2to1.Λ'.{u4, u3, u1, u2} K _inst_1 Γ Λ) Λ) (Turing.TM2to1.trNormal.{u4, u3, u1, u2} K _inst_1 Γ Λ (Turing.TM2to1.stRun.{u4, u3, u1, u2} K _inst_1 Γ Λ _inst_2 σ _inst_3)) (Turing.TM1.Stmt.goto.{max u4 u3, max (max (max u2 u1) u3) u4, u2} (Turing.TM2to1.Γ'.{u4, u3} K _inst_1) (Turing.TM2to1.Λ'.{u4, u3, u1, u2} K _inst_1 Γ Λ) Λ (fun (x._@.Mathlib.Computability.TuringMachine._hyg.57672 : Turing.TM2to1.Γ'.{u4, u3} K _inst_1) (x._@.Mathlib.Computability.TuringMachine._hyg.57674 : Λ) => Turing.TM2to1.Λ'.go.{u4, u3, u1, u2} K _inst_1 Γ Λ _inst_2 σ _inst_3))
 Case conversion may be inaccurate. Consider using '#align turing.TM2to1.tr_normal_run Turing.TM2to1.trNormal_runₓ'. -/
 theorem trNormal_run {k} (s q) : tr_normal (st_run s q) = goto fun _ _ => go k s q := by
   rcases s with (_ | _ | _) <;> rfl

Mathbin/SetTheory/Ordinal/Arithmetic.lean

@@ -3332,7 +3332,7 @@ theorem enumOrd_def' (o) :
 lean 3 declaration is
   forall {S : Set.{succ u1} Ordinal.{u1}}, (Set.Unbounded.{succ u1} Ordinal.{u1} (LT.lt.{succ u1} Ordinal.{u1} (Preorder.toLT.{succ u1} Ordinal.{u1} (PartialOrder.toPreorder.{succ u1} Ordinal.{u1} Ordinal.partialOrder.{u1}))) S) -> (forall (a : Ordinal.{u1}), Set.Nonempty.{succ u1} Ordinal.{u1} (Inter.inter.{succ u1} (Set.{succ u1} Ordinal.{u1}) (Set.hasInter.{succ u1} Ordinal.{u1}) S (Set.Ici.{succ u1} Ordinal.{u1} (PartialOrder.toPreorder.{succ u1} Ordinal.{u1} Ordinal.partialOrder.{u1}) a)))
 but is expected to have type
-  forall {S : Set.{succ u1} Ordinal.{u1}}, (Set.Unbounded.{succ u1} Ordinal.{u1} (fun (x._@.Mathlib.SetTheory.Ordinal.Arithmetic._hyg.28532 : Ordinal.{u1}) (x._@.Mathlib.SetTheory.Ordinal.Arithmetic._hyg.28534 : Ordinal.{u1}) => LT.lt.{succ u1} Ordinal.{u1} (Preorder.toLT.{succ u1} Ordinal.{u1} (PartialOrder.toPreorder.{succ u1} Ordinal.{u1} Ordinal.partialOrder.{u1})) x._@.Mathlib.SetTheory.Ordinal.Arithmetic._hyg.28532 x._@.Mathlib.SetTheory.Ordinal.Arithmetic._hyg.28534) S) -> (forall (a : Ordinal.{u1}), Set.Nonempty.{succ u1} Ordinal.{u1} (Inter.inter.{succ u1} (Set.{succ u1} Ordinal.{u1}) (Set.instInterSet.{succ u1} Ordinal.{u1}) S (Set.Ici.{succ u1} Ordinal.{u1} (PartialOrder.toPreorder.{succ u1} Ordinal.{u1} Ordinal.partialOrder.{u1}) a)))
+  forall {S : Set.{succ u1} Ordinal.{u1}}, (Set.Unbounded.{succ u1} Ordinal.{u1} (fun (x._@.Mathlib.SetTheory.Ordinal.Arithmetic._hyg.28545 : Ordinal.{u1}) (x._@.Mathlib.SetTheory.Ordinal.Arithmetic._hyg.28547 : Ordinal.{u1}) => LT.lt.{succ u1} Ordinal.{u1} (Preorder.toLT.{succ u1} Ordinal.{u1} (PartialOrder.toPreorder.{succ u1} Ordinal.{u1} Ordinal.partialOrder.{u1})) x._@.Mathlib.SetTheory.Ordinal.Arithmetic._hyg.28545 x._@.Mathlib.SetTheory.Ordinal.Arithmetic._hyg.28547) S) -> (forall (a : Ordinal.{u1}), Set.Nonempty.{succ u1} Ordinal.{u1} (Inter.inter.{succ u1} (Set.{succ u1} Ordinal.{u1}) (Set.instInterSet.{succ u1} Ordinal.{u1}) S (Set.Ici.{succ u1} Ordinal.{u1} (PartialOrder.toPreorder.{succ u1} Ordinal.{u1} Ordinal.partialOrder.{u1}) a)))
 Case conversion may be inaccurate. Consider using '#align ordinal.enum_ord_def'_nonempty Ordinal.enumOrd_def'_nonemptyₓ'. -/
 /-- The set in `enum_ord_def'` is nonempty. -/
 theorem enumOrd_def'_nonempty (hS : Unbounded (· < ·) S) (a) : (S ∩ Set.Ici a).Nonempty :=

lake-manifest.json

@@ -4,15 +4,15 @@
  [{"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "668bc1480fc50bf078c1ea800c59f6cf3a021292",
+    "rev": "f5bcf09819b97396508b74f32ef17b0918c30f2a",
     "name": "lean3port",
-    "inputRev?": "668bc1480fc50bf078c1ea800c59f6cf3a021292"}},
+    "inputRev?": "f5bcf09819b97396508b74f32ef17b0918c30f2a"}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "6e9bc1c3e77ef62e656c98f20d3239116ea0cb8d",
+    "rev": "50c0cdf6c6c99d39c04ca48dfc381ab298a45dc4",
     "name": "mathlib",
-    "inputRev?": "6e9bc1c3e77ef62e656c98f20d3239116ea0cb8d"}},
+    "inputRev?": "50c0cdf6c6c99d39c04ca48dfc381ab298a45dc4"}},
   {"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-03-27-06"
+def tag : String := "nightly-2023-03-27-08"
 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"@"668bc1480fc50bf078c1ea800c59f6cf3a021292"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"f5bcf09819b97396508b74f32ef17b0918c30f2a"
 
 @[default_target]
 lean_lib Mathbin where