Trigger CI for leanprover-community/batteries#1727

Author: mathlib-nightly-testing[bot]

.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: b6def9edd1c39de8602b8c177c66e9416e5dbc60
+    default: ca86f6900d53e503e28ec1cfa2bff2f505474553
   path:
     description: Checkout destination path.
     required: false

.github/workflows/build_template.yml

@@ -743,6 +743,12 @@ jobs:
       - name: clean up the import graph file
         run: rm import_graph.dot
 
+      - name: check all scripts build successfully
+        run: |
+          lake env lean scripts/create_deprecated_modules.lean
+          lake env lean scripts/autolabel.lean
+          lake exe check_title_labels --labels "t-algebra" "feat: dummy PR for testing"
+
       - name: build everything
         # make sure everything is available for test/import_all.lean
         # and that miscellaneous executables still work

.github/workflows/rm_set_option.yml

@@ -2,14 +2,20 @@ name: Remove unnecessary set_option lines
 
 on:
   schedule:
-    - cron: "0 4 * * 1" # At 04:00 UTC on Monday.
+    # Run several hours before the technical debt report which runs Mondays at 04:00 UTC
+    - cron: "20 23 * * 0" # At 23:20 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
       global_timeout:
         description: 'Global timeout in seconds (default: 18000 = 5 hours)'
         required: false
@@ -121,7 +127,7 @@ jobs:
           base: master
           title: "chore: remove unnecessary set_option lines"
           body: ${{ steps.pr_body.outputs.body }}
-          # labels: "auto-merge-after-CI"
+          labels: ${{ toJson(inputs.auto_merge) == 'true' && 'auto-merge-after-CI' || '' }}
 
       - name: Send Zulip message (success)
         if: steps.pr.outcome == 'success'

Archive/Imo/Imo1962Q1.lean

@@ -105,9 +105,7 @@ lemma case_more_digits {c n : ℕ} (hc : (digits 10 c).length ≥ 6) (hpp : Prob
 Now we combine these cases to show that 153846 is the smallest solution.
 -/
 
-lemma satisfied_by_153846 : ProblemPredicate 153846 := by
-  norm_num [ProblemPredicate]
-  decide
+lemma satisfied_by_153846 : ProblemPredicate 153846 := by simp +decide [ProblemPredicate]
 
 lemma no_smaller_solutions (n : ℕ) (hn : ProblemPredicate n) : n ≥ 153846 := by
   have ⟨c, hcn⟩ := without_digits hn

Archive/Imo/Imo1962Q4.lean

@@ -59,8 +59,7 @@ Now we can solve for `x` using basic-ish trigonometry.
 -/
 theorem solve_cos2_half {x : ℝ} : cos x ^ 2 = 1 / 2 ↔ ∃ k : ℤ, x = (2 * ↑k + 1) * π / 4 := by
   rw [cos_sq]
-  simp only [add_eq_left, div_eq_zero_iff]
-  norm_num
+  simp only [add_eq_left, div_eq_zero_iff, OfNat.ofNat_ne_zero, or_false]
   rw [cos_eq_zero_iff]
   constructor <;>
     · rintro ⟨k, h⟩

Archive/Imo/Imo1988Q6.lean

@@ -179,7 +179,7 @@ theorem constant_descent_vieta_jumping (x y : ℕ) {claim : Prop} {H : ℕ → 
     suffices hc : c ≠ mx from lt_of_le_of_ne (mod_cast c_lt) hc
     -- However, recall that B(m_x) ≠ m_x + m_y.
     -- If c = m_x, we can prove B(m_x) = m_x + m_y.
-    contrapose! hm_B₂
+    contrapose hm_B₂
     subst c
     simp [hV₁]
     -- Hence p' = (c, m_x) lies on the upper branch, and we are done.
@@ -281,7 +281,7 @@ example {a b : ℕ} (h : a * b ∣ a ^ 2 + b ^ 2 + 1) : 3 * a * b = a ^ 2 + b ^
       apply ne_of_gt
       push Not at h_base
       calc
-        z * y > x * y := by apply mul_lt_mul_of_pos_right <;> lia
+        z * y > x * y := by gcongr; lia
         _ ≥ x * (x + 1) := by apply mul_le_mul <;> lia
         _ > x * x + 1 := by
           rw [mul_add]

Archive/Imo/Imo2002Q3.lean

@@ -12,7 +12,7 @@ import Mathlib.RingTheory.Polynomial.Content
 Find all pairs of positive integers $m,n ≥ 3$ for which there exist infinitely many
 positive integers $a$ such that $(a^m+a-1) / (a^n+a^2-1)$ is itself an integer.
 
-# Solution
+## Solution
 
 It suffices to find $(m,n)$ pairs for which $a^n+a^2-1 ∣ a^m+a-1$, where both sides are viewed as
 polynomials in $a$. This automatically gives $n ≤ m$, so we have

Archive/Imo/Imo2008Q2.lean

@@ -46,9 +46,9 @@ theorem imo2008_q2a (x y z : ℝ) (h : x * y * z = 1) (hx : x ≠ 1) (hy : y ≠
     x ^ 2 / (x - 1) ^ 2 + y ^ 2 / (y - 1) ^ 2 + z ^ 2 / (z - 1) ^ 2 ≥ 1 := by
   obtain ⟨a, b, c, ha, hb, hc, rfl, rfl, rfl⟩ := subst_abc h
   obtain ⟨m, n, rfl, rfl⟩ : ∃ m n, b = c - m ∧ a = c - m - n := by use c - b, b - a; simp
-  have hm_ne_zero : m ≠ 0 := by contrapose! hy; simpa [field]
-  have hn_ne_zero : n ≠ 0 := by contrapose! hx; simpa [field]
-  have hmn_ne_zero : m + n ≠ 0 := by contrapose! hz; field_simp; linarith
+  have hm_ne_zero : m ≠ 0 := by contrapose hy; simpa [field]
+  have hn_ne_zero : n ≠ 0 := by contrapose hx; simpa [field]
+  have hmn_ne_zero : m + n ≠ 0 := by contrapose hz; field_simp; linarith
   have hc_sub_sub : c - (c - m - n) = m + n := by abel
   rw [ge_iff_le, ← sub_nonneg]
   convert sq_nonneg ((c * (m ^ 2 + n ^ 2 + m * n) - m * (m + n) ^ 2) / (m * n * (m + n)))

Archive/Imo/Imo2010Q5.lean

@@ -25,7 +25,7 @@ Determine if there exists a finite sequence of operations of the allowed types,
 that the five boxes $B_1, B_2, B_3, B_4, B_5$ become empty, while box $B_6$ contains exactly
 $2010^{2010^{2010}}$ coins.
 
-# Solution
+## Solution
 
 We follow the solution from https://web.evanchen.cc/exams/IMO-2010-notes.pdf.
 

Archive/Imo/Imo2019Q4.lean

@@ -75,6 +75,7 @@ theorem upper_bound {k n : ℕ} (hk : k > 0)
 
 end Imo2019Q4
 
+set_option linter.flexible false in -- TODO: fix non-terminal simp
 theorem imo2019_q4 {k n : ℕ} (hk : 0 < k) (hn : 0 < n) :
     (k ! : ℤ) = ∏ i ∈ range n, ((2 : ℤ) ^ n - (2 : ℤ) ^ i) ↔ (k, n) = (1, 1) ∨ (k, n) = (3, 2) := by
   -- The implication `←` holds.
@@ -90,7 +91,7 @@ theorem imo2019_q4 {k n : ℕ} (hk : 0 < k) (hn : 0 < n) :
   -- n = 2
   · right; congr; norm_num [prod_range_succ] at h; norm_cast at h; rwa [← factorial_inj']
     norm_num
-  all_goals exfalso; norm_num [prod_range_succ] at h; norm_cast at h
+  all_goals exfalso; simp [prod_range_succ] at h; norm_cast at h
   -- n = 3
   · refine monotone_factorial.ne_of_lt_of_lt_nat 5 ?_ ?_ _ h <;> decide
   -- n = 4