Bump mathlib to v4.22.0

Author: YaelDillies

PersistentDecomp/DirectSumDecomposition.lean

@@ -254,7 +254,7 @@ lemma Indecomposable_of_mem_Min_Direct_sum_decomposition
     (D : DirectSumDecomposition M) (N : PersistenceSubmodule M) (hN : N ∈ D) (hmax : IsMax D) :
     Indecomposable N := by
   by_contra hNotMax
-  simp only [_root_.Indecomposable, not_forall, Classical.not_imp, not_or] at hNotMax
+  simp only [_root_.Indecomposable, not_forall, not_or] at hNotMax
   obtain ⟨x, y, hxy, rfl, hx, hy⟩ := hNotMax
   let B (N) (hN : N ∈ D) : Set (PersistenceSubmodule M) := if N = x ⊔ y then {x, y} else {N}
   set newD : DirectSumDecomposition M := refinement

PersistentDecomp/DirectSumDecompositionDual.lean

@@ -341,7 +341,7 @@ lemma Indecomposable_of_mem_Min_Direct_sum_decomposition
     (D : DirectSumDecomposition M) (N : PersistenceSubmodule M) (hN : N ∈ D) (hmax : IsMin D) :
     Indecomposable N := by
   by_contra hNotMax
-  simp only [_root_.Indecomposable, not_forall, Classical.not_imp, not_or] at hNotMax
+  simp only [_root_.Indecomposable, not_forall, not_or] at hNotMax
   obtain ⟨x, y, hxy, rfl, hx, hy⟩ := hNotMax
   let B (N) (hN : N ∈ D) : Set (PersistenceSubmodule M) := if N = x ⊔ y then {x, y} else {N}
   set newD : DirectSumDecomposition M := refinement

PersistentDecomp/Mathlib/Algebra/DirectSum/Basic.lean

@@ -20,7 +20,7 @@ lemma IsInternal.eq_zero_of_subsingleton_preimage (hA : IsInternal A) {κ : Type
     (hf₀ : ∑ k ∈ s, f k = 0) {k : κ} (hk : k ∈ s) : f k = 0 := by
   classical
   letI := hA.chooseDecomposition
-  have (k) : decompose A (f k) = DirectSum.of (fun i ↦ A i) (g k) ⟨f k, hfg k⟩ :=
+  have (k : κ) : decompose A (f k) = DirectSum.of (fun i ↦ A i) (g k) ⟨f k, hfg k⟩ :=
     (decompose A).symm.injective (by simp)
   have hf₀ := congr((decomposeAddEquiv A $hf₀ (g k)).1)
   simp only [map_sum, decomposeAddEquiv_apply,

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 = "PersistentDecomp"

lean-toolchain

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