update Lean and Mathlib from 4.13 to 4.14

Makefile

@@ -22,7 +22,7 @@ dependencies.svg: Pdl/*.lean
 
 update-fix:
 	rm -rf .lake
-	echo "leanprover/lean4:v4.12.0" > lean-toolchain
+	echo "leanprover/lean4:v4.14.0" > lean-toolchain
 	echo "If next command fails, edit lakefile.lean manually."
-	grep v4.12.0 lakefile.lean
+	grep v4.14.0 lakefile.lean
 	lake update -R

Pdl/Examples.lean

@@ -8,7 +8,7 @@ import Pdl.Semantics
 import Pdl.Star
 import Pdl.UnfoldBox
 
-open Vector HasSat
+open HasSat
 
 -- some simple silly stuff
 theorem mytaut1 (p : Nat) : tautology ((·p) ↣ (·p)) :=

Pdl/LocalTableau.lean

@@ -750,13 +750,6 @@ theorem node_to_multiset_of_precon {O Ocond Onew : Olf}
     all_goals cases Ocond_Def : Ocond <;> try (cases Ocond_def2 : Ocond)
     all_goals cases Onew_Def : Onew <;> try (cases Onew_def2 : Onew)
     all_goals simp_all [Olf.toForm, Olf.change, Option.insHasSdiff]
-    all_goals
-      rcases precon with ⟨_Lpre, _Rpre, Opre⟩
-      subst_eqs
-    · rename_i lf
-      cases lf <;> simp
-    · rename_i lf1 lf2
-      cases lf1 <;> simp
   rw [claim]
   -- we now get 3 * 3 * 3 = 27 cases
   all_goals cases O <;> try (rename_i O; cases O)
@@ -867,12 +860,12 @@ theorem H_goes_down (α : Program) φ {Fs δ} (in_H : (Fs, δ) ∈ H α) {ψ} (i
   · simp_all [H]
   case sequence α β =>
     simp only [lmOfFormula]
-    simp only [H, List.mem_join, List.mem_map, Prod.exists] at in_H
+    simp only [H, List.mem_flatten, List.mem_map, Prod.exists] at in_H
     rcases in_H with ⟨l, ⟨Fs', δ', in_H, def_l⟩, in_l⟩
     · subst def_l
       by_cases δ' = []
       · subst_eqs
-        simp_all only [List.nil_append, ite_true, List.mem_join, List.mem_map, Prod.exists]
+        simp_all only [List.nil_append, ite_true, List.mem_flatten, List.mem_map, Prod.exists]
         rcases in_l with ⟨l, ⟨Fs'', δ'', in_Hβ, def_l⟩, in_l⟩
         subst def_l
         simp only [List.mem_singleton, Prod.mk.injEq] at in_l

Pdl/Syntax.lean

@@ -1,4 +1,4 @@
-import Mathlib.Order.BoundedOrder
+import Mathlib.Order.BoundedOrder.Basic
 
 mutual
   inductive Formula : Type

lake-manifest.json

@@ -1,85 +1,95 @@
 {"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/leanprover-community/batteries",
+ [{"url": "https://github.com/leanprover-community/mathlib4.git",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "4bbdccd9c5f862bf90ff12f0a9e2c8be032b9a84",
+   "name": "mathlib",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.14.0",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "31a10a332858d6981dbcf55d54ee51680dd75f18",
-   "name": "batteries",
+   "rev": "42dc02bdbc5d0c2f395718462a76c3d87318f7fa",
+   "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/quote4",
+  {"url": "https://github.com/leanprover-community/LeanSearchClient",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "1357f4f49450abb9dfd4783e38219f4ce84f9785",
-   "name": "Qq",
+   "rev": "d7caecce0d0f003fd5e9cce9a61f1dd6ba83142b",
+   "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "main",
    "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/aesop",
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/import-graph",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "5f934891e11d70a1b86e302fdf9cecfc21e8de46",
-   "name": "aesop",
+   "rev": "519e509a28864af5bed98033dd33b95cf08e9aa7",
+   "name": "importGraph",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "v4.14.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "baa65c6339a56bd22b7292aa4511c54b3cc7a6af",
+   "rev": "68280daef58803f68368eb2e53046dabcd270c9d",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.43",
+   "inputRev": "v0.0.47",
    "inherited": true,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover/lean4-cli",
+  {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "scope": "leanprover",
-   "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0",
-   "name": "Cli",
+   "scope": "leanprover-community",
+   "rev": "5a0ec8588855265ade536f35bcdcf0fb24fd6030",
+   "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.14.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/import-graph",
+  {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "984d7ee170b75d6b03c0903e0b750ee2c6d1e3fb",
-   "name": "importGraph",
+   "rev": "303b23fbcea94ac4f96e590c1cad6618fd4f5f41",
+   "name": "Qq",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "master",
    "inherited": true,
-   "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/LeanSearchClient",
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "7bedaed1ef024add1e171cc17706b012a9a37802",
-   "name": "LeanSearchClient",
+   "rev": "8d6c853f11a5172efa0e96b9f2be1a83d861cdd9",
+   "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.14.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/mathlib4.git",
+  {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
-   "scope": "",
-   "rev": "d5ab93e3a3afadaf265a583a92f7e7c47203b540",
-   "name": "mathlib",
+   "scope": "leanprover",
+   "rev": "726b3c9ad13acca724d4651f14afc4804a7b0e4d",
+   "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.13.0",
-   "inherited": false,
-   "configFile": "lakefile.lean"}],
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"}],
  "name": "pdl",
  "lakeDir": ".lake"}

lakefile.lean

@@ -4,7 +4,7 @@ open Lake DSL
 package «pdl»
 
 require mathlib from git
-  "https://github.com/leanprover-community/mathlib4.git"@"v4.13.0"
+  "https://github.com/leanprover-community/mathlib4.git"@"v4.14.0"
 
 @[default_target]
 lean_lib «Pdl»

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.13.0
+leanprover/lean4:v4.14.0