chore(algebra/{ordered_group, linear_ordered_comm_group_with_zero.lea…

…n}): rename one lemma, remove more @s (#7895)

The more substantial part of this PR is changing the name of a lemma from `div_lt_div_iff'` to `mul_inv_lt_mul_inv_iff'`: the lemma proves `a * b⁻¹ ≤ c * d⁻¹ ↔ a * d ≤ c * b`.

Furthermore, in the same spirit as a couple of my recent short PRs, I am removing a few more `@`, in order to sweep under the rug, later on, a change in typeclass assumptions.  This PR only changes a name, which was used only once, and a few proofs, but no statement.

On the path towards PR #7645.

src/algebra/linear_ordered_comm_group_with_zero.lean

@@ -170,11 +170,11 @@ le_of_le_mul_right h (by simpa [h] using hab)
 
 lemma div_le_div' (a b c d : α) (hb : b ≠ 0) (hd : d ≠ 0) :
   a * b⁻¹ ≤ c * d⁻¹ ↔ a * d ≤ c * b :=
-begin
-  by_cases ha : a = 0, { simp [ha] },
-  by_cases hc : c = 0, { simp [inv_ne_zero hb, hc, hd], },
-  exact @div_le_div_iff' _ _ (units.mk0 a ha) (units.mk0 b hb) (units.mk0 c hc) (units.mk0 d hd)
-end
+if ha : a = 0 then by simp [ha] else
+if hc : c = 0 then by simp [inv_ne_zero hb, hc, hd] else
+show (units.mk0 a ha) * (units.mk0 b hb)⁻¹ ≤ (units.mk0 c hc) * (units.mk0 d hd)⁻¹ ↔
+  (units.mk0 a ha) * (units.mk0 d hd) ≤ (units.mk0 c hc) * (units.mk0 b hb),
+from mul_inv_le_mul_inv_iff'
 
 @[simp] lemma units.zero_lt (u : units α) : (0 : α) < u :=
 zero_lt_iff.2 $ u.ne_zero
@@ -184,9 +184,8 @@ have hb : b ≠ 0 := ne_zero_of_lt hab,
 have hd : d ≠ 0 := ne_zero_of_lt hcd,
 if ha : a = 0 then by { rw [ha, zero_mul, zero_lt_iff], exact mul_ne_zero hb hd } else
 if hc : c = 0 then by { rw [hc, mul_zero, zero_lt_iff], exact mul_ne_zero hb hd } else
-have hab0 : (units.mk0 a ha) < (units.mk0 b hb) := hab,
-have hcd0 : (units.mk0 c hc) < (units.mk0 d hd) := hcd,
-by apply mul_lt_mul''' hab0 hcd0
+show (units.mk0 a ha) * (units.mk0 c hc) < (units.mk0 b hb) * (units.mk0 d hd),
+from mul_lt_mul''' hab hcd
 
 lemma mul_inv_lt_of_lt_mul' (h : x < y * z) : x * z⁻¹ < y :=
 have hz : z ≠ 0 := (mul_ne_zero_iff.1 $ ne_zero_of_lt h).2,
@@ -203,10 +202,12 @@ lemma pow_lt_pow' {x : α} {m n : ℕ} (hx : 1 < x) (hmn : m < n) : x ^ m < x ^
 by { induction hmn with n hmn ih, exacts [pow_lt_pow_succ hx, lt_trans ih (pow_lt_pow_succ hx)] }
 
 lemma inv_lt_inv'' (ha : a ≠ 0) (hb : b ≠ 0) : a⁻¹ < b⁻¹ ↔ b < a :=
-@inv_lt_inv_iff _ _ (units.mk0 a ha) (units.mk0 b hb)
+show (units.mk0 a ha)⁻¹ < (units.mk0 b hb)⁻¹ ↔ (units.mk0 b hb) < (units.mk0 a ha),
+from inv_lt_inv_iff
 
 lemma inv_le_inv'' (ha : a ≠ 0) (hb : b ≠ 0) : a⁻¹ ≤ b⁻¹ ↔ b ≤ a :=
-@inv_le_inv_iff _ _ (units.mk0 a ha) (units.mk0 b hb)
+show (units.mk0 a ha)⁻¹ ≤ (units.mk0 b hb)⁻¹ ↔ (units.mk0 b hb) ≤ (units.mk0 a ha),
+from inv_le_inv_iff
 
 instance : linear_ordered_add_comm_group_with_top (additive (order_dual α)) :=
 { neg_top := inv_zero,

src/algebra/ordered_group.lean

@@ -406,7 +406,7 @@ lemma inv_mul_lt_iff_lt_mul_right : c⁻¹ * a < b ↔ a < b * c :=
 by rw [inv_mul_lt_iff_lt_mul, mul_comm]
 
 @[to_additive add_neg_le_add_neg_iff]
-lemma div_le_div_iff' : a * b⁻¹ ≤ c * d⁻¹ ↔ a * d ≤ c * b :=
+lemma mul_inv_le_mul_inv_iff' : a * b⁻¹ ≤ c * d⁻¹ ↔ a * d ≤ c * b :=
 begin
   split ; intro h,
   have := mul_le_mul_right' (mul_le_mul_right' h b) d,