From 676c38191b244d19576a2546bcb1f4a0b3cfa243 Mon Sep 17 00:00:00 2001
From: monsterkrampe <monsterkrampe@users.noreply.github.com>
Date: Fri, 2 Feb 2024 08:19:37 +0100
Subject: [PATCH] Upgrade Lean to v4.5.0

---
 FormalSystems/Chomsky/Regular/TotalDFA.lean |  4 ++--
 FormalSystems/Preliminaries/Word.lean       | 10 ++++-----
 lake-manifest.json                          | 23 ++++++++++++++-------
 lakefile.lean                               |  2 +-
 lean-toolchain                              |  2 +-
 5 files changed, 25 insertions(+), 16 deletions(-)

diff --git a/FormalSystems/Chomsky/Regular/TotalDFA.lean b/FormalSystems/Chomsky/Regular/TotalDFA.lean
index f392e8f..50cc8a1 100644
--- a/FormalSystems/Chomsky/Regular/TotalDFA.lean
+++ b/FormalSystems/Chomsky/Regular/TotalDFA.lean
@@ -24,8 +24,8 @@ theorem total_del_star_eq {M: TotalDFA α qs} {q: _} {w: _}:
   induction w generalizing q
   case nil => rfl
   case cons _ _ ih =>
-    simp [del_star', DFA.del_star_curried]
-    rw [total_del_eq, Option.bind_eq_bind, Option.some_bind]
+    unfold DFA.del_star_curried
+    rw [total_del_eq] 
     apply ih
 
 theorem in_language_iff_del_star_final
diff --git a/FormalSystems/Preliminaries/Word.lean b/FormalSystems/Preliminaries/Word.lean
index 8c50a30..8136943 100644
--- a/FormalSystems/Preliminaries/Word.lean
+++ b/FormalSystems/Preliminaries/Word.lean
@@ -14,18 +14,18 @@ instance Word.monoid: CancelMonoid (Word α) where
   one := List.nil
   one_mul := List.nil_append
   mul_one := List.append_nil
-  mul_left_cancel u v w := List.append_left_cancel
-  mul_right_cancel u v w := List.append_right_cancel
+  mul_left_cancel u v w := List.append_cancel_left
+  mul_right_cancel u v w := List.append_cancel_right
 
 theorem Word.mul_eq_cons { w v : Word α } :
   w * v = x :: xs ↔ w = [] ∧ v = x :: xs ∨ ∃ (w': Word _), w = x :: w' ∧ xs = w' * v :=
   List.append_eq_cons
 
 def Word.mul_right_cancel {w₁ w₂ t : Word α} (h : w₁ * t = w₂ * t) : w₁ = w₂ :=
-  List.append_right_cancel h
+  List.append_cancel_right h
 
 def Word.mul_left_cancel {w₁ w₂ t : Word α} (h : t * w₁ = t * w₂) : w₁ = w₂ :=
-  List.append_left_cancel h
+  List.append_cancel_left h
 
 def Nat.fin_mod (n : ℕ) (h: N > 0) : Fin N := ⟨ n % N, Nat.mod_lt n h ⟩
 
@@ -112,4 +112,4 @@ instance : GetElem (Word α) ℕ α (λw i ↦ i < w.length) where
 
 @[simp] theorem Word.map_append (f : α → β) : 
   ∀ (u v : Word _), f <$> (u * v) = (f <$> u) * (f <$> v) := 
-  List.map_append f
\ No newline at end of file
+  List.map_append f
diff --git a/lake-manifest.json b/lake-manifest.json
index 2a5657c..0f3d6d2 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "af7f36db6e7e9e395710a70635f915e8e3a0e69b",
+   "rev": "08ec2584b1892869e3a5f4122b029989bcb4ca79",
    "name": "std",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -13,7 +13,7 @@
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
-   "rev": "ccba5d35d07a448fab14c0e391c8105df6e2564c",
+   "rev": "1c88406514a636d241903e2e288d21dc6d861e01",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -22,7 +22,7 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "646be3a3604d0f2a3c1800cb4279a36493474b18",
+   "rev": "cebd10ba6d22457e364ba03320cfd9fc7511e520",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -31,10 +31,10 @@
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
-   "rev": "909febc72b4f64628f8d35cd0554f8a90b6e0749",
+   "rev": "8dd18350791c85c0fc9adbd6254c94a81d260d35",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.23",
+   "inputRev": "v0.0.25",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
@@ -46,13 +46,22 @@
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/import-graph.git",
+   "type": "git",
+   "subDir": null,
+   "rev": "8079d2d1d0e073bde42eab159c24f4c2d0d3a871",
+   "name": "importGraph",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/mathlib4",
    "type": "git",
    "subDir": null,
-   "rev": "cf8e23a62939ed7cc530fbb68e83539730f32f86",
+   "rev": "feec58a7ee9185f92abddcf7631643b53181a7d3",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.4.0",
+   "inputRev": "v4.5.0",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "formal_systems",
diff --git a/lakefile.lean b/lakefile.lean
index 290dfee..4551fd4 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -4,7 +4,7 @@ open Lake DSL
 package formal_systems
 
 require mathlib
-  from git "https://github.com/leanprover-community/mathlib4"@"v4.4.0"
+  from git "https://github.com/leanprover-community/mathlib4"@"v4.5.0"
 
 @[default_target]
 lean_lib FormalSystems
diff --git a/lean-toolchain b/lean-toolchain
index 26638e0..bd59abf 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.4.0
+leanprover/lean4:v4.5.0