Merge remote-tracking branch 'upstream/master' into bump/v4.31.0

Author: mathlib4-bot

Mathlib/Analysis/Complex/CoveringMap.lean

@@ -89,7 +89,7 @@ theorem isCoveringMapOn_zpow (n : ℤ) (hn : (n : 𝕜) ≠ 0) :
   refine .of_isCoveringMap_restrictPreimage _ (by simp) ?_ ?_
   · convert isClosed_singleton (x := (0 : 𝕜)).isOpen_compl using 1
     ext; simp [this]
-  · convert (isCoveringMap_zpow n hn).comp_homeomorph (.setCongr _) using 1
+  · convert (isCoveringMap_zpow n hn).comp_homeomorph (.ofEqSubtypes _) using 1
     ext; simpa using (this _).not
 
 attribute [-instance] Units.mulAction'
@@ -103,9 +103,9 @@ theorem isQuotientCoveringMap_npow (n : ℕ) (hn : (n : 𝕜) ≠ 0)
     (by fun_prop) (.restrictPreimage _ surj)
   have : IsQuotientMap fun x : 𝕜ˣ ↦ x ^ n := by
     let e := unitsHomeomorphNeZero (G₀ := 𝕜)
-    convert (e.symm.isQuotientMap.comp this).comp (e.trans (.setCongr _)).isQuotientMap
+    convert (e.symm.isQuotientMap.comp this).comp (e.trans (.ofEqSubtypes _)).isQuotientMap
     · exact (e.left_inv _).symm
-    · ext; simp [NeZero.ne]; rfl
+    · ext; simp [NeZero.ne]
   refine this.isQuotientCoveringMap_of_subgroup _
     (Set.Finite.isDiscrete <| inferInstanceAs (Finite (rootsOfUnity ..))) ?_
   simp [mul_pow, mul_inv_eq_one, eq_comm]

Mathlib/Analysis/Normed/Group/FunctionSeries.lean

@@ -74,7 +74,7 @@ theorem tendstoUniformlyOn_tsum_of_cofinite_eventually {ι : Type*} {f : ι →
   apply lt_of_le_of_lt _ (ht n (Finset.union_subset_right hn))
   apply (norm_tsum_le_tsum_norm (A.subtype _)).trans
   apply (A.subtype _).tsum_le_tsum _ (hu.subtype _)
-  simp only [comp_apply, Subtype.forall, imp_false]
+  simp only [comp_apply, Subtype.forall]
   apply fun i hi => HN i ?_ x hx
   have : i ∉ hN.toFinset := fun hg ↦ hi (Finset.union_subset_left hn hg)
   simp_all

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

@@ -261,17 +261,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

@@ -167,13 +167,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 (ι := ιᵒᵈ)
@@ -236,7 +236,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