merge: include feat/lipschitzSmooth-cocoercive for CocoerciveWith predicate

Author: FordUniver

.github/actions/get-mathlib-ci/action.yml

@@ -10,7 +10,7 @@ inputs:
     # Default pinned commit used by workflows unless they explicitly override.
     # Update this ref as needed to pick up changes to mathlib-ci scripts
     # This is also updated automatically by .github/workflows/update_dependencies.yml
-    default: 99a8d566da03485d4e08fa0a85e38200f2d4e964
+    default: 78f34ded6a5f5aa11ea5b7c3120fe5d8422db1da
   path:
     description: Checkout destination path.
     required: false

.github/workflows/labels_from_comment.yml

@@ -29,7 +29,7 @@ jobs:
     steps:
     - name: Add / remove label based on comment
       run: |
-        labelArray=("awaiting-author" "awaiting-zulip" "WIP" "easy" "please-adopt" "help-wanted" "CI" "brownian" "carleson" "CFT" "FLT" "infinity-cosmos" "sphere-packing" "toric" "IMO" "t-algebra" "t-algebraic-geometry" "t-algebraic-topology" "t-analysis" "t-category-theory" "t-combinatorics" "t-computability" "t-condensed" "t-convex-geometry" "t-data" "t-differential-geometry" "t-dynamics" "t-euclidean-geometry" "t-geometric-group-theory" "t-group-theory" "t-linter" "t-logic" "t-measure-probability" "t-meta" "t-number-theory" "t-order" "t-ring-theory" "t-set-theory" "t-topology")
+        labelArray=("awaiting-author" "awaiting-zulip" "WIP" "easy" "please-adopt" "help-wanted" "CI" "brownian" "carleson" "CFT" "FLT" "infinity-cosmos" "sphere-packing" "toric" "LLM-generated" "IMO" "t-algebra" "t-algebraic-geometry" "t-algebraic-topology" "t-analysis" "t-category-theory" "t-combinatorics" "t-computability" "t-condensed" "t-convex-geometry" "t-data" "t-differential-geometry" "t-dynamics" "t-euclidean-geometry" "t-geometric-group-theory" "t-group-theory" "t-linter" "t-logic" "t-measure-probability" "t-meta" "t-number-theory" "t-order" "t-ring-theory" "t-set-theory" "t-topology")
 
         # we strip `\r` since line endings from GitHub contain this character
         COMMENT="${COMMENT//$'\r'/}"

.github/workflows/shake.yaml

@@ -0,0 +1,153 @@
+name: shake
+
+on:
+  schedule:
+    # Run several hours before the technical debt report which runs Mondays at 04:00 UTC
+    - cron: "10 20 * * 0" # At 20:10 UTC on Sunday.
+  workflow_dispatch:
+    inputs:
+      dry_run:
+        description: 'If true, only scan and report without modifying files or opening a PR'
+        required: false
+        default: false
+        type: boolean
+      # auto_merge:
+      #   description: 'If true, apply the auto-merge-after-CI label when creating a PR'
+      #   required: false
+      #   default: true
+      #   type: boolean
+
+jobs:
+  build:
+    name: lake shake --fix
+    runs-on: ubuntu-latest
+    if: github.repository == 'leanprover-community/mathlib4'
+    permissions:
+      contents: read
+      id-token: write
+    steps:
+      - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+
+      - name: Configure Lean
+        uses: leanprover/lean-action@c544e89643240c6b398f14a431bcdc6309e36b3e # v1.4.0
+        with:
+          auto-config: false
+          use-github-cache: false
+          use-mathlib-cache: true
+
+      # - name: lake build
+      #   run: |
+      #     lake build Archive Counterexamples
+
+      - name: lake shake
+        id: shake
+        run: |
+          # Add back Archive and Counterexamples when they've been modulized
+          lake shake --add-public --keep-implied --keep-prefix --fix --explain Mathlib > explain.txt 2>&1
+          if git diff --quiet; then
+            echo "changed=false" >> "$GITHUB_OUTPUT"
+          else
+            echo "changed=true" >> "$GITHUB_OUTPUT"
+          fi
+
+      - name: Parse shake stats
+        id: stats
+        if: steps.shake.outputs.changed == 'true'
+        run: |
+          scripts/parse_shake_output.py explain.txt "$GITHUB_OUTPUT"
+
+      - name: Upload explain.txt
+        id: upload-artifact
+        if: failure() || steps.shake.outputs.changed == 'true'
+        uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4.6.2
+        with:
+          name: shake-explain
+          path: explain.txt
+
+      - name: Cleanup explain.txt
+        if: steps.shake.outputs.changed == 'true'
+        run: |
+          rm -f explain.txt
+
+      - name: Build PR body
+        id: pr_body
+        if: steps.shake.outputs.changed == 'true' && toJson(inputs.dry_run) != 'true'
+        shell: bash
+        env:
+          RUN_URL: ${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }}
+          ARTIFACT_ID: ${{ steps.upload-artifact.outputs.artifact-id }}
+          CHANGED_FILES: ${{ steps.stats.outputs.changed_files }}
+          ADDED: ${{ steps.stats.outputs.added }}
+          REMOVED: ${{ steps.stats.outputs.removed }}
+        run: |
+          {
+            echo "body<<EOF"
+            echo "I am happy to shake some imports for you!"
+            echo ""
+            echo "**${CHANGED_FILES} files changed** · +${ADDED} imports added · -${REMOVED} imports removed"
+            echo ""
+            echo "---"
+            echo ""
+            echo "[workflow run for this PR](${RUN_URL})"
+            echo "[explain.txt](${RUN_URL}/artifacts/${ARTIFACT_ID})"
+            echo "EOF"
+          } >> "$GITHUB_OUTPUT"
+
+      - name: Generate app token
+        id: app-token
+        if: steps.shake.outputs.changed == 'true' && toJson(inputs.dry_run) != 'true'
+        uses: leanprover-community/mathlib-ci/.github/actions/azure-create-github-app-token@3bb576208589a435eeaeac9b144a1b7c3e948760
+        with:
+          app-id: ${{ secrets.MATHLIB_NOLINTS_APP_ID }}
+          key-vault-name: ${{ vars.MATHLIB_AZ_KEY_VAULT_NAME }}
+          key-name: mathlib-nolints-app-pk
+          azure-client-id: ${{ vars.GH_APP_AZURE_CLIENT_ID_PR_WRITERS }}
+          azure-tenant-id: ${{ secrets.LPC_AZ_TENANT_ID }}
+
+      - name: Create Pull Request
+        id: pr
+        if: steps.shake.outputs.changed == 'true' && toJson(inputs.dry_run) != 'true'
+        uses: peter-evans/create-pull-request@c0f553fe549906ede9cf27b5156039d195d2ece0 # v8.1.0
+        with:
+          author: "mathlib-nolints[bot] <258989889+mathlib-nolints[bot]@users.noreply.github.com>"
+          token: "${{ steps.app-token.outputs.token }}"
+          commit-message: |
+            chore: lake shake --add-public --keep-implied --keep-prefix --fix
+
+            ${{ steps.stats.outputs.changed_files }} files changed · +${{ steps.stats.outputs.added }} imports added · -${{ steps.stats.outputs.removed }} imports removed
+          branch: "shake"
+          base: master
+          title: "chore: lake shake --add-public --keep-implied --keep-prefix --fix"
+          body: ${{ steps.pr_body.outputs.body }}
+          # labels: ${{ (github.event_name == 'schedule' || toJson(inputs.auto_merge) == 'true') && 'auto-merge-after-CI' || '' }}
+
+      - name: Send Zulip message (success)
+        if: steps.pr.outcome == 'success'
+        uses: zulip/github-actions-zulip/send-message@e4c8f27c732ba9bd98ac6be0583096dea82feea5 # v1.0.2
+        with:
+          api-key: ${{ secrets.ZULIP_API_KEY }}
+          email: 'github-mathlib4-bot@leanprover.zulipchat.com'
+          organization-url: 'https://leanprover.zulipchat.com'
+          to: 'nightly-testing-mathlib'
+          type: 'stream'
+          topic: 'Mathlib `shake --fix`'
+          content: |
+            Please review #${{ steps.pr.outputs.pull-request-number }} which changes
+            ${{ steps.stats.outputs.changed_files }} files:
+            - +${{ steps.stats.outputs.added }} imports added
+            - -${{ steps.stats.outputs.removed }} imports removed
+
+      - name: Send Zulip message (failure)
+        if: ${{ toJson(inputs.dry_run) != 'true' && failure() }}
+        uses: zulip/github-actions-zulip/send-message@e4c8f27c732ba9bd98ac6be0583096dea82feea5 # v1.0.2
+        with:
+          api-key: ${{ secrets.ZULIP_API_KEY }}
+          email: 'github-mathlib4-bot@leanprover.zulipchat.com'
+          organization-url: 'https://leanprover.zulipchat.com'
+          to: 'nightly-testing-mathlib'
+          type: 'stream'
+          topic: 'Mathlib `shake --fix`'
+          content: |
+            [`shake` workflow run failed](${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }})
+
+            triggered by: `${{ github.event_name }}`

Archive/Examples/IfNormalization/Result.lean

@@ -13,8 +13,8 @@ import Mathlib.Tactic.Recall
 See `Statement.lean` for background.
 -/
 
-macro "◾" : tactic => `(tactic| aesop)
-macro "◾" : term => `(term| by aesop)
+local macro "◾" : tactic => `(tactic| aesop)
+local macro "◾" : term => `(term| by aesop)
 
 namespace IfExpr
 

Archive/Imo/Imo2024Q5.lean

@@ -938,8 +938,7 @@ lemma winningStrategy_play_one_eq_none_or_play_two_eq_none_of_edge_zero (hN : 2
         lia
       · simp at hm
         exact m.notMem_monsterCells_of_fst_eq_zero rfl hm
-      · simp at h
-        lia
+      · simp [eqComm] at h
       · dsimp only [Nat.reduceAdd, Nat.reduceDiv, Fin.mk_one] at hm
         have h1N : 1 ≤ N := by lia
         rw [m.mk_mem_monsterCells_iff_of_le (le_refl _) h1N] at hm

Archive/Imo/Imo2025Q3.lean

@@ -154,8 +154,8 @@ lemma isBonza : IsBonza fExample := by
     · simp [fExample, ch1]
     by_cases ch2 : a = 2
     · simp only [fExample, ch2, dvd_refl, not_true_eq_false, ↓reduceIte, Nat.cast_ofNat,
-        Nat.two_dvd_ne_zero, Nat.cast_ite, Nat.cast_one, Nat.cast_pow, ite_pow, one_pow,
-        Int.reducePow]
+        Nat.two_dvd_ne_zero]
+      push_cast
       split_ifs with hb1 hb2
       · grind [sq_mod_four_eq_one_of_odd]
       · simp [hb2]

Archive/Sensitivity.lean

@@ -329,7 +329,7 @@ set_option backward.isDefEq.respectTransparency false in
 theorem g_injective : Injective (g m) := by
   rw [g]
   intro x₁ x₂ h
-  simp only [V, LinearMap.prod_apply, LinearMap.id_apply, Prod.mk_inj, Pi.prod] at h
+  simp only [V, LinearMap.prod_apply, LinearMap.id_apply, Prod.mk_inj, Function.prod_apply] at h
   exact h.right
 
 set_option backward.isDefEq.respectTransparency false in

Cache/Requests.lean

@@ -94,7 +94,7 @@ def findMathlibRemote (mathlibDepPath : FilePath) : IO String := do
       let remoteUrl := parts[1]!.takeWhile (· != ' ') |>.copy -- Remove (fetch) or (push) suffix
 
       -- Check if this remote points to leanprover-community/mathlib4
-      let isMathlibRepo := remoteUrl.containsSubstr "leanprover-community/mathlib4"
+      let isMathlibRepo := remoteUrl.contains "leanprover-community/mathlib4"
 
       if isMathlibRepo then
         if remoteName == "origin" then