update lean

8 files changed, 30 insertions, 23 deletions

diff --git a/Nominal/Helpers/CountableString.lean b/Nominal/Helpers/CountableString.lean
index 7d2fcb7..7d94516 100644
--- a/Nominal/Helpers/CountableString.lean
+++ b/Nominal/Helpers/CountableString.lean
@@ -9,4 +9,6 @@ instance : Countable Char where
 
 instance : Countable String := Countable.of_equiv (List Char)
   { toFun := String.mk
-    invFun := String.data }
+    invFun := String.data
+    left_inv x := by simp
+    right_inv x := by simp }
diff --git a/Nominal/LambdaCalculus/Preterms.lean b/Nominal/LambdaCalculus/Preterms.lean
index 74f7397..c133343 100644
--- a/Nominal/LambdaCalculus/Preterms.lean
+++ b/Nominal/LambdaCalculus/Preterms.lean
@@ -114,7 +114,7 @@ instance : NominalSet Var Preterm where
         simp only [PermSet.fix', smul_abs, Preterm.abs.injEq, Set.mem_setOf_eq]
         simp only [PermSet.fix, vars, Set.singleton_union, Set.mem_insert_iff, forall_eq_or_imp, Set.mem_setOf_eq] at hπ
         exact ⟨hπ.left, a_ih.left hπ.right⟩
-      · simp [vars, Set.Finite.insert, a_ih]
+      · simp [vars, a_ih]
     · constructor
       · intro π hπ
         simp only [PermSet.fix', smul_app, Preterm.app.injEq, Set.mem_setOf_eq]
diff --git a/Nominal/LambdaCalculus/Terms.lean b/Nominal/LambdaCalculus/Terms.lean
index 2118156..c698b65 100644
--- a/Nominal/LambdaCalculus/Terms.lean
+++ b/Nominal/LambdaCalculus/Terms.lean
@@ -229,7 +229,12 @@ private def equiv : EquivariantEquiv Var Term (Var ⊕ (NameAbstraction Var Term
       (by
         intro t u htu
         cases htu
-        sorry)
+        · sorry
+        · sorry
+        · sorry
+        · sorry
+        · sorry
+        · sorry)
     invFun
       | .inl x => .var x
       | .inr (.inl x) => Quotient.liftOn x
diff --git a/Nominal/Support.lean b/Nominal/Support.lean
index b8e6809..93e7aaa 100644
--- a/Nominal/Support.lean
+++ b/Nominal/Support.lean
@@ -153,9 +153,9 @@ lemma support_inter {x : X} {S T : Set 𝔸} : HasSupport 𝔸 x S → S.Finite
 
 /-- For a finite number of finite supports, the intersection is also a support. -/
 lemma support_sInter {x : X} {C : Set (Set 𝔸)}: C.Finite → C.Nonempty → (∀ S ∈ C, HasSupport 𝔸 x S ∧ S.Finite) → HasSupport 𝔸 x (⋂₀ C) := by
-  suffices (C : Finset (Set 𝔸)) : C.Nonempty → (∀ S ∈ C, HasSupport 𝔸 x S ∧ S.Finite) → HasSupport 𝔸 x (⋂₀ C.toSet) ∧ (⋂₀ C.toSet).Finite
+  suffices (C : Finset (Set 𝔸)) : C.Nonempty → (∀ S ∈ C, HasSupport 𝔸 x S ∧ S.Finite) → HasSupport 𝔸 x (⋂₀ C) ∧ (⋂₀ (↑C : Set (Set 𝔸))).Finite
   · intro hfin
-    rw [show C = hfin.toFinset.toSet by simp]
+    rw [show C = hfin.toFinset by simp]
     intro hne h
     exact (this hfin.toFinset hne h).left
   · have : DecidableEq (Set 𝔸) := Classical.typeDecidableEq (Set 𝔸)
diff --git a/flake.lock b/flake.lock
index 6650c8f..99d3a8f 100644
--- a/flake.lock
+++ b/flake.lock
@@ -20,11 +20,11 @@
     },
     "nixpkgs": {
       "locked": {
-        "lastModified": 1758213207,
-        "narHash": "sha256-rqoqF0LEi+6ZT59tr+hTQlxVwrzQsET01U4uUdmqRtM=",
+        "lastModified": 1764167966,
+        "narHash": "sha256-nXv6xb7cq+XpjBYIjWEGTLCqQetxJu6zvVlrqHMsCOA=",
         "owner": "nixos",
         "repo": "nixpkgs",
-        "rev": "f4b140d5b253f5e2a1ff4e5506edbf8267724bde",
+        "rev": "5c46f3bd98147c8d82366df95bbef2cab3a967ea",
         "type": "github"
       },
       "original": {
diff --git a/lake-manifest.json b/lake-manifest.json
index e793730..6dce1af 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,17 +5,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "37df177aaa770670452312393d4e84aaad56e7b6",
+   "rev": "1ccd71f89cbbd82ae7d097723ce1722ca7b01c33",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.23.0",
+   "inputRev": "v4.25.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a22e7c1fa7707fb7ea75f2f9fd6b14de2b7b87a9",
+   "rev": "2503bfb5e2d4d8202165f5bd2cc39e44a3be31c3",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "99657ad92e23804e279f77ea6dbdeebaa1317b98",
+   "rev": "2ed4ba69b6127de8f5c2af83cccacd3c988b06bf",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "7fca1d4a190761bac0028848f73dc9a59fcb4957",
+   "rev": "009064c21bad4d7f421f2901c5e817c8bf3468cb",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,17 +45,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "6e47cc88cfbf1601ab364e9a4de5f33f13401ff8",
+   "rev": "e8ef4bdd7a23c3a37170fbd3fa7ee07ef2a54c2d",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.71",
+   "inputRev": "v0.0.79",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "247ff80701c76760523b5d7c180b27b7708faf38",
+   "rev": "26e4c7c0e63eb3e6cce3cf7faba27b8526ea8349",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "9b703a545097978aef0e7e243ab8b71c32a9ff65",
+   "rev": "2781d8ad404303b2fe03710ac7db946ddfe3539f",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "d117e2c28cba42e974bc22568ac999492a34e812",
+   "rev": "5c78955e8375f872c085514cb521216bac1bda17",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,11 +85,11 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "41c5d0b8814dec559e2e1441171db434fe2281cc",
+   "rev": "1dae8b12f8ba27576ffe5ddee78bebf6458157b0",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.25.0",
    "inherited": true,
    "configFile": "lakefile.toml"}],
- "name": "Nominal",
+ "name": "CoalgebraicAutomata",
  "lakeDir": ".lake"}
diff --git a/lakefile.toml b/lakefile.toml
index 45c09ba..bf4beec 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -5,7 +5,7 @@ defaultTargets = ["Nominal"]
 [[require]]
 name = "mathlib"
 scope = "leanprover-community"
-rev = "v4.23.0"
+rev = "v4.25.0"
 
 [[lean_lib]]
 name = "Nominal"
diff --git a/lean-toolchain b/lean-toolchain
index 7f254a9..e5ab73a 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.23.0
+leanprover/lean4:v4.25.0