Merge branch 'master' into patch-2

Author: SnirBroshi

.github/workflows/build_template.yml

@@ -247,76 +247,6 @@ jobs:
             echo "✅ All inputRevs in lake-manifest.json are valid"
           fi
 
-      - name: validate ProofWidgets source repository
-        # Only enforce this on the main mathlib4 repository, not on nightly-testing
-        if: github.repository == 'leanprover-community/mathlib4'
-        shell: bash
-        run: |
-          cd pr-branch
-
-          expected_url='https://github.com/leanprover-community/ProofWidgets4'
-          proofwidgets_count=$(jq '[.packages[] | select(.name == "proofwidgets")] | length' lake-manifest.json)
-          if [ "$proofwidgets_count" -ne 1 ]; then
-            echo "❌ Error: expected exactly one proofwidgets entry in lake-manifest.json, found $proofwidgets_count"
-            exit 1
-          fi
-
-          proofwidgets_url=$(jq -r '.packages[] | select(.name == "proofwidgets") | .url' lake-manifest.json)
-          normalized_url="${proofwidgets_url%.git}"
-          if [ "$normalized_url" != "$expected_url" ]; then
-            echo "❌ Error: invalid ProofWidgets source URL in lake-manifest.json"
-            echo "  expected: $expected_url"
-            echo "  found:    $proofwidgets_url"
-            exit 1
-          fi
-
-          echo "✅ ProofWidgets source URL is allowed: $proofwidgets_url"
-
-      - name: verify ProofWidgets lean-toolchain matches on versioned releases
-        # Only enforce this on the main mathlib4 repository, not on nightly-testing
-        if: github.repository == 'leanprover-community/mathlib4'
-        shell: bash
-        run: |
-          cd pr-branch
-
-          # Read the lean-toolchain file
-          TOOLCHAIN=$(cat lean-toolchain | tr -d '[:space:]')
-          echo "Lean toolchain: $TOOLCHAIN"
-
-          # Check if toolchain matches the versioned release pattern: leanprover/lean4:vX.Y.Z (with optional suffix like -rc1)
-          if [[ "$TOOLCHAIN" =~ ^leanprover/lean4:v[0-9]+\.[0-9]+\.[0-9]+(-[a-zA-Z0-9.-]+)?$ ]]; then
-            echo "✓ Detected versioned Lean release: $TOOLCHAIN"
-            echo "Verifying ProofWidgets lean-toolchain matches..."
-
-            # Check if ProofWidgets lean-toolchain exists
-            if [ ! -f .lake/packages/proofwidgets/lean-toolchain ]; then
-              echo "❌ Error: .lake/packages/proofwidgets/lean-toolchain does not exist"
-              echo "This file should be created by 'lake env' during dependency download."
-              exit 1
-            fi
-
-            # Read ProofWidgets lean-toolchain
-            PROOFWIDGETS_TOOLCHAIN=$(cat .lake/packages/proofwidgets/lean-toolchain | tr -d '[:space:]')
-            echo "ProofWidgets toolchain: $PROOFWIDGETS_TOOLCHAIN"
-
-            # Compare the two
-            if [ "$TOOLCHAIN" != "$PROOFWIDGETS_TOOLCHAIN" ]; then
-              echo "❌ Error: Lean toolchain mismatch!"
-              echo "  Main lean-toolchain: $TOOLCHAIN"
-              echo "  ProofWidgets lean-toolchain: $PROOFWIDGETS_TOOLCHAIN"
-              echo ""
-              echo "When using a versioned Lean release (leanprover/lean4:vX.Y.Z),"
-              echo "the ProofWidgets dependency must use the same toolchain."
-              echo "Please update the ProofWidgets dependency to use $TOOLCHAIN"
-              exit 1
-            else
-              echo "✅ ProofWidgets lean-toolchain matches: $TOOLCHAIN"
-            fi
-          else
-            echo "ℹ Lean toolchain is not a versioned release (pattern: leanprover/lean4:vX.Y.Z)"
-            echo "Skipping ProofWidgets toolchain verification."
-          fi
-
       - name: get cache (1/3 - setup and initial fetch)
         id: get_cache_part1_setup
         shell: bash # only runs `cache get` from `tools-branch`, so doesn't need to be inside landrun
@@ -327,7 +257,7 @@ jobs:
 
           # Fail quickly if the cache is completely cold, by checking for Mathlib.Init
           echo "Attempting to fetch olean for Mathlib/Init.lean from cache..."
-          ../tools-branch/.lake/build/bin/cache --skip-proofwidgets get Mathlib/Init.lean
+          ../tools-branch/.lake/build/bin/cache get Mathlib/Init.lean
 
       - name: get cache (2/3 - test Mathlib.Init cache)
         id: get_cache_part2_test
@@ -381,9 +311,9 @@ jobs:
             echo "Warming up cache using previous commit: $PREV_SHA (source: $PREV_SHA_SOURCE)"
             if git cat-file -e "$PREV_SHA^{commit}" 2>/dev/null || git fetch --no-tags --depth=1 origin "$PREV_SHA"; then
               git checkout "$PREV_SHA"
-              ../tools-branch/.lake/build/bin/cache --skip-proofwidgets get
+              ../tools-branch/.lake/build/bin/cache get
               # Run again with --repo, to ensure we actually get the oleans.
-              ../tools-branch/.lake/build/bin/cache --repo="$CACHE_REPO" --skip-proofwidgets get
+              ../tools-branch/.lake/build/bin/cache --repo="$CACHE_REPO" get
 
               echo "Switching back to branch head"
               git checkout "$ORIG_SHA"
@@ -396,18 +326,10 @@ jobs:
 
           echo "Fetching all remaining cache..."
 
-          ../tools-branch/.lake/build/bin/cache --skip-proofwidgets get
+          ../tools-branch/.lake/build/bin/cache get
 
           # Run again with --repo, to ensure we actually get the oleans.
-          ../tools-branch/.lake/build/bin/cache --repo="$CACHE_REPO" --skip-proofwidgets get
-
-      - name: fetch ProofWidgets release
-        # We need network access for ProofWidgets frontend assets.
-        # Run inside landrun so PR-controlled code remains sandboxed.
-        shell: landrun --unrestricted-network --rox /etc --rox /usr --rw /dev --rox /home/lean/.elan --rox /home/lean/actions-runner/_work --rw pr-branch/.lake/ --env PATH --env HOME --env GITHUB_OUTPUT --env CI -- bash -euxo pipefail {0}
-        run: |
-          cd pr-branch
-          lake build proofwidgets:release
+          ../tools-branch/.lake/build/bin/cache --repo="$CACHE_REPO" get
 
       - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean
         id: mk_all
@@ -462,8 +384,8 @@ jobs:
         shell: bash
         run: |
           cd pr-branch
-          ../tools-branch/.lake/build/bin/cache --skip-proofwidgets get Archive.lean
-          ../tools-branch/.lake/build/bin/cache --skip-proofwidgets get Counterexamples.lean
+          ../tools-branch/.lake/build/bin/cache get Archive.lean
+          ../tools-branch/.lake/build/bin/cache get Counterexamples.lean
 
       - name: build archive
         id: archive
@@ -955,6 +877,7 @@ jobs:
             steps.get-label-actor.outputs.username == 'mathlib-update-dependencies' ||
             steps.get-label-actor.outputs.username == 'mathlib-splicebot' ||
             contains(steps.actorTeams.outputs.teams, 'mathlib-maintainers') ||
+            contains(steps.actorTeams.outputs.teams, 'lean-release-managers') ||
             contains(steps.actorTeams.outputs.teams, 'bot-users')
           )
         name: If `auto-merge-after-CI` is present, add a `bors merge` comment.

.github/workflows/maintainer_merge_wf_run.yml

@@ -150,7 +150,8 @@ jobs:
             legacy_suffix=" (legacy)"
           fi
           metadata=$'['"${trigger_name}"$']('"${trigger_run_url}"$'), [wf_run]('"${wf_run_url}"$')'"${legacy_suffix}"
-          message="${message}"$'\n\n---\n'"${metadata}"
+          echo "${metadata}"
+          # message="${message}"$'\n\n---\n'"${metadata}"
           printf 'title<<EOF\n%s\nEOF' "${message}" | tee "$GITHUB_OUTPUT"
         env:
           AUTHOR: ${{ steps.inputs.outputs.author }}
@@ -188,7 +189,8 @@ jobs:
             legacy_suffix=" (legacy)"
           fi
           metadata=$'['"${trigger_name}"$']('"${trigger_run_url}"$'), [wf_run]('"${wf_run_url}"$')'"${legacy_suffix}"
-          body="${body}"$'\n\n---\n'"${metadata}"
+          echo "${metadata}"
+          # body="${body}"$'\n\n---\n'"${metadata}"
           printf 'body<<EOF\n%s\nEOF\n' "${body}" | tee -a "$GITHUB_OUTPUT"
 
       - name: Add comment to PR

Archive/Examples/Kuratowski.lean

@@ -233,7 +233,7 @@ theorem not_eq_univ_of_mem_theClosedSix_fourteenSet {s}
   rw [theClosedSix, kckckc_fourteenSet, kckck_fourteenSet,
     kckc_fourteenSet, kck_fourteenSet, kc_fourteenSet, k_fourteenSet] at h
   rw [Ne, eq_univ_iff_forall]
-  push_neg
+  push Not
   repeat obtain _ | ⟨_, h⟩ := h; rotate_left
   · use 1 / 2; norm_num
   · use 1 / 2; norm_num

Archive/Imo/Imo1988Q6.lean

@@ -139,7 +139,7 @@ theorem constant_descent_vieta_jumping (x y : ℕ) {claim : Prop} {H : ℕ → 
   -- 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
-  push_neg 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.
   rcases h_base with ⟨h_base, hmx, hm_diag, hm_B₁, hm_B₂⟩
@@ -279,7 +279,7 @@ example {a b : ℕ} (h : a * b ∣ a ^ 2 + b ^ 2 + 1) : 3 * a * b = a ^ 2 + b ^
       lia
     · contrapose! hV₀ with x_lt_z
       apply ne_of_gt
-      push_neg at h_base
+      push Not at h_base
       calc
         z * y > x * y := by apply mul_lt_mul_of_pos_right <;> lia
         _ ≥ x * (x + 1) := by apply mul_le_mul <;> lia

Archive/Imo/Imo2006Q5.lean

@@ -107,7 +107,7 @@ theorem Polynomial.isPeriodicPt_eval_two {P : Polynomial ℤ} {t : ℤ}
       simp [IsPeriodicPt, IsFixedPt, H]
   · -- We take two nonequal consecutive entries.
     rw [Cycle.chain_map, periodicOrbit_chain' _ ht] at HC'
-    push_neg at HC'
+    push Not at HC'
     obtain ⟨n, hn⟩ := HC'
     -- They must have opposite sign, so that P^{k + 1}(t) - P^k(t) = P^{k + 2}(t) - P^{k + 1}(t).
     rcases Int.natAbs_eq_natAbs_iff.1 (Habs n n.succ) with hn' | hn'

Archive/Imo/Imo2024Q3.lean

@@ -941,8 +941,6 @@ lemma exists_a_apply_add_eq : ∃ b c, 0 < c ∧ ∀ n, b < n →
     rcases hc.even_p (by lia) (hs n) with ⟨_, ht⟩
     simp [ht, ← two_mul]
 
-variable {a N}
-
 end Condition
 
 theorem result {a : ℕ → ℕ} {N : ℕ} (h : Condition a N) :

Archive/Wiedijk100Theorems/BallotProblem.lean

@@ -358,7 +358,7 @@ theorem ballot_problem :
   simp only [Ne, ENNReal.div_eq_top, tsub_eq_zero_iff_le, Nat.cast_le, not_le,
     add_eq_zero, Nat.cast_eq_zero, ENNReal.add_eq_top, ENNReal.natCast_ne_top, or_self_iff,
     not_false_iff, and_true]
-  push_neg
+  push Not
   exact ⟨fun _ _ => by linarith, (tsub_le_self.trans_lt (ENNReal.natCast_ne_top p).lt_top).ne⟩
 
 end Ballot

Archive/Wiedijk100Theorems/FriendshipGraphs.lean

@@ -150,7 +150,7 @@ theorem isRegularOf_not_existsPolitician (hG' : ¬ExistsPolitician G) :
   intro x
   by_cases hvx : G.Adj v x; swap; · exact (degree_eq_of_not_adj hG hvx).symm
   dsimp only [Theorems100.ExistsPolitician] at hG'
-  push_neg at hG'
+  push Not at hG'
   rcases hG' v with ⟨w, hvw', hvw⟩
   rcases hG' x with ⟨y, hxy', hxy⟩
   by_cases hxw : G.Adj x w

Archive/Wiedijk100Theorems/SumOfPrimeReciprocalsDiverges.lean

@@ -97,7 +97,7 @@ of `p`.
 theorem range_sdiff_eq_biUnion {x k : ℕ} : range x \ M x k = U x k := by
   ext e
   simp only [mem_biUnion, not_and, Finset.mem_sdiff, mem_filter, mem_range, U, M, P]
-  push_neg
+  push Not
   constructor
   · rintro ⟨hex, hexh⟩
     obtain ⟨p, ⟨hpp, hpe1⟩, hpk⟩ := hexh hex

Archive/ZagierTwoSquares.lean

@@ -107,9 +107,9 @@ def complexInvo : Function.End (zagierSet k) := fun ⟨⟨x, y, z⟩, h⟩ =>
   · -- less: `x + z < y` (`x < y - z` as stated by Zagier)
     rw [Nat.sub_sub]; zify [less.le] at h ⊢; linarith [h]
   · -- more: `2 * y < x`
-    push_neg at less; zify [less, more.le] at h ⊢; linarith [h]
+    push Not at less; zify [less, more.le] at h ⊢; linarith [h]
   · -- middle: `x` is neither less than `y - z` or more than `2 * y`
-    push_neg at less more; zify [less, more] at h ⊢; linarith [h]⟩
+    push Not at less more; zify [less, more] at h ⊢; linarith [h]⟩
 
 variable [hk : Fact (4 * k + 1).Prime]
 
@@ -127,12 +127,12 @@ theorem complexInvo_sq : complexInvo k ^ 2 = 1 := by
     rw [Nat.sub_sub, two_mul, ← tsub_add_eq_add_tsub (by linarith), ← add_assoc,
       Nat.add_sub_cancel, add_comm (x + z), Nat.sub_add_cancel less.le]
   · -- more
-    push_neg at less
+    push Not at less
     simp only [show x - 2 * y + y < x + z - y by zify [less, more.le]; linarith, ite_true]
     rw [Nat.sub_add_cancel more.le, Nat.sub_right_comm, Nat.sub_sub _ _ y, ← two_mul, add_comm,
       Nat.add_sub_assoc more.le, Nat.add_sub_cancel]
   · -- middle
-    push_neg at less more
+    push Not at less more
     simp only [show ¬(2 * y - x + (x + z - y) < y) by zify [less, more]; linarith,
       show ¬(2 * y < 2 * y - x) by zify [more]; linarith, ite_false]
     rw [tsub_tsub_assoc (2 * y).le_refl more, tsub_self, zero_add,