Merge branch 'master' into MR-charts-diffeos2

.github/workflows/bors.yml

@@ -200,10 +200,12 @@ jobs:
         # but not if it was skipped.
         if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
         run: |
+          # TODO: this is not doing anything currently, and needs to be integrated with put-unpacked
+          # lake exe cache commit || true
           # run this in CI if it gets an incorrect lake hash for existing cache files somehow
-          # lake exe cache pack! || true
-          lake exe cache commit || true
-          lake exe cache put || true
+          # lake exe cache put!
+          # do not try to upload files just downloaded
+          lake exe cache put-unpacked
         env:
           MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
           MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}

.github/workflows/build.yml

@@ -207,10 +207,12 @@ jobs:
         # but not if it was skipped.
         if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
         run: |
+          # TODO: this is not doing anything currently, and needs to be integrated with put-unpacked
+          # lake exe cache commit || true
           # run this in CI if it gets an incorrect lake hash for existing cache files somehow
-          # lake exe cache pack! || true
-          lake exe cache commit || true
-          lake exe cache put || true
+          # lake exe cache put!
+          # do not try to upload files just downloaded
+          lake exe cache put-unpacked
         env:
           MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
           MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}

.github/workflows/build.yml.in

@@ -186,10 +186,12 @@ jobs:
         # but not if it was skipped.
         if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
         run: |
+          # TODO: this is not doing anything currently, and needs to be integrated with put-unpacked
+          # lake exe cache commit || true
           # run this in CI if it gets an incorrect lake hash for existing cache files somehow
-          # lake exe cache pack! || true
-          lake exe cache commit || true
-          lake exe cache put || true
+          # lake exe cache put!
+          # do not try to upload files just downloaded
+          lake exe cache put-unpacked
         env:
           MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
           MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}

.github/workflows/build_fork.yml

@@ -204,10 +204,12 @@ jobs:
         # but not if it was skipped.
         if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
         run: |
+          # TODO: this is not doing anything currently, and needs to be integrated with put-unpacked
+          # lake exe cache commit || true
           # run this in CI if it gets an incorrect lake hash for existing cache files somehow
-          # lake exe cache pack! || true
-          lake exe cache commit || true
-          lake exe cache put || true
+          # lake exe cache put!
+          # do not try to upload files just downloaded
+          lake exe cache put-unpacked
         env:
           MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
           MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}

.vscode/settings.json

@@ -10,5 +10,9 @@
   "githubPullRequests.ignoredPullRequestBranches": [
     "master"
   ],
-  "git.ignoreLimitWarning": true
+  "git.ignoreLimitWarning": true,
+  "files.readonlyInclude": {
+    "**/.elan/**": true,
+    "**/.lake/**": true
+  }
 }

Archive/Examples/IfNormalization/Statement.lean

@@ -89,7 +89,7 @@ def normalized (e : IfExpr) : Bool :=
   !e.hasNestedIf && !e.hasConstantIf && !e.hasRedundantIf && e.disjoint
 
 /--
-The evaluation of an if expresssion at some assignment of variables.
+The evaluation of an if expression at some assignment of variables.
 -/
 def eval (f : Nat → Bool) : IfExpr → Bool
   | lit b => b

Archive/Hairer.lean

@@ -95,7 +95,7 @@ lemma inj_L : Injective (L ι) :=
   (injective_iff_map_eq_zero _).mpr fun p hp ↦ by
     have H : ∀ᵐ x : EuclideanSpace ℝ ι, x ∈ ball 0 1 → eval x p = 0 :=
       isOpen_ball.ae_eq_zero_of_integral_contDiff_smul_eq_zero
-        (by exact continuous_eval p |>.locallyIntegrable.locallyIntegrableOn _)
+        (continuous_eval p |>.locallyIntegrable.locallyIntegrableOn _)
         fun g hg _h2g g_supp ↦ by
           simpa [mul_comm (g _), L] using congr($hp ⟨g, g_supp.trans ball_subset_closedBall, hg⟩)
     simp_rw [MvPolynomial.funext_iff, map_zero]

Archive/Imo/Imo1960Q1.lean

@@ -95,20 +95,15 @@ theorem right_direction {n : ℕ} : ProblemPredicate n → SolutionPredicate n :
   iterate 82
     replace :=
       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)
+        (by norm_num <;> decide)
   exact searchUpTo_end this
 #align imo1960_q1.right_direction Imo1960Q1.right_direction
 
 /-
 Now we just need to prove the equivalence, for the precise problem statement.
 -/
 theorem left_direction (n : ℕ) (spn : SolutionPredicate n) : ProblemPredicate n := by
-  -- Porting note: This is very slow
-  rcases spn with (rfl | rfl) <;> refine' ⟨_, by decide, _⟩ <;> rfl
+  rcases spn with (rfl | rfl) <;> refine' ⟨_, by decide, _⟩ <;> norm_num <;> rfl
 #align imo1960_q1.left_direction Imo1960Q1.left_direction
 
 end Imo1960Q1

Archive/Imo/Imo1962Q1.lean

@@ -130,17 +130,7 @@ Now we combine these cases to show that 153846 is the smallest solution.
 
 
 theorem satisfied_by_153846 : ProblemPredicate 153846 := by
-  -- 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
+  norm_num [ProblemPredicate]
   decide
 #align imo1962_q1.satisfied_by_153846 Imo1962Q1.satisfied_by_153846
 

Archive/Imo/Imo1981Q3.lean

@@ -149,7 +149,7 @@ variable {K : ℕ} (HK : N < fib K + fib (K + 1)) {N}
 theorem m_n_bounds {m n : ℕ} (h1 : NatPredicate N m n) : m ≤ fib K ∧ n ≤ fib (K + 1) := by
   obtain ⟨k : ℕ, hm : m = fib k, hn : n = fib (k + 1)⟩ := h1.imp_fib m
   by_cases h2 : k < K + 1
-  · have h3 : k ≤ K := lt_succ_iff.mp h2
+  · have h3 : k ≤ K := Nat.lt_succ_iff.mp h2
     constructor
     · calc
         m = fib k := hm

Archive/Imo/Imo1986Q5.lean

@@ -71,7 +71,7 @@ theorem isGood_iff {f : ℝ≥0 → ℝ≥0} : IsGood f ↔ f = fun x ↦ 2 / (2
   rintro rfl
   constructor
   case map_two => simp
-  case map_ne_zero => intro x hx; simpa
+  case map_ne_zero => intro x hx; simpa [tsub_eq_zero_iff_le]
   case map_add_rev =>
     intro x y
     cases lt_or_le y 2 with

Archive/Imo/Imo2008Q2.lean

@@ -3,6 +3,7 @@ Copyright (c) 2021 Manuel Candales. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Manuel Candales
 -/
+import Mathlib.Algebra.Parity
 import Mathlib.Data.Real.Basic
 import Mathlib.Data.Set.Finite
 import Mathlib.Tactic.FieldSimp

Archive/MiuLanguage/DecisionSuf.lean

@@ -158,7 +158,7 @@ private theorem le_pow2_and_pow2_eq_mod3' (c : ℕ) (x : ℕ) (h : c = 1 ∨ c =
   refine' ⟨g + 2, _, _⟩
   · rw [mul_succ, ← add_assoc, pow_add]
     change c + 3 * k + 3 ≤ 2 ^ g * (1 + 3); rw [mul_add (2 ^ g) 1 3, mul_one]
-    linarith [hkg, one_le_two_pow g]
+    linarith [hkg, @Nat.one_le_two_pow g]
   · rw [pow_add, ← mul_one c]
     exact ModEq.mul hgmod rfl
 

Archive/Wiedijk100Theorems/FriendshipGraphs.lean

@@ -178,7 +178,7 @@ theorem isRegularOf_not_existsPolitician (hG' : ¬ExistsPolitician G) :
   This essentially means that the graph has `d ^ 2 - d + 1` vertices. -/
 theorem card_of_regular (hd : G.IsRegularOfDegree d) : d + (Fintype.card V - 1) = d * d := by
   have v := Classical.arbitrary V
-  trans (G.adjMatrix ℕ ^ 2).mulVec (fun _ => 1) v
+  trans ((G.adjMatrix ℕ ^ 2) *ᵥ (fun _ => 1)) v
   · rw [adjMatrix_sq_of_regular hG hd, mulVec, dotProduct, ← insert_erase (mem_univ v)]
     simp only [sum_insert, mul_one, if_true, Nat.cast_id, eq_self_iff_true, mem_erase, not_true,
       Ne.def, not_false_iff, add_right_inj, false_and_iff, of_apply]

Archive/Wiedijk100Theorems/PerfectNumbers.lean

@@ -37,7 +37,7 @@ theorem odd_mersenne_succ (k : ℕ) : ¬2 ∣ mersenne (k + 1) := by
 
 namespace Nat
 
-open Nat.ArithmeticFunction Finset
+open ArithmeticFunction Finset
 
 theorem sigma_two_pow_eq_mersenne_succ (k : ℕ) : σ 1 (2 ^ k) = mersenne (k + 1) := by
   simp_rw [sigma_one_apply, mersenne, show 2 = 1 + 1 from rfl, ← geom_sum_mul_add 1 (k + 1)]

Cache/IO.lean

@@ -290,7 +290,8 @@ def allExist (paths : List (FilePath × Bool)) : IO Bool := do
   pure true
 
 /-- Compresses build files into the local cache and returns an array with the compressed files -/
-def packCache (hashMap : HashMap) (overwrite verbose : Bool) (comment : Option String := none) :
+def packCache (hashMap : HashMap) (overwrite verbose unpackedOnly : Bool)
+    (comment : Option String := none) :
     IO <| Array String := do
   mkDir CACHEDIR
   IO.println "Compressing cache"
@@ -302,14 +303,16 @@ def packCache (hashMap : HashMap) (overwrite verbose : Bool) (comment : Option S
     let buildPaths ← mkBuildPaths path
     if ← allExist buildPaths then
       if overwrite || !(← zipPath.pathExists) then
+        acc := acc.push (path, zip)
         tasks := tasks.push <| ← IO.asTask do
           -- Note here we require that the `.trace` file is first
           -- in the list generated by `mkBuildPaths`.
           let trace :: args := (← buildPaths.filterM (·.1.pathExists)) |>.map (·.1.toString)
             | unreachable!
           runCmd (← getLeanTar) <| #[zipPath.toString, trace] ++
             (if let some c := comment then #["-c", s!"git=mathlib4@{c}"] else #[]) ++ args
-      acc := acc.push (path, zip)
+      else if !unpackedOnly then
+        acc := acc.push (path, zip)
   for task in tasks do
     _ ← IO.ofExcept task.get
   acc := acc.qsort (·.1.1 < ·.1.1)

Cache/Main.lean

@@ -25,6 +25,7 @@ Commands:
   # Privilege required
   put          Run 'mk' then upload linked files missing on the server
   put!         Run 'mk' then upload all linked files
+  put-unpacked 'put' only files not already 'pack'ed; intended for CI use
   commit       Write a commit on the server
   commit!      Overwrite a commit on the server
   collect      TODO
@@ -57,7 +58,7 @@ def toPaths (args : List String) : List FilePath :=
       mkFilePath (arg.toName.components.map Name.toString) |>.withExtension "lean"
 
 def curlArgs : List String :=
-  ["get", "get!", "get-", "put", "put!", "commit", "commit!"]
+  ["get", "get!", "get-", "put", "put!", "put-unpacked", "commit", "commit!"]
 
 def leanTarArgs : List String :=
   ["get", "get!", "pack", "pack!", "unpack", "lookup"]
@@ -76,26 +77,28 @@ def main (args : List String) : IO Unit := do
   let hashMap := hashMemo.hashMap
   let goodCurl ← pure !curlArgs.contains (args.headD "") <||> validateCurl
   if leanTarArgs.contains (args.headD "") then validateLeanTar
+  let get (args : List String) (force := false) (decompress := true) := do
+    let hashMap ← if args.isEmpty then pure hashMap else hashMemo.filterByFilePaths (toPaths args)
+    getFiles hashMap force force goodCurl decompress
+  let pack (overwrite verbose unpackedOnly := false) := do
+    packCache hashMap overwrite verbose unpackedOnly (← getGitCommitHash)
+  let put (overwrite unpackedOnly := false) := do
+    putFiles (← pack overwrite (verbose := true) unpackedOnly) overwrite (← getToken)
   match args with
-  | ["get"] => getFiles hashMap false false goodCurl true
-  | ["get!"] => getFiles hashMap true true goodCurl true
-  | ["get-"] => getFiles hashMap false false goodCurl false
-  | "get"  :: args =>
-    getFiles (← hashMemo.filterByFilePaths (toPaths args)) false false goodCurl true
-  | "get!" :: args =>
-    getFiles (← hashMemo.filterByFilePaths (toPaths args)) true true goodCurl true
-  | "get-" :: args =>
-    getFiles (← hashMemo.filterByFilePaths (toPaths args)) false false goodCurl false
-  | ["pack"] => discard <| packCache hashMap false false (← getGitCommitHash)
-  | ["pack!"] => discard <| packCache hashMap true false (← getGitCommitHash)
+  | "get"  :: args => get args
+  | "get!" :: args => get args (force := true)
+  | "get-" :: args => get args (decompress := false)
+  | ["pack"] => discard <| pack
+  | ["pack!"] => discard <| pack (overwrite := true)
   | ["unpack"] => unpackCache hashMap false
   | ["unpack!"] => unpackCache hashMap true
   | ["clean"] =>
     cleanCache <| hashMap.fold (fun acc _ hash => acc.insert <| CACHEDIR / hash.asLTar) .empty
   | ["clean!"] => cleanCache
-  -- We allow arguments for `put` and `put!` so they can be added to the `roots`.
-  | "put" :: _ => putFiles (← packCache hashMap false true (← getGitCommitHash)) false (← getToken)
-  | "put!" :: _ => putFiles (← packCache hashMap false true (← getGitCommitHash)) true (← getToken)
+  -- We allow arguments for `put*` so they can be added to the `roots`.
+  | "put" :: _ => put
+  | "put!" :: _ => put (overwrite := true)
+  | "put-unpacked" :: _ => put (unpackedOnly := true)
   | ["commit"] =>
     if !(← isGitStatusClean) then IO.println "Please commit your changes first" return else
     commit hashMap false (← getToken)

Counterexamples/SeminormLatticeNotDistrib.lean

@@ -65,7 +65,7 @@ theorem not_distrib : ¬(p ⊔ q1) ⊓ (p ⊔ q2) ≤ p ⊔ q1 ⊓ q2 := by
         _ ≤ 4 * |1 - x.snd| := by gcongr; apply le_abs_self
         _ = q2 ((1, 1) - x) := by simp; rfl
         _ ≤ (p ⊔ q2) ((1, 1) - x) := le_sup_right
-        _ ≤ (p ⊔ q1) x + (p ⊔ q2) ((1, 1) - x) := le_add_of_nonneg_left (map_nonneg _ _)
+        _ ≤ (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
@@ -78,7 +78,7 @@ theorem not_distrib : ¬(p ⊔ q1) ⊓ (p ⊔ q2) ≤ p ⊔ q1 ⊓ q2 := by
       _ ≤ 4 * |x.fst| := by gcongr; apply le_abs_self
       _ = q1 x := rfl
       _ ≤ (p ⊔ q1) x := le_sup_right
-      _ ≤ (p ⊔ q1) x + (p ⊔ q2) ((1, 1) - x) := le_add_of_nonneg_right (map_nonneg _ _)
+      _ ≤ (p ⊔ q1) x + (p ⊔ q2) ((1, 1) - x) := le_add_of_nonneg_right (apply_nonneg _ _)
 #align counterexample.seminorm_not_distrib.not_distrib Counterexample.SeminormNotDistrib.not_distrib
 
 end SeminormNotDistrib