chore (Data.Multiset.Basic): avoid bundled ordered algebra for basic …

…results on multisets (#14477)

`Data.Multiset.Basic` is a fairly low-level file. Currently, it imports `Algebra.Order.Monoid.Defs` to establish that multisets on a type are an `StrictOrderedAddCancelCommMonoid` and uses that classes API in a dozen places. Unfortunately, this also adds, to this file and all that import it, the projections from the ordered monoids defined in `Algebra.Order.Monoid.Defs` as instances for Lean to try when synthesizing a `CommMonoid` impacting performance. This PR moves the ordered monoid instances to a new file `Data.Multiset.OrderedMonoid` and makes minor changes to `Basic` to avoid this import.



Co-authored-by: Matthew Robert Ballard <[email protected]>

Mathlib.lean

@@ -645,9 +645,10 @@ import Mathlib.Algebra.Order.Ring.Unbundled.Basic
 import Mathlib.Algebra.Order.Ring.Unbundled.Nonneg
 import Mathlib.Algebra.Order.Ring.WithTop
 import Mathlib.Algebra.Order.Sub.Basic
-import Mathlib.Algebra.Order.Sub.Canonical
 import Mathlib.Algebra.Order.Sub.Defs
 import Mathlib.Algebra.Order.Sub.Prod
+import Mathlib.Algebra.Order.Sub.Unbundled.Basic
+import Mathlib.Algebra.Order.Sub.Unbundled.Hom
 import Mathlib.Algebra.Order.Sub.WithTop
 import Mathlib.Algebra.Order.Sum
 import Mathlib.Algebra.Order.ToIntervalMod
@@ -2290,6 +2291,7 @@ import Mathlib.Data.Multiset.Interval
 import Mathlib.Data.Multiset.Lattice
 import Mathlib.Data.Multiset.NatAntidiagonal
 import Mathlib.Data.Multiset.Nodup
+import Mathlib.Data.Multiset.OrderedMonoid
 import Mathlib.Data.Multiset.Pi
 import Mathlib.Data.Multiset.Powerset
 import Mathlib.Data.Multiset.Range

Mathlib/Algebra/BigOperators/Group/Finset.lean

@@ -39,6 +39,7 @@ See the documentation of `to_additive.attr` for more information.
 -- assert_not_exists AddCommMonoidWithOne
 assert_not_exists MonoidWithZero
 assert_not_exists MulAction
+assert_not_exists OrderedCommMonoid
 
 variable {ι κ α β γ : Type*}
 
@@ -1455,11 +1456,12 @@ theorem eq_prod_range_div' {M : Type*} [CommGroup M] (f : ℕ → M) (n : ℕ) :
 reduces to the difference of the last and first terms
 when the function we are summing is monotone.
 -/
-theorem sum_range_tsub [CanonicallyOrderedAddCommMonoid α] [Sub α] [OrderedSub α]
-    [ContravariantClass α α (· + ·) (· ≤ ·)] {f : ℕ → α} (h : Monotone f) (n : ℕ) :
+theorem sum_range_tsub [AddCommMonoid α] [PartialOrder α] [Sub α] [OrderedSub α]
+    [CovariantClass α α (· + ·) (· ≤ ·)] [ContravariantClass α α (· + ·) (· ≤ ·)] [ExistsAddOfLE α]
+    {f : ℕ → α} (h : Monotone f) (n : ℕ) :
     ∑ i ∈ range n, (f (i + 1) - f i) = f n - f 0 := by
   apply sum_range_induction
-  case base => apply tsub_self
+  case base => apply tsub_eq_of_eq_add; rw [zero_add]
   case step =>
     intro n
     have h₁ : f n ≤ f (n + 1) := h (Nat.le_succ _)
@@ -1684,7 +1686,7 @@ theorem prod_ite_one (s : Finset α) (p : α → Prop) [DecidablePred p]
     exact fun i hi => if_neg (h i hi)
 
 @[to_additive]
-theorem prod_erase_lt_of_one_lt {γ : Type*} [DecidableEq α] [OrderedCommMonoid γ]
+theorem prod_erase_lt_of_one_lt {γ : Type*} [DecidableEq α] [CommMonoid γ] [Preorder γ]
     [CovariantClass γ γ (· * ·) (· < ·)] {s : Finset α} {d : α} (hd : d ∈ s) {f : α → γ}
     (hdf : 1 < f d) : ∏ m ∈ s.erase d, f m < ∏ m ∈ s, f m := by
   conv in ∏ m ∈ s, f m => rw [← Finset.insert_erase hd]

Mathlib/Algebra/Order/Antidiag/Prod.lean

@@ -3,6 +3,7 @@ Copyright (c) 2023 Antoine Chambert-Loir and María Inés de Frutos-Fernández.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Antoine Chambert-Loir, María Inés de Frutos-Fernández, Bhavik Mehta, Eric Wieser
 -/
+import Mathlib.Algebra.Order.Monoid.Canonical.Defs
 import Mathlib.Algebra.Order.Sub.Defs
 import Mathlib.Data.Finset.Basic
 import Mathlib.Order.Interval.Finset.Defs

Mathlib/Algebra/Order/BigOperators/Group/Finset.lean

@@ -5,6 +5,7 @@ Authors: Johannes Hölzl
 -/
 import Mathlib.Algebra.BigOperators.Group.Finset
 import Mathlib.Algebra.Order.BigOperators.Group.Multiset
+import Mathlib.Data.Multiset.OrderedMonoid
 import Mathlib.Tactic.Bound.Attribute
 import Mathlib.Tactic.NormNum.Basic
 import Mathlib.Tactic.Positivity.Core

Mathlib/Algebra/Order/Field/Pi.lean

@@ -3,6 +3,7 @@ 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.Order.Monoid.Defs
 import Mathlib.Data.Finset.Lattice
 import Mathlib.Data.Fintype.Card
 

Mathlib/Algebra/Order/Ring/Canonical.lean

@@ -3,8 +3,9 @@ Copyright (c) 2016 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro
 -/
+import Mathlib.Algebra.Order.Monoid.Canonical.Defs
 import Mathlib.Algebra.Order.Ring.Defs
-import Mathlib.Algebra.Order.Sub.Canonical
+import Mathlib.Algebra.Order.Sub.Basic
 import Mathlib.Algebra.Ring.Parity
 
 /-!

Mathlib/Algebra/Order/Sub/Basic.lean

@@ -3,58 +3,199 @@ Copyright (c) 2021 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn
 -/
+import Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE
+import Mathlib.Algebra.Order.Monoid.Canonical.Defs
+import Mathlib.Algebra.Order.Sub.Unbundled.Basic
 import Mathlib.Algebra.Group.Equiv.Basic
-import Mathlib.Algebra.Ring.Basic
-import Mathlib.Algebra.Order.Sub.Defs
-import Mathlib.Order.Hom.Basic
-
+import Mathlib.Algebra.Group.Even
 /-!
-# Additional results about ordered Subtraction
-
+# Lemmas about subtraction in unbundled canonically ordered monoids
 -/
 
+variable {α : Type*}
+
+section CanonicallyOrderedAddCommMonoid
+
+variable [CanonicallyOrderedAddCommMonoid α] [Sub α] [OrderedSub α] {a b c d : α}
+
+theorem add_tsub_cancel_iff_le : a + (b - a) = b ↔ a ≤ b :=
+  ⟨fun h => le_iff_exists_add.mpr ⟨b - a, h.symm⟩, add_tsub_cancel_of_le⟩
+
+theorem tsub_add_cancel_iff_le : b - a + a = b ↔ a ≤ b := by
+  rw [add_comm]
+  exact add_tsub_cancel_iff_le
+
+-- This was previously a `@[simp]` lemma, but it is not necessarily a good idea, e.g. in
+-- `example (h : n - m = 0) : a + (n - m) = a := by simp_all`
+theorem tsub_eq_zero_iff_le : a - b = 0 ↔ a ≤ b := by
+  rw [← nonpos_iff_eq_zero, tsub_le_iff_left, add_zero]
+
+alias ⟨_, tsub_eq_zero_of_le⟩ := tsub_eq_zero_iff_le
+
+attribute [simp] tsub_eq_zero_of_le
+
+theorem tsub_self (a : α) : a - a = 0 :=
+  tsub_eq_zero_of_le le_rfl
+
+theorem tsub_le_self : a - b ≤ a :=
+  tsub_le_iff_left.mpr <| le_add_left le_rfl
+
+theorem zero_tsub (a : α) : 0 - a = 0 :=
+  tsub_eq_zero_of_le <| zero_le a
+
+theorem tsub_self_add (a b : α) : a - (a + b) = 0 :=
+  tsub_eq_zero_of_le <| self_le_add_right _ _
+
+theorem tsub_pos_iff_not_le : 0 < a - b ↔ ¬a ≤ b := by
+  rw [pos_iff_ne_zero, Ne, tsub_eq_zero_iff_le]
+
+theorem tsub_pos_of_lt (h : a < b) : 0 < b - a :=
+  tsub_pos_iff_not_le.mpr h.not_le
+
+theorem tsub_lt_of_lt (h : a < b) : a - c < b :=
+  lt_of_le_of_lt tsub_le_self h
+
+namespace AddLECancellable
+
+protected theorem tsub_le_tsub_iff_left (ha : AddLECancellable a) (hc : AddLECancellable c)
+    (h : c ≤ a) : a - b ≤ a - c ↔ c ≤ b := by
+  refine ⟨?_, fun h => tsub_le_tsub_left h a⟩
+  rw [tsub_le_iff_left, ← hc.add_tsub_assoc_of_le h, hc.le_tsub_iff_right (h.trans le_add_self),
+    add_comm b]
+  apply ha
+
+protected theorem tsub_right_inj (ha : AddLECancellable a) (hb : AddLECancellable b)
+    (hc : AddLECancellable c) (hba : b ≤ a) (hca : c ≤ a) : a - b = a - c ↔ b = c := by
+  simp_rw [le_antisymm_iff, ha.tsub_le_tsub_iff_left hb hba, ha.tsub_le_tsub_iff_left hc hca,
+    and_comm]
+
+end AddLECancellable
+
+/-! #### Lemmas where addition is order-reflecting. -/
+
+
+section Contra
+
+variable [ContravariantClass α α (· + ·) (· ≤ ·)]
+
+theorem tsub_le_tsub_iff_left (h : c ≤ a) : a - b ≤ a - c ↔ c ≤ b :=
+  Contravariant.AddLECancellable.tsub_le_tsub_iff_left Contravariant.AddLECancellable h
+
+theorem tsub_right_inj (hba : b ≤ a) (hca : c ≤ a) : a - b = a - c ↔ b = c :=
+  Contravariant.AddLECancellable.tsub_right_inj Contravariant.AddLECancellable
+    Contravariant.AddLECancellable hba hca
+
+variable (α)
+
+/-- A `CanonicallyOrderedAddCommMonoid` with ordered subtraction and order-reflecting addition is
+cancellative. This is not an instance as it would form a typeclass loop.
+
+See note [reducible non-instances]. -/
+abbrev CanonicallyOrderedAddCommMonoid.toAddCancelCommMonoid : AddCancelCommMonoid α :=
+  { (by infer_instance : AddCommMonoid α) with
+    add_left_cancel := fun a b c h => by
+      simpa only [add_tsub_cancel_left] using congr_arg (fun x => x - a) h }
+
+end Contra
+
+end CanonicallyOrderedAddCommMonoid
+
+/-! ### Lemmas in a linearly canonically ordered monoid. -/
+
+
+section CanonicallyLinearOrderedAddCommMonoid
+
+variable [CanonicallyLinearOrderedAddCommMonoid α] [Sub α] [OrderedSub α] {a b c d : α}
+
+@[simp]
+theorem tsub_pos_iff_lt : 0 < a - b ↔ b < a := by rw [tsub_pos_iff_not_le, not_le]
+
+theorem tsub_eq_tsub_min (a b : α) : a - b = a - min a b := by
+  rcases le_total a b with h | h
+  · rw [min_eq_left h, tsub_self, tsub_eq_zero_of_le h]
+  · rw [min_eq_right h]
+
+namespace AddLECancellable
+
+protected theorem lt_tsub_iff_right (hc : AddLECancellable c) : a < b - c ↔ a + c < b :=
+  ⟨lt_imp_lt_of_le_imp_le tsub_le_iff_right.mpr, hc.lt_tsub_of_add_lt_right⟩
+
+protected theorem lt_tsub_iff_left (hc : AddLECancellable c) : a < b - c ↔ c + a < b :=
+  ⟨lt_imp_lt_of_le_imp_le tsub_le_iff_left.mpr, hc.lt_tsub_of_add_lt_left⟩
+
+protected theorem tsub_lt_tsub_iff_right (hc : AddLECancellable c) (h : c ≤ a) :
+    a - c < b - c ↔ a < b := by rw [hc.lt_tsub_iff_left, add_tsub_cancel_of_le h]
+
+protected theorem tsub_lt_self (ha : AddLECancellable a) (h₁ : 0 < a) (h₂ : 0 < b) : a - b < a := by
+  refine tsub_le_self.lt_of_ne fun h => ?_
+  rw [← h, tsub_pos_iff_lt] at h₁
+  exact h₂.not_le (ha.add_le_iff_nonpos_left.1 <| add_le_of_le_tsub_left_of_le h₁.le h.ge)
+
+protected theorem tsub_lt_self_iff (ha : AddLECancellable a) : a - b < a ↔ 0 < a ∧ 0 < b := by
+  refine
+    ⟨fun h => ⟨(zero_le _).trans_lt h, (zero_le b).lt_of_ne ?_⟩, fun h => ha.tsub_lt_self h.1 h.2⟩
+  rintro rfl
+  rw [tsub_zero] at h
+  exact h.false
+
+/-- See `lt_tsub_iff_left_of_le_of_le` for a weaker statement in a partial order. -/
+protected theorem tsub_lt_tsub_iff_left_of_le (ha : AddLECancellable a) (hb : AddLECancellable b)
+    (h : b ≤ a) : a - b < a - c ↔ c < b :=
+  lt_iff_lt_of_le_iff_le <| ha.tsub_le_tsub_iff_left hb h
+
+end AddLECancellable
+
+section Contra
+
+variable [ContravariantClass α α (· + ·) (· ≤ ·)]
 
-variable {α β : Type*}
+/-- This lemma also holds for `ENNReal`, but we need a different proof for that. -/
+theorem tsub_lt_tsub_iff_right (h : c ≤ a) : a - c < b - c ↔ a < b :=
+  Contravariant.AddLECancellable.tsub_lt_tsub_iff_right h
 
-section Add
+theorem tsub_lt_self : 0 < a → 0 < b → a - b < a :=
+  Contravariant.AddLECancellable.tsub_lt_self
 
-variable [Preorder α] [Add α] [Sub α] [OrderedSub α] {a b c d : α}
+@[simp] theorem tsub_lt_self_iff : a - b < a ↔ 0 < a ∧ 0 < b :=
+  Contravariant.AddLECancellable.tsub_lt_self_iff
 
-theorem AddHom.le_map_tsub [Preorder β] [Add β] [Sub β] [OrderedSub β] (f : AddHom α β)
-    (hf : Monotone f) (a b : α) : f a - f b ≤ f (a - b) := by
-  rw [tsub_le_iff_right, ← f.map_add]
-  exact hf le_tsub_add
+/-- See `lt_tsub_iff_left_of_le_of_le` for a weaker statement in a partial order. -/
+theorem tsub_lt_tsub_iff_left_of_le (h : b ≤ a) : a - b < a - c ↔ c < b :=
+  Contravariant.AddLECancellable.tsub_lt_tsub_iff_left_of_le Contravariant.AddLECancellable h
 
-theorem le_mul_tsub {R : Type*} [Distrib R] [Preorder R] [Sub R] [OrderedSub R]
-    [CovariantClass R R (· * ·) (· ≤ ·)] {a b c : R} : a * b - a * c ≤ a * (b - c) :=
-  (AddHom.mulLeft a).le_map_tsub (monotone_id.const_mul' a) _ _
+lemma tsub_tsub_eq_min (a b : α) : a - (a - b) = min a b := by
+  rw [tsub_eq_tsub_min _ b, tsub_tsub_cancel_of_le (min_le_left a _)]
 
-theorem le_tsub_mul {R : Type*} [CommSemiring R] [Preorder R] [Sub R] [OrderedSub R]
-    [CovariantClass R R (· * ·) (· ≤ ·)] {a b c : R} : a * c - b * c ≤ (a - b) * c := by
-  simpa only [mul_comm _ c] using le_mul_tsub
+end Contra
 
-end Add
+/-! ### Lemmas about `max` and `min`. -/
 
-/-- An order isomorphism between types with ordered subtraction preserves subtraction provided that
-it preserves addition. -/
-theorem OrderIso.map_tsub {M N : Type*} [Preorder M] [Add M] [Sub M] [OrderedSub M]
-    [PartialOrder N] [Add N] [Sub N] [OrderedSub N] (e : M ≃o N)
-    (h_add : ∀ a b, e (a + b) = e a + e b) (a b : M) : e (a - b) = e a - e b := by
-  let e_add : M ≃+ N := { e with map_add' := h_add }
-  refine le_antisymm ?_ (e_add.toAddHom.le_map_tsub e.monotone a b)
-  suffices e (e.symm (e a) - e.symm (e b)) ≤ e (e.symm (e a - e b)) by simpa
-  exact e.monotone (e_add.symm.toAddHom.le_map_tsub e.symm.monotone _ _)
 
-/-! ### Preorder -/
+theorem tsub_add_eq_max : a - b + b = max a b := by
+  rcases le_total a b with h | h
+  · rw [max_eq_right h, tsub_eq_zero_of_le h, zero_add]
+  · rw [max_eq_left h, tsub_add_cancel_of_le h]
 
+theorem add_tsub_eq_max : a + (b - a) = max a b := by rw [add_comm, max_comm, tsub_add_eq_max]
 
-section Preorder
+theorem tsub_min : a - min a b = a - b := by
+  rcases le_total a b with h | h
+  · rw [min_eq_left h, tsub_self, tsub_eq_zero_of_le h]
+  · rw [min_eq_right h]
 
-variable [Preorder α]
-variable [AddCommMonoid α] [Sub α] [OrderedSub α] {a b c d : α}
+theorem tsub_add_min : a - b + min a b = a := by
+  rw [← tsub_min, @tsub_add_cancel_of_le]
+  apply min_le_left
 
-theorem AddMonoidHom.le_map_tsub [Preorder β] [AddCommMonoid β] [Sub β] [OrderedSub β] (f : α →+ β)
-    (hf : Monotone f) (a b : α) : f a - f b ≤ f (a - b) :=
-  f.toAddHom.le_map_tsub hf a b
+-- `Odd.tsub` requires `CanonicallyLinearOrderedSemiring`, which we don't have
+lemma Even.tsub
+    [ContravariantClass α α (· + ·) (· ≤ ·)] {m n : α} (hm : Even m) (hn : Even n) :
+    Even (m - n) := by
+  obtain ⟨a, rfl⟩ := hm
+  obtain ⟨b, rfl⟩ := hn
+  refine ⟨a - b, ?_⟩
+  obtain h | h := le_total a b
+  · rw [tsub_eq_zero_of_le h, tsub_eq_zero_of_le (add_le_add h h), add_zero]
+  · exact (tsub_add_tsub_comm h h).symm
 
-end Preorder
+end CanonicallyLinearOrderedAddCommMonoid