Bump Mathlib and upgrade deprecated lemmas

.gitignore

@@ -0,0 +1,2 @@
+/lean/.lake
+/.vscode/

lean/LoVe/LoVe03_BackwardProofs_Demo.lean

@@ -326,10 +326,10 @@ theorem add_assoc (l m n : ℕ) :
 associative operator using the type class instance mechanism (explained in
 lecture 5). This is useful for the `ac_rfl` invocation below. -/
 
-instance IsAssociative_add : IsAssociative ℕ add :=
+instance IsAssociative_add : Std.Associative add :=
   { assoc := add_assoc }
 
-instance IsCommutative_add : IsCommutative ℕ add :=
+instance IsCommutative_add : Std.Commutative add :=
   { comm := add_comm }
 
 theorem mul_add (l m n : ℕ) :

lean/LoVe/LoVe05_FunctionalProgramming_Demo.lean

@@ -3,7 +3,6 @@ Johannes Hölzl, and Jannis Limperg. See `LICENSE.txt`. -/
 
 import LoVe.LoVelib
 
-
 /- # LoVe Demo 5: Functional Programming
 
 We take a closer look at the basics of typed functional programming: inductive

lean/LoVe/LoVe05_FunctionalProgramming_ExerciseSheet.lean

@@ -3,7 +3,6 @@ Johannes Hölzl, and Jannis Limperg. See `LICENSE.txt`. -/
 
 import LoVe.LoVe04_ForwardProofs_Demo
 
-
 /- # LoVe Exercise 5: Functional Programming
 
 Replace the placeholders (e.g., `:= sorry`) with your solutions. -/
@@ -145,7 +144,7 @@ theorem take_drop {α : Type} :
 
 -- enter your definition here
 
-/- 3.2 (**optional**). Register a textual representation of the type `term` as
+/- 3.2 (**optional**). Register a textual representation of the type `Term` as
 an instance of the `Repr` type class. Make sure to supply enough parentheses to
 guarantee that the output is unambiguous. -/
 

lean/LoVe/LoVe07_EffectfulProgramming_HomeworkSheet.lean

@@ -31,7 +31,7 @@ types. Inventory all the arguments and operations available (e.g., `pure`,
 bricks. -/
 
 def map {m : Type → Type} [LawfulMonad m] {α β : Type} (f : α → β) (ma : m α) :
-  m β := :=
+    m β :=
   sorry
 
 /- 1.2 (1 point). Prove the identity law for `map`.

lean/LoVe/LoVelib.lean

@@ -1,14 +1,12 @@
 /- Copyright © 2018–2024 Anne Baanen, Alexander Bentkamp, Jasmin Blanchette,
 Johannes Hölzl, and Jannis Limperg. See `LICENSE.txt`. -/
 
-import Aesop
 import Mathlib.Algebra.Field.Defs
 import Mathlib.Data.Finset.Basic
-import Mathlib.Tactic.LibrarySearch
+import Mathlib.Data.Tree.Basic
 import Mathlib.Tactic.Linarith
 import Mathlib.Tactic.Ring
 
-
 /- # LoVelib: Logical Verification Library -/
 
 

lean/lake-manifest.json

@@ -1,64 +1,71 @@
-{"version": 7,
+{"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/leanprover/std4",
+ [{"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "rev": "a7543d1a6934d52086971f510e482d743fe30cf3",
-   "name": "std",
+   "scope": "leanprover-community",
+   "rev": "0f3e143dffdc3a591662f3401ce1d7a3405227c0",
+   "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.6.0",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
-   "rev": "fd760831487e6835944e7eeed505522c9dd47563",
+   "scope": "leanprover-community",
+   "rev": "01ad33937acd996ee99eb74eefb39845e4e4b9f5",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
    "inherited": true,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/JLimperg/aesop",
+  {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "c51fa8ea4de8b203f64929cba19d139e555f9f6b",
+   "scope": "leanprover-community",
+   "rev": "209712c78b16c795453b6da7f7adbda4589a8f21",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "stable",
-   "inherited": false,
-   "configFile": "lakefile.lean"},
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
-   "rev": "16cae05860b208925f54e5581ec5fd264823440c",
+   "scope": "leanprover-community",
+   "rev": "c87908619cccadda23f71262e6898b9893bffa36",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.29",
+   "inputRev": "v0.0.40",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
-   "rev": "a751d21d4b68c999accb6fc5d960538af26ad5ec",
+   "scope": "",
+   "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/import-graph.git",
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/import-graph",
    "type": "git",
    "subDir": null,
-   "rev": "64d082eeaad1a8e6bbb7c23b7a16b85a1715a02f",
+   "scope": "leanprover-community",
+   "rev": "543725b3bfed792097fc134adca628406f6145f5",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
-   "configFile": "lakefile.lean"},
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/mathlib4",
    "type": "git",
    "subDir": null,
-   "rev": "7ca43cbd6aa34058a1afad8e47190af3ec1f9bdb",
+   "scope": "",
+   "rev": "a719ba5c3115d47b68bf0497a9dd1bcbb21ea663",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "stable",

lean/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.6.0
+leanprover/lean4:v4.10.0