Merge remote-tracking branch 'origin/master' into SG_faa1

.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}"

.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.')

.vscode/deprecated-alias.code-snippets → .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",

Archive/Examples/IfNormalization/WithoutAesop.lean

@@ -92,8 +92,8 @@ def normalize' (l : AList (fun _ : ℕ => Bool)) :
               · simp_all
         · have := ht₃ v
           have := he₃ v
-          simp_all? says simp_all only [normalized, Bool.and_eq_true, Bool.not_eq_true',
-              AList.lookup_insert_eq_none, ne_eq, AList.lookup_insert]
+          simp_all? says simp_all only [normalized, Bool.and_eq_true, Bool.not_eq_eq_eq_not,
+              Bool.not_true, AList.lookup_insert_eq_none, ne_eq, AList.lookup_insert]
           obtain ⟨⟨⟨tn, tc⟩, tr⟩, td⟩ := ht₂
           split <;> rename_i h'
           · subst h'
@@ -103,9 +103,9 @@ def normalize' (l : AList (fun _ : ℕ => Bool)) :
           have := he₃ w
           by_cases h : w = v
           · subst h; simp_all
-          · simp_all? says simp_all only [normalized, Bool.and_eq_true, Bool.not_eq_true',
-              AList.lookup_insert_eq_none, ne_eq, not_false_eq_true, AList.lookup_insert_ne,
-              implies_true]
+          · simp_all? says simp_all only [normalized, Bool.and_eq_true, Bool.not_eq_eq_eq_not,
+              Bool.not_true, AList.lookup_insert_eq_none, ne_eq, not_false_eq_true,
+              AList.lookup_insert_ne, implies_true]
             obtain ⟨⟨⟨en, ec⟩, er⟩, ed⟩ := he₂
             split at b <;> rename_i h'
             · subst h'; simp_all

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

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

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) :

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

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
 

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

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
 
 /-!

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]
 

Cache/IO.lean

@@ -338,7 +338,7 @@ def packCache (hashMap : HashMap) (overwrite verbose unpackedOnly : Bool)
 /-- Gets the set of all cached files -/
 def getLocalCacheSet : IO <| Lean.RBTree String compare := do
   let paths ← getFilesWithExtension CACHEDIR "ltar"
-  return .fromList (paths.data.map (·.withoutParent CACHEDIR |>.toString)) _
+  return .fromList (paths.toList.map (·.withoutParent CACHEDIR |>.toString)) _
 
 def isPathFromMathlib (path : FilePath) : Bool :=
   match path.components with

Cache/Requests.lean

@@ -184,7 +184,7 @@ def UPLOAD_URL : String :=
 /-- Formats the config file for `curl`, containing the list of files to be uploaded -/
 def mkPutConfigContent (fileNames : Array String) (token : String) : IO String := do
   let token := if useFROCache then "" else s!"?{token}" -- the FRO cache doesn't pass the token here
-  let l ← fileNames.data.mapM fun fileName : String => do
+  let l ← fileNames.toList.mapM fun fileName : String => do
     pure s!"-T {(IO.CACHEDIR / fileName).toString}\nurl = {mkFileURL UPLOAD_URL fileName}{token}"
   return "\n".intercalate l
 

Counterexamples/Phillips.lean

@@ -6,7 +6,7 @@ Authors: Sébastien Gouëzel
 import Mathlib.Analysis.NormedSpace.HahnBanach.Extension
 import Mathlib.MeasureTheory.Integral.SetIntegral
 import Mathlib.MeasureTheory.Measure.Lebesgue.Basic
-import Mathlib.Topology.ContinuousFunction.Bounded
+import Mathlib.Topology.ContinuousMap.Bounded
 
 /-!
 # A counterexample on Pettis integrability

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