[auto-sync] Merge upstream mathlib4 into master (PR #77)

Auto-merged by sync_finalize after CI success.

Author: winstonyin-ax

.git-blame-ignore-revs

@@ -4,3 +4,5 @@
 fc48848e4374f13c796a7399bfccd2e228f776df
 # 2025-11-19 move Mathlib to the module system (#31786)
 6a54a80825b060ab20dc31751ebdce78b3a3b518
+# 2025-12-01 fix spelling in doc-strings (#32286)
+b728e1450a53133aa4171eeadc0bc8d3ee58415c

.github/workflows/zulip_emoji_reconcile.yml

@@ -0,0 +1,45 @@
+# Periodic safety net that keeps the Zulip emoji reactions on PR-related messages
+# in sync with each PR's actual state (open/closed/merged, labels, CI result).
+# The event-driven zulip_emoji_* workflows react to individual label/close/CI
+# events; this sweep repairs any drift they miss (dropped webhooks, outages,
+# state changes while a workflow was broken). See
+# https://github.com/leanprover-community/mathlib-ci/blob/master/docs/zulip-emoji-reconcile.md
+name: Zulip emoji reconcile
+
+on:
+  schedule:
+    - cron: "37 * * * *"  # hourly, offset to dodge top-of-hour runner load
+  workflow_dispatch:
+    inputs:
+      dry-run:
+        description: Log planned reaction changes without modifying Zulip
+        type: boolean
+        default: false
+
+concurrency:
+  group: ${{ github.workflow }}
+  cancel-in-progress: false
+
+permissions:
+  contents: read
+  pull-requests: read
+
+jobs:
+  reconcile:
+    if: github.repository == 'leanprover-community/mathlib4'
+    runs-on: ubuntu-latest
+    steps:
+      - name: Check out reconcile config
+        uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
+        with:
+          sparse-checkout: .github/zulip-emoji-config.json
+          sparse-checkout-cone-mode: false
+
+      - name: Reconcile
+        uses: leanprover-community/mathlib-ci/.github/actions/zulip-emoji-reconcile@5668fbbccf0fecefdfcddf539b8406db197dfc59
+        with:
+          config: .github/zulip-emoji-config.json
+          sweep: true
+          dry-run: ${{ github.event_name == 'workflow_dispatch' && inputs.dry-run }}
+          zulip-api-key: ${{ secrets.ZULIP_API_KEY }}
+          github-token: ${{ github.token }}

.github/zulip-emoji-config.json

@@ -0,0 +1,63 @@
+{
+  "_comment": "Config for the zulip-emoji-reconcile action (see .github/workflows/zulip_emoji_reconcile.yml), which keeps Zulip emoji reactions in sync with PR state. Format and semantics: https://github.com/leanprover-community/mathlib-ci/blob/master/docs/zulip-emoji-reconcile.md. Derived from scripts/zulip/examples/mathlib4-config.json in that repo; keep the two in sync when the emoji table changes.",
+
+  "github_repo": "leanprover-community/mathlib4",
+
+  "_merged_comment": "bors merges by rebasing a PR's commits onto master, so GitHub reports the PR as CLOSED (not merged) and renames its title to start with '[Merged by Bors] -'. Treat such closed PRs as merged so they get the 'merge' emoji rather than 'closed-pr'. Drop this key for repos that merge via the GitHub merge button/queue, where the PR state is reported as MERGED directly.",
+  "merged_title_prefix": "[Merged by Bors] -",
+
+  "zulip": {
+    "site": "https://leanprover.zulipchat.com",
+    "email": "github-mathlib4-bot@leanprover.zulipchat.com"
+  },
+
+  "channels": {
+    "pr_reviews": "PR reviews",
+    "reviewers": "mathlib reviewers",
+    "rss_allow": ["mathlib bors notifications"]
+  },
+
+  "ci": {
+    "_comment": "Case-insensitive substring match against check-run name, workflow name, or status context. The first three select the gating jobs of 'continuous integration' / 'continuous integration (mathlib forks)' -- their check runs are named 'ci / Build', 'ci (fork) / Build', etc. -- while leaving auxiliary jobs (Upload to cache, Post-CI job) out of the emoji. 'Check workflows' is the actionlint workflow: it runs only on PRs touching .github/**, so it contributes nothing on ordinary PRs and becomes the CI signal on workflows-only PRs where the main CI never triggers.",
+    "check_names": ["Build", "Lint style", "Post-Build Step", "Check workflows"]
+  },
+
+  "states": [
+    {
+      "name": "merged", "group": "pr", "priority": 30,
+      "source": {"state": "merged"}, "emoji": "merge"
+    },
+    {
+      "name": "closed", "group": "pr", "priority": 20,
+      "source": {"state": "closed"},
+      "emoji": "closed-pr", "emoji_code": "61293", "reaction_type": "realm_emoji"
+    },
+    {
+      "name": "ready-to-merge", "group": "pr", "priority": 12,
+      "source": {"label": "ready-to-merge"},
+      "emoji": "bors", "emoji_code": "22134", "reaction_type": "realm_emoji"
+    },
+    {
+      "name": "delegated", "group": "pr", "priority": 11,
+      "source": {"label": "delegated"}, "emoji": "peace_sign"
+    },
+    {
+      "name": "awaiting-author", "group": "pr", "priority": 10,
+      "source": {"label": "awaiting-author"}, "emoji": "writing"
+    },
+
+    {"name": "ci-running", "group": "ci", "source": {"ci": "running"}, "emoji": "yellow"},
+    {"name": "ci-success", "group": "ci", "source": {"ci": "success"}, "emoji": "check"},
+    {"name": "ci-failure", "group": "ci", "source": {"ci": "failure"}, "emoji": "cross_mark"},
+
+    {
+      "name": "maintainer-merge", "group": null,
+      "source": {"label": "maintainer-merge"}, "emoji": "hammer",
+      "suppress_in": {"channel": "reviewers", "subject_prefix": "maintainer merge"}
+    },
+    {
+      "name": "migrated", "group": null, "sticky": true,
+      "source": {"label": "migrated-from-branch"}, "emoji": "skip_forward"
+    }
+  ]
+}

Archive/Imo/Imo1987Q1.lean

@@ -56,7 +56,7 @@ fixed points. -/
 def fiber (k : ℕ) : Set (Perm α) :=
   {σ : Perm α | card (fixedPoints σ) = k}
 
-instance {k : ℕ} : Fintype (fiber α k) := inferInstanceAs <| Fintype (setOf _)
+instance {k : ℕ} : Fintype (fiber α k) := inferInstanceAs <| Fintype (Set.ofPred _)
 
 @[simp]
 theorem mem_fiber {σ : Perm α} {k : ℕ} : σ ∈ fiber α k ↔ card (fixedPoints σ) = k :=

Archive/Imo/Imo1988Q6.lean

@@ -92,7 +92,7 @@ theorem constant_descent_vieta_jumping (x y : ℕ) {claim : Prop} {H : ℕ → 
   -- Our assumptions ensure that we can then prove the claim.
   suffices exc : exceptional.Nonempty by
     -- Suppose that there exists an element in the exceptional locus.
-    simp only [Set.Nonempty, Prod.exists, Set.mem_setOf_eq, exceptional] at exc
+    simp only [Set.Nonempty, Prod.exists, Set.mem_ofPred_eq, exceptional] at exc
     -- Let (a,b) be such an element, and consider all the possible cases.
     rcases exc with ⟨a, b, hH, hb⟩
     rcases hb with (_ | rfl | rfl | hB | hB)
@@ -138,7 +138,7 @@ theorem constant_descent_vieta_jumping (x y : ℕ) {claim : Prop} {H : ℕ → 
   -- This means that m_y = m,
   -- and the conditions H(m_x, m_y) and m_x < m_y are satisfied.
   simp only at mx_lt_my hHm m_eq
-  simp only [exceptional, hHm, Set.mem_setOf_eq, true_and] at h_base
+  simp only [exceptional, hHm, Set.mem_ofPred_eq, true_and] at h_base
   push Not at h_base
   -- Finally, it also means that (m_x, m_y) does not lie in the base locus,
   -- that m_x ≠ 0, m_x ≠ m_y, B(m_x) ≠ m_y, and B(m_x) ≠ m_x + m_y.

Archive/Imo/Imo2008Q2.lean

@@ -65,7 +65,7 @@ theorem imo2008_q2b : Set.Infinite rationalSolutions := by
   have hW_sub_S : W ⊆ rationalSolutions := by
     intro s hs_in_W
     rw [rationalSolutions]
-    simp only [Set.mem_setOf_eq] at hs_in_W ⊢
+    simp only [Set.mem_ofPred_eq] at hs_in_W ⊢
     rcases hs_in_W with ⟨x, y, z, h₁, t, ht_gt_zero, hx_t, hy_t, hz_t⟩
     use x, y, z
     have key_gt_zero : 0 < t ^ 2 + t + 1 := by linarith [pow_pos ht_gt_zero 2, ht_gt_zero]
@@ -99,7 +99,7 @@ theorem imo2008_q2b : Set.Infinite rationalSolutions := by
         set z : ℚ := -t * (t + 1) with hz_def
         simp only [t, W, K, g, Set.mem_image, Prod.exists]
         use x, y, z; constructor
-        · simp only [Set.mem_setOf_eq]
+        · simp only [Set.mem_ofPred_eq]
           use x, y, z; constructor
           · rfl
           · use t; constructor