upgrade to Lean v4.21.0

lean/LoVe/LoVe05_FunctionalProgramming_Demo.lean

@@ -394,7 +394,7 @@ theorem length_zip {α β : Type} (xs : List α) (ys : List β) :
     length (zip xs ys) = min (length xs) (length ys) :=
   by
     induction xs generalizing ys with
-    | nil           => simp [min, length]
+    | nil           => simp [zip, min, length]
     | cons x xs' ih =>
       cases ys with
       | nil        => rfl

lean/LoVe/LoVe08_Metaprogramming_Demo.lean

@@ -490,6 +490,8 @@ theorem Nat.symm_manual (x y : ℕ) (h : x = y) :
     apply symm
     hypothesis
 
+set_option maxHeartbeats 1000000
+
 theorem Nat.trans (x y z : ℕ) (hxy : x = y) (hyz : y = z) :
     x = z :=
   by prove_direct

lean/LoVe/LoVe13_BasicMathematicalStructures_Demo.lean

@@ -421,7 +421,7 @@ instance List.length.Preorder {α : Type} : Preorder (List α) :=
       by
         intro xs ys zs
         exact Nat.le_trans
-    lt_iff_le_not_le :=
+    lt_iff_le_not_ge :=
       by
         intro a b
         exact Nat.lt_iff_le_not_le }

lean/LoVe/LoVelib.lean

@@ -4,8 +4,8 @@ Xavier Généreux, Johannes Hölzl, and Jannis Limperg. See `LICENSE.txt`. -/
 import Aesop
 import Mathlib.Algebra.Field.Defs
 import Mathlib.Algebra.Order.Ring.Abs
-import Mathlib.Algebra.BigOperators.Group.List
-import Mathlib.Algebra.BigOperators.Group.Multiset
+import Mathlib.Algebra.BigOperators.Group.List.Basic
+import Mathlib.Algebra.BigOperators.Group.Multiset.Basic
 import Mathlib.Data.Finset.Basic
 import Mathlib.Data.Tree.Basic
 import Mathlib.Tactic.Linarith
@@ -151,7 +151,7 @@ instance Set.PartialOrder {α : Type} : PartialOrder (Set α) :=
       by
         intro A B C hAB hBC a ha
         aesop,
-    lt_iff_le_not_le :=
+    lt_iff_le_not_ge :=
       by
         intro A B
         apply Iff.intro

lean/lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "4bbdccd9c5f862bf90ff12f0a9e2c8be032b9a84",
+   "rev": "308445d7985027f538e281e18df29ca16ede2ba3",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "stable",
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "42dc02bdbc5d0c2f395718462a76c3d87318f7fa",
+   "rev": "c4aa78186d388e50a436e8362b947bae125a2933",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "d7caecce0d0f003fd5e9cce9a61f1dd6ba83142b",
+   "rev": "6c62474116f525d2814f0157bb468bf3a4f9f120",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,57 +35,57 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "519e509a28864af5bed98033dd33b95cf08e9aa7",
+   "rev": "d07bd64f1910f1cc5e4cc87b6b9c590080e7a457",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.14.0",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "68280daef58803f68368eb2e53046dabcd270c9d",
+   "rev": "6980f6ca164de593cb77cd03d8eac549cc444156",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.47",
+   "inputRev": "v0.0.62",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "5a0ec8588855265ade536f35bcdcf0fb24fd6030",
+   "rev": "8ff27701d003456fd59f13a9212431239d902aef",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.14.0",
+   "inputRev": "master",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "303b23fbcea94ac4f96e590c1cad6618fd4f5f41",
+   "rev": "e9c65db4823976353cd0bb03199a172719efbeb7",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
    "inherited": true,
-   "configFile": "lakefile.lean"},
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "8d6c853f11a5172efa0e96b9f2be1a83d861cdd9",
+   "rev": "8d2067bf518731a70a255d4a61b5c103922c772e",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.14.0",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "726b3c9ad13acca724d4651f14afc4804a7b0e4d",
+   "rev": "7c6aef5f75a43ebbba763b44d535175a1b04c9e0",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lean/lean-toolchain

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