refactor(Algebra/Order/Module): don't use elim as a field name (leanprover-community#29340)

This prevented us from defining further typeclasses by extending.

Also move earlier an instance that somehow got stranded in `Data.Finsupp.Weight`.

Author: YaelDillies

Mathlib/Algebra/Order/Module/Defs.lean

@@ -21,14 +21,13 @@ variable [Semifield 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddComm
 -- See note [lower instance priority]
 instance (priority := 100) PosSMulMono.toPosSMulReflectLE [MulAction 𝕜 G] [PosSMulMono 𝕜 G] :
     PosSMulReflectLE 𝕜 G where
-  elim _a ha b₁ b₂ h := by
+  le_of_smul_le_smul_left _a ha b₁ b₂ h := by
     simpa [ha.ne'] using smul_le_smul_of_nonneg_left h <| inv_nonneg.2 ha.le
 
 -- See note [lower instance priority]
 instance (priority := 100) PosSMulStrictMono.toPosSMulReflectLT [MulActionWithZero 𝕜 G]
     [PosSMulStrictMono 𝕜 G] : PosSMulReflectLT 𝕜 G :=
-  PosSMulReflectLT.of_pos fun a ha b₁ b₂ h ↦ by
-    simpa [ha.ne'] using smul_lt_smul_of_pos_left h <| inv_pos.2 ha
+  .of_pos fun a ha b₁ b₂ h ↦ by simpa [ha.ne'] using smul_lt_smul_of_pos_left h <| inv_pos.2 ha
 
 end LinearOrderedSemifield
 

Mathlib/Algebra/Order/Module/Field.lean

@@ -59,10 +59,10 @@ variable [Semiring R] [PartialOrder R] [AddCommMonoid M] [PartialOrder M]
   [SMulWithZero R M] [OrderedSMul R M]
 
 instance OrderedSMul.toPosSMulStrictMono : PosSMulStrictMono R M where
-  elim _a ha _b₁ _b₂ hb := OrderedSMul.smul_lt_smul_of_pos hb ha
+  smul_lt_smul_of_pos_left _a ha _b₁ _b₂ hb := OrderedSMul.smul_lt_smul_of_pos hb ha
 
 instance OrderedSMul.toPosSMulReflectLT : PosSMulReflectLT R M :=
-  PosSMulReflectLT.of_pos fun _a ha _b₁ _b₂ h ↦ OrderedSMul.lt_of_smul_lt_smul_of_pos h ha
+  .of_pos fun _a ha _b₁ _b₂ h ↦ OrderedSMul.lt_of_smul_lt_smul_of_pos h ha
 
 instance OrderDual.instOrderedSMul : OrderedSMul R Mᵒᵈ where
   smul_lt_smul_of_pos := OrderedSMul.smul_lt_smul_of_pos (M := M)

Mathlib/Algebra/Order/Module/OrderedSMul.lean

@@ -14,10 +14,12 @@ import Mathlib.Data.Rat.Cast.Order
 variable {α : Type*}
 
 instance PosSMulMono.nnrat_of_rat [Preorder α] [MulAction ℚ α] [PosSMulMono ℚ α] :
-    PosSMulMono ℚ≥0 α where elim _q hq _a₁ _a₂ ha := smul_le_smul_of_nonneg_left (α := ℚ) ha hq
+    PosSMulMono ℚ≥0 α where
+  smul_le_smul_of_nonneg_left _q hq _a₁ _a₂ ha := smul_le_smul_of_nonneg_left (α := ℚ) ha hq
 
 instance PosSMulStrictMono.nnrat_of_rat [Preorder α] [MulAction ℚ α] [PosSMulStrictMono ℚ α] :
-    PosSMulStrictMono ℚ≥0 α where elim _q hq _a₁ _a₂ ha := smul_lt_smul_of_pos_left (α := ℚ) ha hq
+    PosSMulStrictMono ℚ≥0 α where
+  smul_lt_smul_of_pos_left _q hq _a₁ _a₂ ha := smul_lt_smul_of_pos_left (α := ℚ) ha hq
 
 section LinearOrderedAddCommGroup
 variable [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α]
@@ -37,7 +39,7 @@ section LinearOrderedSemifield
 variable [Semifield α] [LinearOrder α] [IsStrictOrderedRing α]
 
 instance LinearOrderedSemifield.toPosSMulStrictMono_rat : PosSMulStrictMono ℚ≥0 α where
-  elim q hq a b hab := by
+  smul_lt_smul_of_pos_left q hq a b hab := by
     rw [NNRat.smul_def, NNRat.smul_def]; exact mul_lt_mul_of_pos_left hab <| NNRat.cast_pos.2 hq
 
 end LinearOrderedSemifield
@@ -46,7 +48,7 @@ section LinearOrderedField
 variable [Field α] [LinearOrder α] [IsStrictOrderedRing α]
 
 instance LinearOrderedField.toPosSMulStrictMono_rat : PosSMulStrictMono ℚ α where
-  elim q hq a b hab := by
+  smul_lt_smul_of_pos_left q hq a b hab := by
     rw [Rat.smul_def, Rat.smul_def]; exact mul_lt_mul_of_pos_left hab <| Rat.cast_pos.2 hq
 
 end LinearOrderedField

Mathlib/Algebra/Order/Module/Rat.lean

@@ -359,14 +359,14 @@ variable [Semiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R]
   [StarModule R A] [IsScalarTower R A A] [SMulCommClass R A A]
 
 instance : PosSMulMono R A where
-  elim r hr a b hab := by
+  smul_le_smul_of_nonneg_left r hr a b hab := by
     rw [StarOrderedRing.nonneg_iff] at hr
     rw [StarOrderedRing.le_iff] at hab ⊢
     obtain ⟨a, ha, rfl⟩ := hab
     exact ⟨r • a, smul_mem_closure_star_mul hr ha, smul_add ..⟩
 
 instance : SMulPosMono R A where
-  elim a ha r s hrs := by
+  smul_le_smul_of_nonneg_right a ha r s hrs := by
     rw [StarOrderedRing.nonneg_iff] at ha
     rw [StarOrderedRing.le_iff] at hrs ⊢
     obtain ⟨r, hr, rfl⟩ := hrs
@@ -375,15 +375,15 @@ instance : SMulPosMono R A where
 variable [IsCancelAdd A] [NoZeroSMulDivisors R A]
 
 instance : PosSMulStrictMono R A where
-  elim r hr a b hab := by
+  smul_lt_smul_of_pos_left r hr a b hab := by
     rw [StarOrderedRing.pos_iff] at hr
     rw [StarOrderedRing.lt_iff] at hab ⊢
     obtain ⟨a, ha₀, ha, rfl⟩ := hab
     obtain ⟨hr₀, hr⟩ := hr
     exact ⟨r • a, smul_ne_zero hr₀ ha₀, smul_mem_closure_star_mul hr ha, smul_add ..⟩
 
 instance [IsCancelAdd R] : SMulPosStrictMono R A where
-  elim a ha r s hrs := by
+  smul_lt_smul_of_pos_right a ha r s hrs := by
     rw [StarOrderedRing.pos_iff] at ha
     rw [StarOrderedRing.lt_iff] at hrs ⊢
     obtain ⟨r, hr₀, hr, rfl⟩ := hrs

Mathlib/Algebra/Order/Star/Basic.lean

@@ -88,10 +88,11 @@ theorem toReal_smul (r : ℝ≥0) (s : ℝ≥0∞) : (r • s).toReal = r • s.
   rfl
 
 instance : PosSMulStrictMono ℝ≥0 ℝ≥0∞ where
-  elim _r hr _a _b hab := ENNReal.mul_lt_mul_left' (coe_pos.2 hr).ne' coe_ne_top hab
+  smul_lt_smul_of_pos_left _r hr _a _b hab :=
+    ENNReal.mul_lt_mul_left' (coe_pos.2 hr).ne' coe_ne_top hab
 
 instance : SMulPosMono ℝ≥0 ℝ≥0∞ where
-  elim _r _ _a _b hab := mul_le_mul_right' (coe_le_coe.2 hab) _
+  smul_le_smul_of_nonneg_right _r _ _a _b hab := mul_le_mul_right' (coe_le_coe.2 hab) _
 
 end Actions
 

Mathlib/Data/ENNReal/Action.lean

@@ -137,11 +137,6 @@ variable [AddCommMonoid M] [PartialOrder M] [IsOrderedAddMonoid M] (w : σ → M
   {R : Type*} [CommSemiring R] [PartialOrder R] [IsOrderedRing R]
   [CanonicallyOrderedAdd R] [NoZeroDivisors R] [Module R M]
 
-instance : SMulPosMono ℕ M :=
-  ⟨fun b hb m m' h ↦ by
-    rw [← Nat.add_sub_of_le h, add_smul]
-    exact le_add_of_nonneg_right (nsmul_nonneg hb (m' - m))⟩
-
 variable {w} in
 theorem le_weight_of_ne_zero (hw : ∀ s, 0 ≤ w s) {s : σ} {f : σ →₀ ℕ} (hs : f s ≠ 0) :
     w s ≤ weight w f := by

Mathlib/Data/Finsupp/Weight.lean

@@ -393,11 +393,11 @@ example : NoMaxOrder ℝ≥0 := by infer_instance
 
 instance instPosSMulStrictMono {α} [Preorder α] [MulAction ℝ α] [PosSMulStrictMono ℝ α] :
     PosSMulStrictMono ℝ≥0 α where
-  elim _r hr _a₁ _a₂ ha := (smul_lt_smul_of_pos_left ha (coe_pos.2 hr):)
+  smul_lt_smul_of_pos_left _r hr _a₁ _a₂ ha := (smul_lt_smul_of_pos_left ha (coe_pos.2 hr) :)
 
 instance instSMulPosStrictMono {α} [Zero α] [Preorder α] [MulAction ℝ α] [SMulPosStrictMono ℝ α] :
     SMulPosStrictMono ℝ≥0 α where
-  elim _a ha _r₁ _r₂ hr := (smul_lt_smul_of_pos_right (coe_lt_coe.2 hr) ha :)
+  smul_lt_smul_of_pos_right _a ha _r₁ _r₂ hr := (smul_lt_smul_of_pos_right (coe_lt_coe.2 hr) ha :)
 
 /-- If `a` is a nonnegative real number, then the closed interval `[0, a]` in `ℝ` is order
 isomorphic to the interval `Set.Iic a`. -/