Trigger CI for leanprover/lean4#5542

Author: leanprover-community-mathlib4-bot

Diff for: .github/build.in.yml

@@ -133,8 +133,8 @@ jobs:
         run: |
           rm -rf .lake/build/lib/Mathlib/
           # Fail quickly if the cache is completely cold, by checking for Mathlib.Init
-          lake exe cache get Mathlib.Init
-          lake build --no-build Mathlib.Init && lake exe cache get || echo "No cache for 'Mathlib.Init' available"
+          lake exe cache get #Mathlib.Init
+          #lake build --no-build Mathlib.Init && lake exe cache get || echo "No cache for 'Mathlib.Init' available"
 
       - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean
         id: mk_all

Diff for: .github/workflows/PR_summary.yml

@@ -55,12 +55,27 @@ jobs:
         PR="${{ github.event.pull_request.number }}"
         title="### PR summary"
 
+        graphAndHighPercentReports=$(python ./scripts/import-graph-report.py base.json head.json changed_files.txt)
+
         ## Import count comment
         importCount=$(
-          python ./scripts/import-graph-report.py base.json head.json changed_files.txt
+          printf '%s\n' "${graphAndHighPercentReports}" | sed '/^Import changes exceeding/Q'
           ./scripts/import_trans_difference.sh
         )
 
+        ## High percentage imports
+        high_percentages=$(
+          printf '%s\n' "${graphAndHighPercentReports}" | sed -n '/^Import changes exceeding/,$p'
+        )
+        # if there are files with large increase in transitive imports, then we add the `large-import` label
+        if [ -n "${high_percentages}" ]
+        then
+          high_percentages=$'\n\n'"${high_percentages}"
+          gh pr edit "${PR}" --add-label large-import
+        else # otherwise, we remove the label
+          gh pr edit "${PR}" --remove-label large-import
+        fi
+
         if [ "$(printf '%s' "${importCount}" | wc -l)" -gt 12 ]
         then
           importCount="$(printf '<details><summary>\n\n%s\n\n</summary>\n\n%s\n\n</details>\n' "#### Import changes for modified files" "${importCount}")"
@@ -80,6 +95,6 @@ jobs:
         currentHash="$(git rev-parse HEAD)"
         hashURL="https://github.com/${{ github.repository }}/pull/${{ github.event.pull_request.number }}/commits/${currentHash}"
 
-        message="$(printf '%s [%s](%s)\n\n%s\n\n---\n\n%s\n' "${title}" "$(git rev-parse --short HEAD)" "${hashURL}" "${importCount}" "${declDiff}")"
+        message="$(printf '%s [%s](%s)%s\n\n%s\n\n---\n\n%s\n' "${title}" "$(git rev-parse --short HEAD)" "${hashURL}" "${high_percentages}" "${importCount}" "${declDiff}")"
 
         ./scripts/update_PR_comment.sh "${message}" "${title}" "${PR}"

Diff for: .github/workflows/bors.yml

@@ -143,8 +143,8 @@ jobs:
         run: |
           rm -rf .lake/build/lib/Mathlib/
           # Fail quickly if the cache is completely cold, by checking for Mathlib.Init
-          lake exe cache get Mathlib.Init
-          lake build --no-build Mathlib.Init && lake exe cache get || echo "No cache for 'Mathlib.Init' available"
+          lake exe cache get #Mathlib.Init
+          #lake build --no-build Mathlib.Init && lake exe cache get || echo "No cache for 'Mathlib.Init' available"
 
       - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean
         id: mk_all

Diff for: .github/workflows/build.yml

@@ -150,8 +150,8 @@ jobs:
         run: |
           rm -rf .lake/build/lib/Mathlib/
           # Fail quickly if the cache is completely cold, by checking for Mathlib.Init
-          lake exe cache get Mathlib.Init
-          lake build --no-build Mathlib.Init && lake exe cache get || echo "No cache for 'Mathlib.Init' available"
+          lake exe cache get #Mathlib.Init
+          #lake build --no-build Mathlib.Init && lake exe cache get || echo "No cache for 'Mathlib.Init' available"
 
       - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean
         id: mk_all

Diff for: .github/workflows/build_fork.yml

@@ -147,8 +147,8 @@ jobs:
         run: |
           rm -rf .lake/build/lib/Mathlib/
           # Fail quickly if the cache is completely cold, by checking for Mathlib.Init
-          lake exe cache get Mathlib.Init
-          lake build --no-build Mathlib.Init && lake exe cache get || echo "No cache for 'Mathlib.Init' available"
+          lake exe cache get #Mathlib.Init
+          #lake build --no-build Mathlib.Init && lake exe cache get || echo "No cache for 'Mathlib.Init' available"
 
       - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean
         id: mk_all

Diff for: .github/workflows/lean4checker.yml

@@ -70,7 +70,7 @@ jobs:
         run: |
           git clone https://github.com/leanprover/lean4checker
           cd lean4checker
-          git checkout v4.12.0-rc1
+          git checkout v4.13.0-rc3
           # Now that the git hash is embedded in each olean,
           # we need to compile lean4checker on the same toolchain
           cp ../lean-toolchain .

Diff for: .github/workflows/nightly_detect_failure.yml

@@ -23,6 +23,7 @@ jobs:
         topic: 'Mathlib status updates'
         content: |
           ❌ The latest CI for Mathlib's branch#nightly-testing has [failed](https://github.com/${{ github.repository }}/actions/runs/${{ github.event.workflow_run.id }}) ([${{ github.sha }}](https://github.com/${{ github.repository }}/commit/${{ github.sha }})).
+          You can `git fetch; git checkout nightly-testing` and push a fix.
 
   handle_success:
     if: ${{ github.event.workflow_run.conclusion == 'success' && github.event.workflow_run.head_branch == 'nightly-testing' }}
@@ -211,25 +212,14 @@ jobs:
             payload = f"🛠️: it looks like it's time to create a new bump/nightly-{current_version} branch from nightly-testing (specifically {sha}), and then PR that to {bump_branch}. "
             payload += "To do so semi-automatically, run the following script from mathlib root:\n\n"
             payload += f"```bash\n./scripts/create-adaptation-pr.sh --bumpversion={bump_branch_suffix} --nightlydate={current_version} --nightlysha={sha}\n```\n"
-            # Only post if the message is different
-            # We compare the first 160 characters, since that includes the date and bump version
-            if not messages or messages[0]['content'][:160] != payload[:160]:
-                # Log messages, because the bot seems to repeat itself...
-                if messages:
-                    print("###### Last message:")
-                    print(messages[0]['content'])
-                    print("###### Current message:")
-                    print(payload)
-                else:
-                    print('The strings match!')
-                # Post the reminder message
-                request = {
-                    'type': 'stream',
-                    'to': 'nightly-testing',
-                    'topic': 'Mathlib bump branch reminders',
-                    'content': payload
-                }
-                result = client.send_message(request)
-                print(result)
+            # Post the reminder message
+            request = {
+                'type': 'stream',
+                'to': 'nightly-testing',
+                'topic': 'Mathlib bump branch reminders',
+                'content': payload
+            }
+            result = client.send_message(request)
+            print(result)
         else:
             print('No action needed.')

Diff for: .github/workflows/update_dependencies_zulip.yml

@@ -40,7 +40,7 @@ jobs:
                 });
               }
             } else {
-              output += "No PR found for this run!";
+              output += "No PR found for this run! If you are feeling impatient and have write access, please go to the following page and click the "Run workflow" button!\nhttps://github.com/leanprover-community/mathlib4/actions/workflows/update_dependencies.yml";
             }
             return output;
 

Diff for: .vscode/deprecated-alias.code-snippets renamed to .vscode/deprecated.code-snippets

@@ -1,4 +1,11 @@
 {
+	"Deprecation for mathlib": {
+		"scope": "lean4",
+		"prefix": "deprecated",
+		"body": [
+			"@[deprecated $1 (since := \"${CURRENT_YEAR}-${CURRENT_MONTH}-${CURRENT_DATE}\")]"
+		]
+	},
 	"Deprecated alias for mathlib": {
 		"scope": "lean4",
 		"prefix": "deprecated alias",

Diff for: Archive/Imo/Imo1962Q1.lean

@@ -107,7 +107,7 @@ lemma case_more_digits {c n : ℕ} (hc : (digits 10 c).length ≥ 6) (hpp : Prob
   calc
     n ≥ 10 * c := le.intro hpp.left.symm
     _ ≥ 10 ^ (digits 10 c).length := base_pow_length_digits_le 10 c (by decide) hnz
-    _ ≥ 10 ^ 6 := pow_le_pow_right (by decide) hc
+    _ ≥ 10 ^ 6 := pow_right_mono₀ (by decide) hc
     _ ≥ 153846 := by norm_num
 
 /-!

Diff for: Archive/Imo/Imo1972Q5.lean

@@ -50,7 +50,7 @@ theorem imo1972_q5 (f g : ℝ → ℝ) (hf1 : ∀ x, ∀ y, f (x + y) + f (x - y
       calc
         0 < ‖f x‖ := norm_pos_iff.mpr hx
         _ ≤ k := hk₁ x
-    rw [div_lt_iff]
+    rw [div_lt_iff₀]
     · apply lt_mul_of_one_lt_right h₁ hneg
     · exact zero_lt_one.trans hneg
   -- Demonstrate that `k ≤ k'` using `hk₂`.
@@ -87,7 +87,7 @@ theorem imo1972_q5' (f g : ℝ → ℝ) (hf1 : ∀ x, ∀ y, f (x + y) + f (x -
   have h : ∀ x, ‖f x‖ ≤ k := le_ciSup hf2
   have hgy : 0 < ‖g y‖ := by linarith
   have k_pos : 0 < k := lt_of_lt_of_le (norm_pos_iff.mpr hx) (h x)
-  have : k / ‖g y‖ < k := (div_lt_iff hgy).mpr (lt_mul_of_one_lt_right k_pos H)
+  have : k / ‖g y‖ < k := (div_lt_iff₀ hgy).mpr (lt_mul_of_one_lt_right k_pos H)
   have : k ≤ k / ‖g y‖ := by
     suffices ∀ x, ‖f x‖ ≤ k / ‖g y‖ from ciSup_le this
     intro x

Diff for: Archive/Imo/Imo1986Q5.lean

@@ -54,7 +54,7 @@ theorem map_of_lt_two (hx : x < 2) : f x = 2 / (2 - x) := by
   have hx' : 0 < 2 - x := tsub_pos_of_lt hx
   have hfx : f x ≠ 0 := hf.map_ne_zero_iff.2 hx
   apply le_antisymm
-  · rw [le_div_iff₀ hx', ← NNReal.le_div_iff' hfx, tsub_le_iff_right, ← hf.map_eq_zero,
+  · rw [le_div_iff₀ hx', ← le_div_iff₀' hfx.bot_lt, tsub_le_iff_right, ← hf.map_eq_zero,
      hf.map_add, div_mul_cancel₀ _ hfx, hf.map_two, zero_mul]
   · rw [div_le_iff₀' hx', ← hf.map_eq_zero]
     refine (mul_eq_zero.1 ?_).resolve_right hfx

Diff for: Archive/Imo/Imo2006Q5.lean

@@ -122,7 +122,7 @@ theorem Polynomial.iterate_comp_sub_X_ne {P : Polynomial ℤ} (hP : 1 < P.natDeg
     (hk : 0 < k) : P.comp^[k] X - X ≠ 0 := by
   rw [sub_ne_zero]
   apply_fun natDegree
-  simpa using (one_lt_pow hP hk.ne').ne'
+  simpa using (one_lt_pow₀ hP hk.ne').ne'
 
 /-- We solve the problem for the specific case k = 2 first. -/
 theorem imo2006_q5' {P : Polynomial ℤ} (hP : 1 < P.natDegree) :

Diff for: Archive/Imo/Imo2013Q5.lean

@@ -38,9 +38,9 @@ theorem le_of_all_pow_lt_succ {x y : ℝ} (hx : 1 < x) (hy : 1 < y)
     have hterm : ∀ i : ℕ, i ∈ Finset.range n → 1 ≤ x ^ i * y ^ (n - 1 - i) := by
       intro i _
       calc
-        1 ≤ x ^ i := one_le_pow_of_one_le hx.le i
+        1 ≤ x ^ i := one_le_pow₀ hx.le
         _ = x ^ i * 1 := by ring
-        _ ≤ x ^ i * y ^ (n - 1 - i) := by gcongr; apply one_le_pow_of_one_le hy.le
+        _ ≤ x ^ i * y ^ (n - 1 - i) := by gcongr; apply one_le_pow₀ hy.le
     calc
       (x - y) * (n : ℝ) = (n : ℝ) * (x - y) := by ring
       _ = (∑ _i ∈ Finset.range n, (1 : ℝ)) * (x - y) := by
@@ -134,7 +134,7 @@ theorem fixed_point_of_pos_nat_pow {f : ℚ → ℝ} {n : ℕ} (hn : 0 < n)
     (H1 : ∀ x y, 0 < x → 0 < y → f (x * y) ≤ f x * f y) (H4 : ∀ n : ℕ, 0 < n → (n : ℝ) ≤ f n)
     (H5 : ∀ x : ℚ, 1 < x → (x : ℝ) ≤ f x) {a : ℚ} (ha1 : 1 < a) (hae : f a = a) :
     f (a ^ n) = a ^ n := by
-  have hh0 : (a : ℝ) ^ n ≤ f (a ^ n) := mod_cast H5 (a ^ n) (one_lt_pow ha1 hn.ne')
+  have hh0 : (a : ℝ) ^ n ≤ f (a ^ n) := mod_cast H5 (a ^ n) (one_lt_pow₀ ha1 hn.ne')
   have hh1 :=
     calc
       f (a ^ n) ≤ f a ^ n := pow_f_le_f_pow hn ha1 H1 H4
@@ -206,7 +206,7 @@ theorem imo2013_q5 (f : ℚ → ℝ) (H1 : ∀ x y, 0 < x → 0 < y → f (x * y
       intro n hn
       calc
         (x : ℝ) ^ n - 1 < f (x ^ n) :=
-            mod_cast fx_gt_xm1 (one_le_pow_of_one_le hx.le n) H1 H2 H4
+            mod_cast fx_gt_xm1 (one_le_pow₀ hx.le) H1 H2 H4
         _ ≤ f x ^ n := pow_f_le_f_pow hn hx H1 H4
     have hx' : 1 < (x : ℝ) := mod_cast hx
     have hxp : 0 < x := by positivity

Diff for: Archive/Imo/Imo2019Q2.lean

@@ -57,7 +57,7 @@ rather than more literally with `affineSegment`.
 -/
 
 
-open Affine Affine.Simplex EuclideanGeometry FiniteDimensional
+open Affine Affine.Simplex EuclideanGeometry Module
 
 open scoped Affine EuclideanGeometry Real
 

Diff for: Archive/Sensitivity.lean

@@ -41,7 +41,7 @@ noncomputable section
 
 local notation "√" => Real.sqrt
 
-open Function Bool LinearMap Fintype FiniteDimensional Module.DualBases
+open Function Bool LinearMap Fintype Module Module.DualBases
 
 /-!
 ### The hypercube
@@ -374,7 +374,7 @@ theorem exists_eigenvalue (H : Set (Q m.succ)) (hH : Card H ≥ 2 ^ m + 1) :
   suffices 0 < dim (W ⊓ img) by
     exact mod_cast exists_mem_ne_zero_of_rank_pos this
   have dim_le : dim (W ⊔ img) ≤ 2 ^ (m + 1 : Cardinal) := by
-    convert ← rank_submodule_le (W ⊔ img)
+    convert ← Submodule.rank_le (W ⊔ img)
     rw [← Nat.cast_succ]
     apply dim_V
   have dim_add : dim (W ⊔ img) + dim (W ⊓ img) = dim W + 2 ^ m := by

Diff for: Archive/Wiedijk100Theorems/AbelRuffini.lean

@@ -115,7 +115,7 @@ theorem real_roots_Phi_ge_aux (hab : b < a) :
   · have hf1 : f 1 < 0 := by simp [hf, hb]
     have hfa : 0 ≤ f a := by
       simp_rw [hf, ← sq]
-      refine add_nonneg (sub_nonneg.mpr (pow_le_pow_right ha ?_)) ?_ <;> norm_num
+      refine add_nonneg (sub_nonneg.mpr (pow_right_mono₀ ha ?_)) ?_ <;> norm_num
     obtain ⟨x, ⟨-, hx1⟩, hx2⟩ := intermediate_value_Ico' hle (hc _) (Set.mem_Ioc.mpr ⟨hf1, hf0⟩)
     obtain ⟨y, ⟨hy1, -⟩, hy2⟩ := intermediate_value_Ioc ha (hc _) (Set.mem_Ioc.mpr ⟨hf1, hfa⟩)
     exact ⟨x, y, (hx1.trans hy1).ne, hx2, hy2⟩
@@ -126,7 +126,7 @@ theorem real_roots_Phi_ge_aux (hab : b < a) :
         f (-a) = (a : ℝ) ^ 2 - (a : ℝ) ^ 5 + b := by
           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_right ha ?_) _) ?_ <;> linarith
+          refine add_le_add (sub_le_sub_left (pow_right_mono₀ ha ?_) _) ?_ <;> linarith
         _ = -((a : ℝ) - 1) ^ 2 * (a + 1) := by ring
         _ ≤ 0 := by nlinarith
     have ha' := neg_nonpos.mpr (hle.trans ha)

Diff for: Archive/Wiedijk100Theorems/AscendingDescendingSequences.lean

@@ -3,6 +3,7 @@ Copyright (c) 2020 Bhavik Mehta. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Bhavik Mehta
 -/
+import Mathlib.Data.Finset.Max
 import Mathlib.Data.Fintype.Powerset
 
 /-!

Diff for: Archive/Wiedijk100Theorems/BallotProblem.lean

@@ -235,7 +235,7 @@ theorem first_vote_neg (p q : ℕ) (h : 0 < p + q) :
   have := condCount_compl
     {l : List ℤ | l.headI = 1}ᶜ (countedSequence_finite p q) (countedSequence_nonempty p q)
   rw [compl_compl, first_vote_pos _ _ h] at this
-  rw [← ENNReal.sub_eq_of_add_eq _ this, ENNReal.eq_div_iff, ENNReal.mul_sub, mul_one,
+  rw [ENNReal.eq_sub_of_add_eq _ this, ENNReal.eq_div_iff, ENNReal.mul_sub, mul_one,
     ENNReal.mul_div_cancel', ENNReal.add_sub_cancel_left]
   all_goals simp_all [ENNReal.div_eq_top]
 

Diff for: Archive/Wiedijk100Theorems/SumOfPrimeReciprocalsDiverges.lean

@@ -154,7 +154,7 @@ theorem card_le_two_pow {x k : ℕ} :
     card M₁ ≤ card (image f K) := card_le_card h
     _ ≤ card K := card_image_le
     _ ≤ 2 ^ card (image Nat.succ (range k)) := by simp only [K, card_powerset]; rfl
-    _ ≤ 2 ^ card (range k) := pow_le_pow_right one_le_two card_image_le
+    _ ≤ 2 ^ card (range k) := pow_right_mono₀ one_le_two card_image_le
     _ = 2 ^ k := by rw [card_range k]
 
 /--

Diff for: Counterexamples/SeminormLatticeNotDistrib.lean

@@ -57,14 +57,14 @@ theorem not_distrib : ¬(p ⊔ q1) ⊓ (p ⊔ q2) ≤ p ⊔ q1 ⊓ q2 := by
         4 / 3 = 4 * (1 - 2 / 3) := by norm_num
         _ ≤ 4 * (1 - x.snd) := by gcongr
         _ ≤ 4 * |1 - x.snd| := by gcongr; apply le_abs_self
-        _ = q2 ((1, 1) - x) := by simp; rfl
+        _ = q2 ((1, 1) - x) := rfl
         _ ≤ (p ⊔ q2) ((1, 1) - x) := le_sup_right
         _ ≤ (p ⊔ q1) x + (p ⊔ q2) ((1, 1) - x) := le_add_of_nonneg_left (apply_nonneg _ _)
     · calc
         4 / 3 = 2 / 3 + (1 - 1 / 3) := by norm_num
         _ ≤ x.snd + (1 - x.fst) := by gcongr
         _ ≤ |x.snd| + |1 - x.fst| := add_le_add (le_abs_self _) (le_abs_self _)
-        _ ≤ p x + p ((1, 1) - x) := by exact add_le_add le_sup_right le_sup_left
+        _ ≤ p x + p ((1, 1) - x) := add_le_add le_sup_right le_sup_left
         _ ≤ (p ⊔ q1) x + (p ⊔ q2) ((1, 1) - x) := add_le_add le_sup_left le_sup_left
   · calc
       4 / 3 = 4 * (1 / 3) := by norm_num

Diff for: Counterexamples/SorgenfreyLine.lean

@@ -141,7 +141,7 @@ theorem continuous_toReal : Continuous toReal :=
     exact inf_le_left
 
 instance : OrderClosedTopology ℝₗ :=
-  ⟨isClosed_le_prod.preimage (continuous_toReal.prod_map continuous_toReal)⟩
+  ⟨isClosed_le_prod.preimage (continuous_toReal.prodMap continuous_toReal)⟩
 
 instance : ContinuousAdd ℝₗ := by
   refine ⟨continuous_iff_continuousAt.2 ?_⟩