Merge remote-tracking branch 'origin/master' into polynomial-sequences

* origin/master: (294 commits) feat: equalizers and coequalizers in the category of ind-objects (#21139) doc: turn more links to Stacks into `@[stacks]` tags (#21135) feat(Asymptotics): prove `IsLittleOTVS.add` (#20578) feat(Algebra/Polynomial): `Polynomial.aeval` for product algebras (#21062) chore: import Std in Mathlib.lean (#21126) feat(Data/Matroid/Circuit): fundamental circuits and extensionality (#21145) feat(CategoryTheory/Endofunctor): prove the dual form of Lambek's Lemma on terminal coalgebra (#21140) feat(SetTheory/Game/PGame): rewrite left moves of `-x` as right moves of `x` under binders (#21109) feat(RingTheory/Localization/Pi): localization of a finite direct product is a product of localizations (#19042) doc: fixed notation error in customizing category composition (#21132) feat(Matrix): more lemmas for `PEquiv.toMatrix` (#21143) chore(SupIndep): speedup the `Decidable` instance (#21114) fix(CI): use `Elab.async=false` for late importers workflow (#21147) feat(Topology/Algebra/Indicator): indicator of a clopen is continuous (#20687) feat(Data/Matroid/Rank/Cardinal): Cardinality-valued rank function (#20921) feat(Algebra): `Pi.single_induction` (#21141) chore(BigOperators/Fin): golf a proof (#21131) feat: generalize tangent cone lemmas to TVS (#20859) feat(CategoryTheory): `Comma.snd L R` is final if `R` is final and domains are filtered (#21136) refactor: unapply matrix lemmas (#21091) chore(Algebra/Category): `erw` -> `rw` (#21130) feat(CategoryTheory): filteredness of Comma catgories given finality of one of the functors (#21128) feat(Algebra/Category): `ConcreteCategory` instance for `ModuleCat` (#21125) feat: PSum of finite sorts is finite (#20285) feat: inequality on the integral of a convex function of a RN derivative (#21093) feat: `(v +ᵥ s) -ᵥ (v +ᵥ t) = s -ᵥ t` (#21058) chore: rename the fact that `(∀ a < a₁, a ≤ a₂) ↔ a₁ ≤ a₂` in a dense order (#20317) feat: a `RelHom` preserves directedness (#20080) feat(Combinatorics/SimpleGraph): add definitions and theorems about the coloring of sum graphs (#18677) chore(Data/Matrix/PEquiv): clean up names (#21108) feat(Algebra/Category): `ConcreteCategory` instances for rings (#20815) feat: define Descriptive.Tree (#18763) chore(Data/Complex/Exponential): split trig functions to new file (#21075) feat(Logic/IsEmpty/Relator): empty on sides (#20319) feat(Algebra/Category): `ConcreteCategory` instance for `AlgebraCat` (#21121) feat(NumberTheory/LSeries): results involving partial sums of coefficients (part 1) (#20661) feat(RingTheory/LaurentSeries): add algebraEquiv (#21004) chore(SetTheory/Game/Impartial): golf two proofs (#21074) feat(CategoryTheory/Subpresheaf): preimage/image/range of subpresheaves (#21047) feat(RingTheory/IntegralClosure): `Algebra.IsIntegral` transfers via surjective homomorphisms (#21023) feat(`InformationTheory/Hamming`): Add AddGroup instances (#20994) feat(RingTheory/IntegralClosure): prove `Module.Finite R (adjoin R S)` for finite set `S` of integral elements (#20970) feat(RingTheory/Artinian): `IsUnit a` iff `a ∈ R⁰` for an artinian ring `R` (#21084) feat: separating set in the category of ind-objects (#21082) feat: derivWithin lemmas (#21092) chore(Fintype): golf a proof (#21113) chore: golf using `funext₂` (#21106) chore(Algebra/Group/Submonoid/Operations): move instances to new file (#21067) doc(Algebra/BigOperators/Fin): change 'product' to 'sum' in doc-string of additivised declarations (#21101) doc(ComputeDegree): typos (#21095) ...
leanprover-community · Jan 28, 2025 · c572510 · c572510
2 parents 3de084c + afd713f
commit c572510
Show file tree

Hide file tree

Showing 1,030 changed files with 25,796 additions and 9,523 deletions.
diff --git a/.github/workflows/PR_summary.yml b/.github/workflows/PR_summary.yml
@@ -14,6 +14,27 @@ jobs:
       with:
         fetch-depth: 0
 
+    - name: Update the merge-conflict label
+      run: |
+        printf 'PR number: "%s"\n' "${{ github.event.pull_request.number }}"
+        if git merge origin/master --no-ff --no-commit
+        then
+          git merge --abort || true
+          echo "This PR does not have merge conflicts with master."
+          # we use curl rather than octokit/request-action so that the job won't fail
+          # (and send an annoying email) if the labels don't exist
+          curl --request DELETE \
+            --url https://api.github.com/repos/${{ github.repository }}/issues/${{ github.event.pull_request.number }}/labels/merge-conflict \
+            --header 'authorization: Bearer ${{ secrets.GITHUB_TOKEN }}'
+        else
+          echo "This PR has merge conflicts with main."
+          # we use curl rather than octokit/request-action so that the job won't fail
+          # (and send an annoying email) if the labels don't exist
+          curl --request POST \
+            --url https://api.github.com/repos/${{ github.repository }}/issues/${{ github.event.pull_request.number }}/labels/merge-conflict \
+            --header 'authorization: Bearer ${{ secrets.GITHUB_TOKEN }}'
+        fi
+
     - name: Set up Python
       uses: actions/setup-python@v5
       with:

diff --git a/.github/workflows/latest_import.yml b/.github/workflows/latest_import.yml
@@ -48,8 +48,10 @@ jobs:
 
     - name: add minImports linter option
       run: |
-        # set `linter.minImports option` to true in `lakefile`
-        sed -i -- '/^  -- '\`'latest_import.yml'\`' uses this comment/{s=^=  ⟨`linter.minImports, true⟩,\n=}' lakefile.lean
+        # we disable checking for backticks inside single quotes with the next line
+        # shellcheck disable=SC2016
+        # set `linter.minImports option` to true and `Elab.async` to false in `lakefile`
+        sed -i -- '/^  -- '\`'latest_import.yml'\`' uses this comment/{s=^=  ⟨`linter.minImports, true⟩,\n  ⟨`Elab.async, false⟩,\n=}' lakefile.lean
 
         # import the `minImports` linter in `Mathlib.Init`
         sed -i -z 's=^=import Mathlib.Tactic.Linter.MinImports\n=' Mathlib/Init.lean

diff --git a/.github/workflows/zulip_emoji_closed_pr.yaml b/.github/workflows/zulip_emoji_closed_pr.yaml
@@ -0,0 +1,61 @@
+name: Add "closed-pr" emoji in Zulip
+# adds a reaction to Zulip messages that refer to a PR that was closed, but not merged
+
+# triggers the action when
+on:
+  pull_request:
+    # the pull request is closed or reopened, to add or remove the emoji
+    types: [closed, reopened]
+
+jobs:
+  add_closed_pr_emoji:
+    # we set the `TITLE` of the PR as a variable, this shields from possible code injection
+    env:
+      TITLE: ${{ github.event.pull_request.title }}
+
+    name: Add closed-pr emoji in Zulip
+    runs-on: ubuntu-latest
+    steps:
+      - name: Debugging information
+        run: |
+          # may be superfluous: GitHub may print the values of the environment variables by default
+          printf '%s' "${TITLE}" | hexdump -cC
+          printf 'PR title:"%s"\n' "${TITLE}"
+          printf 'issue number: "%s"\npull request number: "%s"\n' "${{ github.event.issue.number }}" "${{ github.event.pull_request.number }}"
+
+      - name: Set up Python
+        if: ${{ ! startsWith(github.event.pull_request.title, '[Merged by Bors]') ||
+                github.event_name == 'reopened' }}
+        uses: actions/setup-python@v5
+        with:
+          python-version: '3.x'
+
+      - name: Install dependencies
+        if: ${{ ! startsWith(github.event.pull_request.title, '[Merged by Bors]') ||
+                github.event_name == 'reopened' }}
+        run: |
+          python -m pip install --upgrade pip
+          pip install zulip
+
+      - name: checkout zulip_emoji_merge_delegate script
+        if: ${{ ! startsWith(github.event.pull_request.title, '[Merged by Bors]') ||
+                github.event_name == 'reopened' }}
+        uses: actions/checkout@v4
+        with:
+          sparse-checkout: |
+            scripts/zulip_emoji_merge_delegate.py
+
+      - name: Run Zulip Emoji Merge Delegate Script
+        if: ${{ ! startsWith(github.event.pull_request.title, '[Merged by Bors]') ||
+                github.event_name == 'reopened' }}
+        env:
+          ZULIP_API_KEY: ${{ secrets.ZULIP_API_KEY }}
+          ZULIP_EMAIL: [email protected]
+          ZULIP_SITE: https://leanprover.zulipchat.com
+        run: |
+          # ${{ github.event.action }} is either "closed" or "reopened"
+          # however, it only matters that it is either "closed" or
+          # something different from "closed"
+          # the effect is to add the "closed-pr" emoji to the message, if it is "closed"
+          # and to remove it otherwise
+          python scripts/zulip_emoji_merge_delegate.py "$ZULIP_API_KEY" "$ZULIP_EMAIL" "$ZULIP_SITE" "${{ github.event.action }}" "${{ github.event.pull_request.number }}"
diff --git a/Archive.lean b/Archive.lean
@@ -46,6 +46,7 @@ import Archive.Imo.Imo2020Q2
 import Archive.Imo.Imo2021Q1
 import Archive.Imo.Imo2024Q1
 import Archive.Imo.Imo2024Q2
+import Archive.Imo.Imo2024Q3
 import Archive.Imo.Imo2024Q5
 import Archive.Imo.Imo2024Q6
 import Archive.MiuLanguage.Basic

diff --git a/Archive/Imo/Imo1998Q2.lean b/Archive/Imo/Imo1998Q2.lean
@@ -39,9 +39,6 @@ the lower bound: `a(b-1)^2/2 ≤ |A|`.
 Rearranging gives the result.
 -/
 
-
-open scoped Classical
-
 variable {C J : Type*} (r : C → J → Prop)
 
 namespace Imo1998Q2
@@ -86,21 +83,25 @@ theorem JudgePair.agree_iff_same_rating (p : JudgePair J) (c : C) :
     p.Agree r c ↔ (r c p.judge₁ ↔ r c p.judge₂) :=
   Iff.rfl
 
+open scoped Classical in
 /-- The set of contestants on which two judges agree. -/
 def agreedContestants [Fintype C] (p : JudgePair J) : Finset C :=
   Finset.univ.filter fun c => p.Agree r c
 section
 
 variable [Fintype J] [Fintype C]
 
+open scoped Classical in
 /-- All incidences of agreement. -/
 def A : Finset (AgreedTriple C J) :=
   Finset.univ.filter @fun (a : AgreedTriple C J) =>
     (a.judgePair.Agree r a.contestant ∧ a.judgePair.Distinct)
 
+open scoped Classical in
 theorem A_maps_to_offDiag_judgePair (a : AgreedTriple C J) :
     a ∈ A r → a.judgePair ∈ Finset.offDiag (@Finset.univ J _) := by simp [A, Finset.mem_offDiag]
 
+open scoped Classical in
 theorem A_fibre_over_contestant (c : C) :
     (Finset.univ.filter fun p : JudgePair J => p.Agree r c ∧ p.Distinct) =
       ((A r).filter fun a : AgreedTriple C J => a.contestant = c).image Prod.snd := by
@@ -110,6 +111,7 @@ theorem A_fibre_over_contestant (c : C) :
   · rintro ⟨_, h₂⟩; refine ⟨(c, p), ?_⟩; tauto
   · intro h; aesop
 
+open scoped Classical in
 theorem A_fibre_over_contestant_card (c : C) :
     (Finset.univ.filter fun p : JudgePair J => p.Agree r c ∧ p.Distinct).card =
       ((A r).filter fun a : AgreedTriple C J => a.contestant = c).card := by
@@ -119,13 +121,15 @@ theorem A_fibre_over_contestant_card (c : C) :
   rintro ⟨a, p⟩ h ⟨a', p'⟩ h' rfl
   aesop (add simp AgreedTriple.contestant)
 
+open scoped Classical in
 theorem A_fibre_over_judgePair {p : JudgePair J} (h : p.Distinct) :
     agreedContestants r p = ((A r).filter fun a : AgreedTriple C J => a.judgePair = p).image
     AgreedTriple.contestant := by
   dsimp only [A, agreedContestants]; ext c; constructor <;> intro h
   · rw [Finset.mem_image]; refine ⟨⟨c, p⟩, ?_⟩; aesop
   · aesop
 
+open scoped Classical in
 theorem A_fibre_over_judgePair_card {p : JudgePair J} (h : p.Distinct) :
     (agreedContestants r p).card =
       ((A r).filter fun a : AgreedTriple C J => a.judgePair = p).card := by
@@ -138,6 +142,7 @@ theorem A_card_upper_bound {k : ℕ}
     (hk : ∀ p : JudgePair J, p.Distinct → (agreedContestants r p).card ≤ k) :
     (A r).card ≤ k * (Fintype.card J * Fintype.card J - Fintype.card J) := by
   change _ ≤ k * (Finset.card _ * Finset.card _ - Finset.card _)
+  classical
   rw [← Finset.offDiag_card]
   apply Finset.card_le_mul_card_image_of_maps_to (A_maps_to_offDiag_judgePair r)
   intro p hp
@@ -162,6 +167,7 @@ section
 
 variable [Fintype J]
 
+open scoped Classical in
 theorem judge_pairs_card_lower_bound {z : ℕ} (hJ : Fintype.card J = 2 * z + 1) (c : C) :
     2 * z * z + 2 * z + 1 ≤ (Finset.univ.filter fun p : JudgePair J => p.Agree r c).card := by
   let x := (Finset.univ.filter fun j => r c j).card
@@ -173,6 +179,7 @@ theorem judge_pairs_card_lower_bound {z : ℕ} (hJ : Fintype.card J = 2 * z + 1)
   suffices x + y = 2 * z + 1 by simp [← Int.ofNat_add, this]
   rw [Finset.filter_card_add_filter_neg_card_eq_card, ← hJ]; rfl
 
+open scoped Classical in
 theorem distinct_judge_pairs_card_lower_bound {z : ℕ} (hJ : Fintype.card J = 2 * z + 1) (c : C) :
     2 * z * z ≤ (Finset.univ.filter fun p : JudgePair J => p.Agree r c ∧ p.Distinct).card := by
   let s := Finset.univ.filter fun p : JudgePair J => p.Agree r c
@@ -192,6 +199,7 @@ theorem distinct_judge_pairs_card_lower_bound {z : ℕ} (hJ : Fintype.card J = 2
 
 theorem A_card_lower_bound [Fintype C] {z : ℕ} (hJ : Fintype.card J = 2 * z + 1) :
     2 * z * z * Fintype.card C ≤ (A r).card := by
+  classical
   have h : ∀ a, a ∈ A r → Prod.fst a ∈ @Finset.univ C _ := by intros; apply Finset.mem_univ
   apply Finset.mul_card_image_le_card_of_maps_to h
   intro c _