Merge remote-tracking branch 'origin/master' into sg/new-mvcgen

Author: sgraf812

.github/workflows/ci.yml

@@ -545,7 +545,7 @@ jobs:
           GITHUB_TOKEN: ${{ secrets.RELEASE_INDEX_TOKEN }}
       - name: Generate mathlib nightly-testing app token
         id: mathlib-app-token
-        uses: actions/create-github-app-token@29824e69f54612133e76f7eaac726eef6c875baf # v2.2.1
+        uses: actions/create-github-app-token@f8d387b68d61c58ab83c6c016672934102569859 # v3.0.0
         continue-on-error: true
         with:
           app-id: ${{ secrets.MATHLIB_NIGHTLY_TESTING_APP_ID }}

.github/workflows/grove.yml

@@ -59,7 +59,7 @@ jobs:
       - name: Download toolchain for this commit
         if: ${{ steps.should-run.outputs.should-run == 'true' }}
         id: download-toolchain
-        uses: dawidd6/action-download-artifact@v11
+        uses: dawidd6/action-download-artifact@v19
         with:
           commit: ${{ steps.workflow-info.outputs.sourceHeadSha }}
           workflow: ci.yml
@@ -147,7 +147,7 @@ jobs:
       # https://github.com/nwtgck/actions-netlify/issues/545
       # We work around by using a comment to post the latest link
       - name: "Comment on PR with preview links"
-        uses: marocchino/sticky-pull-request-comment@v2
+        uses: marocchino/sticky-pull-request-comment@v3
         if: ${{ steps.should-run.outputs.should-run == 'true' && steps.workflow-info.outputs.pullRequestNumber != '' }}
         with:
           number: ${{ env.PR_NUMBER }}

.github/workflows/pr-release.yml

@@ -36,7 +36,7 @@ jobs:
       - name: Download artifact from the previous workflow.
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
         id: download-artifact
-        uses: dawidd6/action-download-artifact@v11 # https://github.com/marketplace/actions/download-workflow-artifact
+        uses: dawidd6/action-download-artifact@v19 # https://github.com/marketplace/actions/download-workflow-artifact
         with:
           run_id: ${{ github.event.workflow_run.id }}
           path: artifacts
@@ -175,7 +175,7 @@ jobs:
       - name: Generate GitHub App token for Lean PR comments
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
         id: mathlib-comment-token
-        uses: actions/create-github-app-token@3ff1caaa28b64c9cc276ce0a02e2ff584f3900c5 # v2.0.2
+        uses: actions/create-github-app-token@f8d387b68d61c58ab83c6c016672934102569859 # v3.0.0
         with:
           app-id: ${{ secrets.MATHLIB_LEAN_PR_TESTING_APP_ID }}
           private-key: ${{ secrets.MATHLIB_LEAN_PR_TESTING_PRIVATE_KEY }}
@@ -414,7 +414,7 @@ jobs:
       - name: Generate GitHub App token for leanprover-community repos
         if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
         id: mathlib-app-token
-        uses: actions/create-github-app-token@3ff1caaa28b64c9cc276ce0a02e2ff584f3900c5 # v2.0.2
+        uses: actions/create-github-app-token@f8d387b68d61c58ab83c6c016672934102569859 # v3.0.0
         with:
           app-id: ${{ secrets.MATHLIB_NIGHTLY_TESTING_APP_ID }}
           private-key: ${{ secrets.MATHLIB_NIGHTLY_TESTING_PRIVATE_KEY }}

src/Init/Control/Except.lean

@@ -330,6 +330,7 @@ instance ExceptT.finally {m : Type u → Type v} {ε : Type u} [MonadFinally m]
     | (_,        .error e) => pure (.error e)  -- second error has precedence
     | (.error e, _)        => pure (.error e)
 
+set_option linter.checkUnivs false in
 instance [Monad m] [MonadAttach m] : MonadAttach (ExceptT ε m) where
   CanReturn x a := MonadAttach.CanReturn (m := m) x (.ok a)
   attach x := show m (Except ε _) from

src/Init/Control/Lawful/Instances.lean

@@ -32,6 +32,7 @@ namespace ExceptT
 
 @[simp] theorem stM_eq [Monad m] : stM m (ExceptT ε m) α = Except ε α := rfl
 
+set_option linter.checkUnivs false in
 @[simp, grind =] theorem run_mk (x : m (Except ε α)) : run (mk x : ExceptT ε m α) = x := rfl
 
 @[simp, grind =] theorem run_pure [Monad m] (x : α) : run (pure x : ExceptT ε m α) = pure (Except.ok x) := rfl

src/Init/Data/Array/Lemmas.lean

@@ -4348,6 +4348,7 @@ theorem sum_toList [Add α] [Zero α] {as : Array α} : as.toList.sum = as.sum :
   cases as
   simp [Array.sum, List.sum]
 
+set_option linter.defProp false in
 @[deprecated sum_toList (since := "2026-01-14")]
 def sum_eq_sum_toList := @sum_toList
 

src/Init/Data/Array/Subarray.lean

@@ -66,10 +66,12 @@ def Subarray.start (xs : Subarray α) : Nat :=
 def Subarray.stop (xs : Subarray α) : Nat :=
   xs.internalRepresentation.stop
 
+set_option linter.defProp false in
 @[always_inline, inline, expose, inherit_doc Internal.SubarrayData.start_le_stop]
 def Subarray.start_le_stop (xs : Subarray α) : xs.start ≤ xs.stop :=
   xs.internalRepresentation.start_le_stop
 
+set_option linter.defProp false in
 @[always_inline, inline, expose, inherit_doc Internal.SubarrayData.stop_le_array_size]
 def Subarray.stop_le_array_size (xs : Subarray α) : xs.stop ≤ xs.array.size :=
   xs.internalRepresentation.stop_le_array_size

src/Init/Data/BitVec/Bitblast.lean

@@ -873,7 +873,7 @@ structure DivModState.Lawful {w : Nat} (args : DivModArgs w) (qr : DivModState w
   hdiv : args.n.toNat >>> qr.wn = args.d.toNat * qr.q.toNat + qr.r.toNat
 
 /-- A lawful DivModState implies `w > 0`. -/
-def DivModState.Lawful.hw {args : DivModArgs w} {qr : DivModState w}
+theorem DivModState.Lawful.hw {args : DivModArgs w} {qr : DivModState w}
     {h : DivModState.Lawful args qr} : 0 < w := by
   have hd := h.hdPos
   rcases w with rfl | w
@@ -891,7 +891,7 @@ def DivModState.init (w : Nat) : DivModState w := {
 }
 
 /-- The initial state is lawful. -/
-def DivModState.lawful_init {w : Nat} (args : DivModArgs w) (hd : 0#w < args.d) :
+theorem DivModState.lawful_init {w : Nat} (args : DivModArgs w) (hd : 0#w < args.d) :
     DivModState.Lawful args (DivModState.init w) := by
   simp only [BitVec.DivModState.init]
   exact {
@@ -951,7 +951,7 @@ structure DivModState.Poised {w : Nat} (args : DivModArgs w) (qr : DivModState w
 In the shift subtract input, the dividend is at least one bit long (`wn > 0`), so
 the remainder has bits to be computed (`wr < w`).
 -/
-def DivModState.wr_lt_w {qr : DivModState w} (h : qr.Poised args) : qr.wr < w := by
+theorem DivModState.wr_lt_w {qr : DivModState w} (h : qr.Poised args) : qr.wr < w := by
   have hwrn := h.hwrn
   have hwn_lt := h.hwn_lt
   omega

src/Init/Data/Fin/Lemmas.lean

@@ -520,8 +520,6 @@ theorem coe_cast (h : n = m) (i : Fin n) : (i.cast h : Nat) = i := rfl
 @[simp, grind =] theorem cast_cast {k : Nat} (h : n = m) (h' : m = k) {i : Fin n} :
     (i.cast h).cast h' = i.cast (Eq.trans h h') := rfl
 
-@[deprecated cast_cast (since := "2025-09-03")] abbrev cast_trans := @cast_cast
-
 theorem castLE_of_eq {m n : Nat} (h : m = n) {h' : m ≤ n} : castLE h' = Fin.cast h := rfl
 
 @[simp, grind =] theorem val_castAdd (m : Nat) (i : Fin n) : (castAdd m i : Nat) = i := rfl

src/Init/Data/Int/DivMod/Bootstrap.lean

@@ -111,27 +111,15 @@ where
       ← Int.neg_neg (_-_), Int.neg_sub, Int.sub_sub_self, Int.add_right_comm]
     exact congrArg (fun x => -(ofNat x + 1)) (Nat.mod_add_div ..)
 
-@[deprecated emod_add_mul_ediv (since := "2025-09-01")]
-def emod_add_ediv := @emod_add_mul_ediv
-
 theorem emod_add_ediv_mul (a b : Int) : a % b + a / b * b = a := by
   rw [Int.mul_comm]; exact emod_add_mul_ediv ..
 
-@[deprecated emod_add_ediv_mul (since := "2025-09-01")]
-def emod_add_ediv' := @emod_add_ediv_mul
-
 theorem mul_ediv_add_emod (a b : Int) : b * (a / b) + a % b = a := by
   rw [Int.add_comm]; exact emod_add_mul_ediv ..
 
-@[deprecated mul_ediv_add_emod (since := "2025-09-01")]
-def ediv_add_emod := @mul_ediv_add_emod
-
 theorem ediv_mul_add_emod (a b : Int) : a / b * b + a % b = a := by
   rw [Int.mul_comm]; exact mul_ediv_add_emod ..
 
-@[deprecated ediv_mul_add_emod (since := "2025-09-01")]
-def ediv_add_emod' := @ediv_mul_add_emod
-
 theorem emod_def (a b : Int) : a % b = a - b * (a / b) := by
   rw [← Int.add_sub_cancel (a % b), emod_add_mul_ediv]