Merge branch 'repfinsupp' of https://github.com/leanprover-community/…

…mathlib4 into coinvariantsstuffhalf

.github/build.in.yml

@@ -339,6 +339,15 @@ jobs:
           # Only return if PR is still open
           filterOutClosed: true
 
+      - if: contains(steps.PR.outputs.pr_labels, 'bench-after-CI')
+        name: If `bench-after-CI` is present, add a `!bench` comment.
+        uses: GrantBirki/comment@v2
+        with:
+          token: ${{ secrets.AUTO_MERGE_TOKEN }}
+          issue-number: ${{ steps.PR.outputs.number }}
+          body: |
+            !bench
+
       - id: remove_labels
         name: Remove "awaiting-CI"
         # we use curl rather than octokit/request-action so that the job won't fail

.github/workflows/PR_summary.yml

@@ -121,7 +121,7 @@ jobs:
         techDebtVar="$(./scripts/technical-debt-metrics.sh pr_summary)"
 
         # store in a file, to avoid "long arguments" error.
-        printf '%s [%s](%s)%s\n\n%s\n\n---\n\n%s\n\n---\n\n%s\n' "${title}" "$(git rev-parse --short HEAD)" "${hashURL}" "${high_percentages}" "${importCount}" "${declDiff}" "${techDebtVar}" > messageFile.md
+        printf '%s [%s](%s)%s\n\n%s\n\n---\n\n%s\n\n---\n\n%s\n' "${title}" "$(git rev-parse --short HEAD)" "${hashURL}" "${high_percentages}" "${importCount}" "${declDiff}" "${techDebtVar}" > please_merge_master.md
 
-        cat messageFile.md
-        ./scripts/update_PR_comment.sh messageFile.md "${title}" "${PR}"
+        cat please_merge_master.md
+        ./scripts/update_PR_comment.sh please_merge_master.md "${title}" "${PR}"

.github/workflows/bench_summary_comment.yml

@@ -33,3 +33,11 @@ jobs:
         env:
           PR:  ${{ github.event.issue.number }}
           GH_TOKEN: ${{secrets.GITHUB_TOKEN}}
+
+      - name: Remove "bench-after-CI"
+        # 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
+        run: |
+          curl --request DELETE \
+            --url https://api.github.com/repos/${{ github.repository }}/issues/${{ github.event.issue.number }}/labels/bench-after-CI \
+            --header 'authorization: Bearer ${{ secrets.GITHUB_TOKEN }}'

.github/workflows/bors.yml

@@ -349,6 +349,15 @@ jobs:
           # Only return if PR is still open
           filterOutClosed: true
 
+      - if: contains(steps.PR.outputs.pr_labels, 'bench-after-CI')
+        name: If `bench-after-CI` is present, add a `!bench` comment.
+        uses: GrantBirki/comment@v2
+        with:
+          token: ${{ secrets.AUTO_MERGE_TOKEN }}
+          issue-number: ${{ steps.PR.outputs.number }}
+          body: |
+            !bench
+
       - id: remove_labels
         name: Remove "awaiting-CI"
         # we use curl rather than octokit/request-action so that the job won't fail

.github/workflows/build.yml

@@ -356,6 +356,15 @@ jobs:
           # Only return if PR is still open
           filterOutClosed: true
 
+      - if: contains(steps.PR.outputs.pr_labels, 'bench-after-CI')
+        name: If `bench-after-CI` is present, add a `!bench` comment.
+        uses: GrantBirki/comment@v2
+        with:
+          token: ${{ secrets.AUTO_MERGE_TOKEN }}
+          issue-number: ${{ steps.PR.outputs.number }}
+          body: |
+            !bench
+
       - id: remove_labels
         name: Remove "awaiting-CI"
         # we use curl rather than octokit/request-action so that the job won't fail

.github/workflows/build_fork.yml

@@ -353,6 +353,15 @@ jobs:
           # Only return if PR is still open
           filterOutClosed: true
 
+      - if: contains(steps.PR.outputs.pr_labels, 'bench-after-CI')
+        name: If `bench-after-CI` is present, add a `!bench` comment.
+        uses: GrantBirki/comment@v2
+        with:
+          token: ${{ secrets.AUTO_MERGE_TOKEN }}
+          issue-number: ${{ steps.PR.outputs.number }}
+          body: |
+            !bench
+
       - id: remove_labels
         name: Remove "awaiting-CI"
         # we use curl rather than octokit/request-action so that the job won't fail

.github/workflows/daily.yml

@@ -37,6 +37,10 @@ jobs:
           ./elan-init -y --default-toolchain none
           echo "$HOME/.elan/bin" >> "${GITHUB_PATH}"
 
+      # Checkout repository, so that we can fetch tags to decide which branch we want.
+      - name: Checkout branch or tag
+        uses: actions/checkout@v4
+
       - name: Fetch latest tags (if nightly)
         if: matrix.branch_type == 'nightly'
         run: |
@@ -52,6 +56,7 @@ jobs:
             echo "BRANCH_REF=${{ env.LATEST_TAG }}" >> "$GITHUB_ENV"
           fi
 
+      # Checkout the branch or tag we want to test.
       - name: Checkout branch or tag
         uses: actions/checkout@v4
         with:

.github/workflows/maintainer_bors.yml

@@ -34,14 +34,19 @@ jobs:
           printf '%s' "${COMMENT}" | hexdump -cC
           printf 'Comment:"%s"\n' "${COMMENT}"
           m_or_d="$(printf '%s' "${COMMENT}" |
-            sed -n 's=^bors  *\(merge\|r+\) *$=ready-to-merge=p; s=^bors  *d.*=delegated=p' | head -1)"
+            sed -n 's=^bors  *\(merge\|r+\) *$=ready-to-merge=p; s=^bors  *\(delegate\|d+\|d\=\).*=delegated=p' | head -1)"
+
+          remove_labels="$(printf '%s' "${COMMENT}" |
+            sed -n 's=^bors  *\(merge\|r\|d\)- *$=remove-labels=p' | head -1)"
 
           printf $'"bors delegate" or "bors merge" found? \'%s\'\n' "${m_or_d}"
+          printf $'"bors r-" or "bors d-" found? \'%s\'\n' "${remove_labels}"
           printf $'AUTHOR: \'%s\'\n' "${AUTHOR}"
           printf $'PR_NUMBER: \'%s\'\n' "${{ github.event.issue.number }}${{ github.event.pull_request.number }}"
           printf $'%s' "${{ github.event.issue.number }}${{ github.event.pull_request.number }}" | hexdump -cC
 
           printf $'mOrD=%s\n' "${m_or_d}" >> "${GITHUB_OUTPUT}"
+          printf $'removeLabels=%s\n' "${remove_labels}" >> "${GITHUB_OUTPUT}"
           if [ "${AUTHOR}" == 'leanprover-community-mathlib4-bot' ] ||
              [ "${AUTHOR}" == 'leanprover-community-bot-assistant' ]
           then
@@ -54,7 +59,7 @@ jobs:
 
       - name: Check whether user is a mathlib admin
         id: user_permission
-        if: ${{ ! steps.merge_or_delegate.outputs.mOrD == '' }}
+        if: ${{ ! steps.merge_or_delegate.outputs.mOrD == '' || ! steps.merge_or_delegate.outputs.removeLabels == '' }}
         uses: actions-cool/check-user-permission@v2
         with:
           require: 'admin'
@@ -87,6 +92,18 @@ jobs:
               --header 'authorization: Bearer ${{ secrets.TRIAGE_TOKEN }}'
           done
 
+      - name: On bors r/d-, remove ready-to-merge or delegated label
+        if: ${{ ! steps.merge_or_delegate.outputs.removeLabels == '' &&
+          steps.user_permission.outputs.require-result == 'true' }}
+        # 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
+        run: |
+          for label in ready-to-merge delegated; do
+            curl --request DELETE \
+              --url "https://api.github.com/repos/${{ github.repository }}/issues/${{ github.event.issue.number }}${{ github.event.pull_request.number }}/labels/${label}" \
+              --header 'authorization: Bearer ${{ secrets.TRIAGE_TOKEN }}'
+          done
+
       - name: Set up Python
         if: ${{ ! steps.merge_or_delegate.outputs.mOrD == '' &&
           ( steps.user_permission.outputs.require-result == 'true' ||

Archive/Arithcc.lean

@@ -191,12 +191,12 @@ protected theorem StateEqRs.refl (t : Register) (ζ : State) : ζ ≃[t]/ac ζ :
 @[symm]
 protected theorem StateEqRs.symm {t : Register} (ζ₁ ζ₂ : State) :
     ζ₁ ≃[t]/ac ζ₂ → ζ₂ ≃[t]/ac ζ₁ := by
-  simp_all [StateEqRs] -- Porting note: was `finish [StateEqRs]`
+  simp_all [StateEqRs]
 
 @[trans]
 protected theorem StateEqRs.trans {t : Register} (ζ₁ ζ₂ ζ₃ : State) :
     ζ₁ ≃[t]/ac ζ₂ → ζ₂ ≃[t]/ac ζ₃ → ζ₁ ≃[t]/ac ζ₃ := by
-  simp_all [StateEqRs] -- Porting note: was `finish [StateEqRs]`
+  simp_all [StateEqRs]
 
 /-- Machine states ζ₁ and ζ₂ are equal except for registers {x | x ≥ t}. -/
 def StateEq (t : Register) (ζ₁ ζ₂ : State) : Prop :=

Archive/Examples/PropEncodable.lean

@@ -34,13 +34,6 @@ inductive PropForm (α : Type*)
   | and : PropForm α → PropForm α → PropForm α
   | or : PropForm α → PropForm α → PropForm α
 
-/-!
-The next three functions make it easier to construct functions from a small
-`Fin`.
--/
-
--- Porting note: using `![_, _]` notation instead
-
 namespace PropForm
 
 private def Constructors (α : Type*) :=

Archive/Imo/Imo1975Q1.lean

@@ -3,7 +3,7 @@ Copyright (c) 2022 Mantas Bakšys. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mantas Bakšys
 -/
-import Mathlib.Algebra.BigOperators.Ring
+import Mathlib.Algebra.BigOperators.Ring.Finset
 import Mathlib.Algebra.Order.Rearrangement
 import Mathlib.Data.Real.Basic
 import Mathlib.Order.Interval.Finset.Nat

Archive/Imo/Imo1982Q1.lean

@@ -64,11 +64,9 @@ lemma f₁ : f 1 = 0 := by
   · cases Nat.succ_ne_zero _ h₂.symm
 
 lemma f₃ : f 3 = 1 := by
-    have h : f 3 = f 2 + f 1 ∨ f 3  = f 2 + f 1 + 1 := by apply hf.rel 2 1
-    rw [hf.f₁, hf.f₂, add_zero, zero_add] at h
-    have not_left : ¬ f 3 = 0 := by apply ne_of_gt hf.hf₃
-    rw [or_iff_right (not_left)] at h
-    exact h
+  have h : f 3 = f 2 + f 1 ∨ f 3 = f 2 + f 1 + 1 := hf.rel 2 1
+  rw [hf.f₁, hf.f₂, add_zero, zero_add] at h
+  exact h.resolve_left hf.hf₃.ne'
 
 lemma superadditive {m n : ℕ+} : f m + f n ≤ f (m + n) := by
   have h := hf.rel m n
@@ -98,7 +96,7 @@ lemma part_1 : 660 ≤ f (1980) := by
 
 lemma part_2 : f 1980 ≤ 660 := by
   have h : 5 * f 1980 + 33 * f 3 ≤ 5 * 660 + 33 := by
-    calc (5 : ℕ+) * f 1980 + (33 : ℕ+) * f 3 ≤  f (5 * 1980 + 33 * 3) := by apply hf.superlinear
+    calc (5 : ℕ+) * f 1980 + (33 : ℕ+) * f 3 ≤ f (5 * 1980 + 33 * 3) := by apply hf.superlinear
     _ = f 9999 := by rfl
     _ = 5 * 660 + 33 := by rw [hf.f_9999]
   rw [hf.f₃, mul_one] at h

Archive/Imo/Imo1998Q2.lean

@@ -211,10 +211,7 @@ end
 theorem clear_denominators {a b k : ℕ} (ha : 0 < a) (hb : 0 < b) :
     (b - 1 : ℚ) / (2 * b) ≤ k / a ↔ ((b : ℕ) - 1) * a ≤ k * (2 * b) := by
   rw [div_le_div_iff₀]
-  -- Porting note: proof used to finish with `<;> norm_cast <;> simp [ha, hb]`
-  · convert Nat.cast_le (α := ℚ)
-    · aesop
-    · norm_cast
+  on_goal 1 => convert Nat.cast_le (α := ℚ)
   all_goals simp [ha, hb]
 
 end

Archive/Imo/Imo2013Q1.lean

@@ -67,8 +67,7 @@ theorem imo2013_q1 (n : ℕ+) (k : ℕ) :
         field_simp
         ring
       _ = (1 + 1 / (2 * t + 2 ^ pk.succ)) * (1 + (2 ^ pk - 1) / t_succ) := by
-        -- Porting note: used to work with `norm_cast`
-        simp only [t_succ, PNat.mk_coe, Nat.cast_add, Nat.cast_one, mul_eq_mul_right_iff, pow_succ']
+        simp [pow_succ', PNat.mk_coe, t_succ]
       _ = (∏ i ∈ Finset.range pk, (1 + 1 / (m i : ℚ))) * (1 + 1 / m pk) := by
         rw [prod_lemma, hpm, ← hmpk, mul_comm]
       _ = ∏ i ∈ Finset.range pk.succ, (1 + 1 / (m i : ℚ)) := by rw [← Finset.prod_range_succ _ pk]

Archive/Imo/Imo2024Q1.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Myers
 -/
 import Mathlib.Algebra.BigOperators.Intervals
-import Mathlib.Algebra.BigOperators.Ring
+import Mathlib.Algebra.BigOperators.Ring.Finset
 import Mathlib.Algebra.Order.ToIntervalMod
 import Mathlib.Data.Real.Archimedean
 import Mathlib.Tactic.Peel

Archive/Imo/Imo2024Q5.lean

@@ -5,6 +5,7 @@ Authors: Joseph Myers
 -/
 import Mathlib.Data.Fin.VecNotation
 import Mathlib.Data.List.ChainOfFn
+import Mathlib.Data.List.TakeWhile
 import Mathlib.Data.Nat.Dist
 import Mathlib.Order.Fin.Basic
 import Mathlib.Tactic.IntervalCases

Archive/MiuLanguage/Basic.lean

@@ -139,18 +139,17 @@ instance stringCoeMiustr : Coe String Miustr :=
 -/
 
 
--- Porting note: Added a lot of `↑` to coerce `List MiuAtom` to `Miustr`
 /--
 The inductive type `Derivable` has five constructors. The nonrecursive constructor `mk` corresponds
 to Hofstadter's axiom that `"MI"` is derivable. Each of the constructors `r1`, `r2`, `r3`, `r4`
 corresponds to the one of Hofstadter's rules of inference.
 -/
 inductive Derivable : Miustr → Prop
   | mk : Derivable "MI"
-  | r1 {x} : Derivable (x ++ ↑[I]) → Derivable (x ++ ↑[I, U])
+  | r1 {x} : Derivable (x ++ [I]) → Derivable (x ++ [I, U])
   | r2 {x} : Derivable (M :: x) → Derivable (M :: x ++ x)
-  | r3 {x y} : Derivable (x ++ ↑[I, I, I] ++ y) → Derivable (x ++ ↑(U :: y))
-  | r4 {x y} : Derivable (x ++ ↑[U, U] ++ y) → Derivable (x ++ y)
+  | r3 {x y} : Derivable (x ++ [I, I, I] ++ y) → Derivable (x ++ (U :: y))
+  | r4 {x y} : Derivable (x ++ [U, U] ++ y) → Derivable (x ++ y)
 
 /-!
 ### Rule usage examples

Archive/MiuLanguage/DecisionNec.lean

@@ -120,32 +120,27 @@ We'll show, for each `i` from 1 to 4, that if `en` follows by Rule `i` from `st`
 -/
 
 
-theorem goodm_of_rule1 (xs : Miustr) (h₁ : Derivable (xs ++ ↑[I])) (h₂ : Goodm (xs ++ ↑[I])) :
-    Goodm (xs ++ ↑[I, U]) := by
+theorem goodm_of_rule1 (xs : Miustr) (h₁ : Derivable (xs ++ [I])) (h₂ : Goodm (xs ++ [I])) :
+    Goodm (xs ++ [I, U]) := by
   cases' h₂ with mhead nmtail
-  have : xs ≠ nil := by rintro rfl; contradiction
   constructor
-  · -- Porting note: Original proof was `rwa [head_append] at * <;> exact this`.
-    -- However, there is no `headI_append`
-    cases xs
-    · contradiction
-    exact mhead
-  · change ¬M ∈ tail (xs ++ ↑([I] ++ [U]))
+  · cases xs <;> simp_all
+  · change ¬M ∈ tail (xs ++ ([I] ++ [U]))
     rw [← append_assoc, tail_append_singleton_of_ne_nil]
     · simp_rw [mem_append, mem_singleton, reduceCtorEq, or_false]; exact nmtail
-    · exact append_ne_nil_of_left_ne_nil this _
+    · simp
 
 theorem goodm_of_rule2 (xs : Miustr) (_ : Derivable (M :: xs)) (h₂ : Goodm (M :: xs)) :
-    Goodm (↑(M :: xs) ++ xs) := by
+    Goodm ((M :: xs) ++ xs) := by
   constructor
   · rfl
   · cases' h₂ with mhead mtail
     contrapose! mtail
     rw [cons_append] at mtail
     exact or_self_iff.mp (mem_append.mp mtail)
 
-theorem goodm_of_rule3 (as bs : Miustr) (h₁ : Derivable (as ++ ↑[I, I, I] ++ bs))
-    (h₂ : Goodm (as ++ ↑[I, I, I] ++ bs)) : Goodm (as ++ ↑(U :: bs)) := by
+theorem goodm_of_rule3 (as bs : Miustr) (h₁ : Derivable (as ++ [I, I, I] ++ bs))
+    (h₂ : Goodm (as ++ [I, I, I] ++ bs)) : Goodm (as ++ (U :: bs)) := by
   cases' h₂ with mhead nmtail
   have k : as ≠ nil := by rintro rfl; contradiction
   constructor
@@ -162,8 +157,8 @@ The proof of the next lemma is identical, on the tactic level, to the previous p
 -/
 
 
-theorem goodm_of_rule4 (as bs : Miustr) (h₁ : Derivable (as ++ ↑[U, U] ++ bs))
-    (h₂ : Goodm (as ++ ↑[U, U] ++ bs)) : Goodm (as ++ bs) := by
+theorem goodm_of_rule4 (as bs : Miustr) (h₁ : Derivable (as ++ [U, U] ++ bs))
+    (h₂ : Goodm (as ++ [U, U] ++ bs)) : Goodm (as ++ bs) := by
   cases' h₂ with mhead nmtail
   have k : as ≠ nil := by rintro rfl; contradiction
   constructor

Archive/OxfordInvariants/Summer2021/Week3P1.lean

@@ -3,7 +3,7 @@ Copyright (c) 2021 Yaël Dillies, Bhavik Mehta. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies, Bhavik Mehta
 -/
-import Mathlib.Algebra.BigOperators.Ring
+import Mathlib.Algebra.BigOperators.Ring.Finset
 import Mathlib.Algebra.Order.BigOperators.Group.Finset
 import Mathlib.Data.Nat.Cast.Field
 import Mathlib.Data.Nat.Cast.Order.Field