chore: bump toolchain to v4.34.0-rc1

Algorithm/Data/Classes/DefaultDict.lean

@@ -138,8 +138,8 @@ lemma getElem_listIndicator [DecidableEq ι] (l : List ι) (f : ∀ i ∈ l, α)
     split_ifs with h₁ h₂ h₂
     · simp [h₁]
     · simp [h₁] at h₂
-    · simp_rw [getElem_listIndicator, dif_pos (List.mem_of_ne_of_mem h₁ h₂)]
-    · simp_rw [getElem_listIndicator, dif_neg (List.not_mem_of_not_mem_cons h₂)]
+    · simp_rw [getElem_listIndicator, dite_eq_left (List.mem_of_ne_of_mem h₁ h₂)]
+    · simp_rw [getElem_listIndicator, dite_eq_right (List.not_mem_of_not_mem_cons h₂)]
 
 variable [Ext C ι α d]
 variable (C)
@@ -165,7 +165,7 @@ lemma getElem_indicator [DecidableEq ι] (s : Finset ι) (f : ∀ i ∈ s, α) (
 abbrev toOfFn [Fintype ι] (f : ι → α) : OfFn C ι α f where
   ofFn := indicator C Finset.univ (fun i _ ↦ f i)
   getElem_ofFn _ := by
-    convert (getElem_indicator _ _ _).trans <| dif_pos <| Finset.mem_univ _
+    convert (getElem_indicator _ _ _).trans <| dite_eq_left <| Finset.mem_univ _
     classical infer_instance
 
 end DefaultDict

Algorithm/Data/DFinsupp/Basic.lean

@@ -59,10 +59,10 @@ theorem filter_apply (p : ι → Prop) [DecidablePred p] (i : ι) (f : Π₀' i,
   rfl
 
 theorem filter_apply_pos {p : ι → Prop} [DecidablePred p] (f : Π₀' i, [β i, d i]) {i : ι}
-    (h : p i) : f.filter p i = f i := by simp only [filter_apply, if_pos h]
+    (h : p i) : f.filter p i = f i := by simp only [filter_apply, ite_eq_left h]
 
 theorem filter_apply_neg {p : ι → Prop} [DecidablePred p] (f : Π₀' i, [β i, d i]) {i : ι}
-    (h : ¬p i) : f.filter p i = d i := by simp only [filter_apply, if_neg h]
+    (h : ¬p i) : f.filter p i = d i := by simp only [filter_apply, ite_eq_right h]
 
 @[simp]
 theorem filter_default (p : ι → Prop) [DecidablePred p] :
@@ -111,11 +111,11 @@ theorem filter_single (p : ι → Prop) [DecidablePred p] (i : ι) (x : β i) :
 
 @[simp]
 theorem filter_single_pos {p : ι → Prop} [DecidablePred p] (i : ι) (x : β i) (h : p i) :
-    (single d i x).filter p = single d i x := by rw [filter_single, if_pos h]
+    (single d i x).filter p = single d i x := by rw [filter_single, ite_eq_left h]
 
 @[simp]
 theorem filter_single_neg {p : ι → Prop} [DecidablePred p] (i : ι) (x : β i) (h : ¬p i) :
-    (single d i x).filter p = default := by rw [filter_single, if_neg h]
+    (single d i x).filter p = default := by rw [filter_single, ite_eq_right h]
 
 theorem piecewise_single_erase (x : Π₀' i, [β i, d i]) (i : ι)
     [∀ i' : ι, Decidable <| (i' ∈ ({i} : Set ι))] : -- Porting note: added Decidable hypothesis

Algorithm/Data/DFinsupp/Defs.lean

@@ -196,7 +196,7 @@ variable (d) in
 defined on this `Finset`. -/
 def mk (s : Finset ι) (x : ∀ i : (↑s : Set ι), β (i : ι)) : Π₀' i, [β i, d i] :=
   ⟨fun i => if H : i ∈ s then x ⟨i, H⟩ else d i,
-    Trunc.mk ⟨s.1, fun i => if H : i ∈ s then Or.inl H else Or.inr <| dif_neg H⟩⟩
+    Trunc.mk ⟨s.1, fun i => if H : i ∈ s then Or.inl H else Or.inr <| dite_eq_right H⟩⟩
 
 variable {s : Finset ι} {x : ∀ i : (↑s : Set ι), β i} {i : ι}
 
@@ -205,10 +205,10 @@ theorem mk_apply : (mk d s x : ∀ i, β i) i = if H : i ∈ s then x ⟨i, H⟩
   rfl
 
 theorem mk_of_mem (hi : i ∈ s) : (mk d s x : ∀ i, β i) i = x ⟨i, hi⟩ :=
-  dif_pos hi
+  dite_eq_left hi
 
 theorem mk_of_not_mem (hi : i ∉ s) : (mk d s x : ∀ i, β i) i = d i :=
-  dif_neg hi
+  dite_eq_right hi
 
 variable (d) in
 theorem mk_injective (s : Finset ι) : Function.Injective (@mk ι β d _ s) := by
@@ -217,7 +217,7 @@ theorem mk_injective (s : Finset ι) : Function.Injective (@mk ι β d _ s) := b
   have h1 : (mk d s x : ∀ i, β i) i = (mk d s y : ∀ i, β i) i := by rw [H]
   obtain ⟨i, hi : i ∈ s⟩ := i
   dsimp only [mk_apply, Subtype.coe_mk] at h1
-  simpa only [dif_pos hi] using h1
+  simpa only [dite_eq_left hi] using h1
 
 end mk
 
@@ -279,7 +279,7 @@ theorem single_eq_same {i b} : single d i b i = b := by
   simp only [single_apply, dite_eq_ite, ite_true]
 
 theorem single_eq_of_ne {i i' b} (h : i ≠ i') : single d i b i' = d i' := by
-  simp only [single_apply, dif_neg h]
+  simp only [single_apply, dite_eq_right h]
 
 theorem single_injective {i} : Function.Injective (single d i) := fun _ _ H =>
   Function.update_injective _ i <| DFunLike.coe_injective.eq_iff.mpr H
@@ -417,12 +417,12 @@ theorem erase_single (j : ι) (i : ι) (x : β i) :
 
 @[simp]
 theorem erase_single_same (i : ι) (x : β i) : (single d i x).erase i = default := by
-  rw [erase_single, if_pos rfl]
+  rw [erase_single, ite_eq_left rfl]
 
 @[simp]
 theorem erase_single_ne {i j : ι} (x : β i) (h : i ≠ j) :
     (single d i x).erase j = single d i x := by
-  rw [erase_single, if_neg h]
+  rw [erase_single, ite_eq_right h]
 
 @[simp]
 theorem update_eq_erase (f : Π₀' i, [β i, d i]) (i : ι) :
@@ -444,9 +444,10 @@ theorem single_zipWith_erase (f : ∀ i, β i → β i → β i)
     zipWith f (fun _ ↦ hf₁ _ _) (single d i (x i)) (x.erase i) = x :=
   ext fun i' =>
     if h : i = i' then by
-      subst h; simp only [zipWith_apply, single_apply, erase_apply, hf₂, dite_eq_ite, if_true]
+      subst h; simp only [zipWith_apply, single_apply, erase_apply, hf₂, dite_eq_ite, ite_true]
     else by
-      simp only [zipWith_apply, single_apply, erase_apply, dif_neg h, if_neg (Ne.symm h), hf₁]
+      simp only [zipWith_apply, single_apply, erase_apply, dite_eq_right h,
+        ite_eq_right (Ne.symm h), hf₁]
 
 protected theorem induction_on {p : (Π₀' i, [β i, d i]) → Prop} (x : Π₀' i, [β i, d i])
     (f : ∀ i, β i → β i → β i) (hf₁ : ∀ i x, f i (d i) x = x) (hf₂ : ∀ i x, f i x (d i) = x)
@@ -468,7 +469,7 @@ protected theorem induction_on {p : (Π₀' i, [β i, d i]) → Prop} (x : Π₀
       intro j
       cases H j with | _ H2
       · cases Multiset.mem_cons.1 H2 with | _ H3
-        · right; exact if_pos H3
+        · right; exact ite_eq_left H3
         · left; exact H3
       right
       split_ifs <;> [rfl; exact H2]

Algorithm/Data/UnionFind.lean

@@ -41,14 +41,14 @@ termination_by wf.wrap i
 
 lemma rootCore_of_eq (parent : P) (wf : WellFounded fun j k : ι ↦ j ≠ k ∧ j = parent[k]) (i : ι)
     (hi : parent[i] = i) : rootCore parent wf i = i := by
-  rw [rootCore, if_pos hi]
+  rw [rootCore, ite_eq_left hi]
 
 @[simp]
 lemma rootCore_parent (parent : P) (wf : WellFounded fun j k : ι ↦ j ≠ k ∧ j = parent[k]) (i : ι) :
     rootCore parent wf parent[i] = rootCore parent wf i := by
   conv_rhs => rw [rootCore]
   split_ifs with h
-  · rw [rootCore, h, if_pos h]
+  · rw [rootCore, h, ite_eq_left h]
   · rfl
 
 @[simp]
@@ -63,7 +63,7 @@ termination_by wf.wrap i
 lemma transGen_rootCore (parent : P) (wf : WellFounded fun j k : ι ↦ j ≠ k ∧ j = parent[k])
     (i : ι) (hi : parent[i] ≠ i) :
     Relation.TransGen (fun i j ↦ i ≠ j ∧ i = parent[j]) (rootCore parent wf i) i := by
-  rw [rootCore, if_neg hi, rootCore]
+  rw [rootCore, ite_eq_right hi, rootCore]
   split_ifs with h
   · exact .single ⟨hi, rfl⟩
   · rw [rootCore_parent]
@@ -260,7 +260,7 @@ lemma link_root (self : UnionFind ι P S) (i j : ι) (hi : self.parent[i] = i)
         self.root k := by
   ext k; unfold link; dsimp
   obtain (hij | rfl) := decEq i j
-  · rw [if_neg hij]
+  · rw [ite_eq_right hij]
     split_ifs with hk hs <;> aesop
   · aesop
 
@@ -314,7 +314,7 @@ lemma setParent_wf (self : UnionFind ι P S)
       rw [rootCore]
       split_ifs with h
       · rw [root_of_parent_eq _ _ h]; tauto
-      · rw [root, rootCore, if_neg h]; tauto
+      · rw [root, rootCore, ite_eq_right h]; tauto
   · simp [hk] at hjk
   · rw [h k hk]
     congr! 3

Algorithm/Graph/DFS.lean

@@ -165,9 +165,9 @@ lemma isDFSForest_dfsForest' (g : G)
       (dfsForest' g vs visited).1 := by
   induction vs, visited using dfsForest'.induct g (BoolArray := BoolArray) with
   | case1 => unfold dfsForest'; constructor
-  | case2 _ _ _ h ih => rwa [dfsForest', if_pos h]
+  | case2 _ _ _ h ih => rwa [dfsForest', ite_eq_left h]
   | case3 visited v vs hv _ _ _ _ hc _ _ _ _ ih₁ ih₂ =>
-    rw [dfsForest', if_neg hv]
+    rw [dfsForest', ite_eq_right hv]
     let rc := dfsForest' g (succList g v) visited[v ↦ true]
     dsimp; apply IsDFSForest.node {v : V | rc.2.val[v]}
     · simp [hv]
@@ -322,13 +322,13 @@ lemma dfsTR_spec' (g : G)
   induction vs, visited using dfsTR.induct g (BoolArray := BoolArray) with
   | case1 => simp [dfsTR]
   | case2 _ v _ hv ih =>
-    simp only [dfsTR, if_pos hv, List.mem_cons]
+    simp only [dfsTR, ite_eq_left hv, List.mem_cons]
     rw [← ih]
     ext w
     simp [traversal]
     aesop
   | case3 _ _ _ hv ih =>
-    rw [dfsTR, if_neg hv, ← ih]
+    rw [dfsTR, ite_eq_right hv, ← ih]
     rw [visited_set_true, traversal_insert]
     · simp [hv]
     · ext; simp (config := { contextual := true })

Algorithm/Graph/Dijkstra.lean

@@ -569,7 +569,8 @@ lemma dijkstraStep_spec (g : G) (c : Info → CostType)
     obtain ⟨d, h₂⟩ := h₂
     use min d <| (Finset.univ (α := ToQuiver.mk g (minIdx heap) ⟶ ToQuiver.mk g w)).inf
       fun e ↦ heap[minIdx heap] + c (e : E g).info
-    constructor; · rw [dijkstraStep_fst_getElem (spec₁ := h₁), if_neg (by tauto), h₂.1, min_assoc]
+    constructor
+    · rw [dijkstraStep_fst_getElem (spec₁ := h₁), ite_eq_right (by tauto), h₂.1, min_assoc]
     replace h₂ := h₂.2
     rw [isLeastOfEdges_congr (dijkstraStep_snd_support _ _ _ _ _)]
     rw [isLeastOfEdges_congr Set.union_singleton.symm]

Algorithm/Tactic/Attr/Register.lean

@@ -18,7 +18,8 @@ macro_rules
 | `(tactic| get_elem_tactic_extensible) =>
   `(tactic| simp +contextual only [getElem_simps,
     ne_eq, ite_true, ite_false, dite_true, dite_false,
-    ite_cond_eq_true, ite_cond_eq_false, dite_cond_eq_true, dite_cond_eq_false, ite_self,
+    ite_eq_left_of_eq_true, ite_eq_right_of_eq_false, dite_eq_left_of_eq_true,
+    dite_eq_right_of_eq_false, ite_self,
     and_true, true_and, and_false, false_and, and_self, and_not_self, not_and_self,
     and_imp, not_and, or_self, or_true, true_or, or_false, false_or,
     iff_self, iff_true, true_iff, iff_false, false_iff, false_implies, forall_false,

lake-manifest.json

@@ -5,17 +5,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "0df444a360eaa60ab8c11dca51a86af692955474",
+   "rev": "de5ce8a9a66a4aa68a9bdbb35b63a06d34d9ca11",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.33.1",
+   "inputRev": "v4.34.0-rc1",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "b7eb3304aeae834b12dda98993a37f6a41f6f0bb",
+   "rev": "38e9c3ce15cbb63c92e90bb9a92e4eb82131f669",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "5f4d51b81cbd3f6b32b156bfad9056621a040404",
+   "rev": "2bc7cf064315b26bc38dac2e9612fb581be9b75f",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "16f02aa7642864af59f1ff0e384a015994db9118",
+   "rev": "978b7ec9fbbf9a535114f1de8fe5b3778b358870",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "4be2e3d5087eeb272cf5a8853b8f9dd025ef5957",
+   "rev": "99e8adeea3c3cd86b6b79ba01a1383bf2d31d055",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "3448c0bcc5ce01b2d1546e483ec3620e32df3d0e",
+   "rev": "c1c4362a130f12e632d252180a6c2a31d8fd4726",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "92c15be17b7caf78c2ad767ec40f89052d908d81",
+   "rev": "3b55e9d00c6b0018e5d984eb011b6f93c09bd163",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "4488d40d070b9700d4d5a6aa342f0d40c31b2a2d",
+   "rev": "01bc479e7432594821ba3fb0ca465211941de86d",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,10 +85,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "6130a47896ce867c6a4a55373441e59e565bad0f",
+   "rev": "af8bc067a4cc6c6df472a68909a3f40b1c76c43e",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.33.0",
+   "inputRev": "v4.34.0-rc1",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "algorithm",

lakefile.lean

@@ -2,7 +2,7 @@ import Lake
 
 open Lake DSL
 
-require "leanprover-community" / "mathlib" @ git "v4.33.1"
+require "leanprover-community" / "mathlib" @ git "v4.34.0-rc1"
 
 abbrev algorithmOnlyLinters : Array LeanOption := #[
   ⟨`linter.mathlibStandardSet, true⟩,

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.33.1
+leanprover/lean4:v4.34.0-rc1