Bump mathlib to v4.22.0

Author: YaelDillies

LeanCamCombi/GraphTheory/ExampleSheet1.lean

@@ -20,7 +20,7 @@ If you solve a question in Lean, feel free to open a Pull Request on Github!
 
 open Fintype (card)
 open Function SimpleGraph
-open scoped BigOperators Cardinal
+open scoped Cardinal SetRel
 
 namespace GraphTheory
 namespace ES1
@@ -208,19 +208,19 @@ all degrees of $$X$$ are finite (while degrees in $$Y$$ have no restriction)?
 
 -- This translation looks slightly painful because of the `cardinal`.
 lemma q14_part1 :
-    ∃ r : ℕ → ℕ → Prop,
-      (∀ A : Finset ℕ, (A.card : Cardinal) ≤ #(Rel.image r A)) ∧
-        ∀ f : ℕ → ℕ, Injective f → ∃ n, ¬ r n (f n) :=
+    ∃ r : SetRel ℕ ℕ,
+      (∀ A : Finset ℕ, (A.card : Cardinal) ≤ #(r.image A)) ∧
+        ∀ f : ℕ → ℕ, Injective f → ∃ n, ¬ n ~[r] f n :=
   sorry
 
-lemma q14_part2 [DecidableEq β] [Countable α] [Countable β] (r : α → β → Prop)
-    [∀ a, Fintype (Rel.image r {a})] (hr : ∀ A : Finset α, A.card ≤ card (Rel.image r A)) :
-    ∃ f : α → β, Injective f ∧ ∀ a, r a (f a) :=
+lemma q14_part2 [DecidableEq β] [Countable α] [Countable β] (r : SetRel α β)
+    [∀ a, Fintype (r.image {a})] (hr : ∀ A : Finset α, A.card ≤ card (r.image A)) :
+    ∃ f : α → β, Injective f ∧ ∀ a, a ~[r] f a :=
   sorry
 
-lemma q14_part3 [DecidableEq β] (r : α → β → Prop) [∀ a, Fintype (Rel.image r {a})]
-    (hr : ∀ A : Finset α, A.card ≤ card (Rel.image r A)) :
-    ∃ f : α → β, Injective f ∧ ∀ a, r a (f a) :=
+lemma q14_part3 [DecidableEq β] (r : SetRel α β) [∀ a, Fintype (r.image {a})]
+    (hr : ∀ A : Finset α, A.card ≤ card (r.image A)) :
+    ∃ f : α → β, Injective f ∧ ∀ a, a ~[r] f a :=
   sorry
 
 /-!

lake-manifest.json

@@ -5,27 +5,27 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "308445d7985027f538e281e18df29ca16ede2ba3",
+   "rev": "79e94a093aff4a60fb1b1f92d9681e407124c2ca",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.21.0",
+   "inputRev": "v4.22.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c4aa78186d388e50a436e8362b947bae125a2933",
+   "rev": "b100ad4c5d74a464f497aaa8e7c74d86bf39a56f",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.22.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/LeanSearchClient",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "6c62474116f525d2814f0157bb468bf3a4f9f120",
+   "rev": "99657ad92e23804e279f77ea6dbdeebaa1317b98",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,57 +35,57 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "d07bd64f1910f1cc5e4cc87b6b9c590080e7a457",
+   "rev": "eb164a46de87078f27640ee71e6c3841defc2484",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.22.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "6980f6ca164de593cb77cd03d8eac549cc444156",
+   "rev": "1253a071e6939b0faf5c09d2b30b0bfc79dae407",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.62",
+   "inputRev": "v0.0.68",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "8ff27701d003456fd59f13a9212431239d902aef",
+   "rev": "1256a18522728c2eeed6109b02dd2b8f207a2a3c",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "v4.22.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "e9c65db4823976353cd0bb03199a172719efbeb7",
+   "rev": "917bfa5064b812b7fbd7112d018ea0b4def25ab3",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "v4.22.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "8d2067bf518731a70a255d4a61b5c103922c772e",
+   "rev": "240676e9568c254a69be94801889d4b13f3b249f",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.22.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "7c6aef5f75a43ebbba763b44d535175a1b04c9e0",
+   "rev": "c682c91d2d4dd59a7187e2ab977ac25bd1f87329",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lakefile.toml

@@ -39,7 +39,7 @@ linter.style.setOption = true
 [[require]]
 name = "mathlib"
 git = "https://github.com/leanprover-community/mathlib4.git"
-rev = "v4.21.0"
+rev = "v4.22.0"
 
 [[lean_lib]]
 name = "LeanCamCombi"

lean-toolchain

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