chore: bump toolchain to v4.26.0-rc1 (#171)

Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Chris Henson <chrishenson.net@gmail.com>
Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>
Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>

Author: 5 people

Cslib/Computability/Languages/Language.lean

@@ -39,25 +39,6 @@ theorem mem_biSup {I : Type*} (s : Set I) (l : I → Language α) (x : List α)
   · apply mem_iUnion₂.mpr
     grind
 
--- This section will be removed once the following PR gets into mathlib:
--- https://github.com/leanprover-community/mathlib4/pull/30913
-section from_mathlib4_30913
-
-/-- The subtraction of two languages is their difference. -/
-instance : Sub (Language α) where
-  sub := SDiff.sdiff
-
-theorem sub_def (l m : Language α) : l - m = (l \ m : Set (List α)) :=
-  rfl
-
-theorem mem_sub (l m : Language α) (x : List α) : x ∈ l - m ↔ x ∈ l ∧ x ∉ m :=
-  Iff.rfl
-
-instance : OrderedSub (Language α) where
-  tsub_le_iff_right _ _ _ := sdiff_le_iff'
-
-end from_mathlib4_30913
-
 theorem le_one_iff_eq : l ≤ 1 ↔ l = 0 ∨ l = 1 :=
   subset_singleton_iff_eq
 

Cslib/Foundations/Data/FinFun.lean

@@ -126,7 +126,8 @@ theorem fromFun_inter [Zero β] [DecidableEq α]
 @[scoped grind =]
 theorem fromFun_comm [Zero β] [DecidableEq α]
     [∀ y : β, Decidable (y = 0)] {f : α → β} {support1 support2 : Finset α} :
-    (f ↾₀ support1) ↾₀ support2 = (f ↾₀ support2) ↾₀ support1 := by grind
+    (f ↾₀ support1) ↾₀ support2 = (f ↾₀ support2) ↾₀ support1 := by
+  grind only [= coe_eq_fn, = fromFun_fn, ←= ext]
 
 end FinFun
 

Cslib/Foundations/Data/Nat/Segment.lean

@@ -193,10 +193,9 @@ private lemma base_zero_strictMono (hm : StrictMono f) :
 theorem segment'_eq_segment (hm : StrictMono f) :
     segment' f = segment f := by
   classical
-  ext k ; unfold segment'
+  ext k; unfold segment'
   rcases (show k < f 0 ∨ k ≥ f 0 by omega) with h_k | h_k
-  · have : k - f 0 = 0 := by grind
-    grind
+  · grind
   unfold segment; congr 1
   simp only [count_eq_card_filter_range]
   suffices h : ∃ g, BijOn g

Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Subtype.lean

@@ -85,7 +85,11 @@ lemma narrow_aux
     subst eq
     have p : ∀ δ, Γ ++ ⟨X, Binding.sub δ⟩ :: Δ ~ ⟨X, Binding.sub δ⟩ :: (Γ ++ Δ) :=
       by grind [perm_middle]
-    by_cases X = X' <;> grind [Sub.weaken, sublist_append_of_sublist_right]
+    by_cases X = X'
+    · grind only [= append_assoc, = Option.or_some, = dlookup_append, weaken, = dlookup_cons_eq,
+        → wf, =_ singleton_append, =_ cons_append, = mem_append, = Option.or_eq_some_iff,
+        = Option.mem_some, =_ append_assoc, trans_tvar, cases Or]
+    · grind [Sub.weaken, sublist_append_of_sublist_right]
   case all => apply Sub.all (free_union Var) <;> grind
   #adaptation_note
   /--

Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean

@@ -94,7 +94,6 @@ lemma narrow (sub : Sub Δ δ δ') (der : Typing (Γ ++ ⟨X, Binding.sub δ'⟩
   generalize eq : Γ ++ ⟨X, Binding.sub δ'⟩ :: Δ = Θ at der
   induction der generalizing Γ
   case var X' _ _ =>
-    have : .sub δ' ∈ dlookup X (Γ ++ ⟨X, .sub δ'⟩ :: Δ) := by grind [List.mem_dlookup]
     grind [Env.Wf.narrow, List.perm_nodupKeys, => List.perm_dlookup]
   case' abs  => apply abs (free_union Var)
   case' tabs => apply tabs (free_union Var)

docs/lakefile.toml

@@ -6,7 +6,7 @@ packagesDir = "../.lake/packages"
 [[require]]
 scope = "leanprover"
 name = "doc-gen4"
-rev = "v4.25.1"
+rev = "v4.26.0-rc1"
 
 [[require]]
 name = "cslib"

docs/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.25.1
+leanprover/lean4:v4.26.0-rc1

lake-manifest.json

@@ -5,17 +5,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "0df2e3c2047ada0d7a2e33dbc6ba2788a44a6062",
+   "rev": "6a54a80825b060ab20dc31751ebdce78b3a3b518",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.25.1",
+   "inputRev": "v4.26.0-rc1",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "0203092c2e5e26edf967000f0e177cf31c72e17a",
+   "rev": "ec4a54b5308c1f46b4b52a9c62fb67d193aa0972",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "3611075024b3529e5798e53c733671039f06f0bd",
+   "rev": "7ff87023a8e1b358d2d01c1bc56b040a60609577",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,17 +45,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "135329b50b116dcc2c021c318c365e82a048856f",
+   "rev": "894c511d39bf442636bcba085245a1cf2bbdf665",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.80",
+   "inputRev": "v0.0.81",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a2e4d9e9aebdbdce1ce6b6f0a19dd49e0120c990",
+   "rev": "c00943d5ff28c6dc623dbc24f8d659a9d3a3d29a",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "9bff22d64abde45944c7b1f55bce6c89dd8307e6",
+   "rev": "1be06a278c3c249edafb722bfb278622024929d8",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "ffad3f5b7ebe1ac3e09779ec8a863a5138c1246c",
+   "rev": "c278d4e94fe43bc38da4966795dc0c72538e68ab",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,10 +85,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "cd188c6ecfbf6c00cf639e4d4fb18bf773ce8c2c",
+   "rev": "00fad25fa9bedece1f1f988ab9c180dfe3d535b3",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.25.1",
+   "inputRev": "v4.26.0-rc1",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "cslib",

lakefile.toml

@@ -16,7 +16,7 @@ weak.linter.allScriptsDocumented = false
 [[require]]
 name = "mathlib"
 scope = "leanprover-community"
-rev = "v4.25.1"
+rev = "v4.26.0-rc1"
 
 [[lean_lib]]
 name = "Cslib"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.25.1
+leanprover/lean4:v4.26.0-rc1