feat(algebra/ordered_field): add inv_le_of_inv_le and `inv_lt_of_in…

…v_lt` (#8565)

These lemmas need positivity of only one of two variables. Mathlib already had lemmas about ordered multiplicative groups with these names, I appended prime to their names.

src/algebra/ordered_field.lean

@@ -240,18 +240,28 @@ by rwa [← one_div a, le_div_iff' ha, ← div_eq_mul_inv, div_le_iff (ha.trans_
 lemma inv_le_inv (ha : 0 < a) (hb : 0 < b) : a⁻¹ ≤ b⁻¹ ↔ b ≤ a :=
 by rw [← one_div, div_le_iff ha, ← div_eq_inv_mul, le_div_iff hb, one_mul]
 
+/-- In a linear ordered field, for positive `a` and `b` we have `a⁻¹ ≤ b ↔ b⁻¹ ≤ a`.
+See also `inv_le_of_inv_le` for a one-sided implication with one fewer assumption. -/
 lemma inv_le (ha : 0 < a) (hb : 0 < b) : a⁻¹ ≤ b ↔ b⁻¹ ≤ a :=
 by rw [← inv_le_inv hb (inv_pos.2 ha), inv_inv']
 
+lemma inv_le_of_inv_le (ha : 0 < a) (h : a⁻¹ ≤ b) : b⁻¹ ≤ a :=
+(inv_le ha ((inv_pos.2 ha).trans_le h)).1 h
+
 lemma le_inv (ha : 0 < a) (hb : 0 < b) : a ≤ b⁻¹ ↔ b ≤ a⁻¹ :=
 by rw [← inv_le_inv (inv_pos.2 hb) ha, inv_inv']
 
 lemma inv_lt_inv (ha : 0 < a) (hb : 0 < b) : a⁻¹ < b⁻¹ ↔ b < a :=
 lt_iff_lt_of_le_iff_le (inv_le_inv hb ha)
 
+/-- In a linear ordered field, for positive `a` and `b` we have `a⁻¹ < b ↔ b⁻¹ < a`.
+See also `inv_lt_of_inv_lt` for a one-sided implication with one fewer assumption. -/
 lemma inv_lt (ha : 0 < a) (hb : 0 < b) : a⁻¹ < b ↔ b⁻¹ < a :=
 lt_iff_lt_of_le_iff_le (le_inv hb ha)
 
+lemma inv_lt_of_inv_lt (ha : 0 < a) (h : a⁻¹ < b) : b⁻¹ < a :=
+(inv_lt ha ((inv_pos.2 ha).trans h)).1 h
+
 lemma lt_inv (ha : 0 < a) (hb : 0 < b) : a < b⁻¹ ↔ b < a⁻¹ :=
 lt_iff_lt_of_le_iff_le (inv_le hb ha)
 

src/algebra/ordered_group.lean

@@ -299,8 +299,8 @@ end
 lemma inv_le' : a⁻¹ ≤ b ↔ b⁻¹ ≤ a :=
 (order_iso.inv α).symm_apply_le
 
-alias inv_le' ↔ inv_le_of_inv_le _
-attribute [to_additive] inv_le_of_inv_le
+alias inv_le' ↔ inv_le_of_inv_le' _
+attribute [to_additive neg_le_of_neg_le] inv_le_of_inv_le'
 
 @[to_additive le_neg]
 lemma le_inv' : a ≤ b⁻¹ ↔ b ≤ a⁻¹ :=
@@ -337,8 +337,8 @@ by rw [← inv_lt_inv_iff, inv_inv]
 alias lt_inv' ↔ lt_inv_of_lt_inv _
 attribute [to_additive] lt_inv_of_lt_inv
 
-alias inv_lt' ↔ inv_lt_of_inv_lt _
-attribute [to_additive] inv_lt_of_inv_lt
+alias inv_lt' ↔ inv_lt_of_inv_lt' _
+attribute [to_additive neg_lt_of_neg_lt] inv_lt_of_inv_lt'
 
 @[to_additive]
 lemma mul_inv_lt_inv_mul_iff : a * b⁻¹ < d⁻¹ * c ↔ d * a < c * b :=