merge nightly-testing-2023-11-04; trigger Mathlib CI for leanprover/l…

…ean4#2783

.github/workflows/bors.yml

@@ -179,7 +179,7 @@ jobs:
 
       - name: check for noisy stdout lines
         run: |
-          ! grep "stdout:" stdout.log
+          ! grep --after-context=1 "stdout:" stdout.log
 
       - name: build library_search cache
         run: lake build -KCI MathlibExtras

.github/workflows/build.yml

@@ -185,7 +185,7 @@ jobs:
 
       - name: check for noisy stdout lines
         run: |
-          ! grep "stdout:" stdout.log
+          ! grep --after-context=1 "stdout:" stdout.log
 
       - name: build library_search cache
         run: lake build -KCI MathlibExtras

.github/workflows/build.yml.in

@@ -165,7 +165,7 @@ jobs:
 
       - name: check for noisy stdout lines
         run: |
-          ! grep "stdout:" stdout.log
+          ! grep --after-context=1 "stdout:" stdout.log
 
       - name: build library_search cache
         run: lake build -KCI MathlibExtras

.github/workflows/build_fork.yml

@@ -183,7 +183,7 @@ jobs:
 
       - name: check for noisy stdout lines
         run: |
-          ! grep "stdout:" stdout.log
+          ! grep --after-context=1 "stdout:" stdout.log
 
       - name: build library_search cache
         run: lake build -KCI MathlibExtras

.github/workflows/label_new_contributor.yml

@@ -0,0 +1,45 @@
+name: Label New Contributors
+
+on:
+  pull_request:
+    types: [opened]
+
+jobs:
+  label-new-contributor:
+    runs-on: ubuntu-latest
+    permissions:
+      pull-requests: write
+
+    steps:
+    - name: Get PR author
+      id: pr-author
+      run: echo "::set-output name=author::$(jq -r .pull_request.user.login "$GITHUB_EVENT_PATH")"
+      shell: bash
+
+    - name: Check if user is new contributor
+      id: check-contributor
+      uses: actions/github-script@v5
+      with:
+        script: |
+          const { owner, repo } = context.repo
+          const author = "${{ steps.pr-author.outputs.author }}"
+          const prs = await github.rest.pulls.list({
+            owner,
+            repo,
+            state: "closed",
+            author
+          })
+          return (prs.data.length < 5)
+
+    - name: Add label if new contributor
+      if: steps.check-contributor.outputs.result == 'true'
+      uses: actions/github-script@v5
+      with:
+        script: |
+          const { owner, repo, number } = context.issue
+          await github.rest.issues.addLabels({
+            owner,
+            repo,
+            issue_number: number,
+            labels: ['new-contributor']
+          })

.github/workflows/nightly_bump_toolchain.yml

@@ -10,7 +10,7 @@ jobs:
 
     steps:
     - name: Checkout code
-      uses: actions/checkout@v2
+      uses: actions/checkout@v3
       with:
         ref: nightly-testing # checkout nightly-testing branch
         token: ${{ secrets.NIGHTLY_TESTING }}

.github/workflows/nightly_detect_failure.yml

@@ -30,9 +30,10 @@ jobs:
 
     steps:
     - name: Checkout code
-      uses: actions/checkout@v2
+      uses: actions/checkout@v3
       with:
         ref: nightly-testing # checkout nightly-testing branch
+        fetch-depth: 0 # checkout all branches so that we can push from `nightly-testing` to `nightly-testing-YYYY-MM-DD`
         token: ${{ secrets.NIGHTLY_TESTING }}
     - name: Update the nightly-testing-YYYY-MM-DD branch
       run: |

.github/workflows/nightly_merge_master.yml

@@ -12,7 +12,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Checkout repository
-        uses: actions/checkout@v2
+        uses: actions/checkout@v3
         with:
           fetch-depth: 0
           token: ${{ secrets.NIGHTLY_TESTING }}

Archive/Imo/Imo1960Q1.lean

@@ -95,7 +95,12 @@ theorem right_direction {n : ℕ} : ProblemPredicate n → SolutionPredicate n :
   have := searchUpTo_start
   iterate 82
     replace :=
-      searchUpTo_step this (by norm_num1; rfl) (by norm_num1; rfl) (by norm_num1; rfl) (by norm_num)
+      searchUpTo_step this (by norm_num1; rfl) (by norm_num1; rfl) (by norm_num1; rfl)
+        (by -- This used to be just `norm_num`, but after leanprover/lean4#2790,
+            -- that triggers a max recursion depth exception. As a workaround, we
+            -- manually rewrite with `Nat.digits_of_two_le_of_pos` first.
+            rw [Nat.digits_of_two_le_of_pos (by norm_num) (by norm_num)]
+            norm_num <;> decide)
   exact searchUpTo_end this
 #align imo1960_q1.right_direction Imo1960Q1.right_direction
 

Archive/Imo/Imo1962Q1.lean

@@ -131,7 +131,18 @@ Now we combine these cases to show that 153846 is the smallest solution.
 
 
 theorem satisfied_by_153846 : ProblemPredicate 153846 := by
-  norm_num [ProblemPredicate]
+  -- This proof used to be the single line `norm_num [ProblemPredicate]`.
+  -- After leanprover/lean4#2790, that triggers a max recursion depth exception.
+  -- As a workaround, we manually apply `Nat.digits_of_two_le_of_pos` a few times
+  -- before invoking `norm_num`.
+  unfold ProblemPredicate
+  have two_le_ten : 2 ≤ 10 := by norm_num
+  rw [Nat.digits_of_two_le_of_pos two_le_ten (by norm_num)]
+  rw [Nat.digits_of_two_le_of_pos two_le_ten (by norm_num)]
+  rw [Nat.digits_of_two_le_of_pos two_le_ten (by norm_num)]
+  rw [Nat.digits_of_two_le_of_pos two_le_ten (by norm_num)]
+  norm_num
+  decide
 #align imo1962_q1.satisfied_by_153846 Imo1962Q1.satisfied_by_153846
 
 theorem no_smaller_solutions (n : ℕ) (h1 : ProblemPredicate n) : n ≥ 153846 := by

Archive/Imo/Imo1964Q1.lean

@@ -34,7 +34,7 @@ theorem two_pow_mod_seven (n : ℕ) : 2 ^ n ≡ 2 ^ (n % 3) [MOD 7] :=
   let t := n % 3
   calc 2 ^ n = 2 ^ (3 * (n / 3) + t) := by rw [Nat.div_add_mod]
     _ = (2 ^ 3) ^ (n / 3) * 2 ^ t := by rw [pow_add, pow_mul]
-    _ ≡ 1 ^ (n / 3) * 2 ^ t [MOD 7] := by gcongr; norm_num
+    _ ≡ 1 ^ (n / 3) * 2 ^ t [MOD 7] := by gcongr; decide
     _ = 2 ^ t := by ring
 
 /-!
@@ -68,5 +68,5 @@ theorem imo1964_q1b (n : ℕ) : ¬7 ∣ 2 ^ n + 1 := by
   have H : 2 ^ t + 1 ≡ 0 [MOD 7]
   · calc 2 ^ t + 1 ≡ 2 ^ n + 1 [MOD 7 ] := by gcongr ?_ + 1; exact (two_pow_mod_seven n).symm
       _ ≡ 0 [MOD 7] := h.modEq_zero_nat
-  interval_cases t <;> norm_num at H
+  interval_cases t <;> contradiction
 #align imo1964_q1b imo1964_q1b

Archive/Imo/Imo1981Q3.lean

@@ -129,7 +129,7 @@ theorem imp_fib {n : ℕ} : ∀ m : ℕ, NatPredicate N m n → ∃ k : ℕ, m =
   obtain (rfl : 1 = n) | (h4 : 1 < n) := (succ_le_iff.mpr h2.n_pos).eq_or_lt
   · use 1
     have h5 : 1 ≤ m := succ_le_iff.mpr h2.m_pos
-    simpa [fib_one, fib_two] using (h3.antisymm h5 : m = 1)
+    simpa [fib_one, fib_two, (by decide : 1 + 1 = 2)] using (h3.antisymm h5 : m = 1)
   · obtain (rfl : m = n) | (h6 : m < n) := h3.eq_or_lt
     · exact absurd h2.eq_imp_1 (Nat.ne_of_gt h4)
     · have h7 : NatPredicate N (n - m) m := h2.reduction h4
@@ -205,5 +205,7 @@ theorem imo1981_q3 : IsGreatest (specifiedSet 1981) 3524578 := by
   have := fun h => @solution_greatest 1981 16 h 3524578
   norm_num at this
   apply this
-  norm_num [ProblemPredicate_iff]
+  · decide
+  · decide
+  · norm_num [ProblemPredicate_iff]; decide
 #align imo1981_q3 imo1981_q3

Archive/Imo/Imo2005Q4.lean

@@ -29,7 +29,7 @@ def a (n : ℕ) : ℤ :=
 theorem find_specified_factor {p : ℕ} (hp : Nat.Prime p) (hp2 : p ≠ 2) (hp3 : p ≠ 3) :
     ↑p ∣ a (p - 2) := by
   -- Since `p` is neither `2` nor `3`, it is coprime with `2`, `3`, and `6`
-  rw [Ne.def, ← Nat.prime_dvd_prime_iff_eq hp (by norm_num), ← Nat.Prime.coprime_iff_not_dvd hp]
+  rw [Ne.def, ← Nat.prime_dvd_prime_iff_eq hp (by decide), ← Nat.Prime.coprime_iff_not_dvd hp]
     at hp2 hp3
   have : Int.gcd p 6 = 1 := Nat.coprime_mul_iff_right.2 ⟨hp2, hp3⟩
   -- Nat arithmetic needed to deal with powers
@@ -71,10 +71,10 @@ theorem imo2005_q4 {k : ℕ} (hk : 0 < k) : (∀ n : ℕ, 1 ≤ n → IsCoprime
   -- For `p = 2` and `p = 3`, take `n = 1` and `n = 2`, respectively
   by_cases hp2 : p = 2
   · rw [hp2] at h
-    apply h 1 <;> norm_num
+    apply h 1 <;> decide
   by_cases hp3 : p = 3
   · rw [hp3] at h
-    apply h 2 <;> norm_num
+    apply h 2 <;> decide
   -- Otherwise, take `n = p - 2`
   refine h (p - 2) ?_ (find_specified_factor hp hp2 hp3)
   calc

Archive/Imo/Imo2019Q1.lean

@@ -27,7 +27,7 @@ theorem imo2019_q1 (f : ℤ → ℤ) :
     (∀ a b : ℤ, f (2 * a) + 2 * f b = f (f (a + b))) ↔ f = 0 ∨ ∃ c, f = fun x => 2 * x + c := by
   constructor; swap
   -- easy way: f(x)=0 and f(x)=2x+c work.
-  · rintro (rfl | ⟨c, rfl⟩) <;> intros <;> simp only [Pi.zero_apply]; ring
+  · rintro (rfl | ⟨c, rfl⟩) <;> intros <;> norm_num; ring
   -- hard way.
   intro hf
   -- functional equation

Archive/Imo/Imo2019Q2.lean

@@ -442,7 +442,7 @@ theorem not_collinear_QPA₂ : ¬Collinear ℝ ({cfg.Q, cfg.P, cfg.A₂} : Set P
   have h : Cospherical ({cfg.B, cfg.A, cfg.A₂} : Set Pt) := by
     refine' cfg.triangleABC.circumsphere.cospherical.subset _
     simp only [Set.insert_subset_iff, cfg.A_mem_circumsphere, cfg.B_mem_circumsphere,
-      cfg.A₂_mem_circumsphere, Sphere.mem_coe, Set.singleton_subset_iff]
+      cfg.A₂_mem_circumsphere, Sphere.mem_coe, Set.singleton_subset_iff, and_true]
   exact h.affineIndependent_of_ne cfg.A_ne_B.symm cfg.A₂_ne_B.symm cfg.A₂_ne_A.symm
 #align imo2019_q2.imo2019q2_cfg.not_collinear_QPA₂ Imo2019Q2.Imo2019q2Cfg.not_collinear_QPA₂
 

Archive/Imo/Imo2019Q4.lean

@@ -65,7 +65,7 @@ theorem upper_bound {k n : ℕ} (hk : k > 0)
     _ ≤ k ! := by gcongr
   clear h h2
   induction' n, hn using Nat.le_induction with n' hn' IH
-  · norm_num
+  · decide
   let A := ∑ i in range n', i
   have le_sum : ∑ i in range 6, i ≤ A
   · apply sum_le_sum_of_subset
@@ -87,8 +87,7 @@ theorem imo2019_q4 {k n : ℕ} (hk : k > 0) (hn : n > 0) :
   -- The implication `←` holds.
   constructor
   swap
-  · rintro (h | h) <;> simp [Prod.ext_iff] at h <;> rcases h with ⟨rfl, rfl⟩ <;>
-    norm_num [prod_range_succ, succ_mul]
+  · rintro (h | h) <;> simp [Prod.ext_iff] at h <;> rcases h with ⟨rfl, rfl⟩ <;> decide
   intro h
   -- We know that n < 6.
   have := Imo2019Q4.upper_bound hk h
@@ -101,9 +100,9 @@ theorem imo2019_q4 {k n : ℕ} (hk : k > 0) (hn : n > 0) :
     exact h; rw [h]; norm_num
   all_goals exfalso; norm_num [prod_range_succ] at h; norm_cast at h
   -- n = 3
-  · refine' monotone_factorial.ne_of_lt_of_lt_nat 5 _ _ _ h <;> norm_num
+  · refine' monotone_factorial.ne_of_lt_of_lt_nat 5 _ _ _ h <;> decide
   -- n = 4
-  · refine' monotone_factorial.ne_of_lt_of_lt_nat 7 _ _ _ h <;> norm_num
+  · refine' monotone_factorial.ne_of_lt_of_lt_nat 7 _ _ _ h <;> decide
   -- n = 5
-  · refine' monotone_factorial.ne_of_lt_of_lt_nat 10 _ _ _ h <;> norm_num
+  · refine' monotone_factorial.ne_of_lt_of_lt_nat 10 _ _ _ h <;> decide
 #align imo2019_q4 imo2019_q4

Archive/MiuLanguage/DecisionNec.lean

@@ -61,7 +61,7 @@ theorem mod3_eq_1_or_mod3_eq_2 {a b : ℕ} (h1 : a % 3 = 1 ∨ a % 3 = 2)
   · rw [h2]; exact h1
   · cases' h1 with h1 h1
     · right; simp [h2, mul_mod, h1, Nat.succ_lt_succ]
-    · left; simp [h2, mul_mod, h1]
+    · left; simp only [h2, mul_mod, h1, mod_mod]; decide
 #align miu.mod3_eq_1_or_mod3_eq_2 Miu.mod3_eq_1_or_mod3_eq_2
 
 /-- `count_equiv_one_or_two_mod3_of_derivable` shows any derivable string must have a `count I` that
@@ -80,7 +80,7 @@ theorem count_equiv_one_or_two_mod3_of_derivable (en : Miustr) :
     simp_rw [count_cons_self, count_nil, count_cons, ite_false, add_right_comm, add_mod_right]
     simp
   · left; rw [count_append, count_append, count_append]
-    simp only [ne_eq, count_cons_of_ne, count_nil, add_zero]
+    simp only [ne_eq, not_false_eq_true, count_cons_of_ne, count_nil, add_zero]
 #align miu.count_equiv_one_or_two_mod3_of_derivable Miu.count_equiv_one_or_two_mod3_of_derivable
 
 /-- Using the above theorem, we solve the MU puzzle, showing that `"MU"` is not derivable.
@@ -134,7 +134,7 @@ theorem goodm_of_rule1 (xs : Miustr) (h₁ : Derivable (xs ++ ↑[I])) (h₂ : G
     exact mhead
   · change ¬M ∈ tail (xs ++ ↑([I] ++ [U]))
     rw [← append_assoc, tail_append_singleton_of_ne_nil]
-    · simp_rw [mem_append, not_or, and_true]; exact nmtail
+    · simp_rw [mem_append, mem_singleton, or_false]; exact nmtail
     · exact append_ne_nil_of_ne_nil_left _ _ this
 #align miu.goodm_of_rule1 Miu.goodm_of_rule1
 
@@ -145,7 +145,7 @@ theorem goodm_of_rule2 (xs : Miustr) (_ : Derivable (M :: xs)) (h₂ : Goodm (M
   · cases' h₂ with mhead mtail
     contrapose! mtail
     rw [cons_append] at mtail
-    exact (or_self_iff _).mp (mem_append.mp mtail)
+    exact or_self_iff.mp (mem_append.mp mtail)
 #align miu.goodm_of_rule2 Miu.goodm_of_rule2
 
 theorem goodm_of_rule3 (as bs : Miustr) (h₁ : Derivable (as ++ ↑[I, I, I] ++ bs))

Archive/MiuLanguage/DecisionSuf.lean

@@ -267,7 +267,7 @@ theorem count_I_eq_length_of_count_U_zero_and_neg_mem {ys : Miustr} (hu : count
       · simpa only [count]
       · rw [mem_cons, not_or] at hm; exact hm.2
     · -- case `x = U` gives a contradiction.
-      exfalso; simp only [count, countP_cons_of_pos] at hu
+      exfalso; simp only [count, countP_cons_of_pos (· == U) _ (rfl : U == U)] at hu
       exact succ_ne_zero _ hu
 set_option linter.uppercaseLean3 false in
 #align miu.count_I_eq_length_of_count_U_zero_and_neg_mem Miu.count_I_eq_length_of_count_U_zero_and_neg_mem
@@ -277,7 +277,8 @@ set_option linter.uppercaseLean3 false in
 theorem base_case_suf (en : Miustr) (h : Decstr en) (hu : count U en = 0) : Derivable en := by
   rcases h with ⟨⟨mhead, nmtail⟩, hi⟩
   have : en ≠ nil := by
-    intro k; simp only [k, count, countP, if_false, zero_mod, zero_ne_one, false_or_iff] at hi
+    intro k
+    simp only [k, count, countP, countP.go, if_false, zero_mod, zero_ne_one, false_or_iff] at hi
   rcases exists_cons_of_ne_nil this with ⟨y, ys, rfl⟩
   rcases mhead
   rsuffices ⟨c, rfl, hc⟩ : ∃ c, replicate c I = ys ∧ (c % 3 = 1 ∨ c % 3 = 2)
@@ -331,7 +332,7 @@ theorem ind_hyp_suf (k : ℕ) (ys : Miustr) (hu : count U ys = succ k) (hdec : D
     rw [cons_append, cons_append]
     dsimp [tail] at nmtail ⊢
     rw [mem_append] at nmtail
-    simpa only [mem_append, mem_cons, false_or_iff, or_false_iff] using nmtail
+    simpa only [append_assoc, cons_append, nil_append, mem_append, mem_cons, false_or] using nmtail
   · rw [count_append, count_append]; rw [← cons_append, count_append] at hic
     simp only [count_cons_self, count_nil, count_cons, if_false] at hic ⊢
     rw [add_right_comm, add_mod_right]; exact hic

Archive/Wiedijk100Theorems/AbelRuffini.lean

@@ -94,10 +94,11 @@ theorem irreducible_Phi (p : ℕ) (hp : p.Prime) (hpa : p ∣ a) (hpb : p ∣ b)
     rw [mem_span_singleton]
     rw [degree_Phi] at hn; norm_cast at hn
     interval_cases hn : n <;>
-    simp only [Φ, coeff_X_pow, coeff_C, Int.coe_nat_dvd.mpr, hpb, if_true, coeff_C_mul, if_false,
-      coeff_X_zero, hpa, coeff_add, zero_add, mul_zero, coeff_sub, add_zero, zero_sub, dvd_neg,
-      neg_zero, dvd_mul_of_dvd_left]
+    simp (config := {decide := true}) only [Φ, coeff_X_pow, coeff_C, Int.coe_nat_dvd.mpr, hpb,
+      if_true, coeff_C_mul, if_false, coeff_X_zero, hpa, coeff_add, zero_add, mul_zero, coeff_sub,
+      add_zero, zero_sub, dvd_neg, neg_zero, dvd_mul_of_dvd_left]
   · simp only [degree_Phi, ← WithBot.coe_zero, WithBot.coe_lt_coe, Nat.succ_pos']
+    decide
   · rw [coeff_zero_Phi, span_singleton_pow, mem_span_singleton]
     exact mt Int.coe_nat_dvd.mp hp2b
   all_goals exact Monic.isPrimitive (monic_Phi a b)
@@ -136,7 +137,7 @@ theorem real_roots_Phi_ge_aux (hab : b < a) :
     have hfa :=
       calc
         f (-a) = (a : ℝ) ^ 2 - (a : ℝ) ^ 5 + b := by
-          norm_num [hf, ← sq, sub_eq_add_neg, add_comm, Odd.neg_pow]
+          norm_num [hf, ← sq, sub_eq_add_neg, add_comm, Odd.neg_pow (by decide : Odd 5)]
         _ ≤ (a : ℝ) ^ 2 - (a : ℝ) ^ 3 + (a - 1) := by
           refine' add_le_add (sub_le_sub_left (pow_le_pow ha _) _) _ <;> linarith
         _ = -((a : ℝ) - 1) ^ 2 * (a + 1) := by ring
@@ -163,7 +164,7 @@ theorem complex_roots_Phi (h : (Φ ℚ a b).Separable) : Fintype.card ((Φ ℚ a
 theorem gal_Phi (hab : b < a) (h_irred : Irreducible (Φ ℚ a b)) :
     Bijective (galActionHom (Φ ℚ a b) ℂ) := by
   apply galActionHom_bijective_of_prime_degree' h_irred
-  · norm_num [natDegree_Phi]
+  · simp only [natDegree_Phi]; decide
   · rw [complex_roots_Phi a b h_irred.separable, Nat.succ_le_succ_iff]
     exact (real_roots_Phi_le a b).trans (Nat.le_succ 3)
   · simp_rw [complex_roots_Phi a b h_irred.separable, Nat.succ_le_succ_iff]
@@ -181,7 +182,7 @@ theorem not_solvable_by_rad (p : ℕ) (x : ℂ) (hx : aeval x (Φ ℚ a b) = 0)
 #align abel_ruffini.not_solvable_by_rad AbelRuffini.not_solvable_by_rad
 
 theorem not_solvable_by_rad' (x : ℂ) (hx : aeval x (Φ ℚ 4 2) = 0) : ¬IsSolvableByRad ℚ x := by
-  apply not_solvable_by_rad 4 2 2 x hx <;> norm_num
+  apply not_solvable_by_rad 4 2 2 x hx <;> decide
 #align abel_ruffini.not_solvable_by_rad' AbelRuffini.not_solvable_by_rad'
 
 /-- **Abel-Ruffini Theorem** -/

Archive/Wiedijk100Theorems/BallotProblem.lean

@@ -221,7 +221,9 @@ theorem first_vote_pos :
     simp [ENNReal.div_self _ _]
   | 0, q + 1, _ => by
     rw [counted_left_zero, condCount_singleton]
-    simp
+    simp only [List.replicate, Nat.add_eq, add_zero, mem_setOf_eq, List.headI_cons, Nat.cast_zero,
+      ENNReal.zero_div, ite_eq_right_iff]
+    decide
   | p + 1, q + 1, _ => by
     simp_rw [counted_succ_succ]
     rw [← condCount_disjoint_union ((countedSequence_finite _ _).image _)