merge master

Author: kim-em

.github/workflows/discover-lean-pr-testing.yml

@@ -18,11 +18,12 @@ jobs:
       with:
         ref: nightly-testing
         fetch-depth: 0  # Fetch all branches
+        token: ${{ secrets.NIGHTLY_TESTING }}
 
     - name: Set up Git
       run: |
-        git config --global user.name "github-actions"
-        git config --global user.email "github-actions@github.com"
+        git config --global user.name "leanprover-community-mathlib4-bot"
+        git config --global user.email "[email protected].github.com"
 
     - name: Configure Lean
       uses: leanprover/lean-action@434f25c2f80ded67bba02502ad3a86f25db50709 # v1.3.0

Archive/Imo/Imo1960Q1.lean

@@ -45,14 +45,14 @@ theorem ge_100 {n : ℕ} (h1 : ProblemPredicate n) : 100 ≤ n := by
     rw [← h1.left]
     refine Nat.base_pow_length_digits_le 10 n ?_ (not_zero h1)
     simp
-  omega
+  lia
 
 theorem lt_1000 {n : ℕ} (h1 : ProblemPredicate n) : n < 1000 := by
   have h2 : n < 10 ^ 3 := by
     rw [← h1.left]
     refine Nat.lt_base_pow_length_digits ?_
     simp
-  omega
+  lia
 
 /-
 We do an exhaustive search to show that all results are covered by `SolutionPredicate`.
@@ -70,7 +70,7 @@ theorem searchUpTo_step {c n} (H : SearchUpTo c n) {c' n'} (ec : c + 1 = c') (en
   refine ⟨by ring, fun m l p => ?_⟩
   obtain ⟨h₁, ⟨m, rfl⟩, h₂⟩ := id p
   by_cases h : 11 * m < c * 11; · exact H _ h p
-  obtain rfl : m = c := by omega
+  obtain rfl : m = c := by lia
   rw [Nat.mul_div_cancel_left _ (by simp : 11 > 0), mul_comm] at h₂
   refine (H' h₂).imp ?_ ?_ <;> · rintro rfl; norm_num
 

Archive/Imo/Imo1962Q1.lean

@@ -53,31 +53,31 @@ Now we can eliminate possibilities for `(digits 10 c).length` until we get to th
 lemma case_0_digits {c n : ℕ} (hc : (digits 10 c).length = 0) : ¬ProblemPredicate' c n := by
   intro hpp
   have hpow : 6 * 10 ^ 0 = 6 * 10 ^ (digits 10 c).length := by rw [hc]
-  omega
+  lia
 
 lemma case_1_digits {c n : ℕ} (hc : (digits 10 c).length = 1) : ¬ProblemPredicate' c n := by
   intro hpp
   have hpow : 6 * 10 ^ 1 = 6 * 10 ^ (digits 10 c).length := by rw [hc]
-  omega
+  lia
 
 lemma case_2_digits {c n : ℕ} (hc : (digits 10 c).length = 2) : ¬ProblemPredicate' c n := by
   intro hpp
   have hpow : 6 * 10 ^ 2 = 6 * 10 ^ (digits 10 c).length := by rw [hc]
-  omega
+  lia
 
 lemma case_3_digits {c n : ℕ} (hc : (digits 10 c).length = 3) : ¬ProblemPredicate' c n := by
   intro hpp
   have hpow : 6 * 10 ^ 3 = 6 * 10 ^ (digits 10 c).length := by rw [hc]
-  omega
+  lia
 
 lemma case_4_digits {c n : ℕ} (hc : (digits 10 c).length = 4) : ¬ProblemPredicate' c n := by
   intro hpp
   have hpow : 6 * 10 ^ 4 = 6 * 10 ^ (digits 10 c).length := by rw [hc]
-  omega
+  lia
 
 /-- Putting this inline causes a deep recursion error, so we separate it out. -/
 private lemma helper_5_digits {c : ℤ} (hc : 6 * 10 ^ 5 + c = 4 * (10 * c + 6)) : c = 15384 := by
-  omega
+  lia
 
 lemma case_5_digits {c n : ℕ} (hc : (digits 10 c).length = 5) (hpp : ProblemPredicate' c n) :
     c = 15384 := by

Archive/Imo/Imo1985Q2.lean

@@ -51,22 +51,22 @@ lemma C_mul_mod {n j : ℕ} (hn : 3 ≤ n) (hj : j ∈ Set.Ico 1 n) (cpj : Nat.C
     have nej : (k + 1) * j % n ≠ j := by
       by_contra! h; nth_rw 2 [← Nat.mod_eq_of_lt hj.2, ← one_mul j] at h
       replace h : (k + 1) % n = 1 % n := Nat.ModEq.cancel_right_of_coprime cpj h
-      rw [Nat.mod_eq_of_lt hk.2, Nat.mod_eq_of_lt (by omega)] at h
-      omega
+      rw [Nat.mod_eq_of_lt hk.2, Nat.mod_eq_of_lt (by lia)] at h
+      lia
     have b₁ : (k + 1) * j % n ∈ Set.Ico 1 n := by
-      refine ⟨?_, Nat.mod_lt _ (by omega)⟩
+      refine ⟨?_, Nat.mod_lt _ (by lia)⟩
       by_contra! h; rw [Nat.lt_one_iff, ← Nat.dvd_iff_mod_eq_zero] at h
       have ek := Nat.eq_zero_of_dvd_of_lt (cpj.dvd_of_dvd_mul_right h) hk.2
-      omega
+      lia
     rw [← ih ⟨hk₁, Nat.lt_of_succ_lt hk.2⟩, hC.2 _ b₁ nej]
     rcases nej.lt_or_gt with h | h
     · rw [Int.natAbs_natCast_sub_natCast_of_ge h.le]
       have b₂ : j - (k + 1) * j % n ∈ Set.Ico 1 n :=
         ⟨Nat.sub_pos_iff_lt.mpr h, (Nat.sub_le ..).trans_lt hj.2⟩
       have q : n - (j - (k + 1) * j % n) = (k + 1) * j % n + (n - j) % n := by
         rw [tsub_tsub_eq_add_tsub_of_le h.le, add_comm, Nat.add_sub_assoc hj.2.le,
-          Nat.mod_eq_of_lt (show n - j < n by omega)]
-      rw [hC.1 _ b₂, q, ← Nat.add_mod_of_add_mod_lt (by omega), ← Nat.add_sub_assoc hj.2.le,
+          Nat.mod_eq_of_lt (show n - j < n by lia)]
+      rw [hC.1 _ b₂, q, ← Nat.add_mod_of_add_mod_lt (by lia), ← Nat.add_sub_assoc hj.2.le,
         add_comm, Nat.add_sub_assoc (Nat.le_mul_of_pos_left _ hk.1), ← tsub_one_mul,
         Nat.add_mod_left, add_tsub_cancel_right]
     · rw [Int.natAbs_natCast_sub_natCast_of_le h.le, Nat.mod_sub_of_le h.le]
@@ -75,13 +75,13 @@ lemma C_mul_mod {n j : ℕ} (hn : 3 ≤ n) (hj : j ∈ Set.Ico 1 n) (cpj : Nat.C
 theorem result {n j : ℕ} (hn : 3 ≤ n) (hj : j ∈ Set.Ico 1 n) (cpj : Coprime n j)
     {C : ℕ → Fin 2} (hC : Condition n j C) {i : ℕ} (hi : i ∈ Set.Ico 1 n) :
     C i = C j := by
-  obtain ⟨v, -, hv⟩ := exists_mul_mod_eq_one_of_coprime cpj.symm (by omega)
+  obtain ⟨v, -, hv⟩ := exists_mul_mod_eq_one_of_coprime cpj.symm (by lia)
   have hvi : i = (v * i % n) * j % n := by
     rw [mod_mul_mod, ← mul_rotate, ← mod_mul_mod, hv, one_mul, mod_eq_of_lt hi.2]
   have vib : v * i % n ∈ Set.Ico 1 n := by
-    refine ⟨(?_ : 0 < _), mod_lt _ (by omega)⟩
+    refine ⟨(?_ : 0 < _), mod_lt _ (by lia)⟩
     by_contra! h; rw [le_zero, ← dvd_iff_mod_eq_zero] at h
-    rw [mul_comm, ← mod_eq_of_lt (show 1 < n by omega)] at hv
+    rw [mul_comm, ← mod_eq_of_lt (show 1 < n by lia)] at hv
     have i0 := eq_zero_of_dvd_of_lt
       ((coprime_of_mul_modEq_one _ hv).symm.dvd_of_dvd_mul_left h) hi.2
     subst i; simp at hi

Archive/Imo/Imo1988Q6.lean

@@ -239,7 +239,7 @@ theorem imo1988_q6 {a b : ℕ} (h : a * b + 1 ∣ a ^ 2 + b ^ 2) :
     · contrapose! hV₀ with x_lt_z
       apply ne_of_gt
       calc
-        z * y > x * x := by apply mul_lt_mul' <;> omega
+        z * y > x * x := by apply mul_lt_mul' <;> lia
         _ ≥ x * x - k := sub_le_self _ (Int.natCast_nonneg k)
   · -- There is no base case in this application of Vieta jumping.
     simp
@@ -276,16 +276,16 @@ example {a b : ℕ} (h : a * b ∣ a ^ 2 + b ^ 2 + 1) : 3 * a * b = a ^ 2 + b ^
     constructor
     · have zy_pos : z * y ≥ 0 := by rw [hV₀]; exact mod_cast Nat.zero_le _
       apply nonneg_of_mul_nonneg_left zy_pos
-      omega
+      lia
     · contrapose! hV₀ with x_lt_z
       apply ne_of_gt
       push_neg at h_base
       calc
-        z * y > x * y := by apply mul_lt_mul_of_pos_right <;> omega
-        _ ≥ x * (x + 1) := by apply mul_le_mul <;> omega
+        z * y > x * y := by apply mul_lt_mul_of_pos_right <;> lia
+        _ ≥ x * (x + 1) := by apply mul_le_mul <;> lia
         _ > x * x + 1 := by
           rw [mul_add]
-          omega
+          lia
   · -- Show the base case.
     intro x y h h_base
     obtain rfl | rfl : x = 0 ∨ x = 1 := by rwa [Nat.le_add_one_iff, Nat.le_zero] at h_base

Archive/Imo/Imo1994Q1.lean

@@ -37,7 +37,7 @@ theorem tedious (m : ℕ) (k : Fin (m + 1)) : m - ((m + 1 - ↑k) + m) % (m + 1)
   rcases hk with ⟨c, rfl⟩
   have : (k + c + 1 - k) + (k + c) = c + (k + c + 1) := by lia
   rw [Fin.val_mk, this, Nat.add_mod_right, Nat.mod_eq_of_lt, Nat.add_sub_cancel]
-  omega
+  lia
 
 end Imo1994Q1
 

Archive/Imo/Imo1997Q3.lean

@@ -74,7 +74,7 @@ lemma sign_eq_of_contra
   | one => rfl
   | mul_right p s sform ih =>
     suffices |S x p - S x (p * s)| ≤ (n + 1 : ℕ) + 1 by
-      rw [ih]; exact sign_eq_of_abs_sub_le (h _) (h _) (by norm_cast; omega) this
+      rw [ih]; exact sign_eq_of_abs_sub_le (h _) (h _) (by norm_cast; lia) this
     rw [Set.mem_range] at sform; obtain ⟨i, hi⟩ := sform
     iterate 2 rw [S, ← sum_add_sum_compl {i.castSucc, i.succ}]
     have cg : ∑ j ∈ {i.castSucc, i.succ}ᶜ, (j + 1) * x ((p * s) j) =
@@ -99,16 +99,16 @@ lemma S_one_add_S_revPerm
   nth_rw 2 [S]; rw [← revPerm.sum_comp _ _ (by simp)]
   simp_rw [revPerm_apply, val_rev, rev_rev, S, Perm.one_apply, ← sum_add_distrib, ← add_mul]
   have cg : ∑ i : Fin n, (i + 1 + ((n - (i + 1) : ℕ) + 1)) * x i = ∑ i, (n + 1) * x i := by
-    congr! 2 with i; norm_cast; omega
-  rw [cg, ← mul_sum, abs_mul, hx₁, mul_one]; exact abs_of_nonneg (by norm_cast; omega)
+    congr! 2 with i; norm_cast; lia
+  rw [cg, ← mul_sum, abs_mul, hx₁, mul_one]; exact abs_of_nonneg (by norm_cast; lia)
 
 theorem result {x : Fin n → ℝ} (hx₁ : |∑ i, x i| = 1) (hx₂ : ∀ i, |x i| ≤ (n + 1) / 2) :
     ∃ p, |S x p| ≤ (n + 1) / 2 := by
   match n with
   | 0 => simp [S]
   | n + 1 =>
     by_contra! h
-    exact (lt_abs_add_of_sign_eq (h _) (h _) (by norm_cast; omega)
+    exact (lt_abs_add_of_sign_eq (h _) (h _) (by norm_cast; lia)
       (sign_eq_of_contra hx₂ h _)).ne' (S_one_add_S_revPerm hx₁)
 
 end Imo1997Q3

Archive/Imo/Imo1998Q2.lean

@@ -176,7 +176,7 @@ theorem judge_pairs_card_lower_bound {z : ℕ} (hJ : Fintype.card J = 2 * z + 1)
   rw [h]; apply Int.le_of_ofNat_le_ofNat; simp only [Int.natCast_add, Int.natCast_mul]
   apply norm_bound_of_odd_sum
   suffices x + y = 2 * z + 1 by simp [← Int.natCast_add, this]
-  rw [Finset.filter_card_add_filter_neg_card_eq_card, ← hJ, Finset.card_univ]
+  rw [Finset.card_filter_add_card_filter_not, ← hJ, Finset.card_univ]
 
 open scoped Classical in
 theorem distinct_judge_pairs_card_lower_bound {z : ℕ} (hJ : Fintype.card J = 2 * z + 1) (c : C) :

Archive/Imo/Imo2001Q3.lean

@@ -66,7 +66,7 @@ lemma card_not_easy_le_five {i : Fin 21} (hG : #(G i) ≤ 6) (hB : ∀ j, ¬Disj
     _ = #((G i).biUnion fun p ↦ {j | p ∈ B j}) := by congr 1; ext j; simp [not_disjoint_iff]
     _ ≤ ∑ p ∈ G i, #{j | p ∈ B j} := card_biUnion_le
     _ ≤ ∑ p ∈ G i, 2 := sum_le_sum fun p mp ↦ Nat.le_of_lt_succ (h p mp)
-    _ ≤ _ := by rw [sum_const, smul_eq_mul]; omega
+    _ ≤ _ := by rw [sum_const, smul_eq_mul]; lia
 
 open Classical in
 /-- There are at most 210 girl-boy pairs who solved some problem in common that was not easy for

Archive/Imo/Imo2001Q6.lean

@@ -22,9 +22,9 @@ variable {a b c d : ℤ}
 theorem imo2001_q6 (hd : 0 < d) (hdc : d < c) (hcb : c < b) (hba : b < a)
     (h : a * c + b * d = (a + b - c + d) * (-a + b + c + d)) : ¬Prime (a * b + c * d) := by
   intro (h0 : Prime (a * b + c * d))
-  have ha : 0 < a := by omega
-  have hb : 0 < b := by omega
-  have hc : 0 < c := by omega
+  have ha : 0 < a := by lia
+  have hb : 0 < b := by lia
+  have hc : 0 < c := by lia
   -- the key step is to show that `a*c + b*d` divides the product `(a*b + c*d) * (a*d + b*c)`
   have dvd_mul : a * c + b * d ∣ (a * b + c * d) * (a * d + b * c) := by
     use b ^ 2 + b * d + d ^ 2