Merge branch 'master' into IsTwoSided_finite

.github/build.in.yml

@@ -322,6 +322,15 @@ jobs:
           cp ../lean-toolchain .
           lake build
 
+      - name: Add the "awaiting-CI" label
+        if: always()
+        # 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 ADD \
+            --url https://api.github.com/repos/${{ github.repository }}/issues/${{ github.event.issue.number }}/labels/awaiting-CI \
+            --header 'authorization: Bearer ${{ secrets.GITHUB_TOKEN }}'
+
   final:
     name: Post-CI jobJOB_NAME
     if: github.repository MAIN_OR_FORK 'leanprover-community/mathlib4'

.github/workflows/bors.yml

@@ -332,6 +332,15 @@ jobs:
           cp ../lean-toolchain .
           lake build
 
+      - name: Add the "awaiting-CI" label
+        if: always()
+        # 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 ADD \
+            --url https://api.github.com/repos/${{ github.repository }}/issues/${{ github.event.issue.number }}/labels/awaiting-CI \
+            --header 'authorization: Bearer ${{ secrets.GITHUB_TOKEN }}'
+
   final:
     name: Post-CI job
     if: github.repository == 'leanprover-community/mathlib4'

.github/workflows/build.yml

@@ -339,6 +339,15 @@ jobs:
           cp ../lean-toolchain .
           lake build
 
+      - name: Add the "awaiting-CI" label
+        if: always()
+        # 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 ADD \
+            --url https://api.github.com/repos/${{ github.repository }}/issues/${{ github.event.issue.number }}/labels/awaiting-CI \
+            --header 'authorization: Bearer ${{ secrets.GITHUB_TOKEN }}'
+
   final:
     name: Post-CI job
     if: github.repository == 'leanprover-community/mathlib4'

.github/workflows/build_fork.yml

@@ -336,6 +336,15 @@ jobs:
           cp ../lean-toolchain .
           lake build
 
+      - name: Add the "awaiting-CI" label
+        if: always()
+        # 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 ADD \
+            --url https://api.github.com/repos/${{ github.repository }}/issues/${{ github.event.issue.number }}/labels/awaiting-CI \
+            --header 'authorization: Bearer ${{ secrets.GITHUB_TOKEN }}'
+
   final:
     name: Post-CI job (fork)
     if: github.repository != 'leanprover-community/mathlib4'

.github/workflows/stale.yml

@@ -18,8 +18,8 @@ jobs:
           close-pr-message: 'Comment on the staled PRs while closed'
           days-before-stale: 60
           days-before-close: 120
-          # search string from the Zulip #queue link at https://bit.ly/4eo6brN
-          # "is:open is:pr -is:draft base:master sort:updated-asc status:success -label:blocked-by-other-PR -label:merge-conflict -label:awaiting-CI -label:WIP -label:awaiting-author -label:delegated -label:auto-merge-after-CI -label:ready-to-merge -label:please-adopt -label:help-wanted -label:awaiting-zulip"
+          # search string from the Zulip #queue link at https://leanprover-community.github.io/queue-redirect
+          # "is:open is:pr -is:draft base:master sort:updated-asc status:success -label:blocked-by-other-PR -label:blocked-by-batt-PR -label:blocked-by-core-PR -label:blocked-by-qq-PR -label:merge-conflict -label:awaiting-author -label:awaiting-CI -label:awaiting-zulip -label:WIP -label:delegated -label:auto-merge-after-CI -label:ready-to-merge -label:please-adopt -label:help-wanted"
           # We want PRs _not_ on the queue, so we keep "is:pr -is:draft base:master" (is:open is added by the action by default) as a prefix for all queries and then negate the rest of the params in separate queries to simulate boolean OR (see https://github.com/actions/stale/pull/1145)
           # except for label:auto-merge-after-CI and label:ready-to-merge which presumably will be noticed before they go stale
-          only-matching-filter: '[ "is:pr -is:draft base:master -status:success", "is:pr -is:draft base:master label:blocked-by-other-PR", "is:pr -is:draft base:master label:merge-conflict", "is:pr -is:draft base:master label:awaiting-CI", "is:pr -is:draft base:master label:WIP", "is:pr -is:draft base:master label:awaiting-author", "is:pr -is:draft base:master label:delegated", "is:pr -is:draft base:master label:please-adopt", "is:pr -is:draft base:master label:help-wanted", "is:pr -is:draft base:master label:awaiting-zulip" ]'
+          only-matching-filter: '[ "is:pr -is:draft base:master -status:success", "is:pr -is:draft base:master label:blocked-by-other-PR", "is:pr -is:draft base:master label:blocked-by-batt-PR", "is:pr -is:draft base:master label:blocked-by-core-PR", "is:pr -is:draft base:master label:blocked-by-qq-PR", "is:pr -is:draft base:master label:merge-conflict", "is:pr -is:draft base:master label:awaiting-author", "is:pr -is:draft base:master label:awaiting-CI", "is:pr -is:draft base:master label:awaiting-zulip", "is:pr -is:draft base:master label:WIP", "is:pr -is:draft base:master label:delegated", "is:pr -is:draft base:master label:please-adopt", "is:pr -is:draft base:master label:help-wanted",  ]'

Archive/Arithcc.lean

@@ -3,7 +3,7 @@ Copyright (c) 2020 Xi Wang. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Xi Wang
 -/
-import Mathlib.Data.Nat.Defs
+import Mathlib.Data.Nat.Basic
 import Mathlib.Order.Basic
 import Mathlib.Tactic.Common
 
@@ -243,7 +243,7 @@ theorem stateEq_implies_write_eq {t : Register} {ζ₁ ζ₂ : State} (h : ζ₁
   intro r hr
   have hr : r ≤ t := Register.le_of_lt_succ hr
   rcases lt_or_eq_of_le hr with hr | hr
-  · cases' h with _ h
+  · obtain ⟨_, h⟩ := h
     specialize h r hr
     simp_all
   · simp_all
@@ -262,7 +262,7 @@ theorem write_eq_implies_stateEq {t : Register} {v : Word} {ζ₁ ζ₂ : State}
   simp [StateEq, StateEqRs] at *
   constructor; · exact h.1
   intro r hr
-  cases' h with _ h
+  obtain ⟨_, h⟩ := h
   specialize h r (lt_trans hr (Register.lt_succ_self _))
   rwa [if_neg (ne_of_lt hr)] at h
 
@@ -320,7 +320,7 @@ theorem compiler_correctness
     have hζ₃_ν₂ : ζ₃.ac = ν₂ := by simp_all [StateEq]
     have hζ₃_ν₁ : read t ζ₃ = ν₁ := by
       simp [StateEq, StateEqRs] at hζ₃ ⊢
-      cases' hζ₃ with _ hζ₃
+      obtain ⟨_, hζ₃⟩ := hζ₃
       specialize hζ₃ t (Register.lt_succ_self _)
       simp_all
     have hζ₄ : ζ₄ ≃[t + 1] { write t ν₁ η with ac := ν } := calc

Archive/Imo/Imo1962Q1.lean

@@ -37,7 +37,7 @@ abbrev ProblemPredicate' (c n : ℕ) : Prop :=
 
 lemma without_digits {n : ℕ} (hn : ProblemPredicate n) : ∃ c : ℕ, ProblemPredicate' c n := by
   use n / 10
-  cases' n with n
+  rcases n with - | n
   · have hpp : ¬ProblemPredicate 0 := by norm_num [ProblemPredicate]
     contradiction
   · rw [ProblemPredicate, digits_def' (by decide : 2 ≤ 10) n.succ_pos, List.headI, List.tail_cons,

Archive/Imo/Imo1987Q1.lean

@@ -5,7 +5,6 @@ Authors: Yury Kudryashov
 -/
 import Mathlib.Data.Fintype.BigOperators
 import Mathlib.Data.Fintype.Perm
-import Mathlib.Data.Fintype.Prod
 import Mathlib.Dynamics.FixedPoints.Basic
 
 /-!
@@ -96,6 +95,6 @@ theorem main₀ (n : ℕ) : ∑ k ∈ range (n + 1), k * p (Fin n) k = n * (n -
 
 /-- Main statement for permutations of `Fin n`. -/
 theorem main {n : ℕ} (hn : 1 ≤ n) : ∑ k ∈ range (n + 1), k * p (Fin n) k = n ! := by
-  rw [main₀, Nat.mul_factorial_pred (zero_lt_one.trans_le hn)]
+  rw [main₀, Nat.mul_factorial_pred hn]
 
 end Imo1987Q1

Archive/Imo/Imo1988Q6.lean

@@ -158,7 +158,7 @@ theorem constant_descent_vieta_jumping (x y : ℕ) {claim : Prop} {H : ℕ → 
   rw [mul_comm] at hV₂
   have Hc := H_desc hmx mx_lt_my h_base hHm c h_root hV₁ hV₂
   -- This means that we may assume that c ≥ 0 and c ≤ m_x.
-  cases' Hc with c_nonneg c_lt
+  obtain ⟨c_nonneg, c_lt⟩ := Hc
   -- In other words, c is a natural number.
   lift c to ℕ using c_nonneg
   -- Recall that we are trying find a point (a,b) such that b ∈ S and b < m.

Archive/Imo/Imo1994Q1.lean

@@ -32,7 +32,7 @@ open Finset
 namespace Imo1994Q1
 
 theorem tedious (m : ℕ) (k : Fin (m + 1)) : m - ((m + 1 - ↑k) + m) % (m + 1) = ↑k := by
-  cases' k with k hk
+  obtain ⟨k, hk⟩ := k
   rw [Nat.lt_succ_iff, le_iff_exists_add] at hk
   rcases hk with ⟨c, rfl⟩
   have : (k + c + 1 - k) + (k + c) = c + (k + c + 1) := by omega
@@ -83,7 +83,7 @@ theorem imo1994_q1 (n : ℕ) (m : ℕ) (A : Finset ℕ) (hm : #A = m + 1)
     have h1 : a i + a (Fin.last m - k) ≤ n := by unfold a; linarith only [h, a.monotone hi]
     have h2 : a i + a (Fin.last m - k) ∈ A := hadd _ (ha _) _ (ha _) h1
     rw [← mem_coe, ← range_orderEmbOfFin A hm, Set.mem_range] at h2
-    cases' h2 with j hj
+    obtain ⟨j, hj⟩ := h2
     refine ⟨j, ⟨?_, Fin.le_last j⟩, hj⟩
     rw [← a.strictMono.lt_iff_lt, hj]
     simpa using (hrange (a i) (ha i)).1

Archive/Imo/Imo1998Q2.lean

@@ -234,6 +234,6 @@ theorem imo1998_q2 [Fintype J] [Fintype C] (a b k : ℕ) (hC : Fintype.card C =
     simp only [mul_comm, add_mul, one_mul, nonpos_iff_eq_zero, add_tsub_cancel_right]; ring
   have hr : 2 * z * z * a = 2 * z * a * z := by ring
   rw [hl, hr] at h
-  cases' z with z
+  rcases z with - | z
   · simp
   · exact le_of_mul_le_mul_right h z.succ_pos

Archive/Imo/Imo2006Q3.lean

@@ -80,7 +80,7 @@ theorem subst_proof₁ (x y z s : ℝ) (hxyz : x + y + z = 0) :
   wlog h' : 0 ≤ x * y generalizing x y z; swap
   · rw [div_mul_eq_mul_div, le_div_iff₀' zero_lt_32]
     exact subst_wlog h' hxyz
-  cases' (mul_nonneg_of_three x y z).resolve_left h' with h h
+  rcases (mul_nonneg_of_three x y z).resolve_left h' with h | h
   · convert this y z x _ h using 2 <;> linarith
   · convert this z x y _ h using 2 <;> linarith
 

Archive/Imo/Imo2006Q5.lean

@@ -53,8 +53,8 @@ theorem Int.natAbs_eq_of_chain_dvd {l : Cycle ℤ} {x y : ℤ} (hl : l.Chain (·
 theorem Int.add_eq_add_of_natAbs_eq_of_natAbs_eq {a b c d : ℤ} (hne : a ≠ b)
     (h₁ : (c - a).natAbs = (d - b).natAbs) (h₂ : (c - b).natAbs = (d - a).natAbs) :
     a + b = c + d := by
-  cases' Int.natAbs_eq_natAbs_iff.1 h₁ with h₁ h₁
-  · cases' Int.natAbs_eq_natAbs_iff.1 h₂ with h₂ h₂
+  rcases Int.natAbs_eq_natAbs_iff.1 h₁ with h₁ | h₁
+  · rcases Int.natAbs_eq_natAbs_iff.1 h₂ with h₂ | h₂
     · exact (hne <| by linarith).elim
     · linarith
   · linarith
@@ -108,9 +108,9 @@ theorem Polynomial.isPeriodicPt_eval_two {P : Polynomial ℤ} {t : ℤ}
   · -- We take two nonequal consecutive entries.
     rw [Cycle.chain_map, periodicOrbit_chain' _ ht] at HC'
     push_neg at HC'
-    cases' HC' with n hn
+    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).
-    cases' Int.natAbs_eq_natAbs_iff.1 (Habs n n.succ) with hn' hn'
+    rcases Int.natAbs_eq_natAbs_iff.1 (Habs n n.succ) with hn' | hn'
     · apply (hn _).elim
       convert hn' <;> simp only [Function.iterate_succ_apply']
     -- We deduce P^{k + 2}(t) = P^k(t) and hence P(P(t)) = t.

Archive/Imo/Imo2008Q3.lean

@@ -48,7 +48,7 @@ theorem p_lemma (p : ℕ) (hpp : Nat.Prime p) (hp_mod_4_eq_1 : p ≡ 1 [MOD 4])
   have hnat₃ : p ≥ 2 * n := by omega
   set k : ℕ := p - 2 * n with hnat₄
   have hnat₅ : p ∣ k ^ 2 + 4 := by
-    cases' hnat₁ with x hx
+    obtain ⟨x, hx⟩ := hnat₁
     have : (p : ℤ) ∣ (k : ℤ) ^ 2 + 4 := by
       use (p : ℤ) - 4 * n + 4 * x
       have hcast₁ : (k : ℤ) = p - 2 * n := by assumption_mod_cast

Archive/Imo/Imo2008Q4.lean

@@ -77,7 +77,7 @@ theorem imo2008_q4 (f : ℝ → ℝ) (H₁ : ∀ x > 0, f x > 0) :
   rw [hfa₂, hfb₂] at H₂
   have h2ab_ne_0 : 2 * (a * b) ≠ 0 := by positivity
   specialize h₃ (a * b) hab
-  cases' h₃ with hab₁ hab₂
+  rcases h₃ with hab₁ | hab₂
   -- f(ab) = ab → b^4 = 1 → b = 1 → f(b) = b → false
   · rw [hab₁, div_left_inj' h2ab_ne_0] at H₂
     field_simp at H₂

Archive/Imo/Imo2013Q1.lean

@@ -50,7 +50,7 @@ theorem imo2013_q1 (n : ℕ+) (k : ℕ) :
   obtain ⟨t, ht : ↑n = t + t⟩ | ⟨t, ht : ↑n = 2 * t + 1⟩ := (n : ℕ).even_or_odd
   · -- even case
     rw [← two_mul] at ht
-    cases' t with t
+    rcases t with - | t
     -- Eliminate the zero case to simplify later calculations.
     · exfalso; rw [Nat.mul_zero] at ht; exact PNat.ne_zero n ht
     -- Now we have ht : ↑n = 2 * (t + 1).

Archive/Imo/Imo2013Q5.lean

@@ -115,7 +115,7 @@ theorem pow_f_le_f_pow {f : ℚ → ℝ} {n : ℕ} (hn : 0 < n) {x : ℚ} (hx :
     f (x ^ n) ≤ f x ^ n := by
   induction' n with pn hpn
   · exfalso; exact Nat.lt_asymm hn hn
-  cases' pn with pn
+  rcases pn with - | pn
   · norm_num
   have hpn' := hpn pn.succ_pos
   rw [pow_succ x (pn + 1), pow_succ (f x) (pn + 1)]
@@ -167,7 +167,7 @@ theorem imo2013_q5 (f : ℚ → ℝ) (H1 : ∀ x y, 0 < x → 0 < y → f (x * y
   obtain ⟨a, ha1, hae⟩ := H_fixed_point
   have H3 : ∀ x : ℚ, 0 < x → ∀ n : ℕ, 0 < n → ↑n * f x ≤ f (n * x) := by
     intro x hx n hn
-    cases' n with n
+    rcases n with - | n
     · exact (lt_irrefl 0 hn).elim
     induction' n with pn hpn
     · norm_num
@@ -208,9 +208,9 @@ theorem imo2013_q5 (f : ℚ → ℝ) (H1 : ∀ x y, 0 < x → 0 < y → f (x * y
   have h_f_commutes_with_pos_nat_mul : ∀ n : ℕ, 0 < n → ∀ x : ℚ, 0 < x → f (n * x) = n * f x := by
     intro n hn x hx
     have h2 : f (n * x) ≤ n * f x := by
-      cases' n with n
+      rcases n with - | n
       · exfalso; exact Nat.lt_asymm hn hn
-      cases' n with n
+      rcases n with - | n
       · norm_num
       have hfneq : f n.succ.succ = n.succ.succ := by
         have :=

Archive/Imo/Imo2019Q1.lean

@@ -39,7 +39,7 @@ theorem imo2019_q1 (f : ℤ → ℤ) :
   -- Hence, `f` is an affine map, `f b = f 0 + m * b`
   obtain ⟨c, H⟩ : ∃ c, ∀ b, f b = c + m * b := by
     refine ⟨f 0, fun b => ?_⟩
-    induction' b using Int.induction_on with b ihb b ihb
+    induction' b with b ihb b ihb
     · simp
     · simp [H, ihb, mul_add, add_assoc]
     · rw [← sub_eq_of_eq_add (H _)]

Archive/Imo/Imo2021Q1.lean

@@ -126,5 +126,5 @@ theorem imo2021_q1 :
   rcases hC with ⟨a, ha, b, hb, hab⟩
   simp only [Finset.subset_iff, Finset.mem_inter] at hCA
   -- Now we split into the two cases C ⊆ [n, 2n] \ A and C ⊆ A, which can be dealt with identically.
-  cases' hCA with hCA hCA <;> [right; left] <;>
+  rcases hCA with hCA | hCA <;> [right; left] <;>
     exact ⟨a, (hCA ha).2, b, (hCA hb).2, hab, h₁ a (hCA ha).1 b (hCA hb).1 hab⟩

Archive/Imo/Imo2024Q3.lean

@@ -3,6 +3,7 @@ Copyright (c) 2024 Joseph Myers. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Myers
 -/
+import Mathlib.Data.Fintype.Pigeonhole
 import Mathlib.Data.Nat.Nth
 
 /-!
@@ -30,7 +31,7 @@ open scoped Finset
 namespace Imo2024Q3
 
 /-- The condition of the problem. Following usual Lean conventions, this is expressed with
-indices starting from 0, rather than from 1 as in the informal statment (but `N` remains as the
+indices starting from 0, rather than from 1 as in the informal statement (but `N` remains as the
 index of the last term for which `a n` is not defined in terms of previous terms). -/
 def Condition (a : ℕ → ℕ) (N : ℕ) : Prop :=
   (∀ i, 0 < a i) ∧ ∀ n, N < n → a n = #{i ∈ Finset.range n | a i = a (n - 1)}

Archive/MiuLanguage/DecisionNec.lean

@@ -53,9 +53,9 @@ example : CountEquivOrEquivTwoMulMod3 "IUIM" "MI" :=
 -/
 theorem mod3_eq_1_or_mod3_eq_2 {a b : ℕ} (h1 : a % 3 = 1 ∨ a % 3 = 2)
     (h2 : b % 3 = a % 3 ∨ b % 3 = 2 * a % 3) : b % 3 = 1 ∨ b % 3 = 2 := by
-  cases' h2 with h2 h2
+  rcases h2 with h2 | h2
   · rw [h2]; exact h1
-  · cases' h1 with h1 h1
+  · rcases h1 with h1 | h1
     · right; simp [h2, mul_mod, h1, Nat.succ_lt_succ]
     · left; simp only [h2, mul_mod, h1, mod_mod]
 
@@ -122,7 +122,7 @@ 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
-  cases' h₂ with mhead nmtail
+  obtain ⟨mhead, nmtail⟩ := h₂
   constructor
   · cases xs <;> simp_all
   · change ¬M ∈ tail (xs ++ ([I] ++ [U]))
@@ -134,14 +134,14 @@ theorem goodm_of_rule2 (xs : Miustr) (_ : Derivable (M :: xs)) (h₂ : Goodm (M
     Goodm ((M :: xs) ++ xs) := by
   constructor
   · rfl
-  · cases' h₂ with mhead mtail
+  · obtain ⟨mhead, mtail⟩ := h₂
     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
-  cases' h₂ with mhead nmtail
+  obtain ⟨mhead, nmtail⟩ := h₂
   have k : as ≠ nil := by rintro rfl; contradiction
   constructor
   · cases as
@@ -159,7 +159,7 @@ 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
-  cases' h₂ with mhead nmtail
+  obtain ⟨mhead, nmtail⟩ := h₂
   have k : as ≠ nil := by rintro rfl; contradiction
   constructor
   · cases as