chore: bump toolchain to v4.19.0-rc1 (#1186)

kim-em · leanprover-community-mathlib4-bot · jcommelin · web-flow · commit 5a56dfa58c18 · 2025-04-02T08:15:01.000Z
Co-authored-by: leanprover-community-mathlib4-bot &lt;leanprover-community-mathlib4-bot@users.noreply.github.com&gt;
Co-authored-by: Johan Commelin &lt;johan@commelin.net&gt;
Co-authored-by: Matthew Ballard &lt;matt@mrb.email&gt;
Co-authored-by: Markus Himmel &lt;markus@lean-fro.org&gt;
Co-authored-by: Kyle Miller &lt;kmill31415@gmail.com&gt;
Co-authored-by: Mario Carneiro &lt;di.gama@gmail.com&gt;
Co-authored-by: Sebastian Ullrich &lt;sebasti@nullri.ch&gt;
Co-authored-by: Joachim Breitner &lt;mail@joachim-breitner.de&gt;
Co-authored-by: Mac Malone &lt;mac@lean-fro.org&gt;
diff --git a/Batteries/Classes/SatisfiesM.lean b/Batteries/Classes/SatisfiesM.lean
@@ -275,9 +275,9 @@ instance [Monad m] [LawfulMonad m] [MonadSatisfying m] : MonadSatisfying (Except
   satisfying {α p x} h :=
     let x' := satisfying (SatisfiesM_ExceptT_eq.mp h)
     ExceptT.mk ((fun ⟨y, w⟩ => y.pmap fun a h => ⟨a, w _ h⟩) <$> x')
-  val_eq {α p x} h:= by
+  val_eq {α p x} h := by
     ext
-    rw [← MonadSatisfying.val_eq (SatisfiesM_ExceptT_eq.mp h)]
+    refine Eq.trans ?_ (MonadSatisfying.val_eq (SatisfiesM_ExceptT_eq.mp h))
     simp
 
 instance : MonadSatisfying (EStateM ε σ) where
diff --git a/Batteries/Data/AssocList.lean b/Batteries/Data/AssocList.lean
@@ -78,7 +78,7 @@ def toListTR (as : AssocList α β) : List (α × β) :=
 
 @[csimp] theorem toList_eq_toListTR : @toList = @toListTR := by
   funext α β as; simp [toListTR]
-  exact .symm <| (Array.foldl_toList_eq_map (toList as) _ id).trans (List.map_id _)
+  exact .symm <| Array.foldl_toList_eq_map.trans (List.map_id _)
 
 /-- `O(n)`. Run monadic function `f` on all elements in the list, from head to tail. -/
 @[specialize] def forM [Monad m] (f : α → β → m PUnit) : AssocList α β → m PUnit
diff --git a/Batteries/Data/ByteArray.lean b/Batteries/Data/ByteArray.lean
@@ -21,7 +21,7 @@ theorem getElem_eq_data_getElem (a : ByteArray) (h : i < a.size) : a[i] = a.data
 
 /-! ### empty -/
 
-@[simp] theorem data_mkEmpty (cap) : (mkEmpty cap).data = #[] := rfl
+@[simp] theorem data_mkEmpty (cap) : (emptyWithCapacity cap).data = #[] := rfl
 
 @[simp] theorem data_empty : empty.data = #[] := rfl
 
@@ -51,7 +51,7 @@ theorem get_push_lt (a : ByteArray) (x : UInt8) (i : Nat) (h : i < a.size) :
   Array.size_set ..
 
 @[simp] theorem get_set_eq (a : ByteArray) (i : Fin a.size) (v : UInt8) : (a.set i v)[i.val] = v :=
-  Array.getElem_set_self _ _ _ _
+  Array.getElem_set_self _
 
 theorem get_set_ne (a : ByteArray) (i : Fin a.size) (v : UInt8) (hj : j < a.size) (h : i.val ≠ j) :
     (a.set i v)[j]'(a.size_set .. ▸ hj) = a[j] :=
@@ -114,13 +114,13 @@ theorem get_extract_aux {a : ByteArray} {start stop} (h : i < (a.extract start s
 
 /--- `ofFn f` with `f : Fin n → UInt8` returns the byte array whose `i`th element is `f i`. --/
 @[inline] def ofFn (f : Fin n → UInt8) : ByteArray :=
-  Fin.foldl n (fun acc i => acc.push (f i)) (mkEmpty n)
+  Fin.foldl n (fun acc i => acc.push (f i)) (emptyWithCapacity n)
 
 @[simp] theorem ofFn_zero (f : Fin 0 → UInt8) : ofFn f = empty := rfl
 
 theorem ofFn_succ (f : Fin (n+1) → UInt8) :
     ofFn f = (ofFn fun i => f i.castSucc).push (f (Fin.last n)) := by
-  simp [ofFn, Fin.foldl_succ_last, mkEmpty]
+  simp [ofFn, Fin.foldl_succ_last, emptyWithCapacity]
 
 @[simp] theorem data_ofFn (f : Fin n → UInt8) : (ofFn f).data = .ofFn f := by
   induction n with
diff --git a/Batteries/Data/HashMap/Basic.lean b/Batteries/Data/HashMap/Basic.lean
@@ -23,7 +23,7 @@ abbrev _root_.Batteries.HashMap (α : Type u) (β : Type v) [BEq α] [Hashable 
 
 /-- Make a new hash map with the specified capacity. -/
 @[inline] def _root_.Batteries.mkHashMap [BEq α] [Hashable α] (capacity := 0) : HashMap α β :=
-  ⟨.empty capacity, .empty⟩
+  ⟨.emptyWithCapacity capacity, .emptyWithCapacity⟩
 
 instance [BEq α] [Hashable α] : Inhabited (HashMap α β) where
   default := mkHashMap
diff --git a/Batteries/Data/HashMap/Lemmas.lean b/Batteries/Data/HashMap/Lemmas.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
 import Batteries.Data.HashMap.Basic
+import Batteries.Tactic.Alias
 
 /-!
 # Lemmas for `Batteries.HashMap`
@@ -14,5 +15,5 @@ more lemmas. See the module `Std.Data.HashMap.Lemmas`.
 
 namespace Batteries.HashMap
 
-@[simp] theorem empty_find? [BEq α] [Hashable α] {a : α} :
-    (∅ : HashMap α β).find? a = none := Std.HashMap.getElem?_empty
+@[deprecated (since := "2025-03-31")]
+alias empty_find? := Std.HashMap.getElem?_empty
diff --git a/Batteries/Data/List/Lemmas.lean b/Batteries/Data/List/Lemmas.lean
@@ -38,7 +38,7 @@ theorem dropLast_eq_eraseIdx {xs : List α} {i : Nat} (last_idx : i + 1 = xs.len
 
 /-! ### set -/
 
-theorem set_eq_modify (a : α) : ∀ n (l : List α), set l n a = modify (fun _ => a) n l
+theorem set_eq_modify (a : α) : ∀ n (l : List α), l.set n a = l.modify n (fun _ => a)
   | 0, l => by cases l <;> rfl
   | _+1, [] => rfl
   | _+1, _ :: _ => congrArg (cons _) (set_eq_modify _ _ _)
@@ -48,7 +48,7 @@ theorem set_eq_take_cons_drop (a : α) {n l} (h : n < length l) :
   rw [set_eq_modify, modify_eq_take_cons_drop h]
 
 theorem modify_eq_set_getElem? (f : α → α) :
-    ∀ n (l : List α), l.modify f n = ((fun a => l.set n (f a)) <$> l[n]?).getD l
+    ∀ n (l : List α), l.modify n f = ((fun a => l.set n (f a)) <$> l[n]?).getD l
   | 0, l => by cases l <;> simp
   | _+1, [] => rfl
   | n+1, b :: l =>
@@ -57,7 +57,7 @@ theorem modify_eq_set_getElem? (f : α → α) :
 @[deprecated (since := "2025-02-15")] alias modify_eq_set_get? := modify_eq_set_getElem?
 
 theorem modify_eq_set_get (f : α → α) {n} {l : List α} (h) :
-    l.modify f n = l.set n (f (l.get ⟨n, h⟩)) := by
+    l.modify n f = l.set n (f (l.get ⟨n, h⟩)) := by
   rw [modify_eq_set_getElem?, getElem?_eq_getElem h]; rfl
 
 theorem getElem?_set_eq_of_lt (a : α) {n} {l : List α} (h : n < length l) :
@@ -184,7 +184,7 @@ theorem disjoint_of_disjoint_cons_left {l₁ l₂} : Disjoint (a :: l₁) l₂ 
 theorem disjoint_of_disjoint_cons_right {l₁ l₂} : Disjoint l₁ (a :: l₂) → Disjoint l₁ l₂ :=
   disjoint_of_subset_right (subset_cons_self _ _)
 
-@[simp] theorem disjoint_nil_left (l : List α) : Disjoint [] l := fun a => (not_mem_nil a).elim
+@[simp] theorem disjoint_nil_left (l : List α) : Disjoint [] l := fun _ => not_mem_nil.elim
 
 @[simp] theorem disjoint_nil_right (l : List α) : Disjoint l [] := by
   rw [disjoint_comm]; exact disjoint_nil_left _
@@ -328,7 +328,7 @@ theorem Sublist.diff_right : ∀ {l₁ l₂ l₃ : List α}, l₁ <+ l₂ → l
 
 theorem Sublist.erase_diff_erase_sublist {a : α} :
     ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → (l₂.erase a).diff (l₁.erase a) <+ l₂.diff l₁
-  | [], _, _ => erase_sublist _ _
+  | [], _, _ => erase_sublist
   | b :: l₁, l₂, h => by
     if heq : b = a then
       simp [heq]
diff --git a/Batteries/Data/List/Monadic.lean b/Batteries/Data/List/Monadic.lean
@@ -20,7 +20,7 @@ theorem satisfiesM_foldlM [Monad m] [LawfulMonad m] {f : β → α → m β} (h
   | cons hd tl ih =>
     simp only [foldlM_cons]
     apply SatisfiesM.bind_pre
-    let ⟨q, qh⟩ := h₁ b h₀ hd (mem_cons_self hd tl)
+    let ⟨q, qh⟩ := h₁ b h₀ hd mem_cons_self
     exact ⟨(fun ⟨b, bh⟩ => ⟨b, ih bh (fun b bh a am => h₁ b bh a (mem_cons_of_mem hd am))⟩) <$> q,
       by simpa using qh⟩
 
@@ -33,7 +33,7 @@ theorem satisfiesM_foldrM [Monad m] [LawfulMonad m] {f : α → β → m β} (h
     simp only [foldrM_cons]
     apply SatisfiesM.bind_pre
     let ⟨q, qh⟩ := ih (fun a am b hb => h₁ a (mem_cons_of_mem hd am) b hb)
-    exact ⟨(fun ⟨b, bh⟩ => ⟨b, h₁ hd (mem_cons_self hd tl) b bh⟩) <$> q,
+    exact ⟨(fun ⟨b, bh⟩ => ⟨b, h₁ hd mem_cons_self b bh⟩) <$> q,
       by simpa using qh⟩
 
 end List
diff --git a/Batteries/Data/List/Pairwise.lean b/Batteries/Data/List/Pairwise.lean
@@ -53,7 +53,7 @@ theorem pwFilter_map [DecidableRel (α := α) R] (f : β → α) :
   | x :: xs => by
     if h : ∀ b ∈ pwFilter R (map f xs), R (f x) b then
       have h' : ∀ b : β, b ∈ pwFilter (fun x y : β => R (f x) (f y)) xs → R (f x) (f b) :=
-        fun b hb => h _ (by rw [pwFilter_map f xs]; apply mem_map_of_mem _ hb)
+        fun b hb => h _ (by rw [pwFilter_map f xs]; apply mem_map_of_mem hb)
       rw [map, pwFilter_cons_of_pos h, pwFilter_cons_of_pos h', pwFilter_map f xs, map]
     else
       rw [map, pwFilter_cons_of_neg h, pwFilter_cons_of_neg ?_, pwFilter_map f xs]
@@ -99,7 +99,7 @@ theorem forall_mem_pwFilter [DecidableRel (α := α) R]
     (∀ b ∈ pwFilter R l, R a b) ↔ ∀ b ∈ l, R a b := by
   refine ⟨?_, fun h b hb => h _ <| pwFilter_subset (R := R) _ hb⟩
   induction l with
-  | nil => exact fun _ _ h => (not_mem_nil _ h).elim
+  | nil => exact fun _ _ h => (not_mem_nil h).elim
   | cons x l IH =>
     simp only [forall_mem_cons]
     if h : ∀ y ∈ pwFilter R l, R x y then
diff --git a/Batteries/Data/List/Perm.lean b/Batteries/Data/List/Perm.lean
@@ -79,7 +79,7 @@ theorem Subperm.filter (p : α → Bool) ⦃l l' : List α⦄ (h : l <+~ l') :
 end Subperm
 
 theorem Subperm.countP_le (p : α → Bool) {l₁ l₂ : List α} : l₁ <+~ l₂ → countP p l₁ ≤ countP p l₂
-  | ⟨_l, p', s⟩ => p'.countP_eq p ▸ s.countP_le p
+  | ⟨_l, p', s⟩ => p'.countP_eq p ▸ s.countP_le
 
 theorem Subperm.count_le [DecidableEq α] {l₁ l₂ : List α} (s : l₁ <+~ l₂) (a) :
     count a l₁ ≤ count a l₂ := s.countP_le _
@@ -102,7 +102,7 @@ theorem cons_subperm_of_not_mem_of_mem {a : α} {l₁ l₂ : List α} (h₁ : a
     | .inl e => subst_vars; exact ⟨_ :: r₁, p.cons _, s'.cons₂ _⟩
     | .inr m => let ⟨t, p', s'⟩ := ih h₁ m p; exact ⟨t, p', s'.cons _⟩
   | @cons₂ _ r₂ b _ ih =>
-    have bm : b ∈ l₁ := p.subset <| mem_cons_self _ _
+    have bm : b ∈ l₁ := p.subset mem_cons_self
     have am : a ∈ r₂ := by
       simp only [find?, mem_cons] at h₂
       exact h₂.resolve_left fun e => h₁ <| e.symm ▸ bm
@@ -174,7 +174,7 @@ theorem subperm_cons_erase (a : α) (l : List α) : l <+~ a :: l.erase a :=
   else
     (erase_of_not_mem h).symm ▸ (sublist_cons_self _ _).subperm
 
-theorem erase_subperm (a : α) (l : List α) : l.erase a <+~ l := (erase_sublist _ _).subperm
+theorem erase_subperm (a : α) (l : List α) : l.erase a <+~ l := erase_sublist.subperm
 
 theorem Subperm.erase {l₁ l₂ : List α} (a : α) (h : l₁ <+~ l₂) : l₁.erase a <+~ l₂.erase a :=
   let ⟨l, hp, hs⟩ := h
@@ -248,7 +248,7 @@ theorem subperm_append_diff_self_of_count_le {l₁ l₂ : List α}
     refine IH fun x hx => ?_
     specialize h x (.tail _ hx)
     rw [perm_iff_count.mp this] at h
-    if hx : x = hd then subst hd; simpa [Nat.succ_le_succ_iff] using h
+    if hx : hd = x then subst hd; simpa [Nat.succ_le_succ_iff] using h
     else simpa [hx] using h
 
 /-- The list version of `Multiset.le_iff_count`. -/
@@ -271,7 +271,7 @@ theorem Subperm.cons_left {l₁ l₂ : List α} (h : l₁ <+~ l₂) (x : α) (hx
   if hy' : y = x then
     subst x; simpa using Nat.succ_le_of_lt hx
   else
-    rw [count_cons_of_ne hy']
+    rw [count_cons_of_ne (Ne.symm hy')]
     refine h y ?_
     simpa [hy'] using hy
 
diff --git a/Batteries/Data/String/Lemmas.lean b/Batteries/Data/String/Lemmas.lean
@@ -430,10 +430,8 @@ theorem splitAux_of_valid (p l m r acc) :
           _ ∧ _ ∧ _),
       List.splitOnP.go, List.reverse_reverse]
     split <;> rename_i h
-    · simp_all only [List.head?_cons, Option.getD_some]
-      simpa [Nat.add_assoc] using splitAux_of_valid p (l++m++[c]) [] r (⟨m⟩::acc)
-    · simp_all only [List.head?_cons, Option.getD_some]
-      simpa [Nat.add_assoc] using splitAux_of_valid p l (m++[c]) r acc
+    · simpa [Nat.add_assoc] using splitAux_of_valid p (l++m++[c]) [] r (⟨m⟩::acc)
+    · simpa [Nat.add_assoc] using splitAux_of_valid p l (m++[c]) r acc
 
 theorem split_of_valid (s p) : split s p = (List.splitOnP p s.1).map mk := by
   simpa [split] using splitAux_of_valid p [] [] s.1 []
diff --git a/Batteries/Lean/Expr.lean b/Batteries/Lean/Expr.lean
@@ -35,7 +35,7 @@ abbrev forallArity := @getNumHeadForalls
 def withApp' (e : Expr) (k : Expr → Array Expr → α) : α :=
   let dummy := mkSort levelZero
   let nargs := e.getAppNumArgs'
-  go e (mkArray nargs dummy) (nargs - 1)
+  go e (.replicate nargs dummy) (nargs - 1)
 where
   /-- Auxiliary definition for `withApp'`. -/
   @[specialize]
diff --git a/Batteries/Linter/UnreachableTactic.lean b/Batteries/Linter/UnreachableTactic.lean
@@ -37,7 +37,7 @@ A list of blacklisted syntax kinds, which are expected to have subterms that con
 unevaluated tactics.
 -/
 initialize ignoreTacticKindsRef : IO.Ref NameHashSet ←
-  IO.mkRef <| Std.HashSet.empty
+  IO.mkRef <| (∅ : NameHashSet)
     |>.insert ``Parser.Term.binderTactic
     |>.insert ``Lean.Parser.Term.dynamicQuot
     |>.insert ``Lean.Parser.Tactic.quotSeq
diff --git a/Batteries/Tactic/Alias.lean b/Batteries/Tactic/Alias.lean
@@ -112,6 +112,7 @@ elab (name := alias) mods:declModifiers "alias " alias:ident " := " name:ident :
     addDeclarationRangesFromSyntax declName (← getRef) alias
     Term.addTermInfo' alias (← mkConstWithLevelParams declName) (isBinder := true)
     addDocString' declName declMods.docString?
+    enableRealizationsForConst declName
     Term.applyAttributes declName declMods.attrs
     let info := (← getAliasInfo name).getD <| AliasInfo.plain name
     setAliasInfo info declName
@@ -123,7 +124,7 @@ elab (name := alias) mods:declModifiers "alias " alias:ident " := " name:ident :
       let mut doc := info.toString
       if let some origDoc ← findDocString? (← getEnv) name then
         doc := s!"{doc}\n\n---\n\n{origDoc}"
-      addDocString declName doc
+      addDocStringCore declName doc
 
 /--
 Given a possibly forall-quantified iff expression `prf`, produce a value for one
@@ -158,7 +159,7 @@ private def addSide (mp : Bool) (declName : Name) (declMods : Modifiers) (thm :
     let mut doc := info.toString
     if let some origDoc ← findDocString? (← getEnv) thm.name then
       doc := s!"{doc}\n\n---\n\n{origDoc}"
-    addDocString declName doc
+    addDocStringCore declName doc
 
 @[inherit_doc «alias»]
 elab (name := aliasLR) mods:declModifiers "alias "
diff --git a/Batteries/Tactic/PrintPrefix.lean b/Batteries/Tactic/PrintPrefix.lean
@@ -53,6 +53,8 @@ private def takeNameSuffix (cnt : Nat) (name : Name) (pre : Name := .anonymous)
 private def matchName (opts : PrintPrefixConfig)
                       (pre : Name) (cinfo : ConstantInfo) : MetaM Bool := do
   let name := cinfo.name
+  unless (← hasConst name) do  -- some compiler decls are not known to the elab env, ignore them
+    return false
   let preCnt := pre.getNumParts
   let nameCnt := name.getNumParts
   if preCnt > nameCnt then return false
diff --git a/Batteries/Tactic/Trans.lean b/Batteries/Tactic/Trans.lean
@@ -169,7 +169,7 @@ elab "trans" t?:(ppSpace colGt term)? : tactic => withMainContext do
             let y ← (t'?.map (pure ·.1)).getD (mkFreshExprMVar ty)
             let g₁ ← mkFreshExprMVar (some <| ← mkAppM' rel #[x, y]) .synthetic
             let g₂ ← mkFreshExprMVar (some <| ← mkAppM' rel #[y, z]) .synthetic
-            g.assign (← mkAppOptM lem (mkArray (arity - 2) none ++ #[some g₁, some g₂]))
+            g.assign (← mkAppOptM lem (.replicate (arity - 2) none ++ #[some g₁, some g₂]))
             pure <| [g₁.mvarId!, g₂.mvarId!] ++
               if let some (_, gs') := t'? then gs' else [y.mvarId!]
           return
@@ -197,7 +197,7 @@ elab "trans" t?:(ppSpace colGt term)? : tactic => withMainContext do
           trace[Tactic.trans]"obtained g₂: {g₂}"
           let g₁ ← mkFreshExprMVar (some <| ← mkAppM' rel #[x, y]) .synthetic
           trace[Tactic.trans]"obtained g₁: {g₁}"
-          g.assign (← mkAppOptM lem (mkArray (arity - 2) none ++ #[some g₁, some g₂]))
+          g.assign (← mkAppOptM lem (.replicate (arity - 2) none ++ #[some g₁, some g₂]))
           pure <| [g₁.mvarId!, g₂.mvarId!] ++ if let some (_, gs') := t'? then gs' else [y.mvarId!]
         return
       catch e =>
diff --git a/Batteries/WF.lean b/Batteries/WF.lean
@@ -46,15 +46,13 @@ instance wfRel {r : α → α → Prop} : WellFoundedRelation { val // Acc r val
   wf  := ⟨fun ac => InvImage.accessible _ ac.2⟩
 
 /-- A computable version of `Acc.rec`. Workaround until Lean has native support for this. -/
-@[specialize, elab_as_elim] private def recC {motive : (a : α) → Acc r a → Sort v}
+@[specialize, elab_as_elim, semireducible] private def recC {motive : (a : α) → Acc r a → Sort v}
     (intro : (x : α) → (h : ∀ (y : α), r y x → Acc r y) →
      ((y : α) → (hr : r y x) → motive y (h y hr)) → motive x (intro x h))
     {a : α} (t : Acc r a) : motive a t :=
   intro a (fun _ h => t.inv h) (fun _ hr => recC intro (t.inv hr))
 termination_by Subtype.mk a t
 
-unseal recC
-
 private theorem recC_intro {motive : (a : α) → Acc r a → Sort v}
     (intro : (x : α) → (h : ∀ (y : α), r y x → Acc r y) →
      ((y : α) → (hr : r y x) → motive y (h y hr)) → motive x (intro x h))
diff --git a/BatteriesTest/help_cmd.lean b/BatteriesTest/help_cmd.lean
@@ -405,7 +405,10 @@ error: no term declarations start with foobarbaz
 #help term foobarbaz
 
 /--
-info:
+info: syntax "debug_assert!"... [Lean.Parser.Term.debugAssert]
+  `debug_assert! cond` panics if `cond` evaluates to `false` and the executing code has been built
+  with debug assertions enabled (see the `debugAssertions` option).
+
 syntax "decl_name%"... [Lean.Parser.Term.declName]
   A macro which evaluates to the name of the currently elaborating declaration.
 
@@ -415,7 +418,11 @@ syntax "default_or_ofNonempty%"... [Lean.Parser.Term.defaultOrOfNonempty]
 #help term de
 
 /--
-info:
+info: syntax "debug_assert!"... [Lean.Parser.Term.debugAssert]
+  `debug_assert! cond` panics if `cond` evaluates to `false` and the executing code has been built
+  with debug assertions enabled (see the `debugAssertions` option).
++ term elab Lean.Elab.Term.elabDebugAssert
+
 syntax "decl_name%"... [Lean.Parser.Term.declName]
   A macro which evaluates to the name of the currently elaborating declaration.
 + term elab Lean.Elab.Term.elabDeclName
diff --git a/BatteriesTest/print_prefix.lean b/BatteriesTest/print_prefix.lean
@@ -129,18 +129,12 @@ def testMatchProof : (n : Nat) → Fin n → Unit
 
 /--
 info: testMatchProof (n : Nat) : Fin n → Unit
-testMatchProof._cstage1 (n : Nat) : Fin n → Unit
-testMatchProof._cstage2 : _obj → _obj → _obj
+testMatchProof._proof_1 (as i : Nat) (h : i.succ < as.succ) : i.succ ≤ as
 testMatchProof._sunfold (n : Nat) : Fin n → Unit
 testMatchProof._unsafe_rec (n : Nat) : Fin n → Unit
 testMatchProof.match_1.{u_1} (motive : (x : Nat) → Fin x → Sort u_1) (x✝ : Nat) (x✝¹ : Fin x✝)
   (h_1 : (n : Nat) → (isLt : 0 < n) → motive n ⟨0, isLt⟩)
   (h_2 : (as i : Nat) → (h : i.succ < as.succ) → motive as.succ ⟨i.succ, h⟩) : motive x✝ x✝¹
-testMatchProof.match_1._cstage1.{u_1} (motive : (x : Nat) → Fin x → Sort u_1) (x✝ : Nat) (x✝¹ : Fin x✝)
-  (h_1 : (n : Nat) → (isLt : 0 < n) → motive n ⟨0, isLt⟩)
-  (h_2 : (as i : Nat) → (h : i.succ < as.succ) → motive as.succ ⟨i.succ, h⟩) : motive x✝ x✝¹
-testMatchProof.proof_1 (as i : Nat) (h : i.succ < as.succ) : i.succ ≤ as
-testMatchProof.proof_2 (as i : Nat) (h : i.succ < as.succ) : i.succ ≤ as
 -/
 #guard_msgs in
 #print prefix +internals testMatchProof
diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.18.0
+leanprover/lean4:v4.19.0-rc1
diff --git a/scripts/runLinter.lean b/scripts/runLinter.lean
@@ -28,17 +28,14 @@ def resolveDefaultRootModules : IO (Array Name) := do
   let some workspace ← loadWorkspace config |>.toBaseIO
     | throw <| IO.userError "failed to load Lake workspace"
 
-  -- resolve the default build specs from the Lake workspace (based on `lake build`)
-  let defaultBuildSpecs ← match resolveDefaultPackageTarget workspace workspace.root with
-    | Except.error e => IO.eprintln s!"Error getting default package target: {e}" *> IO.Process.exit 1
-    | Except.ok targets => pure targets
-
-  -- build an array of all root modules of `lean_exe` and `lean_lib` build targets
-  let defaultTargetModules := defaultBuildSpecs.flatMap <|
-    fun target => match target.info with
-      | BuildInfo.libraryFacet lib _ => lib.roots
-      | BuildInfo.leanExe exe => #[exe.config.root]
-      | _ => #[]
+  -- build an array of all root modules of `lean_exe` and `lean_lib` default targets
+  let defaultTargetModules := workspace.root.defaultTargets.flatMap fun target =>
+    if let some lib := workspace.root.findLeanLib? target then
+      lib.roots
+    else if let some exe := workspace.root.findLeanExe? target then
+      #[exe.config.root]
+    else
+      #[]
   return defaultTargetModules
 
 /--
