refactor: Deduplicate monotonicity of • lemmas (#9179)

Remove the duplicates introduced in #8869 by sorting the lemmas in `Algebra.Order.SMul` into three files:
* `Algebra.Order.Module.Defs` for the order isomorphism induced by scalar multiplication by a positivity element
* `Algebra.Order.Module.Pointwise` for the order properties of scalar multiplication of sets. This file is new. I credit myself for leanprover-community/mathlib#9078
* `Algebra.Order.Module.OrderedSMul`: The material about `OrderedSMul` per se. Inherits the copyright header from `Algebra.Order.SMul`. This file should eventually be deleted.

I move each `#align` to the correct file. On top of that, I delete unused redundant `OrderedSMul` instances (they were useful in Lean 3, but not anymore) and `eq_of_smul_eq_smul_of_pos_of_le`/`eq_of_smul_eq_smul_of_neg_of_le` since those lemmas are weird and unused.

Mathlib.lean

@@ -377,6 +377,8 @@ import Mathlib.Algebra.Order.Kleene
 import Mathlib.Algebra.Order.LatticeGroup
 import Mathlib.Algebra.Order.Module
 import Mathlib.Algebra.Order.Module.Defs
+import Mathlib.Algebra.Order.Module.OrderedSMul
+import Mathlib.Algebra.Order.Module.Pointwise
 import Mathlib.Algebra.Order.Module.Synonym
 import Mathlib.Algebra.Order.Monoid.Basic
 import Mathlib.Algebra.Order.Monoid.Canonical.Defs
@@ -411,7 +413,6 @@ import Mathlib.Algebra.Order.Ring.InjSurj
 import Mathlib.Algebra.Order.Ring.Lemmas
 import Mathlib.Algebra.Order.Ring.Star
 import Mathlib.Algebra.Order.Ring.WithTop
-import Mathlib.Algebra.Order.SMul
 import Mathlib.Algebra.Order.Sub.Basic
 import Mathlib.Algebra.Order.Sub.Canonical
 import Mathlib.Algebra.Order.Sub.Defs

Mathlib/Algebra/Order/Algebra.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import Mathlib.Algebra.Algebra.Basic
-import Mathlib.Algebra.Order.SMul
+import Mathlib.Algebra.Order.Module.OrderedSMul
 
 #align_import algebra.order.algebra from "leanprover-community/mathlib"@"f5a600f8102c8bfdbd22781968a20a539304c1b4"
 
@@ -45,7 +45,7 @@ theorem algebraMap_monotone : Monotone (algebraMap R A) := fun a b h => by
   rw [Algebra.algebraMap_eq_smul_one, Algebra.algebraMap_eq_smul_one, ← sub_nonneg, ← sub_smul]
   trans (b - a) • (0 : A)
   · simp
-  · exact smul_le_smul_of_nonneg zero_le_one (sub_nonneg.mpr h)
+  · exact smul_le_smul_of_nonneg_left zero_le_one (sub_nonneg.mpr h)
 #align algebra_map_monotone algebraMap_monotone
 
 end OrderedAlgebra

Mathlib/Algebra/Order/Module.lean

@@ -3,7 +3,7 @@ Copyright (c) 2020 Frédéric Dupuis. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Frédéric Dupuis, Yaël Dillies
 -/
-import Mathlib.Algebra.Order.SMul
+import Mathlib.Algebra.Order.Module.OrderedSMul
 
 #align_import algebra.order.module from "leanprover-community/mathlib"@"3ba15165bd6927679be7c22d6091a87337e3cd0c"
 
@@ -40,7 +40,7 @@ where `DistribMulActionWithZero k M`is the conjunction of `DistribMulAction k M`
 `SMulWithZero k M`.-/
 theorem smul_neg_iff_of_pos (hc : 0 < c) : c • a < 0 ↔ a < 0 := by
   rw [← neg_neg a, smul_neg, neg_neg_iff_pos, neg_neg_iff_pos]
-  exact smul_pos_iff_of_pos hc
+  exact smul_pos_iff_of_pos_left hc
 #align smul_neg_iff_of_pos smul_neg_iff_of_pos
 
 end Semiring
@@ -51,32 +51,29 @@ variable [OrderedRing k] [OrderedAddCommGroup M] [Module k M] [OrderedSMul k M]
 
 theorem smul_lt_smul_of_neg (h : a < b) (hc : c < 0) : c • b < c • a := by
   rw [← neg_neg c, neg_smul, neg_smul (-c), neg_lt_neg_iff]
-  exact smul_lt_smul_of_pos h (neg_pos_of_neg hc)
+  exact smul_lt_smul_of_pos_left h (neg_pos_of_neg hc)
 #align smul_lt_smul_of_neg smul_lt_smul_of_neg
 
 theorem smul_le_smul_of_nonpos (h : a ≤ b) (hc : c ≤ 0) : c • b ≤ c • a := by
   rw [← neg_neg c, neg_smul, neg_smul (-c), neg_le_neg_iff]
-  exact smul_le_smul_of_nonneg h (neg_nonneg_of_nonpos hc)
+  exact smul_le_smul_of_nonneg_left h (neg_nonneg_of_nonpos hc)
 #align smul_le_smul_of_nonpos smul_le_smul_of_nonpos
 
-theorem eq_of_smul_eq_smul_of_neg_of_le (hab : c • a = c • b) (hc : c < 0) (h : a ≤ b) : a = b := by
-  rw [← neg_neg c, neg_smul, neg_smul (-c), neg_inj] at hab
-  exact eq_of_smul_eq_smul_of_pos_of_le hab (neg_pos_of_neg hc) h
-#align eq_of_smul_eq_smul_of_neg_of_le eq_of_smul_eq_smul_of_neg_of_le
+#noalign eq_of_smul_eq_smul_of_neg_of_le
 
 theorem lt_of_smul_lt_smul_of_nonpos (h : c • a < c • b) (hc : c ≤ 0) : b < a := by
   rw [← neg_neg c, neg_smul, neg_smul (-c), neg_lt_neg_iff] at h
-  exact lt_of_smul_lt_smul_of_nonneg h (neg_nonneg_of_nonpos hc)
+  exact lt_of_smul_lt_smul_of_nonneg_left h (neg_nonneg_of_nonpos hc)
 #align lt_of_smul_lt_smul_of_nonpos lt_of_smul_lt_smul_of_nonpos
 
 theorem smul_lt_smul_iff_of_neg (hc : c < 0) : c • a < c • b ↔ b < a := by
   rw [← neg_neg c, neg_smul, neg_smul (-c), neg_lt_neg_iff]
-  exact smul_lt_smul_iff_of_pos (neg_pos_of_neg hc)
+  exact smul_lt_smul_iff_of_pos_left (neg_pos_of_neg hc)
 #align smul_lt_smul_iff_of_neg smul_lt_smul_iff_of_neg
 
 theorem smul_neg_iff_of_neg (hc : c < 0) : c • a < 0 ↔ 0 < a := by
   rw [← neg_neg c, neg_smul, neg_neg_iff_pos]
-  exact smul_pos_iff_of_pos (neg_pos_of_neg hc)
+  exact smul_pos_iff_of_pos_left (neg_pos_of_neg hc)
 #align smul_neg_iff_of_neg smul_neg_iff_of_neg
 
 theorem smul_pos_iff_of_neg (hc : c < 0) : 0 < c • a ↔ a < 0 := by
@@ -149,7 +146,7 @@ variable [LinearOrderedField k] [OrderedAddCommGroup M] [Module k M] [OrderedSMu
 
 theorem smul_le_smul_iff_of_neg (hc : c < 0) : c • a ≤ c • b ↔ b ≤ a := by
   rw [← neg_neg c, neg_smul, neg_smul (-c), neg_le_neg_iff]
-  exact smul_le_smul_iff_of_pos (neg_pos_of_neg hc)
+  exact smul_le_smul_iff_of_pos_left (neg_pos_of_neg hc)
 #align smul_le_smul_iff_of_neg smul_le_smul_iff_of_neg
 
 theorem inv_smul_le_iff_of_neg (h : c < 0) : c⁻¹ • a ≤ b ↔ c • b ≤ a := by

Mathlib/Algebra/Order/Module/Defs.lean

@@ -248,15 +248,19 @@ variable [Zero α]
 
 lemma monotone_smul_left_of_nonneg [PosSMulMono α β] (ha : 0 ≤ a) : Monotone ((a • ·) : β → β) :=
   PosSMulMono.elim ha
+#align monotone_smul_left monotone_smul_left_of_nonneg
 
 lemma strictMono_smul_left_of_pos [PosSMulStrictMono α β] (ha : 0 < a) :
     StrictMono ((a • ·) : β → β) := PosSMulStrictMono.elim ha
+#align strict_mono_smul_left strictMono_smul_left_of_pos
 
-lemma smul_le_smul_of_nonneg_left [PosSMulMono α β] (hb : b₁ ≤ b₂) (ha : 0 ≤ a) : a • b₁ ≤ a • b₂ :=
-  monotone_smul_left_of_nonneg ha hb
+@[gcongr] lemma smul_le_smul_of_nonneg_left [PosSMulMono α β] (hb : b₁ ≤ b₂) (ha : 0 ≤ a) :
+    a • b₁ ≤ a • b₂ := monotone_smul_left_of_nonneg ha hb
+#align smul_le_smul_of_nonneg smul_le_smul_of_nonneg_left
 
-lemma smul_lt_smul_of_pos_left [PosSMulStrictMono α β] (hb : b₁ < b₂) (ha : 0 < a) :
+@[gcongr] lemma smul_lt_smul_of_pos_left [PosSMulStrictMono α β] (hb : b₁ < b₂) (ha : 0 < a) :
     a • b₁ < a • b₂ := strictMono_smul_left_of_pos ha hb
+#align smul_lt_smul_of_pos smul_lt_smul_of_pos_left
 
 lemma lt_of_smul_lt_smul_left [PosSMulReflectLT α β] (h : a • b₁ < a • b₂) (ha : 0 ≤ a) : b₁ < b₂ :=
   PosSMulReflectLT.elim ha h
@@ -266,16 +270,19 @@ lemma le_of_smul_le_smul_left [PosSMulReflectLE α β] (h : a • b₁ ≤ a •
 
 alias lt_of_smul_lt_smul_of_nonneg_left := lt_of_smul_lt_smul_left
 alias le_of_smul_le_smul_of_pos_left := le_of_smul_le_smul_left
+#align lt_of_smul_lt_smul_of_nonneg lt_of_smul_lt_smul_of_nonneg_left
 
 @[simp]
 lemma smul_le_smul_iff_of_pos_left [PosSMulMono α β] [PosSMulReflectLE α β] (ha : 0 < a) :
     a • b₁ ≤ a • b₂ ↔ b₁ ≤ b₂ :=
   ⟨fun h ↦ le_of_smul_le_smul_left h ha, fun h ↦ smul_le_smul_of_nonneg_left h ha.le⟩
+#align smul_le_smul_iff_of_pos smul_le_smul_iff_of_pos_left
 
 @[simp]
 lemma smul_lt_smul_iff_of_pos_left [PosSMulStrictMono α β] [PosSMulReflectLT α β] (ha : 0 < a) :
     a • b₁ < a • b₂ ↔ b₁ < b₂ :=
   ⟨fun h ↦ lt_of_smul_lt_smul_left h ha.le, fun hb ↦ smul_lt_smul_of_pos_left hb ha⟩
+#align smul_lt_smul_iff_of_pos smul_lt_smul_iff_of_pos_left
 
 end Left
 
@@ -288,10 +295,10 @@ lemma monotone_smul_right_of_nonneg [SMulPosMono α β] (hb : 0 ≤ b) : Monoton
 lemma strictMono_smul_right_of_pos [SMulPosStrictMono α β] (hb : 0 < b) :
     StrictMono ((· • b) : α → β) := SMulPosStrictMono.elim hb
 
-lemma smul_le_smul_of_nonneg_right [SMulPosMono α β] (ha : a₁ ≤ a₂) (hb : 0 ≤ b) :
+@[gcongr] lemma smul_le_smul_of_nonneg_right [SMulPosMono α β] (ha : a₁ ≤ a₂) (hb : 0 ≤ b) :
     a₁ • b ≤ a₂ • b := monotone_smul_right_of_nonneg hb ha
 
-lemma smul_lt_smul_of_pos_right [SMulPosStrictMono α β] (ha : a₁ < a₂) (hb : 0 < b) :
+@[gcongr] lemma smul_lt_smul_of_pos_right [SMulPosStrictMono α β] (ha : a₁ < a₂) (hb : 0 < b) :
     a₁ • b < a₂ • b := strictMono_smul_right_of_pos hb ha
 
 lemma lt_of_smul_lt_smul_right [SMulPosReflectLT α β] (h : a₁ • b < a₂ • b) (hb : 0 ≤ b) :
@@ -381,9 +388,11 @@ lemma posSMulMono_iff_posSMulReflectLT : PosSMulMono α β ↔ PosSMulReflectLT
 
 lemma smul_max_of_nonneg [PosSMulMono α β] (ha : 0 ≤ a) (b₁ b₂ : β) :
     a • max b₁ b₂ = max (a • b₁) (a • b₂) := (monotone_smul_left_of_nonneg ha).map_max
+#align smul_max smul_max_of_nonneg
 
 lemma smul_min_of_nonneg [PosSMulMono α β] (ha : 0 ≤ a) (b₁ b₂ : β) :
     a • min b₁ b₂ = min (a • b₁) (a • b₂) := (monotone_smul_left_of_nonneg ha).map_min
+#align smul_min smul_min_of_nonneg
 
 end Left
 
@@ -440,6 +449,7 @@ variable [Preorder α] [Preorder β]
 
 lemma smul_pos [PosSMulStrictMono α β] (ha : 0 < a) (hb : 0 < b) : 0 < a • b := by
   simpa only [smul_zero] using smul_lt_smul_of_pos_left hb ha
+#align smul_pos smul_pos
 
 lemma smul_neg_of_pos_of_neg [PosSMulStrictMono α β] (ha : 0 < a) (hb : b < 0) : a • b < 0 := by
   simpa only [smul_zero] using smul_lt_smul_of_pos_left hb ha
@@ -448,12 +458,15 @@ lemma smul_neg_of_pos_of_neg [PosSMulStrictMono α β] (ha : 0 < a) (hb : b < 0)
 lemma smul_pos_iff_of_pos_left [PosSMulStrictMono α β] [PosSMulReflectLT α β] (ha : 0 < a) :
     0 < a • b ↔ 0 < b := by
   simpa only [smul_zero] using smul_lt_smul_iff_of_pos_left ha (b₁ := 0) (b₂ := b)
+#align smul_pos_iff_of_pos smul_pos_iff_of_pos_left
 
 lemma smul_nonneg [PosSMulMono α β] (ha : 0 ≤ a) (hb : 0 ≤ b₁) : 0 ≤ a • b₁ := by
   simpa only [smul_zero] using smul_le_smul_of_nonneg_left hb ha
+#align smul_nonneg smul_nonneg
 
 lemma smul_nonpos_of_nonneg_of_nonpos [PosSMulMono α β] (ha : 0 ≤ a) (hb : b ≤ 0) : a • b ≤ 0 := by
   simpa only [smul_zero] using smul_le_smul_of_nonneg_left hb ha
+#align smul_nonpos_of_nonneg_of_nonpos smul_nonpos_of_nonneg_of_nonpos
 
 lemma pos_of_smul_pos_right [PosSMulReflectLT α β] (h : 0 < a • b) (ha : 0 ≤ a) : 0 < b :=
   lt_of_smul_lt_smul_left (by rwa [smul_zero]) ha
@@ -721,22 +734,35 @@ instance PosSMulStrictMono.toSMulPosStrictMono [PosSMulStrictMono α β] : SMulP
 
 end OrderedRing
 
-section Field
+section GroupWithZero
 variable [GroupWithZero α] [Preorder α] [Preorder β] [MulAction α β]
 
 lemma inv_smul_le_iff_of_pos [PosSMulMono α β] [PosSMulReflectLE α β] (ha : 0 < a) :
     a⁻¹ • b₁ ≤ b₂ ↔ b₁ ≤ a • b₂ := by rw [← smul_le_smul_iff_of_pos_left ha, smul_inv_smul₀ ha.ne']
+#align inv_smul_le_iff inv_smul_le_iff_of_pos
 
 lemma le_inv_smul_iff_of_pos [PosSMulMono α β] [PosSMulReflectLE α β] (ha : 0 < a) :
     b₁ ≤ a⁻¹ • b₂ ↔ a • b₁ ≤ b₂ := by rw [← smul_le_smul_iff_of_pos_left ha, smul_inv_smul₀ ha.ne']
+#align le_inv_smul_iff le_inv_smul_iff_of_pos
 
 lemma inv_smul_lt_iff_of_pos [PosSMulStrictMono α β] [PosSMulReflectLT α β] (ha : 0 < a) :
     a⁻¹ • b₁ < b₂ ↔ b₁ < a • b₂ := by rw [← smul_lt_smul_iff_of_pos_left ha, smul_inv_smul₀ ha.ne']
+#align inv_smul_lt_iff inv_smul_lt_iff_of_pos
 
 lemma lt_inv_smul_iff_of_pos [PosSMulStrictMono α β] [PosSMulReflectLT α β] (ha : 0 < a) :
     b₁ < a⁻¹ • b₂ ↔ a • b₁ < b₂ := by rw [← smul_lt_smul_iff_of_pos_left ha, smul_inv_smul₀ ha.ne']
+#align lt_inv_smul_iff lt_inv_smul_iff_of_pos
 
-end Field
+/-- Right scalar multiplication as an order isomorphism. -/
+@[simps!]
+def OrderIso.smulRight [PosSMulMono α β] [PosSMulReflectLE α β] {a : α} (ha : 0 < a) : β ≃o β where
+  toEquiv := Equiv.smulRight ha.ne'
+  map_rel_iff' := smul_le_smul_iff_of_pos_left ha
+#align order_iso.smul_left OrderIso.smulRight
+#align order_iso.smul_left_symm_apply OrderIso.smulRight_symm_apply
+#align order_iso.smul_left_apply OrderIso.smulRight_apply
+
+end GroupWithZero
 
 section LinearOrderedSemifield
 variable [LinearOrderedSemifield α] [AddCommGroup β] [PartialOrder β]
@@ -889,3 +915,82 @@ lemma SMulPosReflectLT.lift [SMulPosReflectLT α γ] : SMulPosReflectLT α β wh
     exact lt_of_smul_lt_smul_right h hb
 
 end Lift
+
+namespace Mathlib.Meta.Positivity
+section OrderedSMul
+variable [Zero α] [Zero β] [SMulZeroClass α β] [Preorder α] [Preorder β] [PosSMulMono α β] {a : α}
+  {b : β}
+
+private theorem smul_nonneg_of_pos_of_nonneg (ha : 0 < a) (hb : 0 ≤ b) : 0 ≤ a • b :=
+  smul_nonneg ha.le hb
+
+private theorem smul_nonneg_of_nonneg_of_pos (ha : 0 ≤ a) (hb : 0 < b) : 0 ≤ a • b :=
+  smul_nonneg ha hb.le
+
+end OrderedSMul
+
+section NoZeroSMulDivisors
+variable [Zero α] [Zero β] [SMul α β] [NoZeroSMulDivisors α β] {a : α} {b : β}
+
+private theorem smul_ne_zero_of_pos_of_ne_zero [Preorder α] (ha : 0 < a) (hb : b ≠ 0) : a • b ≠ 0 :=
+  smul_ne_zero ha.ne' hb
+
+private theorem smul_ne_zero_of_ne_zero_of_pos [Preorder β] (ha : a ≠ 0) (hb : 0 < b) : a • b ≠ 0 :=
+  smul_ne_zero ha hb.ne'
+
+end NoZeroSMulDivisors
+
+open Lean.Meta Qq
+
+/-- Positivity extension for HSMul, i.e. (_ • _).  -/
+@[positivity HSMul.hSMul _ _]
+def evalHSMul : PositivityExt where eval {_u α} zα pα (e : Q($α)) := do
+  let .app (.app (.app (.app (.app (.app
+        (.const ``HSMul.hSMul [u1, _, _]) (β : Q(Type u1))) _) _) _)
+          (a : Q($β))) (b : Q($α)) ← whnfR e | throwError "failed to match hSMul"
+  let zM : Q(Zero $β) ← synthInstanceQ (q(Zero $β))
+  let pM : Q(PartialOrder $β) ← synthInstanceQ (q(PartialOrder $β))
+  -- Using `q()` here would be impractical, as we would have to manually `synthInstanceQ` all the
+  -- required typeclasses. Ideally we could tell `q()` to do this automatically.
+  match ← core zM pM a, ← core zα pα b with
+  | .positive pa, .positive pb =>
+      pure (.positive (← mkAppM ``smul_pos #[pa, pb]))
+  | .positive pa, .nonnegative pb =>
+      pure (.nonnegative (← mkAppM ``smul_nonneg_of_pos_of_nonneg #[pa, pb]))
+  | .nonnegative pa, .positive pb =>
+      pure (.nonnegative (← mkAppM ``smul_nonneg_of_nonneg_of_pos #[pa, pb]))
+  | .nonnegative pa, .nonnegative pb =>
+      pure (.nonnegative (← mkAppM ``smul_nonneg #[pa, pb]))
+  | .positive pa, .nonzero pb =>
+      pure (.nonzero (← mkAppM ``smul_ne_zero_of_pos_of_ne_zero #[pa, pb]))
+  | .nonzero pa, .positive pb =>
+      pure (.nonzero (← mkAppM ``smul_ne_zero_of_ne_zero_of_pos #[pa, pb]))
+  | .nonzero pa, .nonzero pb =>
+      pure (.nonzero (← mkAppM ``smul_ne_zero #[pa, pb]))
+  | _, _ => pure .none
+
+end Mathlib.Meta.Positivity
+
+/-!
+### Deprecated lemmas
+
+Those lemmas have been deprecated on the 2023/12/23.
+-/
+
+@[deprecated] alias monotone_smul_left := monotone_smul_left_of_nonneg
+@[deprecated] alias strict_mono_smul_left := strictMono_smul_left_of_pos
+@[deprecated] alias smul_le_smul_of_nonneg := smul_le_smul_of_nonneg_left
+@[deprecated] alias smul_lt_smul_of_pos := smul_lt_smul_of_pos_left
+@[deprecated] alias lt_of_smul_lt_smul_of_nonneg := lt_of_smul_lt_smul_of_nonneg_left
+@[deprecated] alias smul_le_smul_iff_of_pos := smul_le_smul_iff_of_pos_left
+@[deprecated] alias smul_lt_smul_iff_of_pos := smul_lt_smul_iff_of_pos_left
+@[deprecated] alias smul_max := smul_max_of_nonneg
+@[deprecated] alias smul_min := smul_min_of_nonneg
+@[deprecated] alias smul_pos_iff_of_pos := smul_pos_iff_of_pos_left
+@[deprecated] alias inv_smul_le_iff := inv_smul_le_iff_of_pos
+@[deprecated] alias le_inv_smul_iff := le_inv_smul_iff_of_pos
+@[deprecated] alias inv_smul_lt_iff := inv_smul_lt_iff_of_pos
+@[deprecated] alias lt_inv_smul_iff := lt_inv_smul_iff_of_pos
+@[deprecated] alias OrderIso.smulLeft := OrderIso.smulRight
+@[deprecated] alias OrderIso.smulLeft_symm_apply := OrderIso.smulRight_symm_apply
+@[deprecated] alias OrderIso.smulLeft_apply := OrderIso.smulRight_apply