Merge branch 'master' into ChebyshevExtremalLC

Author: YuvalFilmus

.github/workflows/daily.yml

@@ -33,20 +33,6 @@ jobs:
       - name: Checkout branch or tag
         uses: actions/checkout@1af3b93b6815bc44a9784bd300feb67ff0d1eeb3 # v6.0.0
 
-      # this step needs to be run here while we have `mathlib4` checked out,
-      # or else `gh run view` will try to look for runs in `mathlib4-nightly-testing`
-      - name: Get URLs
-        id: urls
-        env:
-          GH_TOKEN: ${{ github.token }}
-        run: |
-          # adapted from https://cmbuckley.co.uk/blog/2024/04/09/deep-links-to-github-actions-job-logs/
-          lean4checker_url=$(gh run view ${{ github.run_id }} --json jobs --jq '
-            .jobs[] | select(.name == "check-lean4checker (${{ matrix.branch_type }})")
-            | (.url + (.steps[] | select(.name == "Check environments using lean4checker")
-              | "#step:\(.number):1"))')
-          echo "lean4checker_url=$lean4checker_url" | tee -a "$GITHUB_OUTPUT"
-
       - name: Fetch latest tags (if nightly)
         if: matrix.branch_type == 'nightly'
         run: |
@@ -79,7 +65,7 @@ jobs:
           use-mathlib-cache: true
           reinstall-transient-toolchain: true
 
-      - name: Check environments using lean4checker # make sure this name is consistent with "Get URLs"
+      - name: Check environments using lean4checker # make sure this name is consistent with "Get job status and URLs" in the notify job
         id: lean4checker
         continue-on-error: true
         run: |
@@ -110,8 +96,51 @@ jobs:
           # so we explicitly check Batteries as well here.
           lake env lean4checker/.lake/build/bin/lean4checker Batteries Mathlib
 
+  notify-lean4checker:
+    runs-on: ubuntu-latest
+    needs: check-lean4checker
+    if: github.repository == 'leanprover-community/mathlib4' && always()
+    strategy:
+      fail-fast: false
+      matrix:
+        branch_type: [master, nightly]
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@1af3b93b6815bc44a9784bd300feb67ff0d1eeb3 # v6.0.0
+
+      - name: Get job status and URLs
+        id: get-status
+        env:
+          GH_TOKEN: ${{ github.token }}
+        run: |
+          JOB_NAME="check-lean4checker (${{ matrix.branch_type }})"
+          
+          # Get URL to the specific step
+          LEAN4CHECKER_URL=$(gh run view ${{ github.run_id }} --json jobs --jq \
+            ".jobs[] | select(.name == \"$JOB_NAME\") \
+            | (.url + (.steps[] | select(.name == \"Check environments using lean4checker\") \
+              | \"#step:\(.number):1\"))")
+          
+          echo "lean4checker_url=${LEAN4CHECKER_URL}" | tee -a "$GITHUB_OUTPUT"
+
+      - name: Fetch latest tags (if nightly)
+        if: matrix.branch_type == 'nightly'
+        run: |
+          git remote add nightly-testing https://github.com/leanprover-community/mathlib4-nightly-testing.git
+          git fetch nightly-testing --tags
+          LATEST_TAG=$(git tag | grep -E "${{ env.TAG_PATTERN }}" | sort -r | head -n 1)
+          echo "LATEST_TAG=${LATEST_TAG}" | tee -a "$GITHUB_ENV"
+
+      - name: Set branch ref
+        run: |
+          if [ "${{ matrix.branch_type }}" == "master" ]; then
+            echo "BRANCH_REF=${{ env.DEFAULT_BRANCH }}" >> "$GITHUB_ENV"
+          else
+            echo "BRANCH_REF=${{ env.LATEST_TAG }}" >> "$GITHUB_ENV"
+          fi
+
       - name: Post success message for lean4checker on Zulip
-        if: steps.lean4checker.outcome == 'success'
+        if: needs.check-lean4checker.result == 'success'
         uses: zulip/github-actions-zulip/send-message@e4c8f27c732ba9bd98ac6be0583096dea82feea5 # v1.0.2
         with:
           api-key: ${{ secrets.ZULIP_API_KEY }}
@@ -121,10 +150,10 @@ jobs:
           type: 'stream'
           topic: 'lean4checker'
           content: |
-            ✅ lean4checker [succeeded](${{ steps.urls.outputs.lean4checker_url }}) on ${{ github.sha }} (branch: ${{ env.BRANCH_REF }})
+            ✅ lean4checker [succeeded](${{ steps.get-status.outputs.lean4checker_url }}) on ${{ github.sha }} (branch: ${{ env.BRANCH_REF }})
 
       - name: Post failure / cancelled message for lean4checker on Zulip
-        if: steps.lean4checker.outcome == 'failure' || steps.lean4checker.outcome == 'cancelled'
+        if: needs.check-lean4checker.result != 'success'
         uses: zulip/github-actions-zulip/send-message@e4c8f27c732ba9bd98ac6be0583096dea82feea5 # v1.0.2
         with:
           api-key: ${{ secrets.ZULIP_API_KEY }}
@@ -134,7 +163,7 @@ jobs:
           type: 'stream'
           topic: 'lean4checker failure'
           content: |
-            ❌ lean4checker [$${{ steps.lean4checker.outcome }}](${{ steps.urls.outputs.lean4checker_url }}) on ${{ github.sha }} (branch: ${{ env.BRANCH_REF }})
+            ❌ lean4checker [${{ needs.check-lean4checker.result }}](${{ steps.get-status.outputs.lean4checker_url }}) on ${{ github.sha }} (branch: ${{ env.BRANCH_REF }})
 
   check-mathlib_test_executable:
     runs-on: ubuntu-latest
@@ -148,20 +177,6 @@ jobs:
       - name: Checkout branch or tag
         uses: actions/checkout@1af3b93b6815bc44a9784bd300feb67ff0d1eeb3 # v6.0.0
 
-      # this step needs to be run here while we have `mathlib4` checked out,
-      # or else `gh run view` will try to look for runs in `mathlib4-nightly-testing`
-      - name: Get URLs
-        id: urls
-        env:
-          GH_TOKEN: ${{ github.token }}
-        run: |
-          # adapted from https://cmbuckley.co.uk/blog/2024/04/09/deep-links-to-github-actions-job-logs/
-          mathlib_test_executable_url=$(gh run view ${{ github.run_id }} --json jobs --jq '
-            .jobs[] | select(.name == "check-lean4checker (${{ matrix.branch_type }})")
-            | (.url + (.steps[] | select(.name == "Run mathlib_test_executable")
-              | "#step:\(.number):1"))')
-          echo "mathlib_test_executable_url=$mathlib_test_executable_url" | tee -a "$GITHUB_OUTPUT"
-
       - name: Fetch latest tags (if nightly)
         if: matrix.branch_type == 'nightly'
         run: |
@@ -194,14 +209,57 @@ jobs:
           use-mathlib-cache: true
           reinstall-transient-toolchain: true
 
-      - name: Run mathlib_test_executable # make sure this name is consistent with "Get URLs"
+      - name: Run mathlib_test_executable # make sure this name is consistent with "Get job status and URLs" in the notify job
         id: mathlib-test
         continue-on-error: true
         run: |
           lake exe mathlib_test_executable
 
+  notify-mathlib_test_executable:
+    runs-on: ubuntu-latest
+    needs: check-mathlib_test_executable
+    if: github.repository == 'leanprover-community/mathlib4' && always()
+    strategy:
+      fail-fast: false
+      matrix:
+        branch_type: [master, nightly]
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@1af3b93b6815bc44a9784bd300feb67ff0d1eeb3 # v6.0.0
+
+      - name: Get job status and URLs
+        id: get-status
+        env:
+          GH_TOKEN: ${{ github.token }}
+        run: |
+          JOB_NAME="check-mathlib_test_executable (${{ matrix.branch_type }})"
+          
+          # Get URL to the specific step
+          MATHLIB_TEST_EXECUTABLE_URL=$(gh run view ${{ github.run_id }} --json jobs --jq \
+            ".jobs[] | select(.name == \"$JOB_NAME\") \
+            | (.url + (.steps[] | select(.name == \"Run mathlib_test_executable\") \
+              | \"#step:\(.number):1\"))")
+          
+          echo "mathlib_test_executable_url=${MATHLIB_TEST_EXECUTABLE_URL}" | tee -a "$GITHUB_OUTPUT"
+
+      - name: Fetch latest tags (if nightly)
+        if: matrix.branch_type == 'nightly'
+        run: |
+          git remote add nightly-testing https://github.com/leanprover-community/mathlib4-nightly-testing.git
+          git fetch nightly-testing --tags
+          LATEST_TAG=$(git tag | grep -E "${{ env.TAG_PATTERN }}" | sort -r | head -n 1)
+          echo "LATEST_TAG=${LATEST_TAG}" | tee -a "$GITHUB_ENV"
+
+      - name: Set branch ref
+        run: |
+          if [ "${{ matrix.branch_type }}" == "master" ]; then
+            echo "BRANCH_REF=${{ env.DEFAULT_BRANCH }}" >> "$GITHUB_ENV"
+          else
+            echo "BRANCH_REF=${{ env.LATEST_TAG }}" >> "$GITHUB_ENV"
+          fi
+
       - name: Post success message for mathlib_test_executable on Zulip
-        if: steps.mathlib-test.outcome == 'success'
+        if: needs.check-mathlib_test_executable.result == 'success'
         uses: zulip/github-actions-zulip/send-message@e4c8f27c732ba9bd98ac6be0583096dea82feea5 # v1.0.2
         with:
           api-key: ${{ secrets.ZULIP_API_KEY }}
@@ -211,10 +269,10 @@ jobs:
           type: 'stream'
           topic: 'mathlib test executable'
           content: |
-            ✅ mathlib_test_executable [succeeded](${{ steps.urls.outputs.mathlib_test_executable_url }}) on ${{ github.sha }} (branch: ${{ env.BRANCH_REF }})
+            ✅ mathlib_test_executable [succeeded](${{ steps.get-status.outputs.mathlib_test_executable_url }}) on ${{ github.sha }} (branch: ${{ env.BRANCH_REF }})
 
       - name: Post failure / cancelled message for mathlib_test_executable on Zulip
-        if: steps.mathlib-test.outcome == 'failure' || steps.mathlib-test.outcome == 'cancelled'
+        if: needs.check-mathlib_test_executable.result != 'success'
         uses: zulip/github-actions-zulip/send-message@e4c8f27c732ba9bd98ac6be0583096dea82feea5 # v1.0.2
         with:
           api-key: ${{ secrets.ZULIP_API_KEY }}
@@ -224,4 +282,4 @@ jobs:
           type: 'stream'
           topic: 'mathlib test executable failure'
           content: |
-            ❌ mathlib_test_executable [${{ steps.mathlib-test.outcome }}](${{ steps.urls.outputs.mathlib_test_executable_url }}) on ${{ github.sha }} (branch: ${{ env.BRANCH_REF }})
+            ❌ mathlib_test_executable [${{ needs.check-mathlib_test_executable.result }}](${{ steps.get-status.outputs.mathlib_test_executable_url }}) on ${{ github.sha }} (branch: ${{ env.BRANCH_REF }})

Archive/Imo/Imo1994Q1.lean

@@ -69,10 +69,7 @@ theorem imo1994_q1 (n : ℕ) (m : ℕ) (A : Finset ℕ) (hm : #A = m + 1)
   by_contra! h : a k + a (rev k) < n + 1
   -- We exhibit `k+1` elements of `A` greater than `a (rev k)`
   set f : Fin (m + 1) ↪ ℕ :=
-    ⟨fun i => a i + a (rev k), by
-      apply injective_of_le_imp_le
-      intro i j hij
-      rwa [add_le_add_iff_right, a.map_rel_iff] at hij ⟩
+    ⟨fun i => a i + a (rev k), .of_eq_imp_le (a.map_rel_iff.mp <| add_right_cancel · |>.le)⟩
   -- Proof that the `f i` are greater than `a (rev k)` for `i ≤ k`
   have hf : map f (Icc 0 k) ⊆ map a.toEmbedding (Ioc (rev k) (Fin.last m)) := by
     intro x hx

Archive/Imo/Imo2015Q6.lean

@@ -96,8 +96,6 @@ lemma notMem_pool_self : a t ∉ pool a t := by
   obtain ⟨u, lu, hu⟩ := exists_add_eq_of_mem_pool h
   exact lu.ne (ha.2 hu)
 
-@[deprecated (since := "2025-05-23")] alias not_mem_pool_self := notMem_pool_self
-
 /-- The number of balls stays unchanged if there is a ball with height 0 and increases by 1
 otherwise. -/
 lemma card_pool_succ : #(pool a (t + 1)) = #(pool a t) + if 0 ∈ pool a t then 0 else 1 := by

Archive/Imo/Imo2019Q2.lean

@@ -229,8 +229,6 @@ theorem Q_notMem_CB : cfg.Q ∉ line[ℝ, cfg.C, cfg.B] := by
     or_iff_right cfg.C_ne_Q₁, or_iff_right cfg.sbtw_Q_A₁_Q₁.left_ne_right, angle_comm] at hc
   exact cfg.not_collinear_ABC (hc.elim collinear_of_angle_eq_zero collinear_of_angle_eq_pi)
 
-@[deprecated (since := "2025-05-23")] alias Q_not_mem_CB := Q_notMem_CB
-
 theorem Q_ne_B : cfg.Q ≠ cfg.B := by
   intro h
   have h' := cfg.Q_notMem_CB

Archive/Imo/Imo2024Q5.lean

@@ -135,10 +135,6 @@ lemma MonsterData.notMem_monsterCells_of_fst_eq_zero (m : MonsterData N)
     {c : Cell N} (hc : c.1 = 0) : c ∉ m.monsterCells := by
   simp [monsterCells, Prod.ext_iff, hc]
 
-@[deprecated (since := "2025-05-23")]
-alias MonsterData.not_mem_monsterCells_of_fst_eq_zero :=
-  MonsterData.notMem_monsterCells_of_fst_eq_zero
-
 lemma MonsterData.le_N_of_mem_monsterCells {m : MonsterData N} {c : Cell N}
     (hc : c ∈ m.monsterCells) : (c.1 : ℕ) ≤ N := by
   simp only [monsterCells, Set.mem_range, Subtype.exists, Set.mem_Icc] at hc

Archive/Wiedijk100Theorems/AscendingDescendingSequences.lean

@@ -120,7 +120,7 @@ By combining the previous two lemmas, we see that since `f` is injective, the pa
 must also be unique.
 -/
 private lemma paired_injective (hf : Injective f) : Injective (paired f) := by
-  apply injective_of_lt_imp_ne
+  apply Injective.of_lt_imp_ne
   intro i j hij q
   cases lt_or_gt_of_ne (hf.ne hij.ne)
   case inl h => exact (maxIncSequencesTo_lt hij h).ne congr($q.1)

Cache/IO.lean

@@ -459,10 +459,10 @@ Return tuples of the form ("module name", "path to .lean file").
 
 The input string `arg` takes one of the following forms:
 
-1. `Mathlib.Algebra.Fields.Basic`: there exists such a Lean file
-2. `Mathlib.Algebra.Fields`: no Lean file exists but a folder (TODO)
-3. `Mathlib/Algebra/Fields/Basic.lean`: the file exists (note potentially `\` on Windows)
-4. `Mathlib/Algebra/Fields/`: the folder exists (TODO)
+1. `Mathlib.Algebra.Field.Basic`: there exists such a Lean file
+2. `Mathlib.Algebra.Field`: no Lean file exists but a folder (TODO)
+3. `Mathlib/Algebra/Field/Basic.lean`: the file exists (note potentially `\` on Windows)
+4. `Mathlib/Algebra/Field/`: the folder exists (TODO)
 
 Not supported yet:
 

Counterexamples/CliffordAlgebraNotInjective.lean

@@ -62,8 +62,6 @@ theorem X_Y_Z_notMem_kIdeal : (X * Y * Z : MvPolynomial (Fin 3) (ZMod 2)) ∉ kI
     ← Finsupp.equivFunOnFinite_symm_eq_sum] at h
   contradiction
 
-@[deprecated (since := "2025-05-23")] alias X_Y_Z_not_mem_kIdeal := X_Y_Z_notMem_kIdeal
-
 theorem mul_self_mem_kIdeal_of_X_Y_Z_mul_mem {x : MvPolynomial (Fin 3) (ZMod 2)}
     (h : X * Y * Z * x ∈ kIdeal) : x * x ∈ kIdeal := by
   rw [mem_kIdeal_iff] at h

Counterexamples/NowhereDifferentiable.lean

@@ -103,7 +103,7 @@ theorem lt_seq {b : ℝ} (hb : 0 < b) (x : ℝ) (m : ℕ) : x < seq b x m := by
 
 theorem le_seq {b : ℝ} (hb : 0 < b) (x : ℝ) (m : ℕ) : x ≤ seq b x m := (lt_seq hb x m).le
 
-theorem seq_le {b : ℝ} (hb : 0 < b) (x : ℝ) (m : ℕ) : seq b x m ≤ x + (3 / 2) * b⁻¹ ^ m  := by
+theorem seq_le {b : ℝ} (hb : 0 < b) (x : ℝ) (m : ℕ) : seq b x m ≤ x + (3 / 2) * b⁻¹ ^ m := by
   grw [seq, Int.floor_le]
   simp [field]
 
@@ -235,13 +235,13 @@ theorem weierstrass_slope {a : ℝ} (ha : a ∈ Set.Ioo 0 1) {b : ℕ} (hb : Odd
     |seq b x m - x| * ((2 / 3 - π / (a * b - 1)) * (a * b) ^ m) ≤
       |weierstrass a b (seq b x m) - weierstrass a b x| := by
   simp_rw [weierstrass]
-  obtain hsseq := summable_weierstrass ha b (seq b x m)
-  obtain hsx := summable_weierstrass ha b x
-  obtain hsum := hsseq.sub hsx
+  have hsseq := summable_weierstrass ha b (seq b x m)
+  have hsx := summable_weierstrass ha b x
+  have hsum := hsseq.sub hsx
   rw [← hsseq.tsum_sub hsx]
   simp_rw [← mul_sub] at ⊢ hsum
   rw [← hsum.sum_add_tsum_nat_add m]
-  obtain hsum_shift := (summable_nat_add_iff m).mpr hsum
+  have hsum_shift := (summable_nat_add_iff m).mpr hsum
   rw [add_comm]
   refine le_trans ?_ (abs_sub_abs_le_abs_add _ _)
   rw [sub_mul (2 / 3), mul_sub |seq b x m - x|]
@@ -263,7 +263,7 @@ theorem not_differentiableAt_weierstrass
       atTop (𝓝 (f' 1)) := by
     convert (h.lim_real 1).comp (tendsto_seq_sub_inv hb1 x)
     simp
-  obtain h := (continuous_abs.tendsto _).comp this
+  have h := (continuous_abs.tendsto _).comp this
   contrapose! h
   apply not_tendsto_nhds_of_tendsto_atTop
   -- To show the absolute value of slope tends to ∞, it suffices to show its lower bound does.

Counterexamples/SorgenfreyLine.lean

@@ -155,8 +155,8 @@ theorem isClopen_Ico (a b : ℝₗ) : IsClopen (Ico a b) :=
 
 instance : TotallyDisconnectedSpace ℝₗ :=
   ⟨fun _ _ hs x hx y hy =>
-    le_antisymm (hs.subset_isClopen (isClopen_Ici x) ⟨x, hx, left_mem_Ici⟩ hy)
-      (hs.subset_isClopen (isClopen_Ici y) ⟨y, hy, left_mem_Ici⟩ hx)⟩
+    le_antisymm (hs.subset_isClopen (isClopen_Ici x) ⟨x, hx, self_mem_Ici⟩ hy)
+      (hs.subset_isClopen (isClopen_Ici y) ⟨y, hy, self_mem_Ici⟩ hx)⟩
 
 instance : FirstCountableTopology ℝₗ :=
   ⟨fun x => (nhds_basis_Ico_rat x).isCountablyGenerated⟩
@@ -221,7 +221,7 @@ theorem isClosed_of_subset_antidiagonal {s : Set (ℝₗ × ℝₗ)} {c : ℝₗ
   obtain rfl : x + y = c := by
     change (x, y) ∈ {p : ℝₗ × ℝₗ | p.1 + p.2 = c}
     exact closure_minimal (hs : s ⊆ {x | x.1 + x.2 = c}) (isClosed_antidiagonal c) H
-  rcases mem_closure_iff.1 H (Ici (x, y)) (isClopen_Ici_prod _).2 left_mem_Ici with
+  rcases mem_closure_iff.1 H (Ici (x, y)) (isClopen_Ici_prod _).2 self_mem_Ici with
     ⟨⟨x', y'⟩, ⟨hx : x ≤ x', hy : y ≤ y'⟩, H⟩
   convert H
   · refine hx.antisymm ?_