refactor(algebra/order/{smul,module}): Turn lemmas around (#16696)

Match the `mul` lemmas by having the `⁻¹` on the LHS in `inv_smul_le_iff`, `inv_smul_lt_iff`, etc... Also generalize for free to `ordered_add_comm_monoid`.

Author: YaelDillies

src/algebra/order/module.lean

@@ -160,17 +160,17 @@ begin
   exact smul_le_smul_iff_of_pos (neg_pos_of_neg hc),
 end
 
-lemma smul_lt_iff_of_neg (hc : c < 0) : c • a < b ↔ c⁻¹ • b < a :=
-begin
-  rw [←neg_neg c, ←neg_neg a, neg_smul_neg, inv_neg, neg_smul _ b, neg_lt_neg_iff],
-  exact smul_lt_iff_of_pos (neg_pos_of_neg hc),
-end
+lemma inv_smul_le_iff_of_neg (h : c < 0) : c⁻¹ • a ≤ b ↔ c • b ≤ a :=
+by { rw [←smul_le_smul_iff_of_neg h, smul_inv_smul₀ h.ne], apply_instance }
 
-lemma lt_smul_iff_of_neg (hc : c < 0) : a < c • b ↔ b < c⁻¹ • a :=
-begin
-  rw [←neg_neg c, ←neg_neg b, neg_smul_neg, inv_neg, neg_smul _ a, neg_lt_neg_iff],
-  exact lt_smul_iff_of_pos (neg_pos_of_neg hc),
-end
+lemma inv_smul_lt_iff_of_neg (h : c < 0) : c⁻¹ • a < b ↔ c • b < a :=
+by { rw [←smul_lt_smul_iff_of_neg h, smul_inv_smul₀ h.ne], apply_instance }
+
+lemma smul_inv_le_iff_of_neg (h : c < 0) : a ≤ c⁻¹ • b ↔ b ≤ c • a :=
+by { rw [←smul_le_smul_iff_of_neg h, smul_inv_smul₀ h.ne], apply_instance }
+
+lemma smul_inv_lt_iff_of_neg (h : c < 0) : a < c⁻¹ • b ↔ b < c • a :=
+by { rw [←smul_lt_smul_iff_of_neg h, smul_inv_smul₀ h.ne], apply_instance }
 
 variables (M)
 

src/algebra/order/smul.lean

@@ -174,11 +174,8 @@ instance linear_ordered_semiring.to_ordered_smul {R : Type*} [linear_ordered_sem
 ordered_smul.mk'' $ λ c, strict_mono_mul_left_of_pos
 
 section linear_ordered_semifield
-variables [linear_ordered_semifield 𝕜]
-
-section ordered_add_comm_monoid
-variables [ordered_add_comm_monoid M] [ordered_add_comm_monoid N] [mul_action_with_zero 𝕜 M]
-  [mul_action_with_zero 𝕜 N]
+variables [linear_ordered_semifield 𝕜] [ordered_add_comm_monoid M] [ordered_add_comm_monoid N]
+  [mul_action_with_zero 𝕜 M] [mul_action_with_zero 𝕜 N]
 
 /-- To prove that a vector space over a linear ordered field is ordered, it suffices to verify only
 the first axiom of `ordered_smul`. -/
@@ -213,32 +210,24 @@ instance pi.ordered_smul' [ordered_smul 𝕜 M] : ordered_smul 𝕜 (ι → M) :
 /- Sometimes Lean fails to unify the module with the scalars, so we define another instance. -/
 instance pi.ordered_smul'' : ordered_smul 𝕜 (ι → 𝕜) := @pi.ordered_smul' ι 𝕜 𝕜 _ _ _ _
 
-end ordered_add_comm_monoid
-
-section ordered_add_comm_group
-variables [ordered_add_comm_group M] [mul_action_with_zero 𝕜 M] [ordered_smul 𝕜 M] {s : set M}
-  {a b : M} {c : 𝕜}
+variables [ordered_smul 𝕜 M] {s : set M} {a b : M} {c : 𝕜}
 
 lemma smul_le_smul_iff_of_pos (hc : 0 < c) : c • a ≤ c • b ↔ a ≤ b :=
 ⟨λ h, inv_smul_smul₀ hc.ne' a ▸ inv_smul_smul₀ hc.ne' b ▸
   smul_le_smul_of_nonneg h (inv_nonneg.2 hc.le),
   λ h, smul_le_smul_of_nonneg h hc.le⟩
 
-lemma smul_lt_iff_of_pos (hc : 0 < c) : c • a < b ↔ a < c⁻¹ • b :=
-calc c • a < b ↔ c • a < c • c⁻¹ • b : by rw [smul_inv_smul₀ hc.ne']
-... ↔ a < c⁻¹ • b : smul_lt_smul_iff_of_pos hc
+lemma inv_smul_le_iff (h : 0 < c) : c⁻¹ • a ≤ b ↔ a ≤ c • b :=
+by { rw [←smul_le_smul_iff_of_pos h, smul_inv_smul₀ h.ne'], apply_instance }
 
-lemma lt_smul_iff_of_pos (hc : 0 < c) : a < c • b ↔ c⁻¹ • a < b :=
-calc a < c • b ↔ c • c⁻¹ • a < c • b : by rw [smul_inv_smul₀ hc.ne']
-... ↔ c⁻¹ • a < b : smul_lt_smul_iff_of_pos hc
+lemma inv_smul_lt_iff (h : 0 < c) : c⁻¹ • a < b ↔ a < c • b :=
+by { rw [←smul_lt_smul_iff_of_pos h, smul_inv_smul₀ h.ne'], apply_instance }
 
-lemma smul_le_iff_of_pos (hc : 0 < c) : c • a ≤ b ↔ a ≤ c⁻¹ • b :=
-calc c • a ≤ b ↔ c • a ≤ c • c⁻¹ • b : by rw [smul_inv_smul₀ hc.ne']
-... ↔ a ≤ c⁻¹ • b : smul_le_smul_iff_of_pos hc
+lemma le_inv_smul_iff (h : 0 < c) : a ≤ c⁻¹ • b ↔ c • a ≤ b :=
+by { rw [←smul_le_smul_iff_of_pos h, smul_inv_smul₀ h.ne'], apply_instance }
 
-lemma le_smul_iff_of_pos (hc : 0 < c) : a ≤ c • b ↔ c⁻¹ • a ≤ b :=
-calc a ≤ c • b ↔ c • c⁻¹ • a ≤ c • b : by rw [smul_inv_smul₀ hc.ne']
-... ↔ c⁻¹ • a ≤ b : smul_le_smul_iff_of_pos hc
+lemma lt_inv_smul_iff (h : 0 < c) : a < c⁻¹ • b ↔ c • a < b :=
+by { rw [←smul_lt_smul_iff_of_pos h, smul_inv_smul₀ h.ne'], apply_instance }
 
 variables (M)
 
@@ -264,7 +253,6 @@ variables {M}
 @[simp] lemma bdd_above_smul_iff_of_pos (hc : 0 < c) : bdd_above (c • s) ↔ bdd_above s :=
 (order_iso.smul_left _ hc).bdd_above_image
 
-end ordered_add_comm_group
 end linear_ordered_semifield
 
 namespace tactic

src/linear_algebra/affine_space/ordered.lean

@@ -203,7 +203,7 @@ begin
   vsub_eq_sub, vsub_eq_sub, vsub_eq_sub, vadd_eq_add, vadd_eq_add,
   smul_eq_mul, add_sub_cancel, smul_sub, smul_sub, smul_sub,
   sub_le_iff_le_add, mul_inv_rev, mul_smul, mul_smul, ←smul_sub, ←smul_sub, ←smul_add, smul_smul,
-  ← mul_inv_rev, smul_le_iff_of_pos (inv_pos.2 h), inv_inv, smul_smul,
+  ← mul_inv_rev, inv_smul_le_iff h, smul_smul,
   mul_inv_cancel_right₀ (right_ne_zero_of_mul h.ne'), smul_add,
   smul_inv_smul₀ (left_ne_zero_of_mul h.ne')],
   apply_instance
@@ -236,11 +236,10 @@ begin
   rw [← line_map_apply_one_sub, ← line_map_apply_one_sub _ _ r],
   revert h, generalize : 1 - r = r', clear r, intro h,
   simp_rw [line_map_apply, slope, vsub_eq_sub, vadd_eq_add, smul_eq_mul],
-  rw [sub_add_eq_sub_sub_swap, sub_self, zero_sub, le_smul_iff_of_pos, inv_inv, smul_smul,
-    neg_mul_eq_mul_neg, neg_sub, mul_inv_cancel_right₀, le_sub, ← neg_sub (f b), smul_neg,
-    neg_add_eq_sub],
+  rw [sub_add_eq_sub_sub_swap, sub_self, zero_sub, neg_mul_eq_mul_neg, neg_sub, le_inv_smul_iff h,
+    smul_smul, mul_inv_cancel_right₀, le_sub, ← neg_sub (f b), smul_neg, neg_add_eq_sub],
   { exact right_ne_zero_of_mul h.ne' },
-  { simpa [mul_sub] using h }
+  { apply_instance }
 end
 
 /-- Given `c = line_map a b r`, `c < b`, the point `(c, f c)` is non-strictly above the