fix: use getDecLevel/isLevelDefEq for for loop mut var universe constraints (#13332)

This PR fixes universe unification for `for` loops with `mut` variables
whose types span multiple implicit universes. The old approach used
`ensureHasType (mkSort mi.u.succ)` per variable, which generated
constraints like `max (?u+1) (?v+1) =?= ?u+1` that the universe solver
cannot decompose. The new approach uses `getDecLevel`/`isLevelDefEq` on
the decremented level, producing `max ?u ?v =?= ?u` which `solveSelfMax`
handles directly.

Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>

.github/workflows/build-template.yml

@@ -131,7 +131,7 @@ jobs:
           [ -d build ] || mkdir build
           cd build
           # arguments passed to `cmake`
-          OPTIONS=(-DLEAN_EXTRA_MAKE_OPTS=-DwarningAsError=true)
+          OPTIONS=(-DWFAIL=ON)
           if [[ -n '${{ matrix.release }}' ]]; then
             # this also enables githash embedding into stage 1 library, which prohibits reusing
             # `.olean`s across commits, so we don't do it in the fast non-release CI

.github/workflows/update-stage0.yml

@@ -77,7 +77,7 @@ jobs:
       # sync options with `Linux Lake` to ensure cache reuse
       run: |
         mkdir -p build
-        cmake --preset release -B build -DLEAN_EXTRA_MAKE_OPTS=-DwarningAsError=true
+        cmake --preset release -B build -DWFAIL=ON
       shell: 'nix develop -c bash -euxo pipefail {0}'
     - if: env.should_update_stage0 == 'yes'
       run: |

script/release_steps.py

@@ -481,11 +481,9 @@ def execute_release_steps(repo, version, config):
         run_command("lake update", cwd=repo_path, stream_output=True)
     elif repo_name == "verso":
         # verso has nested Lake projects in test-projects/ that each have their own
-        # lake-manifest.json with a subverso pin. After updating the root manifest via
-        # `lake update`, sync the de-modulized subverso rev into all sub-manifests.
-        # The sub-projects use an old toolchain (v4.21.0) that doesn't support module/prelude
-        # syntax, so they need the de-modulized version (tagged no-modules/<root-rev>).
-        # The "SubVerso version consistency" CI check accepts either the root or de-modulized rev.
+        # lake-manifest.json with a subverso pin and their own lean-toolchain.
+        # After updating the root manifest via `lake update`, sync the de-modulized
+        # subverso rev into all sub-manifests, and update their lean-toolchain files.
         run_command("lake update", cwd=repo_path, stream_output=True)
         print(blue("Syncing de-modulized subverso rev to test-project sub-manifests..."))
         sync_script = (
@@ -498,6 +496,15 @@ def execute_release_steps(repo, version, config):
         )
         run_command(sync_script, cwd=repo_path)
         print(green("Synced de-modulized subverso rev to all test-project sub-manifests"))
+        # Update all lean-toolchain files in test-projects/ to match the root
+        print(blue("Updating lean-toolchain files in test-projects/..."))
+        find_result = run_command("find test-projects -name lean-toolchain", cwd=repo_path)
+        for tc_path in find_result.stdout.strip().splitlines():
+            if tc_path:
+                tc_file = repo_path / tc_path
+                with open(tc_file, "w") as f:
+                    f.write(f"leanprover/lean4:{version}\n")
+                print(green(f"  Updated {tc_path}"))
     elif dependencies:
         run_command(f'perl -pi -e \'s/"v4\\.[0-9]+(\\.[0-9]+)?(-rc[0-9]+)?"/"' + version + '"/g\' lakefile.*', cwd=repo_path)
         run_command("lake update", cwd=repo_path, stream_output=True)
@@ -659,56 +666,61 @@ def execute_release_steps(repo, version, config):
         # Fetch latest changes to ensure we have the most up-to-date nightly-testing branch
         print(blue("Fetching latest changes from origin..."))
         run_command("git fetch origin", cwd=repo_path)
-        
-        try:
-            print(blue("Merging origin/nightly-testing..."))
-            run_command("git merge origin/nightly-testing", cwd=repo_path)
-            print(green("Merge completed successfully"))
-        except subprocess.CalledProcessError:
-            # Merge failed due to conflicts - check which files are conflicted
-            print(blue("Merge conflicts detected, checking which files are affected..."))
-            
-            # Get conflicted files using git status
-            status_result = run_command("git status --porcelain", cwd=repo_path)
-            conflicted_files = []
-            
-            for line in status_result.stdout.splitlines():
-                if len(line) >= 2 and line[:2] in ['UU', 'AA', 'DD', 'AU', 'UA', 'DU', 'UD']:
-                    # Extract filename (skip the first 3 characters which are status codes)
-                    conflicted_files.append(line[3:])
-            
-            # Filter out allowed files
-            allowed_patterns = ['lean-toolchain', 'lake-manifest.json']
-            problematic_files = []
-            
-            for file in conflicted_files:
-                is_allowed = any(pattern in file for pattern in allowed_patterns)
-                if not is_allowed:
-                    problematic_files.append(file)
-            
-            if problematic_files:
-                # There are conflicts in non-allowed files - fail
-                print(red("❌ Merge failed!"))
-                print(red(f"Merging nightly-testing resulted in conflicts in:"))
-                for file in problematic_files:
-                    print(red(f"  - {file}"))
-                print(red("Please resolve these conflicts manually."))
-                return
-            else:
-                # Only allowed files are conflicted - resolve them automatically
-                print(green(f"✅ Only allowed files conflicted: {', '.join(conflicted_files)}"))
-                print(blue("Resolving conflicts automatically..."))
-                
-                # For lean-toolchain and lake-manifest.json, keep our versions
+
+        # Check if nightly-testing branch exists on origin (use local ref after fetch for exact match)
+        nightly_check = run_command("git show-ref --verify --quiet refs/remotes/origin/nightly-testing", cwd=repo_path, check=False)
+        if nightly_check.returncode != 0:
+            print(yellow("No nightly-testing branch found on origin, skipping merge"))
+        else:
+            try:
+                print(blue("Merging origin/nightly-testing..."))
+                run_command("git merge origin/nightly-testing", cwd=repo_path)
+                print(green("Merge completed successfully"))
+            except subprocess.CalledProcessError:
+                # Merge failed due to conflicts - check which files are conflicted
+                print(blue("Merge conflicts detected, checking which files are affected..."))
+
+                # Get conflicted files using git status
+                status_result = run_command("git status --porcelain", cwd=repo_path)
+                conflicted_files = []
+
+                for line in status_result.stdout.splitlines():
+                    if len(line) >= 2 and line[:2] in ['UU', 'AA', 'DD', 'AU', 'UA', 'DU', 'UD']:
+                        # Extract filename (skip the first 3 characters which are status codes)
+                        conflicted_files.append(line[3:])
+
+                # Filter out allowed files
+                allowed_patterns = ['lean-toolchain', 'lake-manifest.json']
+                problematic_files = []
+
                 for file in conflicted_files:
-                    print(blue(f"Keeping our version of {file}"))
-                    run_command(f"git checkout --ours {file}", cwd=repo_path)
-                
-                # Complete the merge
-                run_command("git add .", cwd=repo_path)
-                run_command("git commit --no-edit", cwd=repo_path)
-                
-                print(green("✅ Merge completed successfully with automatic conflict resolution"))
+                    is_allowed = any(pattern in file for pattern in allowed_patterns)
+                    if not is_allowed:
+                        problematic_files.append(file)
+
+                if problematic_files:
+                    # There are conflicts in non-allowed files - fail
+                    print(red("❌ Merge failed!"))
+                    print(red(f"Merging nightly-testing resulted in conflicts in:"))
+                    for file in problematic_files:
+                        print(red(f"  - {file}"))
+                    print(red("Please resolve these conflicts manually."))
+                    return
+                else:
+                    # Only allowed files are conflicted - resolve them automatically
+                    print(green(f"✅ Only allowed files conflicted: {', '.join(conflicted_files)}"))
+                    print(blue("Resolving conflicts automatically..."))
+
+                    # For lean-toolchain and lake-manifest.json, keep our versions
+                    for file in conflicted_files:
+                        print(blue(f"Keeping our version of {file}"))
+                        run_command(f"git checkout --ours {file}", cwd=repo_path)
+
+                    # Complete the merge
+                    run_command("git add .", cwd=repo_path)
+                    run_command("git commit --no-edit", cwd=repo_path)
+
+                    print(green("✅ Merge completed successfully with automatic conflict resolution"))
 
     # Build and test (skip for Mathlib)
     if repo_name not in ["mathlib4"]:

src/CMakeLists.txt

@@ -116,11 +116,19 @@ option(CHECK_OLEAN_VERSION "Only load .olean files compiled with the current ver
 option(USE_LAKE "Use Lake instead of lean.mk for building core libs from language server" ON)
 option(USE_LAKE_CACHE "Use the Lake artifact cache for stage 1 builds (requires USE_LAKE)" OFF)
 
-set(LEAN_EXTRA_MAKE_OPTS "" CACHE STRING "extra options to lean --make")
+set(LEAN_EXTRA_OPTS "" CACHE STRING "extra options to lean (via lake or make)")
+set(LEAN_EXTRA_MAKE_OPTS "" CACHE STRING "extra options to leanmake")
 set(LEANC_CC ${CMAKE_C_COMPILER} CACHE STRING "C compiler to use in `leanc`")
 
 # Temporary, core-only flags. Must be synced with stdlib_flags.h.
-string(APPEND LEAN_EXTRA_MAKE_OPTS " -Dbackward.do.legacy=false")
+string(APPEND LEAN_EXTRA_OPTS " -Dbackward.do.legacy=false")
+
+# option used by the CI to fail on warnings
+option(WFAIL "Fail build if warnings are emitted by Lean" ON)
+if(WFAIL MATCHES "ON")
+  string(APPEND LAKE_EXTRA_ARGS " --wfail")
+  string(APPEND LEAN_EXTRA_MAKE_OPTS " -DwarningAsError=true")
+endif()
 
 if(LAZY_RC MATCHES "ON")
   set(LEAN_LAZY_RC "#define LEAN_LAZY_RC")
@@ -198,7 +206,7 @@ set(CMAKE_ARCHIVE_OUTPUT_DIRECTORY "${CMAKE_BINARY_DIR}/lib/lean")
 
 # OSX default thread stack size is very small. Moreover, in Debug mode, each new stack frame consumes a lot of extra memory.
 if((MULTI_THREAD MATCHES "ON") AND (CMAKE_SYSTEM_NAME MATCHES "Darwin"))
-  string(APPEND LEAN_EXTRA_MAKE_OPTS " -s40000")
+  string(APPEND LEAN_EXTRA_OPTS " -s40000")
 endif()
 
 # We want explicit stack probes in huge Lean stack frames for robust stack overflow detection
@@ -670,6 +678,9 @@ else()
   set(LEAN_PATH_SEPARATOR ":")
 endif()
 
+# inherit genral options for lean.mk.in and stdlib.make.in
+string(APPEND LEAN_EXTRA_MAKE_OPTS " ${LEAN_EXTRA_OPTS}")
+
 # Version
 configure_file("${LEAN_SOURCE_DIR}/version.h.in" "${LEAN_BINARY_DIR}/include/lean/version.h")
 if(STAGE EQUAL 0)
@@ -1054,7 +1065,7 @@ string(REPLACE "ROOT" "${CMAKE_BINARY_DIR}" LEANC_CC "${LEANC_CC}")
 string(REPLACE "ROOT" "${CMAKE_BINARY_DIR}" LEANC_INTERNAL_FLAGS "${LEANC_INTERNAL_FLAGS}")
 string(REPLACE "ROOT" "${CMAKE_BINARY_DIR}" LEANC_INTERNAL_LINKER_FLAGS "${LEANC_INTERNAL_LINKER_FLAGS}")
 
-toml_escape("${LEAN_EXTRA_MAKE_OPTS}" LEAN_EXTRA_OPTS_TOML)
+toml_escape("${LEAN_EXTRA_OPTS}" LEAN_EXTRA_OPTS_TOML)
 
 if(CMAKE_BUILD_TYPE MATCHES "Debug|Release|RelWithDebInfo|MinSizeRel")
   set(CMAKE_BUILD_TYPE_TOML "${CMAKE_BUILD_TYPE}")

src/Init/Data/Array/Basic.lean

@@ -1085,6 +1085,17 @@ Examples:
 def sum {α} [Add α] [Zero α] : Array α → α :=
   foldr (· + ·) 0
 
+/--
+Computes the product of the elements of an array.
+
+Examples:
+ * `#[a, b, c].prod = a * (b * (c * 1))`
+ * `#[1, 2, 5].prod = 10`
+-/
+@[inline, expose]
+def prod {α} [Mul α] [One α] : Array α → α :=
+  foldr (· * ·) 1
+
 /--
 Counts the number of elements in the array `as` that satisfy the Boolean predicate `p`.
 

src/Init/Data/Array/Int.lean

@@ -7,6 +7,7 @@ module
 
 prelude
 public import Init.Data.List.Int.Sum
+public import Init.Data.List.Int.Prod
 public import Init.Data.Array.MinMax
 import Init.Data.Int.Lemmas
 
@@ -74,4 +75,17 @@ theorem sum_div_length_le_max_of_max?_eq_some_int {xs : Array Int} (h : xs.max?
   simpa [List.max?_toArray, List.sum_toArray] using
     List.sum_div_length_le_max_of_max?_eq_some_int (by simpa using h)
 
+@[simp] theorem prod_replicate_int {n : Nat} {a : Int} : (replicate n a).prod = a ^ n := by
+  rw [← List.toArray_replicate, List.prod_toArray]
+  simp
+
+theorem prod_append_int {as₁ as₂ : Array Int} : (as₁ ++ as₂).prod = as₁.prod * as₂.prod := by
+  simp [prod_append]
+
+theorem prod_reverse_int (xs : Array Int) : xs.reverse.prod = xs.prod := by
+  simp [prod_reverse]
+
+theorem prod_eq_foldl_int {xs : Array Int} : xs.prod = xs.foldl (init := 1) (· * ·) := by
+  simp only [foldl_eq_foldr_reverse, Int.mul_comm, ← prod_eq_foldr, prod_reverse_int]
+
 end Array

src/Init/Data/Array/Lemmas.lean

@@ -4380,6 +4380,47 @@ theorem sum_eq_foldl [Zero α] [Add α] [Std.Associative (α := α) (· + ·)]
     xs.sum = xs.foldl (init := 0) (· + ·) := by
   simp [← sum_toList, List.sum_eq_foldl]
 
+/-! ### prod -/
+
+@[simp, grind =] theorem prod_empty [Mul α] [One α] : (#[] : Array α).prod = 1 := rfl
+theorem prod_eq_foldr [Mul α] [One α] {xs : Array α} :
+    xs.prod = xs.foldr (init := 1) (· * ·) :=
+  rfl
+
+@[simp, grind =]
+theorem prod_toList [Mul α] [One α] {as : Array α} : as.toList.prod = as.prod := by
+  cases as
+  simp [Array.prod, List.prod]
+
+@[simp, grind =]
+theorem prod_append [One α] [Mul α] [Std.Associative (α := α) (· * ·)]
+    [Std.LawfulLeftIdentity (α := α) (· * ·) 1]
+    {as₁ as₂ : Array α} : (as₁ ++ as₂).prod = as₁.prod * as₂.prod := by
+  simp [← prod_toList, List.prod_append]
+
+@[simp, grind =]
+theorem prod_singleton [Mul α] [One α] [Std.LawfulRightIdentity (· * ·) (1 : α)] {x : α} :
+    #[x].prod = x := by
+  simp [Array.prod_eq_foldr, Std.LawfulRightIdentity.right_id x]
+
+@[simp, grind =]
+theorem prod_push [Mul α] [One α] [Std.Associative (α := α) (· * ·)]
+    [Std.LawfulIdentity (· * ·) (1 : α)] {xs : Array α} {x : α} :
+    (xs.push x).prod = xs.prod * x := by
+  simp [Array.prod_eq_foldr, Std.LawfulRightIdentity.right_id, Std.LawfulLeftIdentity.left_id,
+    ← Array.foldr_assoc]
+
+@[simp, grind =]
+theorem prod_reverse [One α] [Mul α] [Std.Associative (α := α) (· * ·)]
+    [Std.Commutative (α := α) (· * ·)]
+    [Std.LawfulLeftIdentity (α := α) (· * ·) 1] (xs : Array α) : xs.reverse.prod = xs.prod := by
+  simp [← prod_toList, List.prod_reverse]
+
+theorem prod_eq_foldl [One α] [Mul α] [Std.Associative (α := α) (· * ·)]
+    [Std.LawfulIdentity (· * ·) (1 : α)] {xs : Array α} :
+    xs.prod = xs.foldl (init := 1) (· * ·) := by
+  simp [← prod_toList, List.prod_eq_foldl]
+
 theorem foldl_toList_eq_flatMap {l : List α} {acc : Array β}
     {F : Array β → α → Array β} {G : α → List β}
     (H : ∀ acc a, (F acc a).toList = acc.toList ++ G a) :

src/Init/Data/Array/Nat.lean

@@ -8,6 +8,7 @@ module
 prelude
 public import Init.Data.Array.MinMax
 import Init.Data.List.Nat.Sum
+import Init.Data.List.Nat.Prod
 import Init.Data.Array.Lemmas
 
 public section
@@ -81,4 +82,24 @@ theorem sum_div_length_le_max_of_max?_eq_some_nat {xs : Array Nat} (h : xs.max?
   simpa [List.max?_toArray, List.sum_toArray] using
     List.sum_div_length_le_max_of_max?_eq_some_nat (by simpa using h)
 
+protected theorem prod_pos_iff_forall_pos_nat {xs : Array Nat} : 0 < xs.prod ↔ ∀ x ∈ xs, 0 < x := by
+  simp [← prod_toList, List.prod_pos_iff_forall_pos_nat]
+
+protected theorem prod_eq_zero_iff_exists_zero_nat {xs : Array Nat} :
+    xs.prod = 0 ↔ ∃ x ∈ xs, x = 0 := by
+  simp [← prod_toList, List.prod_eq_zero_iff_exists_zero_nat]
+
+@[simp] theorem prod_replicate_nat {n : Nat} {a : Nat} : (replicate n a).prod = a ^ n := by
+  rw [← List.toArray_replicate, List.prod_toArray]
+  simp
+
+theorem prod_append_nat {as₁ as₂ : Array Nat} : (as₁ ++ as₂).prod = as₁.prod * as₂.prod := by
+  simp [prod_append]
+
+theorem prod_reverse_nat (xs : Array Nat) : xs.reverse.prod = xs.prod := by
+  simp [prod_reverse]
+
+theorem prod_eq_foldl_nat {xs : Array Nat} : xs.prod = xs.foldl (init := 1) (· * ·) := by
+  simp only [foldl_eq_foldr_reverse, Nat.mul_comm, ← prod_eq_foldr, prod_reverse_nat]
+
 end Array

src/Init/Data/List/Basic.lean

@@ -2056,6 +2056,20 @@ def sum {α} [Add α] [Zero α] : List α → α :=
 @[simp, grind =] theorem sum_cons [Add α] [Zero α] {a : α} {l : List α} : (a::l).sum = a + l.sum := rfl
 theorem sum_eq_foldr [Add α] [Zero α] {l : List α} : l.sum = l.foldr (· + ·) 0 := rfl
 
+/--
+Computes the product of the elements of a list.
+
+Examples:
+ * `[a, b, c].prod = a * (b * (c * 1))`
+ * `[1, 2, 5].prod = 10`
+-/
+def prod {α} [Mul α] [One α] : List α → α :=
+  foldr (· * ·) 1
+
+@[simp, grind =] theorem prod_nil [Mul α] [One α] : ([] : List α).prod = 1 := rfl
+@[simp, grind =] theorem prod_cons [Mul α] [One α] {a : α} {l : List α} : (a::l).prod = a * l.prod := rfl
+theorem prod_eq_foldr [Mul α] [One α] {l : List α} : l.prod = l.foldr (· * ·) 1 := rfl
+
 /-! ### range -/
 
 /--

src/Init/Data/List/Int.lean

@@ -7,3 +7,4 @@ module
 
 prelude
 public import Init.Data.List.Int.Sum
+public import Init.Data.List.Int.Prod

src/Init/Data/List/Int/Prod.lean

@@ -0,0 +1,31 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+module
+
+prelude
+import Init.Data.List.Lemmas
+import Init.Data.Int.Lemmas
+public import Init.Data.Int.Pow
+public import Init.Data.List.Basic
+
+public section
+
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+
+namespace List
+
+@[simp]
+theorem prod_replicate_int {n : Nat} {a : Int} : (replicate n a).prod = a ^ n := by
+  induction n <;> simp_all [replicate_succ, Int.pow_succ, Int.mul_comm]
+
+theorem prod_append_int {l₁ l₂ : List Int} : (l₁ ++ l₂).prod = l₁.prod * l₂.prod := by
+  simp [prod_append]
+
+theorem prod_reverse_int (xs : List Int) : xs.reverse.prod = xs.prod := by
+  simp [prod_reverse]
+
+end List

src/Init/Data/List/Lemmas.lean

@@ -1878,6 +1878,24 @@ theorem sum_reverse [Zero α] [Add α] [Std.Associative (α := α) (· + ·)]
     simp_all [sum_append, Std.Commutative.comm (α := α) _ 0,
       Std.LawfulLeftIdentity.left_id, Std.Commutative.comm]
 
+@[simp, grind =]
+theorem prod_append [Mul α] [One α] [Std.LawfulLeftIdentity (α := α) (· * ·) 1]
+    [Std.Associative (α := α) (· * ·)] {l₁ l₂ : List α} : (l₁ ++ l₂).prod = l₁.prod * l₂.prod := by
+  induction l₁ generalizing l₂ <;> simp_all [Std.Associative.assoc, Std.LawfulLeftIdentity.left_id]
+
+@[simp, grind =]
+theorem prod_singleton [Mul α] [One α] [Std.LawfulRightIdentity (· * ·) (1 : α)] {x : α} :
+    [x].prod = x := by
+  simp [List.prod_eq_foldr, Std.LawfulRightIdentity.right_id x]
+
+@[simp, grind =]
+theorem prod_reverse [One α] [Mul α] [Std.Associative (α := α) (· * ·)]
+    [Std.Commutative (α := α) (· * ·)]
+    [Std.LawfulLeftIdentity (α := α) (· * ·) 1] (xs : List α) : xs.reverse.prod = xs.prod := by
+  induction xs <;>
+    simp_all [prod_append, Std.Commutative.comm (α := α) _ 1,
+      Std.LawfulLeftIdentity.left_id, Std.Commutative.comm]
+
 /-! ### concat
 
 Note that `concat_eq_append` is a `@[simp]` lemma, so `concat` should usually not appear in goals.
@@ -2784,6 +2802,11 @@ theorem sum_eq_foldl [Zero α] [Add α] [Std.Associative (α := α) (· + ·)]
     xs.sum = xs.foldl (init := 0) (· + ·) := by
   simp [sum_eq_foldr, foldl_eq_apply_foldr, Std.LawfulLeftIdentity.left_id]
 
+theorem prod_eq_foldl [One α] [Mul α] [Std.Associative (α := α) (· * ·)]
+    [Std.LawfulIdentity (· * ·) (1 : α)] {xs : List α} :
+    xs.prod = xs.foldl (init := 1) (· * ·) := by
+  simp [prod_eq_foldr, foldl_eq_apply_foldr, Std.LawfulLeftIdentity.left_id]
+
 -- The argument `f : α₁ → α₂` is intentionally explicit, as it is sometimes not found by unification.
 theorem foldl_hom (f : α₁ → α₂) {g₁ : α₁ → β → α₁} {g₂ : α₂ → β → α₂} {l : List β} {init : α₁}
     (H : ∀ x y, g₂ (f x) y = f (g₁ x y)) : l.foldl g₂ (f init) = f (l.foldl g₁ init) := by

src/Init/Data/List/Nat.lean

@@ -13,6 +13,7 @@ public import Init.Data.List.Nat.Sublist
 public import Init.Data.List.Nat.TakeDrop
 public import Init.Data.List.Nat.Count
 public import Init.Data.List.Nat.Sum
+public import Init.Data.List.Nat.Prod
 public import Init.Data.List.Nat.Erase
 public import Init.Data.List.Nat.Find
 public import Init.Data.List.Nat.BEq

src/Init/Data/List/Nat/Prod.lean

@@ -0,0 +1,50 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+module
+
+prelude
+import Init.Data.List.Lemmas
+public import Init.BinderPredicates
+public import Init.NotationExtra
+import Init.Data.Nat.Lemmas
+
+public section
+
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+
+namespace List
+
+protected theorem prod_eq_zero_iff_exists_zero_nat {l : List Nat} : l.prod = 0 ↔ ∃ x ∈ l, x = 0 := by
+  induction l with
+  | nil => simp
+  | cons x xs ih =>
+    simp [Nat.mul_eq_zero, ih, eq_comm (a := (0 : Nat))]
+
+protected theorem prod_pos_iff_forall_pos_nat {l : List Nat} : 0 < l.prod ↔ ∀ x ∈ l, 0 < x := by
+  induction l with
+  | nil => simp
+  | cons x xs ih =>
+    simp only [prod_cons, mem_cons, forall_eq_or_imp, ← ih]
+    constructor
+    · intro h
+      exact ⟨Nat.pos_of_mul_pos_right h, Nat.pos_of_mul_pos_left h⟩
+    · exact fun ⟨hx, hxs⟩ => Nat.mul_pos hx hxs
+
+@[simp]
+theorem prod_replicate_nat {n : Nat} {a : Nat} : (replicate n a).prod = a ^ n := by
+  induction n <;> simp_all [replicate_succ, Nat.pow_succ, Nat.mul_comm]
+
+theorem prod_append_nat {l₁ l₂ : List Nat} : (l₁ ++ l₂).prod = l₁.prod * l₂.prod := by
+  simp [prod_append]
+
+theorem prod_reverse_nat (xs : List Nat) : xs.reverse.prod = xs.prod := by
+  simp [prod_reverse]
+
+theorem prod_eq_foldl_nat {xs : List Nat} : xs.prod = xs.foldl (init := 1) (· * ·) := by
+  simp only [foldl_eq_foldr_reverse, Nat.mul_comm, ← prod_eq_foldr, prod_reverse_nat]
+
+end List

src/Init/Data/List/Perm.lean

@@ -606,6 +606,13 @@ theorem sum_nat {l₁ l₂ : List Nat} (h : l₁ ~ l₂) : l₁.sum = l₂.sum :
   | swap => simpa [List.sum_cons] using Nat.add_left_comm ..
   | trans _ _ ih₁ ih₂ => simp [ih₁, ih₂]
 
+theorem prod_nat {l₁ l₂ : List Nat} (h : l₁ ~ l₂) : l₁.prod = l₂.prod := by
+  induction h with
+  | nil => simp
+  | cons _ _ ih => simp [ih]
+  | swap => simpa [List.prod_cons] using Nat.mul_left_comm ..
+  | trans _ _ ih₁ ih₂ => simp [ih₁, ih₂]
+
 theorem all_eq {l₁ l₂ : List α} {f : α → Bool} (hp : l₁.Perm l₂) : l₁.all f = l₂.all f := by
   rw [Bool.eq_iff_iff]; simp [hp.mem_iff]
 
@@ -615,6 +622,9 @@ theorem any_eq {l₁ l₂ : List α} {f : α → Bool} (hp : l₁.Perm l₂) : l
 grind_pattern Perm.sum_nat => l₁ ~ l₂, l₁.sum
 grind_pattern Perm.sum_nat => l₁ ~ l₂, l₂.sum
 
+grind_pattern Perm.prod_nat => l₁ ~ l₂, l₁.prod
+grind_pattern Perm.prod_nat => l₁ ~ l₂, l₂.prod
+
 end Perm
 
 end List

src/Init/Data/List/ToArray.lean

@@ -213,6 +213,9 @@ theorem forM_toArray [Monad m] (l : List α) (f : α → m PUnit) :
 @[simp, grind =] theorem sum_toArray [Add α] [Zero α] (l : List α) : l.toArray.sum = l.sum := by
   simp [Array.sum, List.sum]
 
+@[simp, grind =] theorem prod_toArray [Mul α] [One α] (l : List α) : l.toArray.prod = l.prod := by
+  simp [Array.prod, List.prod]
+
 @[simp, grind =] theorem append_toArray (l₁ l₂ : List α) :
     l₁.toArray ++ l₂.toArray = (l₁ ++ l₂).toArray := by
   apply ext'

src/Init/Data/Nat/Gcd.lean

@@ -60,7 +60,7 @@ theorem gcd_def (x y : Nat) : gcd x y = if x = 0 then y else gcd (y % x) x := by
   cases n with
   | zero => simp
   | succ n =>
-    -- `simp [gcd_succ]` produces an invalid term unless `gcd_succ` is proved with `id rfl` instead
+    -- `simp [gcd_succ]` produces an invalid term unless `gcd_succ` is proved with `(rfl)` instead
     rw [gcd_succ]
     exact gcd_zero_left _
 instance : Std.LawfulIdentity gcd 0 where

src/Init/Data/Range/Polymorphic/NatLemmas.lean

@@ -1718,7 +1718,7 @@ theorem toArray_roc_append_toArray_roc {l m n : Nat} (h : l ≤ m) (h' : m ≤ n
 @[simp]
 theorem getElem_toArray_roc {m n i : Nat} (_h : i < (m<...=n).toArray.size) :
     (m<...=n).toArray[i]'_h = m + 1 + i := by
-simp [toArray_roc_eq_toArray_rco]
+  simp [toArray_roc_eq_toArray_rco]
 
 theorem getElem?_toArray_roc {m n i : Nat} :
     (m<...=n).toArray[i]? = if i < n - m then some (m + 1 + i) else none := by

src/Init/Data/Vector/Basic.lean

@@ -506,6 +506,16 @@ Examples:
 @[inline, expose] def sum [Add α] [Zero α] (xs : Vector α n) : α :=
   xs.toArray.sum
 
+/--
+Computes the product of the elements of a vector.
+
+Examples:
+ * `#v[a, b, c].prod = a * (b * (c * 1))`
+ * `#v[1, 2, 5].prod = 10`
+-/
+@[inline, expose] def prod [Mul α] [One α] (xs : Vector α n) : α :=
+  xs.toArray.prod
+
 /--
 Pad a vector on the left with a given element.
 

src/Init/Data/Vector/Int.lean

@@ -30,4 +30,16 @@ theorem sum_reverse_int (xs : Vector Int n) : xs.reverse.sum = xs.sum := by
 theorem sum_eq_foldl_int {xs : Vector Int n} : xs.sum = xs.foldl (b := 0) (· + ·) := by
   simp only [foldl_eq_foldr_reverse, Int.add_comm, ← sum_eq_foldr, sum_reverse_int]
 
+@[simp] theorem prod_replicate_int {n : Nat} {a : Int} : (replicate n a).prod = a ^ n := by
+  simp [← prod_toArray, Array.prod_replicate_int]
+
+theorem prod_append_int {as₁ as₂ : Vector Int n} : (as₁ ++ as₂).prod = as₁.prod * as₂.prod := by
+  simp [← prod_toArray]
+
+theorem prod_reverse_int (xs : Vector Int n) : xs.reverse.prod = xs.prod := by
+  simp [prod_reverse]
+
+theorem prod_eq_foldl_int {xs : Vector Int n} : xs.prod = xs.foldl (b := 1) (· * ·) := by
+  simp only [foldl_eq_foldr_reverse, Int.mul_comm, ← prod_eq_foldr, prod_reverse_int]
+
 end Vector

src/Init/Data/Vector/Lemmas.lean

@@ -278,6 +278,12 @@ theorem toArray_mk {xs : Array α} (h : xs.size = n) : (Vector.mk xs h).toArray
 @[simp, grind =] theorem sum_toArray [Add α] [Zero α] {xs : Vector α n} :
     xs.toArray.sum = xs.sum := rfl
 
+@[simp] theorem prod_mk [Mul α] [One α] {xs : Array α} (h : xs.size = n) :
+    (Vector.mk xs h).prod = xs.prod := rfl
+
+@[simp, grind =] theorem prod_toArray [Mul α] [One α] {xs : Vector α n} :
+    xs.toArray.prod = xs.prod := rfl
+
 @[simp] theorem eq_mk : xs = Vector.mk as h ↔ xs.toArray = as := by
   cases xs
   simp
@@ -551,6 +557,10 @@ theorem toArray_toList {xs : Vector α n} : xs.toList.toArray = xs.toArray := rf
     xs.toList.sum = xs.sum := by
   rw [← toList_toArray, Array.sum_toList, sum_toArray]
 
+@[simp, grind =] theorem prod_toList [Mul α] [One α] {xs : Vector α n} :
+    xs.toList.prod = xs.prod := by
+  rw [← toList_toArray, Array.prod_toList, prod_toArray]
+
 @[simp] theorem getElem_toList {xs : Vector α n} {i : Nat} (h : i < xs.toList.length) :
     xs.toList[i] = xs[i]'(by simpa using h) := by
   cases xs
@@ -3134,3 +3144,39 @@ theorem sum_eq_foldl [Zero α] [Add α]
     {xs : Vector α n} :
     xs.sum = xs.foldl (b := 0) (· + ·) := by
   simp [← sum_toList, List.sum_eq_foldl]
+
+/-! ### prod -/
+
+@[simp, grind =] theorem prod_empty [Mul α] [One α] : (#v[] : Vector α 0).prod = 1 := rfl
+theorem prod_eq_foldr [Mul α] [One α] {xs : Vector α n} :
+    xs.prod = xs.foldr (b := 1) (· * ·) :=
+  rfl
+
+@[simp, grind =]
+theorem prod_append [One α] [Mul α] [Std.Associative (α := α) (· * ·)]
+    [Std.LeftIdentity (α := α) (· * ·) 1] [Std.LawfulLeftIdentity (α := α) (· * ·) 1]
+    {as₁ as₂ : Vector α n} : (as₁ ++ as₂).prod = as₁.prod * as₂.prod := by
+  simp [← prod_toList, List.prod_append]
+
+@[simp, grind =]
+theorem prod_singleton [Mul α] [One α] [Std.LawfulRightIdentity (· * ·) (1 : α)] {x : α} :
+    #v[x].prod = x := by
+  simp [← prod_toList, Std.LawfulRightIdentity.right_id x]
+
+@[simp, grind =]
+theorem prod_push [Mul α] [One α] [Std.Associative (α := α) (· * ·)]
+    [Std.LawfulIdentity (· * ·) (1 : α)] {xs : Vector α n} {x : α} :
+    (xs.push x).prod = xs.prod * x := by
+  simp [← prod_toArray]
+
+@[simp, grind =]
+theorem prod_reverse [One α] [Mul α] [Std.Associative (α := α) (· * ·)]
+    [Std.Commutative (α := α) (· * ·)]
+    [Std.LawfulLeftIdentity (α := α) (· * ·) 1] (xs : Vector α n) : xs.reverse.prod = xs.prod := by
+  simp [← prod_toList, List.prod_reverse]
+
+theorem prod_eq_foldl [One α] [Mul α]
+    [Std.Associative (α := α) (· * ·)] [Std.LawfulIdentity (· * ·) (1 : α)]
+    {xs : Vector α n} :
+    xs.prod = xs.foldl (b := 1) (· * ·) := by
+  simp [← prod_toList, List.prod_eq_foldl]

src/Init/Data/Vector/Nat.lean

@@ -37,4 +37,23 @@ theorem sum_reverse_nat (xs : Vector Nat n) : xs.reverse.sum = xs.sum := by
 theorem sum_eq_foldl_nat {xs : Vector Nat n} : xs.sum = xs.foldl (b := 0) (· + ·) := by
   simp only [foldl_eq_foldr_reverse, Nat.add_comm, ← sum_eq_foldr, sum_reverse_nat]
 
+protected theorem prod_pos_iff_forall_pos_nat {xs : Vector Nat n} : 0 < xs.prod ↔ ∀ x ∈ xs, 0 < x := by
+  simp [← prod_toArray, Array.prod_pos_iff_forall_pos_nat]
+
+protected theorem prod_eq_zero_iff_exists_zero_nat {xs : Vector Nat n} :
+    xs.prod = 0 ↔ ∃ x ∈ xs, x = 0 := by
+  simp [← prod_toArray, Array.prod_eq_zero_iff_exists_zero_nat]
+
+@[simp] theorem prod_replicate_nat {n : Nat} {a : Nat} : (replicate n a).prod = a ^ n := by
+  simp [← prod_toArray, Array.prod_replicate_nat]
+
+theorem prod_append_nat {as₁ as₂ : Vector Nat n} : (as₁ ++ as₂).prod = as₁.prod * as₂.prod := by
+  simp [← prod_toArray]
+
+theorem prod_reverse_nat (xs : Vector Nat n) : xs.reverse.prod = xs.prod := by
+  simp [prod_reverse]
+
+theorem prod_eq_foldl_nat {xs : Vector Nat n} : xs.prod = xs.foldl (b := 1) (· * ·) := by
+  simp only [foldl_eq_foldr_reverse, Nat.mul_comm, ← prod_eq_foldr, prod_reverse_nat]
+
 end Vector

src/Init/Grind/Ring/Basic.lean

@@ -564,6 +564,28 @@ end Ring
 
 end IsCharP
 
+/--
+`PowIdentity α p` states that `x ^ p = x` holds for all elements of `α`.
+
+The primary source of instances is Fermat's little theorem: for a finite field with `q` elements,
+`x ^ q = x` for every `x`. For `Fin p` or `ZMod p` with prime `p`, this gives `x ^ p = x`.
+
+The `grind` ring solver uses this typeclass to add the relation `x ^ p - x = 0` to the
+Groebner basis, which allows it to reduce high-degree polynomials. Mathlib can provide
+instances for general finite fields via `FiniteField.pow_card`.
+-/
+class PowIdentity (α : Type u) [CommSemiring α] (p : outParam Nat) : Prop where
+  /-- Every element satisfies `x ^ p = x`. -/
+  pow_eq (x : α) : x ^ p = x
+
+namespace PowIdentity
+
+variable [CommSemiring α] [PowIdentity α p]
+
+theorem pow (x : α) : x ^ p = x := pow_eq x
+
+end PowIdentity
+
 open AddCommGroup
 
 theorem no_int_zero_divisors {α : Type u} [IntModule α] [NoNatZeroDivisors α] {k : Int} {a : α}

src/Init/Grind/Ring/Envelope.lean

@@ -193,7 +193,7 @@ theorem mul_assoc (a b c : Q α) : mul (mul a b) c = mul a (mul b c) := by
   simp [Semiring.left_distrib, Semiring.right_distrib]; refine ⟨0, ?_⟩; ac_rfl
 
 theorem mul_one (a : Q α) : mul a (natCast 1) = a := by
-obtain ⟨⟨_, _⟩⟩ := a; simp
+  obtain ⟨⟨_, _⟩⟩ := a; simp
 
 theorem one_mul (a : Q α) : mul (natCast 1) a = a := by
   obtain ⟨⟨_, _⟩⟩ := a; simp

src/Init/GrindInstances/Ring/Fin.lean

@@ -156,6 +156,12 @@ instance [i : NeZero n] : ToInt.Pow (Fin n) (.co 0 n) where
       rw [pow_succ, ToInt.Mul.toInt_mul, ih, ← ToInt.wrap_toInt,
         ← IntInterval.wrap_mul (by simp), Int.pow_succ, ToInt.wrap_toInt]
 
+instance : PowIdentity (Fin 2) 2 where
+  pow_eq x := by
+    match x with
+    | ⟨0, _⟩ => rfl
+    | ⟨1, _⟩ => rfl
+
 end Fin
 
 end Lean.Grind

src/Lean/AddDecl.lean

@@ -9,6 +9,7 @@ prelude
 public import Lean.Meta.Sorry
 public import Lean.Util.CollectAxioms
 public import Lean.OriginalConstKind
+import Lean.Compiler.MetaAttr
 import all Lean.OriginalConstKind  -- for accessing `privateConstKindsExt`
 
 public section
@@ -208,8 +209,12 @@ where
       catch _ => pure ()
 
 
-def addAndCompile (decl : Declaration) (logCompileErrors : Bool := true) : CoreM Unit := do
+def addAndCompile (decl : Declaration) (logCompileErrors : Bool := true)
+    (markMeta : Bool := false) : CoreM Unit := do
   addDecl decl
+  if markMeta then
+    for n in decl.getNames do
+      modifyEnv (Lean.markMeta · n)
   compileDecl decl (logErrors := logCompileErrors)
 
 end Lean

src/Lean/Elab/BuiltinDo/For.lean

@@ -111,8 +111,14 @@ open Lean.Meta
     for x in loopMutVars do
       let defn ← getLocalDeclFromUserName x.getId
       Term.addTermInfo' x defn.toExpr
-      -- ForIn forces all mut vars into the same universe: that of the do block result type.
-      discard <| Term.ensureHasType (mkSort (mi.u.succ)) defn.type
+      -- ForIn forces the mut tuple into the universe mi.u: that of the do block result type.
+      -- If we don't do this, then we are stuck on solving constraints such as
+      --   `max ?u.46 ?u.47 =?= max (max ?u.22 ?u.46) ?u.47`
+      -- It's important we do this as a separate isLevelDefEq check on the decremented level because
+      -- otherwise (`ensureHasType (mkSort mi.u.succ)`) we are stuck on constraints like
+      --   `max (?u+1) (?v+1) =?= ?u+1`
+      let u ← getDecLevel defn.type
+      discard <| isLevelDefEq u mi.u
       defs := defs.push defn.toExpr
     if info.returnsEarly && loopMutVars.isEmpty then
       defs := defs.push (mkConst ``Unit.unit)

src/Lean/Elab/Deriving/Basic.lean

@@ -233,27 +233,41 @@ def processDefDeriving (view : DerivingClassView) (decl : Expr) (isNoncomputable
         finally
           Core.setMessageLog (msgLog ++ (← Core.getMessageLog))
   let env ← getEnv
-  let hints := ReducibilityHints.regular (getMaxHeight env result.value + 1)
-  let decl ← mkDefinitionValInferringUnsafe instName result.levelParams.toList result.type result.value hints
-  -- Pre-check: if the instance value depends on noncomputable definitions and the user didn't write
-  -- `noncomputable`, give an actionable error with a `Try this:` suggestion.
-  unless isNoncomputable || (← read).isNoncomputableSection || (← isProp result.type) do
-    let noncompRef? := preNormValue.foldConsts none fun n acc =>
-      acc <|> if Lean.isNoncomputable (asyncMode := .local) env n then some n else none
-    if let some noncompRef := noncompRef? then
-      if let some cmdRef := cmdRef? then
-        if let some origText := cmdRef.reprint then
-          let newText := (origText.replace "deriving instance " "deriving noncomputable instance ").trimAscii
-          logInfoAt cmdRef m!"Try this: {newText}"
-      throwError "failed to derive instance because it depends on \
-        `{.ofConstName noncompRef}`, which is noncomputable"
-  if isNoncomputable || (← read).isNoncomputableSection then
-    addDecl <| Declaration.defnDecl decl
-    modifyEnv (addNoncomputable · instName)
+  let isPropType ← isProp result.type
+  if isPropType then
+    let decl ← mkThmOrUnsafeDef {
+      name := instName, levelParams := result.levelParams.toList,
+      type := result.type, value := result.value
+    }
+    addDecl decl
   else
-    addAndCompile <| Declaration.defnDecl decl
+    let hints := ReducibilityHints.regular (getMaxHeight env result.value + 1)
+    let decl ← mkDefinitionValInferringUnsafe instName result.levelParams.toList result.type result.value hints
+    -- Pre-check: if the instance value depends on noncomputable definitions and the user didn't write
+    -- `noncomputable`, give an actionable error with a `Try this:` suggestion.
+    unless isNoncomputable || (← read).isNoncomputableSection do
+      let noncompRef? := preNormValue.foldConsts none fun n acc =>
+        acc <|> if Lean.isNoncomputable (asyncMode := .local) env n then some n else none
+      if let some noncompRef := noncompRef? then
+        if let some cmdRef := cmdRef? then
+          if let some origText := cmdRef.reprint then
+            let newText := (origText.replace "deriving instance " "deriving noncomputable instance ").trimAscii
+            logInfoAt cmdRef m!"Try this: {newText}"
+        throwError "failed to derive instance because it depends on \
+          `{.ofConstName noncompRef}`, which is noncomputable"
+    if isNoncomputable || (← read).isNoncomputableSection then
+      addDecl <| Declaration.defnDecl decl
+      modifyEnv (addNoncomputable · instName)
+    else
+      addAndCompile <| Declaration.defnDecl decl
   trace[Elab.Deriving] "Derived instance `{.ofConstName instName}`"
-  registerInstance instName AttributeKind.global (eval_prio default)
+  -- For Prop-typed instances (theorems), skip `implicit_reducible` since reducibility hints are
+  -- irrelevant for theorems. This matches the behavior of the handwritten `instance` command
+  -- (see `MutualDef.lean`).
+  if isPropType then
+    addInstance instName AttributeKind.global (eval_prio default)
+  else
+    registerInstance instName AttributeKind.global (eval_prio default)
   addDeclarationRangesFromSyntax instName (← getRef)
 
 end Term

src/Lean/Elab/Import.lean

@@ -28,7 +28,9 @@ def HeaderSyntax.isModule (header : HeaderSyntax) : Bool :=
 def HeaderSyntax.imports (stx : HeaderSyntax) (includeInit : Bool := true) : Array Import :=
   match stx with
   | `(Parser.Module.header| $[module%$moduleTk]? $[prelude%$preludeTk]? $importsStx*) =>
-    let imports := if preludeTk.isNone && includeInit then #[{ module := `Init : Import }] else #[]
+    let imports := if preludeTk.isNone && includeInit then
+        #[{ module := `Init : Import }, { module := `Init, isMeta := true : Import }]
+      else #[]
     imports ++ importsStx.map fun
       | `(Parser.Module.import| $[public%$publicTk]? $[meta%$metaTk]? import $[all%$allTk]? $n) =>
         { module := n.getId, importAll := allTk.isSome

src/Lean/Elab/ParseImportsFast.lean

@@ -233,7 +233,7 @@ def setImportAll : Parser := fun _ s =>
 
 def main : Parser :=
   keywordCore "module" (setIsModule false) (setIsModule true) >>
-  keywordCore "prelude" (fun _ s => s.pushImport `Init) skip >>
+  keywordCore "prelude" (fun _ s => (s.pushImport `Init).pushImport { module := `Init, isMeta := true }) skip >>
   manyImports (atomic (keywordCore "public" skip setExported >>
     keywordCore "meta" skip setMeta >>
     keyword "import") >>

src/Lean/Linter.lean

@@ -18,3 +18,4 @@ public import Lean.Linter.List
 public import Lean.Linter.Sets
 public import Lean.Linter.UnusedSimpArgs
 public import Lean.Linter.Coe
+public import Lean.Linter.GlobalAttributeIn

src/Lean/Linter/GlobalAttributeIn.lean

@@ -0,0 +1,59 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Wojciech Różowski
+-/
+module
+
+prelude
+public import Lean.Elab.Command
+public import Lean.Linter.Basic
+
+
+namespace Lean.Linter
+open Elab.Command
+
+private structure TopDownSkipQuot where
+  stx : Syntax
+
+def topDownSkipQuot (stx : Syntax) : TopDownSkipQuot := ⟨stx⟩
+
+partial instance [Monad m] : ForIn m TopDownSkipQuot Syntax where
+  forIn := fun ⟨stx⟩ init f => do
+    let rec @[specialize] loop stx b [Inhabited (type_of% b)] := do
+      if stx.isQuot then return ForInStep.yield b
+      match (← f stx b) with
+      | ForInStep.yield b' =>
+        let mut b := b'
+        if let Syntax.node _ _ args := stx then
+          for arg in args do
+            match (← loop arg b) with
+            | ForInStep.yield b' => b := b'
+            | ForInStep.done b'  => return ForInStep.done b'
+        return ForInStep.yield b
+      | ForInStep.done b => return ForInStep.done b
+    match (← @loop stx init ⟨init⟩) with
+    | ForInStep.yield b => return b
+    | ForInStep.done b  => return b
+
+def getGlobalAttributesIn? : Syntax → Option (Ident × Array (TSyntax `attr))
+  | `(attribute [$x,*] $id in $_) =>
+    let xs := x.getElems.filterMap fun a => match a.raw with
+      | `(Parser.Command.eraseAttr| -$_) => none
+      | `(Parser.Term.attrInstance| local $_attr:attr) => none
+      | `(Parser.Term.attrInstance| scoped $_attr:attr) => none
+      | `(attr| $a) => some a
+    (id, xs)
+  | _ => default
+
+def globalAttributeIn : Linter where run := withSetOptionIn fun stx => do
+  for s in topDownSkipQuot stx do
+    if let some (id, nonScopedNorLocal) := getGlobalAttributesIn? s then
+      for attr in nonScopedNorLocal do
+        logErrorAt attr
+          m!"Despite the `in`, the attribute {attr} is added globally to {id}\n\
+          please remove the `in` or make this a `local {attr}`"
+
+builtin_initialize addLinter globalAttributeIn
+
+end Lean.Linter

src/Lean/Meta/SizeOf.lean

@@ -149,17 +149,15 @@ partial def mkSizeOfFn (recName : Name) (declName : Name): MetaM Unit := do
           trace[Meta.sizeOf] "declName: {declName}"
           trace[Meta.sizeOf] "type: {sizeOfType}"
           trace[Meta.sizeOf] "val: {sizeOfValue}"
-          -- We expose the `sizeOf` functions so that the `spec` theorems can be publicly `defeq`
-          withExporting do
-            addDecl <| Declaration.defnDecl {
-              name        := declName
-              levelParams := levelParams
-              type        := sizeOfType
-              value       := sizeOfValue
-              safety      := DefinitionSafety.safe
-              hints       := ReducibilityHints.abbrev
-            }
-            enableRealizationsForConst declName
+          addDecl <| Declaration.defnDecl {
+            name        := declName
+            levelParams := levelParams
+            type        := sizeOfType
+            value       := sizeOfValue
+            safety      := DefinitionSafety.safe
+            hints       := ReducibilityHints.abbrev
+          }
+          enableRealizationsForConst declName
 
 /--
   Create `sizeOf` functions for all inductive datatypes in the mutual inductive declaration containing `typeName`
@@ -469,7 +467,6 @@ private def mkSizeOfSpecTheorem (indInfo : InductiveVal) (sizeOfFns : Array Name
         type        := thmType
         value       := thmValue
       }
-      inferDefEqAttr thmName
       simpAttr.add thmName default .global
       grindAttr.add thmName grindAttrStx .global
 

src/Lean/Meta/Tactic/Grind/Arith/CommRing/Internalize.lean

@@ -112,6 +112,25 @@ private def processInv (e inst a : Expr) : RingM Unit := do
       return ()
   pushNewFact <| mkApp3 (mkConst ``Grind.CommRing.inv_split [ring.u]) ring.type fieldInst a
 
+/--
+For each new variable `x` in a ring with `PowIdentity α p`,
+push the equation `x ^ p = x` as a new fact into grind.
+-/
+private def processPowIdentityVars : RingM Unit := do
+  let ring ← getCommRing
+  let some (powIdentityInst, csInst, p) := ring.powIdentityInst? | return ()
+  let startIdx := ring.powIdentityVarCount
+  let vars := ring.toRing.vars
+  if startIdx >= vars.size then return ()
+  for i in [startIdx:vars.size] do
+    let x := vars[i]!
+    trace_goal[grind.ring] "PowIdentity: pushing x^{p} = x for {x}"
+    -- Construct proof: @PowIdentity.pow_eq α csInst p powIdentityInst x
+    let proof := mkApp5 (mkConst ``Grind.PowIdentity.pow_eq [ring.u])
+      ring.type csInst (mkNatLit p) powIdentityInst x
+    pushNewFact proof
+  modifyCommRing fun s => { s with powIdentityVarCount := vars.size }
+
 /-- Returns `true` if `e` is a term `a⁻¹`. -/
 private def internalizeInv (e : Expr) : GoalM Bool := do
   match_expr e with
@@ -138,6 +157,7 @@ def internalize (e : Expr) (parent? : Option Expr) : GoalM Unit := do
       denote := s.denote.insert { expr := e } re
       denoteEntries := s.denoteEntries.push (e, re)
     }
+    processPowIdentityVars
   else if let some semiringId ← getCommSemiringId? type then SemiringM.run semiringId do
     let some re ← sreify? e | return ()
     trace_goal[grind.ring.internalize] "semiring [{semiringId}]: {e}"

src/Lean/Meta/Tactic/Grind/Arith/CommRing/RingId.lean

@@ -38,11 +38,13 @@ where
     let noZeroDivInst? ← getNoZeroDivInst? u type
     trace_goal[grind.ring] "NoNatZeroDivisors available: {noZeroDivInst?.isSome}"
     let fieldInst? ← synthInstance? <| mkApp (mkConst ``Grind.Field [u]) type
+    let powIdentityInst? ← getPowIdentityInst? u type
+    trace_goal[grind.ring] "PowIdentity available: {powIdentityInst?.isSome}"
     let semiringId? := none
     let id := (← get').rings.size
     let ring : CommRing := {
       id, semiringId?, type, u, semiringInst, ringInst, commSemiringInst,
-      commRingInst, charInst?, noZeroDivInst?, fieldInst?,
+      commRingInst, charInst?, noZeroDivInst?, fieldInst?, powIdentityInst?,
     }
     modify' fun s => { s with rings := s.rings.push ring }
     return some id

src/Lean/Meta/Tactic/Grind/Arith/CommRing/Types.lean

@@ -214,6 +214,8 @@ structure CommRing extends Ring where
   noZeroDivInst? : Option Expr
   /-- `Field` instance for `type` if available. -/
   fieldInst?     : Option Expr
+  /-- `PowIdentity` instance, the synthesized `CommSemiring` instance, and exponent `p` if available. -/
+  powIdentityInst? : Option (Expr × Expr × Nat) := none
   /-- `denoteEntries` is `denote` as a `PArray` for deterministic traversal. -/
   denoteEntries  : PArray (Expr × RingExpr) := {}
   /-- Next unique id for `EqCnstr`s. -/
@@ -238,6 +240,8 @@ structure CommRing extends Ring where
   recheck        : Bool := false
   /-- Inverse theorems that have been already asserted. -/
   invSet         : PHashSet Expr := {}
+  /-- Number of variables for which `PowIdentity` equations have been pushed. -/
+  powIdentityVarCount : Nat := 0
   /--
   An equality of the form `c = 0`. It is used to simplify polynomial coefficients.
   -/

src/Lean/Meta/Tactic/Grind/Arith/Insts.lean

@@ -19,6 +19,20 @@ def getIsCharInst? (u : Level) (type : Expr) (semiringInst : Expr) : GoalM (Opti
   let some n ← evalNat? n | return none
   return some (charInst, n)
 
+def getPowIdentityInst? (u : Level) (type : Expr) : GoalM (Option (Expr × Expr × Nat)) := do withNewMCtxDepth do
+  -- We use a fresh metavar for `CommSemiring` (unlike `getIsCharInst?` which pins the semiring)
+  -- because `PowIdentity` instances may be declared against a canonical `CommSemiring` instance
+  -- that is not definitionally equal to `CommRing.toCommSemiring`. The synthesized `csInst` is
+  -- stored and used in proof terms to ensure type-correctness.
+  let csInst ← mkFreshExprMVar (mkApp (mkConst ``Grind.CommSemiring [u]) type)
+  let p ← mkFreshExprMVar (mkConst ``Nat)
+  let powIdentityType := mkApp3 (mkConst ``Grind.PowIdentity [u]) type csInst p
+  let some inst ← synthInstance? powIdentityType | return none
+  let csInst ← instantiateMVars csInst
+  let p ← instantiateMVars p
+  let some pVal ← evalNat? p | return none
+  return some (inst, csInst, pVal)
+
 def getNoZeroDivInst? (u : Level) (type : Expr) : GoalM (Option Expr) := do
   let natModuleType := mkApp (mkConst ``Grind.NatModule [u]) type
   let some natModuleInst ← synthInstance? natModuleType | return none

src/Lean/Meta/Tactic/Simp/SimpTheorems.lean

@@ -242,7 +242,6 @@ def ppSimpTheorem [Monad m] [MonadEnv m] [MonadError m] (s : SimpTheorem) : m Me
 instance : BEq SimpTheorem where
   beq e₁ e₂ := e₁.proof == e₂.proof
 
-
 /--
 Configuration for `MetaM` used to process global simp theorems
 -/
@@ -256,8 +255,6 @@ def simpGlobalConfig : ConfigWithKey :=
 @[inline] def withSimpGlobalConfig : MetaM α → MetaM α :=
   withConfigWithKey simpGlobalConfig
 
-
-
 private partial def isPerm : Expr → Expr → MetaM Bool
   | .app f₁ a₁, .app f₂ a₂ => isPerm f₁ f₂ <&&> isPerm a₁ a₂
   | .mdata _ s, t => isPerm s t
@@ -370,11 +367,32 @@ private def mkSimpTheoremKeys (type : Expr) (noIndexAtArgs : Bool) : MetaM (Arra
     | some (_, lhs, rhs) => pure (← DiscrTree.mkPath lhs noIndexAtArgs, ← isPerm lhs rhs)
     | none => throwError "Unexpected kind of simp theorem{indentExpr type}"
 
-private def mkSimpTheoremCore (origin : Origin) (e : Expr) (levelParams : Array Name) (proof : Expr) (post : Bool) (prio : Nat) (noIndexAtArgs : Bool) : MetaM SimpTheorem := do
+register_builtin_option simp.rfl.checkTransparency: Bool := {
+  defValue := false
+  descr    := "if true, Lean generates a warning if the left and right-hand sides of the `[simp]` equation are not definitionally equal at the restricted transparency level used by `simp` "
+}
+
+private def mkSimpTheoremCore (origin : Origin) (e : Expr) (levelParams : Array Name) (proof : Expr)
+    (post : Bool) (prio : Nat) (noIndexAtArgs : Bool) : MetaM SimpTheorem := do
   assert! origin != .fvar ⟨.anonymous⟩
   let type ← instantiateMVars (← inferType e)
   let (keys, perm) ← mkSimpTheoremKeys type noIndexAtArgs
-  return { origin, keys, perm, post, levelParams, proof, priority := prio, rfl := (← isRflProof proof) }
+  let rfl ← isRflProof proof
+  if rfl && simp.rfl.checkTransparency.get (← getOptions) then
+    forallTelescopeReducing type fun _ type => do
+      let checkDefEq (lhs rhs : Expr) := do
+        unless (← withTransparency .instances <| isDefEq lhs rhs) do
+          logWarning m!"`{origin.key}` is a `[defeq]` simp theorem, but its left-hand side{indentExpr lhs}\n\
+            is not definitionally equal to the right-hand side{indentExpr rhs}\n\
+            at `.instances` transparency. Possible solutions:\n\
+            1- use `(rfl)` as the proof\n\
+            2- mark constants occurring in the lhs and rhs as `[implicit_reducible]`"
+      match_expr type with
+      | Eq _ lhs rhs => checkDefEq lhs rhs
+      | Iff lhs rhs => checkDefEq lhs rhs
+      | _ =>
+        logWarning m!"'{origin.key}' is a 'rfl' simp theorem, unexpected resulting type{indentExpr type}"
+  return { origin, keys, perm, post, levelParams, proof, priority := prio, rfl }
 
 /--
 Creates a `SimpTheorem` from a global theorem.

src/Lean/Meta/WrapInstance.lean

@@ -112,8 +112,7 @@ partial def wrapInstance (inst expectedType : Expr) (compile : Bool := true)
       return inst
 
   -- Try to reduce it to a constructor.
-  let inst ← whnf inst
-  inst.withApp fun f args => do
+  (← whnf inst).withApp fun f args => do
     let some (.ctorInfo ci) ← f.constName?.mapM getConstInfo
       | do
         trace[Meta.wrapInstance] "did not reduce to constructor application, returning/wrapping as is: {inst}"

src/Lean/Parser/Module.lean

@@ -127,7 +127,10 @@ private def consumeInput (inputCtx : InputContext) (pmctx : ParserModuleContext)
   | none   => s.pos
 
 def topLevelCommandParserFn : ParserFn :=
-  commandParser.fn
+  -- set position to enforce appropriate indentation of applications etc.
+  -- We don't do it for nested commands such as in quotations where
+  -- formatting might be less rigid.
+  (withPosition commandParser).fn
 
 partial def parseCommand (inputCtx : InputContext) (pmctx : ParserModuleContext) (mps : ModuleParserState) (messages : MessageLog) : Syntax × ModuleParserState × MessageLog := Id.run do
   let mut pos := mps.pos

src/Lean/Parser/Term/Basic.lean

@@ -84,11 +84,12 @@ Delimiter-free indentation is determined by the *first* tactic of the sequence.
   tacticSeqBracketed <|> tacticSeq1Indented
 
 /-- Same as [`tacticSeq`] but requires delimiter-free tactic sequence to have strict indentation.
-The strict indentation requirement only apply to *nested* `by`s, as top-level `by`s do not have a
-position set. -/
+Falls back to an empty tactic sequence when no appropriately indented content follows, producing
+an elaboration error (unsolved goals) rather than a parse error. -/
 @[builtin_doc, run_builtin_parser_attribute_hooks]
 def tacticSeqIndentGt := withAntiquot (mkAntiquot "tacticSeq" ``tacticSeq) <| node ``tacticSeq <|
-  tacticSeqBracketed <|> (checkColGt "indented tactic sequence" >> tacticSeq1Indented)
+  tacticSeqBracketed <|> (checkColGt "indented tactic sequence" >> tacticSeq1Indented) <|>
+  node ``tacticSeq1Indented pushNone
 
 /- Raw sequence for quotation and grouping -/
 @[run_builtin_parser_attribute_hooks]

src/Lean/ParserCompiler.lean

@@ -110,9 +110,7 @@ partial def compileParserExpr (e : Expr) : MetaM Expr := do
         }
         -- usually `meta` is inferred during compilation for auxiliary definitions, but as
         -- `ctx.combinatorAttr` may enforce correct use of the modifier, infer now.
-        if isMarkedMeta (← getEnv) c then
-          modifyEnv (markMeta · c')
-        addAndCompile decl
+        addAndCompile decl (markMeta := isMarkedMeta (← getEnv) c)
         modifyEnv (ctx.combinatorAttr.setDeclFor · c c')
         if cinfo.type.isConst then
           if let some kind ← parserNodeKind? cinfo.value! then

src/Lean/Server/InfoUtils.lean

@@ -461,8 +461,7 @@ partial def InfoTree.goalsAt? (text : FileMap) (t : InfoTree) (hoverPos : String
           ctxInfo := ctx
           tacticInfo := ti
           useAfter := hoverPos > pos && !cs.any (hasNestedTactic pos tailPos)
-          -- consider every position unindented after an empty `by` to support "hanging" `by` uses
-          indented := (text.toPosition pos).column > (text.toPosition hoverPos).column && !isEmptyBy ti.stx
+          indented := (text.toPosition pos).column > (text.toPosition hoverPos).column
           -- use goals just before cursor as fall-back only
           -- thus for `(by foo)`, placing the cursor after `foo` shows its state as long
           -- as there is no state on `)`
@@ -485,9 +484,6 @@ where
     | InfoTree.node (Info.ofMacroExpansionInfo _) cs =>
       cs.any (hasNestedTactic pos tailPos)
     | _ => false
-  isEmptyBy (stx : Syntax) : Bool :=
-    -- there are multiple `by` kinds with the same structure
-    stx.getNumArgs == 2 && stx[0].isToken "by" && stx[1].getNumArgs == 1 && stx[1][0].isMissing
 
 
 partial def InfoTree.termGoalAt? (t : InfoTree) (hoverPos : String.Pos.Raw) : Option InfoWithCtx :=

src/lake/Lake/CLI/Shake.lean

@@ -463,6 +463,7 @@ def visitModule (pkgs : Array Name) (srcSearchPath : SearchPath)
   if prelude?.isNone then
     let j : Nat := s.env.getModuleIdx? `Init |>.get!
     deps := deps.union .pub {j}
+    deps := deps.union .metaPub {j}
 
   -- Accumulate `transDeps` which is the non-reflexive transitive closure of the still-live imports
   let mut transDeps := Needs.empty

src/lakefile.toml.in

@@ -41,7 +41,6 @@ leanLibDir = "lib/lean"
 nativeLibDir = "lib/lean"
 
 # Additional options derived from the CMake configuration
-# For example, CI will set `-DwarningAsError=true` through this
 moreLeanArgs = [${LEAN_EXTRA_OPTS_TOML}]
 
 # Uncomment to limit number of reported errors further in case of overwhelming cmdline output