Merge commit '0faddd8413787a897be448e1e1b89535d92016f3' into bump/v4.6.0

.github/workflows/bors.yml

@@ -188,14 +188,17 @@ jobs:
             bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build -KCI | tee stdout.log"
 
       - name: check for noisy stdout lines
+        id: noisy
         run: |
           ! grep --after-context=1 "stdout:" stdout.log
 
       - name: build library_search cache
         run: lake build -KCI MathlibExtras
 
       - name: upload cache
-        if: always()
+        # We only upload the cache if the build ran (either succeeding or failing),
+        # but not if it was skipped.
+        if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
         run: |
           # run this in CI if it gets an incorrect lake hash for existing cache files somehow
           # lake exe cache pack! || true
@@ -217,6 +220,7 @@ jobs:
           fi
 
       - name: build archive
+        id: archive
         run: |
           # Note: we should not be including `Archive` and `Countexamples` in the cache.
           # We do this for now for the sake of not rebuilding them in every CI run
@@ -233,6 +237,7 @@ jobs:
           MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}
 
       - name: build counterexamples
+        id: counterexamples
         run: |
           lake exe cache get Counterexamples.lean
           lake build Counterexamples
@@ -291,9 +296,12 @@ jobs:
           TOKEN: ${{ secrets.LEAN_PR_TESTING }}
           GITHUB_CONTEXT: ${{ toJson(github) }}
           WORKFLOW_URL: https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}
+          BUILD_OUTCOME: ${{ steps.build.outcome }}
+          NOISY_OUTCOME: ${{ steps.noisy.outcome }}
+          ARCHIVE_OUTCOME: ${{ steps.archive.outcome }}
+          COUNTEREXAMPLE_OUTCOME: ${{ steps.counterexamples.outcome }}
           LINT_OUTCOME: ${{ steps.lint.outcome }}
           TEST_OUTCOME: ${{ steps.test.outcome }}
-          BUILD_OUTCOME: ${{ steps.build.outcome }}
           CHECK_OUTCOME: ${{ steps.lean4checker.outcome }}
         run: |
           scripts/lean-pr-testing-comments.sh

.github/workflows/build.yml

@@ -195,14 +195,17 @@ jobs:
             bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build -KCI | tee stdout.log"
 
       - name: check for noisy stdout lines
+        id: noisy
         run: |
           ! grep --after-context=1 "stdout:" stdout.log
 
       - name: build library_search cache
         run: lake build -KCI MathlibExtras
 
       - name: upload cache
-        if: always()
+        # We only upload the cache if the build ran (either succeeding or failing),
+        # but not if it was skipped.
+        if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
         run: |
           # run this in CI if it gets an incorrect lake hash for existing cache files somehow
           # lake exe cache pack! || true
@@ -224,6 +227,7 @@ jobs:
           fi
 
       - name: build archive
+        id: archive
         run: |
           # Note: we should not be including `Archive` and `Countexamples` in the cache.
           # We do this for now for the sake of not rebuilding them in every CI run
@@ -240,6 +244,7 @@ jobs:
           MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}
 
       - name: build counterexamples
+        id: counterexamples
         run: |
           lake exe cache get Counterexamples.lean
           lake build Counterexamples
@@ -298,9 +303,12 @@ jobs:
           TOKEN: ${{ secrets.LEAN_PR_TESTING }}
           GITHUB_CONTEXT: ${{ toJson(github) }}
           WORKFLOW_URL: https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}
+          BUILD_OUTCOME: ${{ steps.build.outcome }}
+          NOISY_OUTCOME: ${{ steps.noisy.outcome }}
+          ARCHIVE_OUTCOME: ${{ steps.archive.outcome }}
+          COUNTEREXAMPLE_OUTCOME: ${{ steps.counterexamples.outcome }}
           LINT_OUTCOME: ${{ steps.lint.outcome }}
           TEST_OUTCOME: ${{ steps.test.outcome }}
-          BUILD_OUTCOME: ${{ steps.build.outcome }}
           CHECK_OUTCOME: ${{ steps.lean4checker.outcome }}
         run: |
           scripts/lean-pr-testing-comments.sh

.github/workflows/build.yml.in

@@ -174,14 +174,17 @@ jobs:
             bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build -KCI | tee stdout.log"
 
       - name: check for noisy stdout lines
+        id: noisy
         run: |
           ! grep --after-context=1 "stdout:" stdout.log
 
       - name: build library_search cache
         run: lake build -KCI MathlibExtras
 
       - name: upload cache
-        if: always()
+        # We only upload the cache if the build ran (either succeeding or failing),
+        # but not if it was skipped.
+        if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
         run: |
           # run this in CI if it gets an incorrect lake hash for existing cache files somehow
           # lake exe cache pack! || true
@@ -203,6 +206,7 @@ jobs:
           fi
 
       - name: build archive
+        id: archive
         run: |
           # Note: we should not be including `Archive` and `Countexamples` in the cache.
           # We do this for now for the sake of not rebuilding them in every CI run
@@ -219,6 +223,7 @@ jobs:
           MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}
 
       - name: build counterexamples
+        id: counterexamples
         run: |
           lake exe cache get Counterexamples.lean
           lake build Counterexamples
@@ -277,9 +282,12 @@ jobs:
           TOKEN: ${{ secrets.LEAN_PR_TESTING }}
           GITHUB_CONTEXT: ${{ toJson(github) }}
           WORKFLOW_URL: https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}
+          BUILD_OUTCOME: ${{ steps.build.outcome }}
+          NOISY_OUTCOME: ${{ steps.noisy.outcome }}
+          ARCHIVE_OUTCOME: ${{ steps.archive.outcome }}
+          COUNTEREXAMPLE_OUTCOME: ${{ steps.counterexamples.outcome }}
           LINT_OUTCOME: ${{ steps.lint.outcome }}
           TEST_OUTCOME: ${{ steps.test.outcome }}
-          BUILD_OUTCOME: ${{ steps.build.outcome }}
           CHECK_OUTCOME: ${{ steps.lean4checker.outcome }}
         run: |
           scripts/lean-pr-testing-comments.sh

.github/workflows/build_fork.yml

@@ -192,14 +192,17 @@ jobs:
             bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build -KCI | tee stdout.log"
 
       - name: check for noisy stdout lines
+        id: noisy
         run: |
           ! grep --after-context=1 "stdout:" stdout.log
 
       - name: build library_search cache
         run: lake build -KCI MathlibExtras
 
       - name: upload cache
-        if: always()
+        # We only upload the cache if the build ran (either succeeding or failing),
+        # but not if it was skipped.
+        if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
         run: |
           # run this in CI if it gets an incorrect lake hash for existing cache files somehow
           # lake exe cache pack! || true
@@ -221,6 +224,7 @@ jobs:
           fi
 
       - name: build archive
+        id: archive
         run: |
           # Note: we should not be including `Archive` and `Countexamples` in the cache.
           # We do this for now for the sake of not rebuilding them in every CI run
@@ -237,6 +241,7 @@ jobs:
           MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}
 
       - name: build counterexamples
+        id: counterexamples
         run: |
           lake exe cache get Counterexamples.lean
           lake build Counterexamples
@@ -295,9 +300,12 @@ jobs:
           TOKEN: ${{ secrets.LEAN_PR_TESTING }}
           GITHUB_CONTEXT: ${{ toJson(github) }}
           WORKFLOW_URL: https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}
+          BUILD_OUTCOME: ${{ steps.build.outcome }}
+          NOISY_OUTCOME: ${{ steps.noisy.outcome }}
+          ARCHIVE_OUTCOME: ${{ steps.archive.outcome }}
+          COUNTEREXAMPLE_OUTCOME: ${{ steps.counterexamples.outcome }}
           LINT_OUTCOME: ${{ steps.lint.outcome }}
           TEST_OUTCOME: ${{ steps.test.outcome }}
-          BUILD_OUTCOME: ${{ steps.build.outcome }}
           CHECK_OUTCOME: ${{ steps.lean4checker.outcome }}
         run: |
           scripts/lean-pr-testing-comments.sh

.github/workflows/nightly_detect_failure.yml

@@ -41,7 +41,15 @@ jobs:
         if [[ $toolchain =~ leanprover/lean4:nightly-([a-zA-Z0-9_-]+) ]]; then
           version=${BASH_REMATCH[1]}
           echo "NIGHTLY=$version" >> $GITHUB_ENV
-          git push origin refs/heads/nightly-testing:refs/heads/nightly-testing-$version
+          # Check if the remote tag exists
+          if git ls-remote --tags --exit-code origin "nightly-testing-$version" >/dev/null; then
+              echo "Tag nightly-testing-$version already exists on the remote."
+          else
+              # If the tag does not exist, create and push the tag to remote
+              echo "Creating tag nightly-testing-$version from the current state of the nightly-testing branch."
+              git tag nightly-testing-$version
+              git push origin nightly-testing-$version
+          fi
         else
           echo "Error: The file lean-toolchain does not contain the expected pattern."
           exit 1

Archive/Imo/Imo2013Q1.lean

@@ -8,6 +8,7 @@ import Mathlib.Data.Nat.Parity
 import Mathlib.Algebra.BigOperators.Pi
 import Mathlib.Tactic.Ring
 import Mathlib.Tactic.FieldSimp
+import Mathlib.Tactic.Positivity.Basic
 
 #align_import imo.imo2013_q1 from "leanprover-community/mathlib"@"308826471968962c6b59c7ff82a22757386603e3"
 

Mathlib.lean

@@ -387,6 +387,7 @@ import Mathlib.Algebra.Order.Hom.Ring
 import Mathlib.Algebra.Order.Interval
 import Mathlib.Algebra.Order.Invertible
 import Mathlib.Algebra.Order.Kleene
+import Mathlib.Algebra.Order.Module.Algebra
 import Mathlib.Algebra.Order.Module.Defs
 import Mathlib.Algebra.Order.Module.OrderedSMul
 import Mathlib.Algebra.Order.Module.Pointwise
@@ -1919,6 +1920,7 @@ import Mathlib.Data.Rat.Floor
 import Mathlib.Data.Rat.Init
 import Mathlib.Data.Rat.Lemmas
 import Mathlib.Data.Rat.NNRat
+import Mathlib.Data.Rat.NNRat.BigOperators
 import Mathlib.Data.Rat.Order
 import Mathlib.Data.Rat.Sqrt
 import Mathlib.Data.Rat.Star
@@ -1980,6 +1982,7 @@ import Mathlib.Data.Set.Intervals.Monoid
 import Mathlib.Data.Set.Intervals.Monotone
 import Mathlib.Data.Set.Intervals.OrdConnected
 import Mathlib.Data.Set.Intervals.OrdConnectedComponent
+import Mathlib.Data.Set.Intervals.OrderEmbedding
 import Mathlib.Data.Set.Intervals.OrderIso
 import Mathlib.Data.Set.Intervals.Pi
 import Mathlib.Data.Set.Intervals.ProjIcc

Mathlib/Algebra/Group/Defs.lean

@@ -28,12 +28,15 @@ The file does not contain any lemmas except for
 
 For basic lemmas about these classes see `Algebra.Group.Basic`.
 
-We also introduce notation classes `lul` and `VAdd` for multiplicative and additive
+We also introduce notation classes `SMul` and `VAdd` for multiplicative and additive
 actions and register the following instances:
 
 - `Pow M ℕ`, for monoids `M`, and `Pow G ℤ` for groups `G`;
 - `SMul ℕ M` for additive monoids `M`, and `SMul ℤ G` for additive groups `G`.
 
+`SMul` is typically, but not exclusively, used for scalar multiplication-like operators.
+See the module `Algebra.AddTorsor` for a motivating example for the name `VAdd` (vector addition)`.
+
 ## Notation
 
 - `+`, `-`, `*`, `/`, `^` : the usual arithmetic operations; the underlying functions are

Mathlib/Algebra/GroupPower/CovariantClass.lean

@@ -167,6 +167,10 @@ theorem pow_left_strictMono (hn : n ≠ 0) : StrictMono (· ^ n : M → M) := st
 #align pow_strict_mono_right' pow_left_strictMono
 #align nsmul_strict_mono_left nsmul_right_strictMono
 
+@[to_additive (attr := mono, gcongr) nsmul_lt_nsmul_right]
+lemma pow_lt_pow_left' (hn : n ≠ 0) {a b : M} (hab : a < b) : a ^ n < b ^ n :=
+  pow_left_strictMono hn hab
+
 end CovariantLTSwap
 
 section CovariantLESwap

Mathlib/Algebra/Order/Interval.lean

@@ -8,7 +8,6 @@ import Mathlib.Algebra.Group.Prod
 import Mathlib.Data.Option.NAry
 import Mathlib.Data.Set.Pointwise.Basic
 import Mathlib.Order.Interval
-import Mathlib.Tactic.Positivity
 
 #align_import algebra.order.interval from "leanprover-community/mathlib"@"f0c8bf9245297a541f468be517f1bde6195105e9"
 

Mathlib/Algebra/Order/Module/Algebra.lean

@@ -0,0 +1,72 @@
+/-
+Copyright (c) 2023 Yaël Dillies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yaël Dillies
+-/
+import Mathlib.Algebra.Algebra.Basic
+import Mathlib.Algebra.Order.Module.Defs
+
+/-!
+# Ordered algebras
+
+This file proves properties of algebras where both rings are ordered compatibly.
+
+### TODO
+
+`positivity` extension for `algebraMap`
+-/
+
+variable {α β : Type*} [OrderedCommSemiring α]
+
+section OrderedSemiring
+variable (β)
+variable [OrderedSemiring β] [Algebra α β] [SMulPosMono α β] {a : α}
+
+@[mono] lemma algebraMap_mono : Monotone (algebraMap α β) :=
+  fun a₁ a₂ ha ↦ by
+    simpa only [Algebra.algebraMap_eq_smul_one] using smul_le_smul_of_nonneg_right ha zero_le_one
+
+/-- A version of `algebraMap_mono` for use by `gcongr` since it currently does not preprocess
+`Monotone` conclusions. -/
+@[gcongr] protected lemma GCongr.algebraMap_le_algebraMap {a₁ a₂ : α} (ha : a₁ ≤ a₂) :
+    algebraMap α β a₁ ≤ algebraMap α β a₂ := algebraMap_mono _ ha
+
+lemma algebraMap_nonneg (ha : 0 ≤ a) : 0 ≤ algebraMap α β a := by simpa using algebraMap_mono β ha
+
+end OrderedSemiring
+
+section StrictOrderedSemiring
+variable [StrictOrderedSemiring β] [Algebra α β]
+
+section SMulPosMono
+variable [SMulPosMono α β] [SMulPosReflectLE α β] {a₁ a₂ : α}
+
+@[simp] lemma algebraMap_le_algebraMap : algebraMap α β a₁ ≤ algebraMap α β a₂ ↔ a₁ ≤ a₂ := by
+  simp [Algebra.algebraMap_eq_smul_one]
+
+end SMulPosMono
+
+section SMulPosStrictMono
+variable [SMulPosStrictMono α β] {a a₁ a₂ : α}
+variable (β)
+
+@[mono] lemma algebraMap_strictMono : StrictMono (algebraMap α β) :=
+  fun a₁ a₂ ha ↦ by
+    simpa only [Algebra.algebraMap_eq_smul_one] using smul_lt_smul_of_pos_right ha zero_lt_one
+
+/-- A version of `algebraMap_strictMono` for use by `gcongr` since it currently does not preprocess
+`Monotone` conclusions. -/
+@[gcongr] protected lemma GCongr.algebraMap_lt_algebraMap {a₁ a₂ : α} (ha : a₁ < a₂) :
+    algebraMap α β a₁ < algebraMap α β a₂ := algebraMap_strictMono _ ha
+
+lemma algebraMap_pos (ha : 0 < a) : 0 < algebraMap α β a := by
+  simpa using algebraMap_strictMono β ha
+
+variable {β}
+variable [SMulPosReflectLT α β]
+
+@[simp] lemma algebraMap_lt_algebraMap : algebraMap α β a₁ < algebraMap α β a₂ ↔ a₁ < a₂ := by
+  simp [Algebra.algebraMap_eq_smul_one]
+
+end SMulPosStrictMono
+end StrictOrderedSemiring

Mathlib/Algebra/Order/Module/Defs.lean

@@ -1123,6 +1123,26 @@ lemma SMulPosReflectLT.lift [SMulPosReflectLT α γ] : SMulPosReflectLT α β wh
 
 end Lift
 
+section Nat
+
+instance OrderedSemiring.toPosSMulMonoNat [OrderedSemiring α] : PosSMulMono ℕ α where
+  elim _n _ _a _b hab := nsmul_le_nsmul_right hab _
+
+instance OrderedSemiring.toSMulPosMonoNat [OrderedSemiring α] : SMulPosMono ℕ α where
+  elim _a ha _m _n hmn := nsmul_le_nsmul_left ha hmn
+
+instance StrictOrderedSemiring.toPosSMulStrictMonoNat [StrictOrderedSemiring α] :
+    PosSMulStrictMono ℕ α where
+  elim _n hn _a _b hab := nsmul_right_strictMono hn.ne' hab
+
+instance StrictOrderedSemiring.toSMulPosStrictMonoNat [StrictOrderedSemiring α] :
+    SMulPosStrictMono ℕ α where
+  elim _a ha _m _n hmn := nsmul_lt_nsmul_left ha hmn
+
+end Nat
+
+-- TODO: Instances for `Int` and `Rat`
+
 namespace Mathlib.Meta.Positivity
 section OrderedSMul
 variable [Zero α] [Zero β] [SMulZeroClass α β] [Preorder α] [Preorder β] [PosSMulMono α β] {a : α}

Mathlib/Algebra/Order/Module/OrderedSMul.lean

@@ -9,7 +9,6 @@ import Mathlib.Algebra.Order.Module.Defs
 import Mathlib.Algebra.Order.Monoid.Prod
 import Mathlib.Algebra.Order.Pi
 import Mathlib.Tactic.GCongr.Core
-import Mathlib.Tactic.Positivity
 
 #align_import algebra.order.smul from "leanprover-community/mathlib"@"3ba15165bd6927679be7c22d6091a87337e3cd0c"
 

Mathlib/Algebra/Order/Pi.lean

@@ -5,7 +5,6 @@ Authors: Simon Hudon, Patrick Massot
 -/
 import Mathlib.Algebra.Order.Ring.Defs
 import Mathlib.Algebra.Ring.Pi
-import Mathlib.Tactic.Positivity
 
 #align_import algebra.order.pi from "leanprover-community/mathlib"@"422e70f7ce183d2900c586a8cda8381e788a0c62"