Merge branch 'master' into codex/tfae-congr-append

Author: CoolRmal

.github/workflows/build_template.yml

@@ -57,6 +57,7 @@ jobs:
       build-outcome: ${{ steps.build.outcome }}
       archive-outcome: ${{ steps.archive.outcome }}
       counterexamples-outcome: ${{ steps.counterexamples.outcome }}
+      wanted-outcome: ${{ steps.wanted.outcome }}
       cache-staging-has-files: ${{ steps.cache_staging_check.outputs.has_files }}
       mk_all-outcome: ${{ steps.mk_all.outcome }}
       noisy-outcome: ${{ steps.noisy.outcome }}
@@ -230,12 +231,13 @@ jobs:
       # storing and transferring oleans over the network.
       # Hopefully a future re-implementation of `cache` will obviate the present need for this hack.
 
-      - name: fetch archive and counterexamples cache
+      - name: fetch archive, counterexamples and wanted cache
         shell: bash
         run: |
           cd pr-branch
           ../tools-branch/.lake/build/bin/cache get Archive.lean
           ../tools-branch/.lake/build/bin/cache get Counterexamples.lean
+          ../tools-branch/.lake/build/bin/cache get Wanted.lean
 
       - name: build archive
         id: archive
@@ -253,8 +255,16 @@ jobs:
           ../tools-branch/scripts/lake-build-with-retry.sh Counterexamples
           # results of build at pr-branch/.lake/build_summary_Counterexamples.json
 
+      - name: build wanted
+        id: wanted
+        continue-on-error: true
+        run: |
+          cd pr-branch
+          ../tools-branch/scripts/lake-build-with-retry.sh Wanted
+          # results of build at pr-branch/.lake/build_summary_Wanted.json
+
       # Runs in the build job because it only needs the freshly-built Mathlib/
-      # Archive/Counterexamples oleans, which are present here; keeping it in
+      # Archive/Counterexamples/Wanted oleans, which are present here; keeping it in
       # `build` also spares `test_lint` from fetching Archive/Counterexamples.
       - name: check for noisy stdout lines
         id: noisy
@@ -263,7 +273,7 @@ jobs:
           buildMsgs="$(
             ##  we exploit `lake`s replay feature: since the cache is present, running
             ##  `lake build` will reproduce all the outputs without having to recompute
-            lake build -q --iofail Mathlib Archive Counterexamples
+            lake build -q --iofail Mathlib Archive Counterexamples Wanted
           )"
           if [ -n "${buildMsgs}" ]
           then
@@ -300,6 +310,13 @@ jobs:
           cd pr-branch
           lake env ../tools-branch/.lake/build/bin/cache --staging-dir="../cache-staging" stage Counterexamples.lean
 
+      - name: stage Wanted cache files
+        if: ${{ steps.wanted.outcome == 'success' }}
+        shell: landrun --rox /usr --ro /etc/timezone --rw /dev --rox /home/lean/.elan --rox /home/lean/actions-runner/_work --rox /home/lean/.cache/mathlib/ --rw /home/lean/.cache/mathlib/ --rw pr-branch/.lake/ --rw cache-staging/ --env PATH --env HOME --env GITHUB_OUTPUT --env CI -- bash -euxo pipefail {0}
+        run: |
+          cd pr-branch
+          lake env ../tools-branch/.lake/build/bin/cache --staging-dir="../cache-staging" stage Wanted.lean
+
       - name: check cache staging contents
         id: cache_staging_check
         if: ${{ always() && (steps.build.outcome == 'success' || steps.build.outcome == 'failure' || steps.build.outcome == 'cancelled') }}
@@ -463,19 +480,19 @@ jobs:
       # the archive/counterexamples builds all succeeded. The condition reads those
       # from the build job's outputs, and the problem-matcher wrap is gated to match.
       - name: begin gh-problem-match-wrap for test step
-        if: ${{ needs.build.outputs.build-outcome == 'success' && needs.build.outputs.mk_all-outcome == 'success' && needs.build.outputs.archive-outcome == 'success' && needs.build.outputs.counterexamples-outcome == 'success' }}
+        if: ${{ needs.build.outputs.build-outcome == 'success' && needs.build.outputs.mk_all-outcome == 'success' && needs.build.outputs.archive-outcome == 'success' && needs.build.outputs.counterexamples-outcome == 'success' && needs.build.outputs.wanted-outcome == 'success' }}
         uses: leanprover-community/gh-problem-matcher-wrap@65a654fcdf7b64ff7633bc7a558f7b46d59a27bf # 2026-06-25
         with:
           action: add # In order to be able to run a multiline script, we need to add/remove the problem matcher before and after.
           linters: lean
       - name: test mathlib
-        if: ${{ needs.build.outputs.build-outcome == 'success' && needs.build.outputs.mk_all-outcome == 'success' && needs.build.outputs.archive-outcome == 'success' && needs.build.outputs.counterexamples-outcome == 'success' }}
+        if: ${{ needs.build.outputs.build-outcome == 'success' && needs.build.outputs.mk_all-outcome == 'success' && needs.build.outputs.archive-outcome == 'success' && needs.build.outputs.counterexamples-outcome == 'success' && needs.build.outputs.wanted-outcome == 'success' }}
         id: test
         run: |
           cd pr-branch
           ../tools-branch/scripts/lake-build-wrapper.py .lake/build_summary_MathlibTest.json lake --iofail test
       - name: end gh-problem-match-wrap for test step
-        if: ${{ needs.build.outputs.build-outcome == 'success' && needs.build.outputs.mk_all-outcome == 'success' && needs.build.outputs.archive-outcome == 'success' && needs.build.outputs.counterexamples-outcome == 'success' }}
+        if: ${{ needs.build.outputs.build-outcome == 'success' && needs.build.outputs.mk_all-outcome == 'success' && needs.build.outputs.archive-outcome == 'success' && needs.build.outputs.counterexamples-outcome == 'success' && needs.build.outputs.wanted-outcome == 'success' }}
         uses: leanprover-community/gh-problem-matcher-wrap@65a654fcdf7b64ff7633bc7a558f7b46d59a27bf # 2026-06-25
         with:
           action: remove

.github/workflows/lake_cache_shadow.yml

@@ -72,7 +72,7 @@ on:
         # Default: the full `Mathlib` library — the representative master shadow.
         # For a cheaper experiment, pass a smaller set, e.g.
         #   Mathlib.Topology.Basic Mathlib.Combinatorics.SimpleGraph.Basic Mathlib.RingTheory.Ideal.Basic
-        # or add `Archive Counterexamples` to also shadow those libraries.
+        # or add `Archive Counterexamples Wanted` to also shadow those libraries.
         default: Mathlib
       toolchain_override:
         description: >-
@@ -582,12 +582,12 @@ jobs:
           # (no rebuild). Deps building is expected and excluded from the grep.
           # Emit an explicit health line (consumed by the Zulip report) and fail
           # the run if it's not a full hit.
-          BUILT_ROOT=$(grep -cE '^✔.*Built (Mathlib|Archive|Counterexamples)([. ]|$)' "$log" || true)
+          BUILT_ROOT=$(grep -cE '^✔.*Built (Mathlib|Archive|Counterexamples|Wanted)([. ]|$)' "$log" || true)
           if [ "$BUILT_ROOT" -ne 0 ]; then
             health="❌ NOT full cache hits — ${BUILT_ROOT} root-package module(s) rebuilt"
             echo "health=${health}" >> "$GITHUB_OUTPUT"
             echo "::error::${health}"
-            grep -E '^✔.*Built (Mathlib|Archive|Counterexamples)([. ]|$)' "$log" || true
+            grep -E '^✔.*Built (Mathlib|Archive|Counterexamples|Wanted)([. ]|$)' "$log" || true
             exit 1
           fi
           health="✅ full cache hits — 0 root-package modules rebuilt (${FETCHED_ARTIFACTS} served from cache)"

.github/workflows/publish_tools.yml

@@ -77,8 +77,8 @@ jobs:
           #                                     We ship the whole build dir, not just the
           #                                     binary, in case it needs other files there
           #                                     to run.
-          #   - scripts/lake-build-with-retry.sh: builds Mathlib/Archive/Counterexamples
-          #                                     with retries.
+          #   - scripts/lake-build-with-retry.sh: builds Mathlib/Archive/Counterexamples/
+          #                                     Wanted with retries.
           #   - scripts/lake-build-wrapper.py:  wraps the `lake test` step.
           #   - lean-toolchain:                 the toolchain this binary was built with;
           #                                     the consumer installs it (via elan) so the

.github/workflows/remove_deprecated_decls.yml

@@ -129,7 +129,7 @@ jobs:
         printf $'::group::Running lake env\n'
         lake env | tr ':' '\n'
         echo "::endgroup::"
-        for repo in Mathlib Archive Counterexamples; do
+        for repo in Mathlib Archive Counterexamples Wanted; do
           echo "::group::Retrieving the cache for ${repo}"
           lake exe cache get "$repo" || true
           echo "::endgroup::"
@@ -141,12 +141,12 @@ jobs:
         NEW_DATE: "${{ steps.process_dates.outputs.to_date }}"
         DRY_RUN: "${{ toJson(inputs.dry_run) }}"
       run: |
-        # We create a temporary file importing `Mathlib`, `Archive` and `Counterexamples`
-        # and running `#clear_deprecations` with the expected date-range.
+        # We create a temporary file importing `Mathlib`, `Archive`, `Counterexamples` and
+        # `Wanted`, and running `#clear_deprecations` with the expected date-range.
         tmplean="$(mktemp -p Mathlib --suffix=.lean RMDXXX)"
         echo "::group::Creating ${tmplean} file"
         {
-          for repo in Mathlib Archive Counterexamples; do
+          for repo in Mathlib Archive Counterexamples Wanted; do
             printf $'import %s\n' "$repo"
           done
           REALLY=$([ "$DRY_RUN" = "true" ] && echo "" || echo "really")

Archive.lean

@@ -67,6 +67,7 @@ import Archive.MiuLanguage.Basic
 import Archive.MiuLanguage.DecisionNec
 import Archive.MiuLanguage.DecisionSuf
 import Archive.OxfordInvariants.Summer2021.Week3P1
+import Archive.RiemannStieltjes
 import Archive.Sensitivity
 import Archive.Wiedijk100Theorems.AbelRuffini
 import Archive.Wiedijk100Theorems.AreaOfACircle

Archive/Arithcc.lean

@@ -262,14 +262,10 @@ theorem write_eq_implies_stateEq {t : Register} {v : Word} {ζ₁ ζ₂ : State}
   intro r hr
   obtain ⟨_, h⟩ := h
   specialize h r (lt_trans hr (Register.lt_succ_self _))
-  rwa [if_neg (ne_of_lt hr)] at h
+  rwa [ite_eq_right (ne_of_lt hr)] at h
 
-set_option linter.flexible false in
-set_option linter.style.whitespace false in -- manual alignment is not recognised
 /-- The main **compiler correctness theorem**.
-
-Unlike Theorem 1 in the paper, both `map` and the assumption on `t` are explicit.
--/
+Unlike Theorem 1 in the paper, both `map` and the assumption on `t` are explicit. -/
 theorem compiler_correctness
     (map : Identifier → Register) (e : Expr) (ξ : Identifier → Word) (η : State) (t : Register)
     (hmap : ∀ x, read (loc x map) η = ξ x) (ht : ∀ x, loc x map < t) :
@@ -324,11 +320,11 @@ theorem compiler_correctness
       simp_all
     have hζ₄ : ζ₄ ≃[t + 1] { write t ν₁ η with ac := ν } := calc
       ζ₄ = step (Instruction.add t) ζ₃ := by simp_all
-      _  = { ζ₃ with ac := read t ζ₃ + ζ₃.ac } := by simp [step]
-      _  = { ζ₃ with ac := ν } := by simp_all
-      _  ≃[t + 1] { { write t ν₁ η with ac := ν₂ } with ac := ν } := by
-        simp [StateEq] at hζ₃ ⊢; cases hζ₃; assumption
-      _  ≃[t + 1] { write t ν₁ η with ac := ν } := by simp_all; rfl
+      _ = { ζ₃ with ac := read t ζ₃ + ζ₃.ac } := by simp [step]
+      _ = { ζ₃ with ac := ν } := by simp_all
+      _ ≃[t + 1] { { write t ν₁ η with ac := ν₂ } with ac := ν } := by
+        simp only [StateEq, true_and]; exact hζ₃.2
+      _ ≃[t + 1] { write t ν₁ η with ac := ν } := by simp_all; rfl
     apply write_eq_implies_stateEq <;> assumption
 
 end Correctness

Archive/Examples/Eisenstein.lean

@@ -25,7 +25,6 @@ namespace Polynomial
 
 open Ideal.Quotient Ideal RingHom
 
-set_option linter.flexible false in
 example : Irreducible (X ^ 4 - 10 * X ^ 2 + 1 : ℤ[X]) := by
   -- We will apply the generalized Eisenstein criterion with `q = X ^ 2 + 1` and `K = ZMod 3`.
   set f : ℤ[X] := X ^ 4 - 10 * X ^ 2 + 1 with hf_eq
@@ -42,7 +41,7 @@ example : Irreducible (X ^ 4 - 10 * X ^ 2 + 1 : ℤ[X]) := by
     have hdeg_q₃ : q₃.natDegree = 2 := by unfold q₃; compute_degree!
     suffices Irreducible q₃ by simpa [q] using this
     apply irreducible_of_degree_le_three_of_not_isRoot
-      (by simp_all) (by simp_all [q₃]; decide)
+      (by simp_all) (by simp_rw [q₃, IsRoot.def, eval_add, eval_pow, eval_X, eval_one]; decide)
   · unfold q; monicity!
   · exact Monic.isPrimitive hf_lC
   · simp_all

Archive/Examples/IfNormalization/WithoutAesop.lean

@@ -60,7 +60,7 @@ def normalize' (l : AList (fun _ : ℕ => Bool)) :
         refine ⟨fun f => ?_, ?_, fun w b => ?_⟩
         · simp only [eval, apply_ite, ite_eq_iff']
           cases hfv : f v
-          · simp +contextual only [cond_false, h, he₁]
+          · simp +contextual only [Bool.cond_false, h, he₁]
             refine ⟨fun _ => ?_, fun _ => ?_⟩
             · congr
               ext w
@@ -74,7 +74,7 @@ def normalize' (l : AList (fun _ : ℕ => Bool)) :
               · subst h
                 simp_all
               · simp_all
-          · simp only [cond_true, h, ht₁]
+          · simp only [Bool.cond_true, h, ht₁]
             refine ⟨fun _ => ?_, fun _ => ?_⟩
             · congr
               ext w

Archive/Imo/Imo1987Q1.lean

@@ -31,7 +31,6 @@ open Finset (range sum_const)
 
 namespace Imo1987Q1
 
-set_option backward.isDefEq.respectTransparency false in
 /-- The set of pairs `(x : α, σ : Perm α)` such that `σ x = x` is equivalent to the set of pairs
 `(x : α, σ : Perm {x}ᶜ)`. -/
 def fixedPointsEquiv : { σx : α × Perm α // σx.2 σx.1 = σx.1 } ≃ Σ x : α, Perm ({x}ᶜ : Set α) :=
@@ -42,7 +41,6 @@ def fixedPointsEquiv : { σx : α × Perm α // σx.2 σx.1 = σx.1 } ≃ Σ x :
       sigmaCongrRight fun x => Equiv.subtypeEquivRight (by simp)
     _ ≃ Σ x : α, Perm ({x}ᶜ : Set α) := sigmaCongrRight fun x => by apply Equiv.Set.compl
 
-set_option backward.isDefEq.respectTransparency false in
 theorem card_fixed_points :
     card { σx : α × Perm α // σx.2 σx.1 = σx.1 } = card α * (card α - 1)! := by
   simp only [card_congr (fixedPointsEquiv α), card_sigma, card_perm]

Archive/Imo/Imo2008Q4.lean

@@ -34,7 +34,6 @@ end Imo2008Q4
 
 open Imo2008Q4
 
-set_option linter.flexible false in
 theorem imo2008_q4 (f : ℝ → ℝ) (H₁ : ∀ x > 0, 0 < f x) :
     (∀ w x y z : ℝ, 0 < w → 0 < x → 0 < y → 0 < z → w * x = y * z →
       (f w ^ 2 + f x ^ 2) / (f (y ^ 2) + f (z ^ 2)) = (w ^ 2 + x ^ 2) / (y ^ 2 + z ^ 2)) ↔