From 7afc87d0f9118cf64d1c2405bfc0b708a19cbe1e Mon Sep 17 00:00:00 2001
From: Adrien Burgun <adrien.burgun@orange.fr>
Date: Sat, 2 Dec 2023 21:39:59 +0100
Subject: [PATCH] :arrow_up: Upgrade mathlib and lean version to latest

---
 Rubin.lean         |  3 +--
 lake-manifest.json | 24 ++++++++++++------------
 lean-toolchain     |  2 +-
 3 files changed, 14 insertions(+), 15 deletions(-)

diff --git a/Rubin.lean b/Rubin.lean
index a95b089..c2b6a1b 100644
--- a/Rubin.lean
+++ b/Rubin.lean
@@ -767,8 +767,7 @@ theorem proposition_3_2 {G α : Type _} [Group G] [TopologicalSpace α] [MulActi
   [hc : ContinuousMulAction G α] :
   TopologicalSpace.IsTopologicalBasis (AssociatedPoset.asSet α) :=
 by
-  -- Note: the name later changes to isTopologicalBasis_of_isOpen_of_nhds
-  apply TopologicalSpace.isTopologicalBasis_of_open_of_nhds
+  apply TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds
   {
     intro U U_in_poset
     rw [AssociatedPoset.mem_asSet] at U_in_poset
diff --git a/lake-manifest.json b/lake-manifest.json
index b8eef49..f5e56e8 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "d3049643f6dded69eb7ce8124796cb1ec8df8840",
+   "rev": "9e37a01f8590f81ace095b56710db694b5bf8ca0",
    "name": "std",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -13,7 +13,7 @@
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
-   "rev": "d3a1d25f3eba0d93a58d5d3d027ffa78ece07755",
+   "rev": "ccba5d35d07a448fab14c0e391c8105df6e2564c",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -22,34 +22,34 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "bf5ab42a58e71de7ebad399ce3f90d29aae7fca9",
+   "rev": "3141402ba5a5f0372d2378fd75a481bc79a74ecf",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
    "inherited": true,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover/lean4-cli",
+  {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
-   "rev": "a751d21d4b68c999accb6fc5d960538af26ad5ec",
-   "name": "Cli",
+   "rev": "909febc72b4f64628f8d35cd0554f8a90b6e0749",
+   "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v0.0.23",
    "inherited": true,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/ProofWidgets4",
+  {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
-   "rev": "c3b9f0d4ebedc43635d3f7e764e277b1010844b7",
-   "name": "proofwidgets",
+   "rev": "a751d21d4b68c999accb6fc5d960538af26ad5ec",
+   "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.22",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "c6979569edc545f999b82d8a833b190c918aec2e",
+   "rev": "c0f7586a3e77660ff51b9156783aaf8eab9506de",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
diff --git a/lean-toolchain b/lean-toolchain
index 24a3cdb..91ccf6a 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.3.0-rc2
+leanprover/lean4:v4.4.0-rc1