bump to nightly-2023-03-31-18

mathlib commit leanprover-community/mathlib@ce11c3c

Mathbin/Order/InitialSeg.lean

@@ -332,6 +332,12 @@ theorem leAdd_apply (r : α → α → Prop) (s : β → β → Prop) (a) : leAd
   rfl
 #align initial_seg.le_add_apply InitialSeg.leAdd_apply
 
+/- warning: initial_seg.acc -> InitialSeg.acc is a dubious translation:
+lean 3 declaration is
+  forall {α : Type.{u1}} {β : Type.{u2}} {r : α -> α -> Prop} {s : β -> β -> Prop} (f : InitialSeg.{u1, u2} α β r s) (a : α), Iff (Acc.{succ u1} α r a) (Acc.{succ u2} β s (coeFn.{max (succ u1) (succ u2), max (succ u1) (succ u2)} (InitialSeg.{u1, u2} α β r s) (fun (_x : InitialSeg.{u1, u2} α β r s) => α -> β) (FunLike.hasCoeToFun.{max (succ u1) (succ u2), succ u1, succ u2} (InitialSeg.{u1, u2} α β r s) α (fun (_x : α) => β) (EmbeddingLike.toFunLike.{max (succ u1) (succ u2), succ u1, succ u2} (InitialSeg.{u1, u2} α β r s) α β (InitialSeg.embeddingLike.{u1, u2} α β r s))) f a))
+but is expected to have type
+  forall {α : Type.{u2}} {β : Type.{u1}} {r : α -> α -> Prop} {s : β -> β -> Prop} (f : InitialSeg.{u2, u1} α β r s) (a : α), Iff (Acc.{succ u2} α r a) (Acc.{succ u1} β s (FunLike.coe.{max (succ u2) (succ u1), succ u2, succ u1} (InitialSeg.{u2, u1} α β r s) α (fun (_x : α) => (fun (x._@.Mathlib.Data.FunLike.Embedding._hyg.19 : α) => β) _x) (EmbeddingLike.toFunLike.{max (succ u2) (succ u1), succ u2, succ u1} (InitialSeg.{u2, u1} α β r s) α β (InitialSeg.instEmbeddingLikeInitialSeg.{u2, u1} α β r s)) f a))
+Case conversion may be inaccurate. Consider using '#align initial_seg.acc InitialSeg.accₓ'. -/
 protected theorem acc (f : r ≼i s) (a : α) : Acc r a ↔ Acc s (f a) :=
   ⟨by
     refine' fun h => Acc.recOn h fun a _ ha => Acc.intro _ fun b hb => _
@@ -697,12 +703,19 @@ def pemptyToPunit : @EmptyRelation PEmpty ≺i @EmptyRelation PUnit :=
 #align principal_seg.pempty_to_punit PrincipalSeg.pemptyToPunit
 -/
 
+/- warning: principal_seg.acc -> PrincipalSeg.acc is a dubious translation:
+lean 3 declaration is
+  forall {α : Type.{u1}} {β : Type.{u2}} {r : α -> α -> Prop} {s : β -> β -> Prop} [_inst_1 : IsTrans.{u2} β s] (f : PrincipalSeg.{u1, u2} α β r s) (a : α), Iff (Acc.{succ u1} α r a) (Acc.{succ u2} β s (coeFn.{max (succ u1) (succ u2), max (succ u1) (succ u2)} (PrincipalSeg.{u1, u2} α β r s) (fun (_x : PrincipalSeg.{u1, u2} α β r s) => α -> β) (PrincipalSeg.hasCoeToFun.{u1, u2} α β r s) f a))
+but is expected to have type
+  forall {α : Type.{u1}} {β : Type.{u2}} {r : α -> α -> Prop} {s : β -> β -> Prop} [_inst_1 : IsTrans.{u2} β s] (f : PrincipalSeg.{u1, u2} α β r s) (a : α), Iff (Acc.{succ u1} α r a) (Acc.{succ u2} β s (FunLike.coe.{max (succ u1) (succ u2), succ u1, succ u2} (Function.Embedding.{succ u1, succ u2} α β) α (fun (_x : α) => (fun (x._@.Mathlib.Data.FunLike.Embedding._hyg.19 : α) => β) _x) (EmbeddingLike.toFunLike.{max (succ u1) (succ u2), succ u1, succ u2} (Function.Embedding.{succ u1, succ u2} α β) α β (Function.instEmbeddingLikeEmbedding.{succ u1, succ u2} α β)) (RelEmbedding.toEmbedding.{u1, u2} α β r s (PrincipalSeg.toRelEmbedding.{u1, u2} α β r s f)) a))
+Case conversion may be inaccurate. Consider using '#align principal_seg.acc PrincipalSeg.accₓ'. -/
 protected theorem acc [IsTrans β s] (f : r ≺i s) (a : α) : Acc r a ↔ Acc s (f a) :=
   (f : r ≼i s).Acc a
 #align principal_seg.acc PrincipalSeg.acc
 
 end PrincipalSeg
 
+#print wellFounded_iff_wellFounded_subrel /-
 /-- A relation is well-founded iff every principal segment of it is well-founded.
 
 In this lemma we use `subrel` to indicate its principal segments because it's usually more
@@ -718,12 +731,15 @@ theorem wellFounded_iff_wellFounded_subrel {β : Type _} {s : β → β → Prop
   obtain ⟨b', rfl⟩ := f.down.mp ((PrincipalSeg.ofElement_top s b).symm ▸ hb' : s b' f.top)
   exact (f.acc b').mp ((wf b).apply b')
 #align well_founded_iff_well_founded_subrel wellFounded_iff_wellFounded_subrel
+-/
 
+#print wellFounded_iff_principalSeg /-
 theorem wellFounded_iff_principalSeg.{u} {β : Type u} {s : β → β → Prop} [IsTrans β s] :
     WellFounded s ↔ ∀ (α : Type u) (r : α → α → Prop) (f : r ≺i s), WellFounded r :=
   ⟨fun wf α r f => RelHomClass.wellFounded f.toRelEmbedding wf, fun h =>
     wellFounded_iff_wellFounded_subrel.mpr fun b => h _ _ (PrincipalSeg.ofElement s b)⟩
 #align well_founded_iff_principal_seg wellFounded_iff_principalSeg
+-/
 
 /-! ### Properties of initial and principal segments -/
 

lake-manifest.json

@@ -4,15 +4,15 @@
  [{"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "b0454e2da1c1b36d9a01127da67847cc5c20361b",
+    "rev": "eefa7c3a55869a392781364897e5354369783a8d",
     "name": "lean3port",
-    "inputRev?": "b0454e2da1c1b36d9a01127da67847cc5c20361b"}},
+    "inputRev?": "eefa7c3a55869a392781364897e5354369783a8d"}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "dcbcc203ad12e36fabe281a0432dee63ee40b8d5",
+    "rev": "b9a0a30342ca06e9817e22dbe46e75fc7f435500",
     "name": "mathlib",
-    "inputRev?": "dcbcc203ad12e36fabe281a0432dee63ee40b8d5"}},
+    "inputRev?": "b9a0a30342ca06e9817e22dbe46e75fc7f435500"}},
   {"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-31-16"
+def tag : String := "nightly-2023-03-31-18"
 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"@"b0454e2da1c1b36d9a01127da67847cc5c20361b"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"eefa7c3a55869a392781364897e5354369783a8d"
 
 @[default_target]
 lean_lib Mathbin where