feat: the smul on measures is ordered (leanprover-community#40101)

Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

Author: sgouezel

Mathlib/Algebra/Order/AddTorsor.lean

@@ -77,7 +77,7 @@ instance [CommMonoid G] [Preorder G] [IsOrderedMonoid G] : IsOrderedSMul G G whe
   smul_le_smul_left _ _ := mul_le_mul_right
   smul_le_smul_right _ _ := mul_le_mul_left
 
-@[to_additive]
+@[to_additive (attr := gcongr)]
 theorem IsOrderedSMul.smul_le_smul [LE G] [Preorder P] [SMul G P] [IsOrderedSMul G P]
     {a b : G} {c d : P} (hab : a ≤ b) (hcd : c ≤ d) : a • c ≤ b • d :=
   (IsOrderedSMul.smul_le_smul_left _ _ hcd _).trans (IsOrderedSMul.smul_le_smul_right _ _ hab _)

Mathlib/Data/ENNReal/Action.lean

@@ -6,6 +6,7 @@ Authors: Johannes Hölzl, Yury Kudryashov
 module
 
 public import Mathlib.Algebra.Module.Torsion.Field
+public import Mathlib.Algebra.Order.AddTorsor
 public import Mathlib.Data.ENNReal.Operations
 
 /-!
@@ -104,11 +105,15 @@ instance : PosSMulStrictMono ℝ≥0 ℝ≥0∞ where
 instance : SMulPosMono ℝ≥0 ℝ≥0∞ where
   smul_le_smul_of_nonneg_right _r _ _a _b hab := _root_.mul_le_mul_left (coe_le_coe.2 hab) _
 
-instance : CovariantClass ℝ≥0∞ ℝ≥0∞ (· • ·) (· ≤ ·) :=
-  inferInstanceAs <| CovariantClass ℝ≥0∞ ℝ≥0∞ (· * ·) (· ≤ ·)
+instance : IsOrderedModule ℝ≥0 ℝ≥0∞ where
 
-instance : CovariantClass ℝ≥0 ℝ≥0∞ (· • ·) (· ≤ ·) :=
-  ⟨fun x x y hxy ↦ by simpa [ENNReal.smul_def] using mul_le_mul_right hxy _⟩
+example : CovariantClass ℝ≥0∞ ℝ≥0∞ (· • ·) (· ≤ ·) := inferInstance
+
+instance : IsOrderedSMul ℝ≥0 ℝ≥0∞ where
+  smul_le_smul_left a b hab c := by gcongr
+  smul_le_smul_right a b hab c := by gcongr
+
+example : CovariantClass ℝ≥0 ℝ≥0∞ (· • ·) (· ≤ ·) := inferInstance
 
 end Actions
 

Mathlib/MeasureTheory/Measure/MeasureSpace.lean

@@ -1087,6 +1087,13 @@ instance [SMul R ℝ≥0∞] [IsScalarTower R ℝ≥0∞ ℝ≥0∞] [CovariantC
     simp only [smul_apply]
     gcongr
 
+instance [SMul R ℝ≥0∞] [LE R] [IsScalarTower R ℝ≥0∞ ℝ≥0∞] [IsOrderedSMul R ℝ≥0∞] :
+    IsOrderedSMul R (Measure α) where
+  smul_le_smul_left μ ν hμν a s := by gcongr
+  smul_le_smul_right a b hab μ s := by
+    simp only [smul_apply]
+    gcongr
+
 section sInf
 
 variable {m : Set (Measure α)}