Merge remote-tracking branch 'upstream/master' into reducible-convert

Author: Vierkantor

.github/actions/get-mathlib-ci/action.yml

@@ -10,7 +10,7 @@ inputs:
     # Default pinned commit used by workflows unless they explicitly override.
     # Update this ref as needed to pick up changes to mathlib-ci scripts
     # This is also updated automatically by .github/workflows/update_dependencies.yml
-    default: 455d84939bba1fbe157ff2c1469a0c258372d05c
+    default: 78f34ded6a5f5aa11ea5b7c3120fe5d8422db1da
   path:
     description: Checkout destination path.
     required: false

.github/workflows/shake.yaml

@@ -35,10 +35,14 @@ jobs:
           use-github-cache: false
           use-mathlib-cache: true
 
+      - name: lake build
+        run: |
+          lake build Mathlib Archive Counterexamples
+
       - name: lake shake
         id: shake
         run: |
-          lake shake --add-public --keep-implied --keep-prefix --fix --explain > explain.txt 2>&1
+          lake shake --add-public --keep-implied --keep-prefix --fix --explain Mathlib Archive Counterexamples > explain.txt 2>&1
           if git diff --quiet; then
             echo "changed=false" >> "$GITHUB_OUTPUT"
           else
@@ -53,12 +57,17 @@ jobs:
 
       - name: Upload explain.txt
         id: upload-artifact
-        if: steps.shake.outputs.changed == 'true'
+        if: failure() || steps.shake.outputs.changed == 'true'
         uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4.6.2
         with:
           name: shake-explain
           path: explain.txt
 
+      - name: Cleanup explain.txt
+        if: steps.shake.outputs.changed == 'true'
+        run: |
+          rm -f explain.txt
+
       - name: Build PR body
         id: pr_body
         if: steps.shake.outputs.changed == 'true' && toJson(inputs.dry_run) != 'true'
@@ -118,7 +127,7 @@ jobs:
           api-key: ${{ secrets.ZULIP_API_KEY }}
           email: 'github-mathlib4-bot@leanprover.zulipchat.com'
           organization-url: 'https://leanprover.zulipchat.com'
-          to: 'nightly-testing'
+          to: 'nightly-testing-mathlib'
           type: 'stream'
           topic: 'Mathlib `shake --fix`'
           content: |

Mathlib/Data/DFinsupp/Interval.lean

@@ -182,20 +182,19 @@ lemma card_uIcc : #(uIcc f g) = ∏ i ∈ f.support ∪ g.support, #(uIcc (f i)
 
 end Lattice
 
-section CanonicallyOrdered
+section IsBotZeroClass
 
 variable [DecidableEq ι] [∀ i, DecidableEq (α i)]
-variable [∀ i, AddCommMonoid (α i)] [∀ i, PartialOrder (α i)] [∀ i, CanonicallyOrderedAdd (α i)]
+variable [∀ i, AddCommMonoid (α i)] [∀ i, PartialOrder (α i)] [∀ i, IsBotZeroClass (α i)]
   [∀ i, OrderBot (α i)] [∀ i, LocallyFiniteOrder (α i)]
 variable (f : Π₀ i, α i)
 
 lemma card_Iic : #(Iic f) = ∏ i ∈ f.support, #(Iic (f i)) := by
-  simp_rw [Iic_eq_Icc, card_Icc, DFinsupp.bot_eq_zero, support_zero, empty_union, zero_apply,
-    bot_eq_zero]
+  simp [Iic_eq_Icc, card_Icc, bot_eq_zero]
 
 lemma card_Iio : #(Iio f) = (∏ i ∈ f.support, #(Iic (f i))) - 1 := by
   rw [card_Iio_eq_card_Iic_sub_one, card_Iic]
 
-end CanonicallyOrdered
+end IsBotZeroClass
 
 end DFinsupp

Mathlib/Data/DFinsupp/Lex.lean

@@ -259,17 +259,27 @@ section OrderedAddMonoid
 variable [LinearOrder ι]
 
 instance Lex.orderBot [∀ i, AddCommMonoid (α i)] [∀ i, PartialOrder (α i)]
-    [∀ i, CanonicallyOrderedAdd (α i)] :
+    [∀ i, IsBotZeroClass (α i)] :
     OrderBot (Lex (Π₀ i, α i)) where
   bot := 0
   bot_le _ := DFinsupp.toLex_monotone bot_le
 
+instance Lex.isBotZeroClass [∀ i, AddCommMonoid (α i)] [∀ i, PartialOrder (α i)]
+    [∀ i, IsBotZeroClass (α i)] :
+    IsBotZeroClass (Lex (Π₀ i, α i)) where
+  isBot_zero := isBot_bot
+
 instance Colex.orderBot [∀ i, AddCommMonoid (α i)] [∀ i, PartialOrder (α i)]
-    [∀ i, CanonicallyOrderedAdd (α i)] :
+    [∀ i, IsBotZeroClass (α i)] :
     OrderBot (Colex (Π₀ i, α i)) where
   bot := 0
   bot_le _ := DFinsupp.toColex_monotone bot_le
 
+instance Colex.isBotZeroClass [∀ i, AddCommMonoid (α i)] [∀ i, PartialOrder (α i)]
+    [∀ i, IsBotZeroClass (α i)] :
+    IsBotZeroClass (Colex (Π₀ i, α i)) where
+  isBot_zero := isBot_bot
+
 instance Lex.isOrderedCancelAddMonoid [∀ i, AddCommMonoid (α i)] [∀ i, PartialOrder (α i)]
     [∀ i, IsOrderedCancelAddMonoid (α i)] :
     IsOrderedCancelAddMonoid (Lex (Π₀ i, α i)) where

Mathlib/Data/DFinsupp/Order.lean

@@ -189,17 +189,23 @@ end Module
 
 section PartialOrder
 
-variable (α) [∀ i, AddCommMonoid (α i)] [∀ i, PartialOrder (α i)] [∀ i, CanonicallyOrderedAdd (α i)]
+variable (α) [∀ i, AddCommMonoid (α i)] [∀ i, PartialOrder (α i)]
 
-instance : OrderBot (Π₀ i, α i) where
+instance [∀ i, IsBotZeroClass (α i)] : OrderBot (Π₀ i, α i) where
   bot := 0
-  bot_le := by simp only [le_def, coe_zero, Pi.zero_apply, imp_true_iff, zero_le]
+  bot_le := by simp [le_def]
+
+instance [∀ i, IsBotZeroClass (α i)] : IsBotZeroClass (Π₀ i, α i) where
+  isBot_zero := isBot_bot
 
 variable {α}
 
-protected theorem bot_eq_zero : (⊥ : Π₀ i, α i) = 0 :=
+@[deprecated _root_.bot_eq_zero (since := "2026-05-07")]
+protected theorem bot_eq_zero [∀ i, IsBotZeroClass (α i)] : (⊥ : Π₀ i, α i) = 0 :=
   rfl
 
+variable [∀ i, CanonicallyOrderedAdd (α i)]
+
 @[simp]
 theorem add_eq_zero_iff (f g : Π₀ i, α i) : f + g = 0 ↔ f = 0 ∧ g = 0 := by
   simp [DFunLike.ext_iff, forall_and]
@@ -289,25 +295,21 @@ theorem subset_support_tsub : f.support \ g.support ⊆ (f - g).support := by
 end PartialOrder
 
 section LinearOrder
-variable [∀ i, AddCommMonoid (α i)] [∀ i, LinearOrder (α i)] [∀ i, CanonicallyOrderedAdd (α i)]
+variable [∀ i, AddCommMonoid (α i)] [∀ i, LinearOrder (α i)] [∀ i, IsBotZeroClass (α i)]
   [DecidableEq ι] {f g : Π₀ i, α i}
 
 @[simp]
 theorem support_inf : (f ⊓ g).support = f.support ∩ g.support := by
   ext
-  simp only [inf_apply, mem_support_iff, Ne, Finset.mem_inter]
-  simp only [← nonpos_iff_eq_zero, min_le_iff, not_or]
+  simp
 
 @[simp]
 theorem support_sup : (f ⊔ g).support = f.support ∪ g.support := by
   ext
-  simp only [Finset.mem_union, mem_support_iff, sup_apply, Ne, ← nonpos_iff_eq_zero, sup_le_iff,
-    Classical.not_and_iff_not_or_not]
+  simp [imp_iff_not_or]
 
 nonrec theorem disjoint_iff : Disjoint f g ↔ Disjoint f.support g.support := by
-  rw [disjoint_iff, disjoint_iff, DFinsupp.bot_eq_zero, ← DFinsupp.support_eq_empty,
-    DFinsupp.support_inf]
-  rfl
+  simp [disjoint_iff, bot_eq_zero, ← DFinsupp.support_eq_empty]
 
 end LinearOrder
 

Mathlib/Data/DFinsupp/WellFounded.lean

@@ -168,13 +168,13 @@ theorem Lex.wellFounded' (hbot : ∀ ⦃i a⦄, ¬s i a 0) (hs : ∀ i, WellFoun
 end Zero
 
 instance Lex.wellFoundedLT [LT ι] [@Std.Trichotomous ι (· < ·)] [hι : WellFoundedGT ι]
-    [∀ i, AddMonoid (α i)] [∀ i, PartialOrder (α i)] [∀ i, CanonicallyOrderedAdd (α i)]
+    [∀ i, AddMonoid (α i)] [∀ i, PartialOrder (α i)] [∀ i, IsBotZeroClass (α i)]
     [hα : ∀ i, WellFoundedLT (α i)] :
     WellFoundedLT (Lex (Π₀ i, α i)) :=
   ⟨Lex.wellFounded' (fun _ _ => not_lt_zero) (fun i => (hα i).wf) hι.wf⟩
 
 instance Colex.wellFoundedLT [LT ι] [@Std.Trichotomous ι (· < ·)] [WellFoundedLT ι]
-    [∀ i, AddMonoid (α i)] [∀ i, PartialOrder (α i)] [∀ i, CanonicallyOrderedAdd (α i)]
+    [∀ i, AddMonoid (α i)] [∀ i, PartialOrder (α i)] [∀ i, IsBotZeroClass (α i)]
     [∀ i, WellFoundedLT (α i)] :
     WellFoundedLT (Colex (Π₀ i, α i)) :=
   Lex.wellFoundedLT (ι := ιᵒᵈ)
@@ -237,7 +237,7 @@ protected theorem DFinsupp.wellFoundedLT [∀ i, Zero (α i)] [∀ i, Preorder (
     exact ⟨i, fun j hj ↦ Quot.sound (he j hj), hl⟩⟩
 
 instance DFinsupp.wellFoundedLT'
-    [∀ i, AddMonoid (α i)] [∀ i, PartialOrder (α i)] [∀ i, CanonicallyOrderedAdd (α i)]
+    [∀ i, AddMonoid (α i)] [∀ i, PartialOrder (α i)] [∀ i, IsBotZeroClass (α i)]
     [∀ i, WellFoundedLT (α i)] : WellFoundedLT (Π₀ i, α i) :=
   DFinsupp.wellFoundedLT fun _ _ => not_lt_zero
 

Mathlib/Data/Finsupp/Interval.lean

@@ -119,19 +119,18 @@ theorem card_uIcc :
 
 end Lattice
 
-section CanonicallyOrdered
+section IsBotZeroClass
 
-variable [AddCommMonoid α] [PartialOrder α] [CanonicallyOrderedAdd α]
+variable [AddCommMonoid α] [PartialOrder α] [IsBotZeroClass α]
   [OrderBot α] [LocallyFiniteOrder α]
 variable [DecidableEq ι] [DecidableEq α] (f : ι →₀ α)
 
 theorem card_Iic : #(Iic f) = ∏ i ∈ f.support, #(Iic (f i)) := by
-  classical simp_rw [Iic_eq_Icc, card_Icc, Finsupp.bot_eq_zero, support_zero, empty_union,
-      zero_apply, bot_eq_zero]
+  classical simp [Iic_eq_Icc, card_Icc, bot_eq_zero]
 
 theorem card_Iio : #(Iio f) = ∏ i ∈ f.support, #(Iic (f i)) - 1 := by
   rw [card_Iio_eq_card_Iic_sub_one, card_Iic]
 
-end CanonicallyOrdered
+end IsBotZeroClass
 
 end Finsupp

Mathlib/Data/Finsupp/Lex.lean

@@ -226,16 +226,24 @@ section OrderedAddMonoid
 
 variable [LinearOrder α]
 
-instance Lex.orderBot [AddCommMonoid N] [PartialOrder N] [CanonicallyOrderedAdd N] :
+instance Lex.orderBot [AddCommMonoid N] [PartialOrder N] [IsBotZeroClass N] :
     OrderBot (Lex (α →₀ N)) where
   bot := 0
   bot_le _ := Finsupp.toLex_monotone bot_le
 
-instance Colex.orderBot [AddCommMonoid N] [PartialOrder N] [CanonicallyOrderedAdd N] :
+instance Lex.isBotZeroClass [AddCommMonoid N] [PartialOrder N] [IsBotZeroClass N] :
+    IsBotZeroClass (Lex (α →₀ N)) where
+  isBot_zero := isBot_bot
+
+instance Colex.orderBot [AddCommMonoid N] [PartialOrder N] [IsBotZeroClass N] :
     OrderBot (Colex (α →₀ N)) where
   bot := 0
   bot_le _ := Finsupp.toColex_monotone bot_le
 
+instance Colex.isBotZeroClass [AddCommMonoid N] [PartialOrder N] [IsBotZeroClass N] :
+    IsBotZeroClass (Colex (α →₀ N)) where
+  isBot_zero := isBot_bot
+
 instance Lex.isOrderedCancelAddMonoid
     [AddCommMonoid N] [PartialOrder N] [IsOrderedCancelAddMonoid N] :
     IsOrderedCancelAddMonoid (Lex (α →₀ N)) where

Mathlib/Data/Finsupp/Order.lean

@@ -209,15 +209,21 @@ end SMulWithZero
 
 section PartialOrder
 
-variable [AddCommMonoid α] [PartialOrder α] [CanonicallyOrderedAdd α] {f g : ι →₀ α}
+variable [AddCommMonoid α] [PartialOrder α] {f g : ι →₀ α}
 
-instance orderBot : OrderBot (ι →₀ α) where
+instance orderBot [IsBotZeroClass α] : OrderBot (ι →₀ α) where
   bot := 0
-  bot_le := by simp only [le_def, coe_zero, Pi.zero_apply, imp_true_iff, zero_le]
+  bot_le := by simp [le_def]
 
-protected theorem bot_eq_zero : (⊥ : ι →₀ α) = 0 :=
+instance [IsBotZeroClass α] : IsBotZeroClass (ι →₀ α) where
+  isBot_zero := isBot_bot
+
+@[deprecated _root_.bot_eq_zero (since := "2026-05-07")]
+protected theorem bot_eq_zero [IsBotZeroClass α] : (⊥ : ι →₀ α) = 0 :=
   rfl
 
+variable [CanonicallyOrderedAdd α]
+
 @[simp]
 theorem add_eq_zero_iff (f g : ι →₀ α) : f + g = 0 ↔ f = 0 ∧ g = 0 := by
   simp [DFunLike.ext_iff, forall_and]
@@ -298,32 +304,26 @@ end PartialOrder
 
 section LinearOrder
 
-variable [AddCommMonoid α] [LinearOrder α] [CanonicallyOrderedAdd α]
+variable [AddCommMonoid α] [LinearOrder α] [IsBotZeroClass α]
 
 @[simp]
 theorem support_inf [DecidableEq ι] (f g : ι →₀ α) : (f ⊓ g).support = f.support ∩ g.support := by
   ext
-  simp only [inf_apply, mem_support_iff, Ne,
-    Finset.mem_inter]
-  simp only [← nonpos_iff_eq_zero, min_le_iff, not_or]
+  simp
 
 @[simp]
 theorem support_sup [DecidableEq ι] (f g : ι →₀ α) : (f ⊔ g).support = f.support ∪ g.support := by
   ext
-  simp only [mem_support_iff, Ne, sup_apply, ← nonpos_iff_eq_zero, sup_le_iff, mem_union,
-    not_and_or]
+  simp [imp_iff_not_or]
 
 nonrec theorem disjoint_iff {f g : ι →₀ α} : Disjoint f g ↔ Disjoint f.support g.support := by
   classical
-    rw [disjoint_iff, disjoint_iff, Finsupp.bot_eq_zero, ← Finsupp.support_eq_empty,
-      Finsupp.support_inf]
-    rfl
+  simp [disjoint_iff, bot_eq_zero, ← Finsupp.support_eq_empty]
 
 end LinearOrder
 
 /-! ### Some lemmas about `ℕ` -/
 
-
 section Nat
 
 theorem sub_single_one_add {a : ι} {u u' : ι →₀ ℕ} (h : u a ≠ 0) :

Mathlib/Data/Finsupp/WellFounded.lean

@@ -53,12 +53,12 @@ theorem Lex.wellFounded' (hbot : ∀ ⦃n⦄, ¬s n 0) (hs : WellFounded s)
     InvImage.wf _ (DFinsupp.Lex.wellFounded' (fun _ => hbot) (fun _ => hs) hr)
 
 instance Lex.wellFoundedLT {α N} [LT α] [@Std.Trichotomous α (· < ·)] [hα : WellFoundedGT α]
-    [AddMonoid N] [PartialOrder N] [CanonicallyOrderedAdd N]
+    [AddMonoid N] [PartialOrder N] [IsBotZeroClass N]
     [hN : WellFoundedLT N] : WellFoundedLT (Lex (α →₀ N)) :=
   ⟨Lex.wellFounded' (fun _ => not_lt_zero) hN.wf hα.wf⟩
 
 instance Colex.wellFoundedLT {α N} [LT α] [@Std.Trichotomous α (· < ·)] [WellFoundedLT α]
-    [AddMonoid N] [PartialOrder N] [CanonicallyOrderedAdd N]
+    [AddMonoid N] [PartialOrder N] [IsBotZeroClass N]
     [WellFoundedLT N] : WellFoundedLT (Colex (α →₀ N)) :=
   Lex.wellFoundedLT (α := αᵒᵈ)
 
@@ -81,7 +81,7 @@ protected theorem wellFoundedLT [Preorder N] [WellFoundedLT N] (hbot : ∀ n : N
   ⟨InvImage.wf toDFinsupp (DFinsupp.wellFoundedLT fun _ a => hbot a).wf⟩
 
 instance wellFoundedLT' {N}
-    [AddMonoid N] [PartialOrder N] [CanonicallyOrderedAdd N] [WellFoundedLT N] :
+    [AddMonoid N] [PartialOrder N] [IsBotZeroClass N] [WellFoundedLT N] :
     WellFoundedLT (α →₀ N) :=
   Finsupp.wellFoundedLT fun _ => not_lt_zero